The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.Through the condition that in a cut-free derivation of (...) the sequent Γ⇒C, no inactive weakening or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only. (shrink)

This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of ‘maximal formula’, ‘segment’ and ‘maximal segment’ suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form (...) and that deductions in normal form have the subformula property. (shrink)

General-elimination harmony articulates Gentzen’s idea that the elimination-rules are justified if they infer from an assertion no more than can already be inferred from the grounds for making it. Dummett described the rules as not only harmonious but stable if the E-rules allow one to infer no more and no less than the I-rules justify. Pfenning and Davies call the rules locally complete if the E-rules are strong enough to allow one (...) to infer the original judgement. A method is given of generating harmonious general-elimination rules from a collection of I-rules. We show that the general-elimination rules satisfy Pfenning and Davies’ test for local completeness, but question whether that is enough to show that they are stable. Alternative conditions for stability are considered, including equivalence between the introduction- and elimination-meanings of a connective, and recovery of the grounds for assertion, finally generalizing the notion of local completeness to capture Dummett’s notion of stability satisfactorily. We show that the general-elimination rules meet the last of these conditions, and so are indeed not only harmonious but also stable. (shrink)

Inferentialism claims that expressions are meaningful by virtue of rules governing their use. In particular, logical expressions are autonomous if given meaning by their introduction-rules, rules specifying the grounds for assertion of propositions containing them. If the elimination-rules do no more, and no less, than is justified by the introduction-rules, the rules satisfy what Prawitz, following Lorenzen, called an inversion principle. This connection between rules leads to a general form of (...) class='Hi'>elimination-rule, and when the rules have this form, they may be said to exhibit “general-elimination” harmony. Ge-harmony ensures that the meaning of a logical expression is clearly visible in its I-rule, and that the I- and E-rules are coherent, in encapsulating the same meaning. However, it does not ensure that the resulting logical system is normalizable, nor that it satisfies the conservative extension property, nor that it is consistent. Thus harmony should not be identified with any of these notions. (shrink)

The paper reports that the explanations of the v-elimination rule in three commonly used introductory logic textbooks are misleading to students and can result in invalid inferences.

Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a version of Parigot’s free deduction. The elimination rules are “general,” but can be systematically simplified. Cut-elimination and normalization hold. Restriction to a single formula in the succedent yields intuitionistic versions of these systems. The rules also yield generalized lambda (...) calculi providing proof terms for natural deduction proofs as in the Curry-Howard isomorphism. Addition of an indirect proof rule yields classical single-conclusion versions of these systems. Gentzen’s standard systems arise as special cases. (shrink)

Cut-elimination theorems constitute one of the most important classes of theorems of proof theory. Since Gentzen’s proof of the cut-elimination theorem for the system LK, several other proofs have been proposed. Even though the techniques of these proofs can be modified to sequent systems other than $$\textbf{LK}$$, they are essentially of a very particular nature; each of them describes an algorithm to transform a given proof to a cut-free proof. However, due to its reliance on heavy syntactic arguments (...) and case distinctions, such an algorithm makes the fundamental structure of the argument rather opaque. We, therefore, consider rules abstractly, within the framework of logical structures familiar from universal logic in the sense of Béziau (Universal logic, Prague, 1994) and aim to clarify the essence of the so-called “elimination theorems”. To do this, we first give a non-algorithmic proof of the cut-elimination theorem for the propositional fragment of $$\textbf{LK}$$. From this proof, we abstract the essential features of the argument and define something called normal sequent structures relative to a particular rule. We then prove a version of the rule-elimination theorem for these. Abstracting even more, we define abstract sequent structures and show that for these structures, the corresponding version of the rule-elimination theorem has a converse as well. (shrink)

We investigate introduction and elimination rules for truth-functional connectives, focusing on the general questions of the existence, for a given connective, of at least one such rule that it satisfies, and the uniqueness of a connective with respect to the set of all of them. The answers are straightforward in the context of rules using general set/set sequents of formulae, but rather complex and asymmetric in the restricted (but more often used) context of set/formula sequents, (...) as also in the intermediate set/formula-or-empty context. (shrink)

In this paper we first give a survey of reductive cut-elimination methods in classical logic. In particular we describe the methods of Gentzen and Schütte-Tait from the abstract point of view of proof reduction. We also present the method CERES which we classify as a semi-semantic method. In a further section we describe the so-called semantic methods. In the second part of the paper we carry the proof analysis further by generalizing the CERES method to CERESD . In the (...) generalized version CERESD we admit general elimination rules which are based on the mere semantical truth of sentences. We construct complete cut-free LK-derivations originating from derivations potentially containing unproven lemmas. Finally we give a comparison of reductive methods and CERESD by presenting a general simulation result. (shrink)

Bilateral proof systems, which provide rules for both affirming and denying sentences, have been prominent in the development of proof-theoretic semantics for classical logic in recent years. However, such systems provide a substantial amount of freedom in the formulation of the rules, and, as a result, a number of different sets of rules have been put forward as definitive of the meanings of the classical connectives. In this paper, I argue that a single general schema for (...) bilateral proof rules has a reasonable claim to inferentially articulating the core meaning of all of the classical connectives. I propose this schema in the context of a bilateral sequent calculus in which each connective is given exactly two rules: a rule for affirmation and a rule for denial. Positive and negative rules for all of the classical connectives are given by a single rule schema, harmony between these positive and negative rules is established at the schematic level by a pair of elimination theorems, and the truth-conditions for all of the classical connectives are read off at once from the schema itself. (shrink)

Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a structure-free logic. The aim of this work is to give such a condition by using algebraic semantics. We consider full Lambek calculus (FL), i.e., intuitionistic (...) logic without any structural rules, as our basic framework. Residuated lattices are the algebraic structures corresponding to FL. In this setting, we introduce a criterion, called the propagation property, that can be stated both in syntactic and algebraic terminologies. We then show that, for any set R of structural rules, the cut elimination theorem holds for FL enriched with R if and only if R satisfies the propagation property. As an application, we show that any set R of structural rules can be "completed" into another set R*, so that the cut elimination theorem holds for FL enriched with R*, while the provability remains the same. (shrink)

This paper considers a formalisation of classical logic using general introduction rules and general elimination rules. It proposes a definition of ‘maximal formula’, ‘segment’ and ‘maximal segment’ suitable to the system, and gives reduction procedures for them. It is then shown that deductions in the system convert into normal form, i.e. deductions that contain neither maximal formulas nor maximal segments, and that deductions in normal form satisfy the subformula property. Tarski’s Rule is treated as a (...) general introduction rule for implication. The general introduction rule for negation has a similar form. Maximal formulas with implication or negation as main operator require reduction procedures of a more intricate kind not present in normalisation for intuitionist logic. (shrink)

Natural deduction with alternatives extends Gentzen–Prawitz-style natural deduction with a single structural addition: negatively signed assumptions, called alternatives. It is a mildly bilateralist, single-conclusion natural deduction proof system in which the connective rules are unmodi_ed from the usual Prawitz introduction and elimination rules — the extension is purely structural. This framework is general: it can be used for (1) classical logic, (2) relevant logic without distribution, (3) affine logic, and (4) linear logic, keeping the connective (...) class='Hi'>rules fixed, and varying purely structural rules. The key result of this paper is that the two principles that introduce kinds of irrelevance to natural deduction proofs: (a) the rule of explosion (from a contradiction, anything follows); and (b) the structural rule of vacuous discharge; are shown to be two sides of a single coin, in the same way that they correspond to the structural rule of weakening in the sequent calculus. The paper also includes a discussion of assumption classes, and how they can play a role in treating additive connectives in substructural natural deduction. (shrink)

We develop a general algebraic and proof-theoretic study of substructural logics that may lack associativity, along with other structural rules. Our study extends existing work on substructural logics over the full Lambek Calculus [34], Galatos and Ono [18], Galatos et al. [17]). We present a Gentzen-style sequent system that lacks the structural rules of contraction, weakening, exchange and associativity, and can be considered a non-associative formulation of . Moreover, we introduce an equivalent Hilbert-style system and show that (...) the logic associated with and is algebraizable, with the variety of residuated lattice-ordered groupoids with unit serving as its equivalent algebraic semantics. Overcoming technical complications arising from the lack of associativity, we introduce a generalized version of a logical matrix and apply the method of quasicompletions to obtain an algebra and a quasiembedding from the matrix to the algebra. By applying the general result to specific cases, we obtain important logical and algebraic properties, including the cut elimination of and various extensions, the strong separation of , and the finite generation of the variety of residuated lattice-ordered groupoids with unit. (shrink)

Arguments by Sorkin (Impossible measurements on quantum fields. In: Directions in general relativity: proceedings of the 1993 International Symposium, Maryland, vol 2, pp 293–305, 1993) and Borsten et al. (Phys Rev D 104(2), 2021. https://doi.org/10.1103/PhysRevD.104.025012 ) establish that a natural extension of quantum measurement theory from non-relativistic quantum mechanics to relativistic quantum theory leads to the unacceptable consequence that expectation values in one region depend on which unitary operation is performed in a spacelike separated region. Sorkin [ 1 ] (...) labels such scenarios ‘impossible measurements’. We explicitly present these arguments as a no-go result with the logical form of a reductio argument and investigate the consequences for measurement in quantum field theory (QFT). Sorkin-type impossible measurement scenarios clearly illustrate the moral that Microcausality is not by itself sufficient to rule out superluminal signalling in relativistic quantum theories that use Lüders’ rule. We review three different approaches to formulating an account of measurement for QFT and analyze their responses to the ‘impossible measurements’ problem. Two of the approaches are: a measurement theory based on detector models proposed in Polo-Gómez et al. (Phys Rev D, 2022. https://doi.org/10.1103/physrevd.105.065003 ) and a measurement framework for algebraic QFT proposed in Fewster and Verch (Commun Math Phys 378(2):851–889, 2020). Of particular interest for foundations of QFT is that they share common features that may hold general morals about how to represent measurement in QFT. These morals are about the role that dynamics plays in eliminating ‘impossible measurements’, the abandonment of the operational interpretation of local algebras \({\mathcal {A}}(O)\) as representing possible operations carried out in region _O_, and the interpretation of state update rules. Finally, we examine the form that the ‘impossible measurements’ problem takes in histories-based approaches and we discuss the remaining challenges. (shrink)

We present our calculus of higher-level rules, extended with propositional quantification within rules. This makes it possible to present general schemas for introduction and elimination rules for arbitrary propositional operators and to define what it means that introductions and eliminations are in harmony with each other. This definition does not presuppose any logical system, but is formulated in terms of rules themselves. We therefore speak of a foundational account of proof-theoretic harmony. With every set (...) of introduction rules a canonical elimination rule, and with every set of elimination rules a canonical introduction rule is associated in such a way that the canonical rule is in harmony with the set of rules it is associated with. An example given by Hazen and Pelletier is used to demonstrate that there are significant connectives, which are characterized by their elimination rules, and whose introduction rule is the canonical introduction rule associated with these elimination rules. Due to the availabiliy of higher-level rules and propositional quantification, the means of expression of the framework developed are sufficient to ensure that the construction of canonical elimination or introduction rules is always possible and does not lead out of this framework. (shrink)

An (n, k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical systems with (n, k)-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion (...) of coherence to characterize strong cutelimination in such systems. We show that the following properties of a canonical system G with arbitrary (n, k)-ary quantifiers are equivalent: (i) G is coherent, (ii) G admits strong cut-elimination, and (iii) G has a strongly characteristic two-valued generalized non-deterministic matrix. In addition, we define simple calculi, an important subclass of canonical calculi, for which coherence is equivalent to the weaker, standard cut-elimination property. (shrink)

We develop a Gentzen-style proof theory for super-Belnap logics, expanding on an approach initiated by Pynko. We show that just like substructural logics may be understood proof-theoretically as logics which relax the structural rules of classical logic but keep its logical rules as well as the rules of Identity and Cut, super-Belnap logics may be seen as logics which relax Identity and Cut but keep the logical rules as well as the structural rules of classical (...) logic. A generalization of the cut elimination theorem for classical propositional logic is then proved and used to establish interpolation for various super-Belnap logics. In particular, we obtain an alternative syntactic proof of a refinement of the Craig interpolation theorem for classical propositional logic discovered recently by Milne. (shrink)

We develop an axiomatic theory of “generalized Routley-Meyer logics.” These are first-order logics which are can be characterized by model theories in a certain generalization of Routley-Meyer semantics. We show that all GRM logics are subclassical, have recursively enumerable consequence relations, satisfy the compactness theorem, and satisfy the standard structural rules and conjunction and disjunction introduction/elimination rules. We also show that the GRM logics include classical logic, intuitionistic logic, LP/K3/FDE, and the relevant logics.

A general model of problem‐solving processes based on misconception elimination is presented to simulate both impasses and solving processes. The model operates on goal‐related rules and a set of constraint rules in the form of “if (state or goal), do not (Action)” for the explicit constraints in the instructions and the implicit constraints that come from misconceptions of legal moves. When impasses occur, a constraint elimination mechanism is applied. Because successive eliminations of implicit constraints enlarge (...) the problem space and have an effect on planning, the model integrates “plan‐based” and “constraint‐based” approaches to problem‐solving behavior.Simulating individual protocols of Tower of Hanoi situations shows that the model, which has a proper set of constraints, predicts a single move with no alternative on about 61% of the movements and that protocols are quite successfully simulated movement by movement. Finally, it is shown that many features of previous models are embedded in the constraint elimination model. (shrink)

The interplay of introduction and elimination rules for propositional connectives is often seen as suggesting a distinguished role for intuitionistic logic. We prove three formal results concerning intuitionistic propositional logic that bear on that perspective, and discuss their significance. First, for a range of connectives including both negation and the falsum, there are no classically or intuitionistically correct introduction rules. Second, irrespective of the choice of negation or the falsum as a primitive connective, classical and intuitionistic consequence (...) satisfy exactly the same structural, introduction, and elimination (briefly, elementary) rules. Third, for falsum as primitive only, intuitionistic consequence is the least consequence relation that satisfies all classically correct elementary rules. (shrink)

Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to (...) rules with unary quantifiers and show that it remains constructive. Then we provide semantics for such canonical systems using 2-valued non-deterministic matrices extended to languages with quantifiers, and prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix. (shrink)

A uniform calculus for linear logic is presented. The calculus has the form of a natural deduction system in sequent calculus style with general introduction and elimination rules. General elimination rules are motivated through an inversion principle, the dual form of which gives the general introduction rules. By restricting all the rules to their single-succedent versions, a uniform calculus for intuitionistic linear logic is obtained. The calculus encompasses both natural deduction and (...) sequent calculus that are obtained as special instances from the uniform calculus. Other instances give all the invertibilities and partial invertibilities for the sequent calculus rules of linear logic. The calculus is normalizing and satisfies the subformula property for normal derivations. (shrink)

Some of our most fundamental moral rules are violated by the practices of torture and war. If one examines the concrete forms these practices take, can the exceptions to the rules necessary to either torture or war be justified? Fighting Hurt brings together key essays by Henry Shue on the issue of torture, and relatedly, the moral challenges surrounding the initiation and conduct of war, and features a new introduction outlining the argument of the essays, putting them into (...) context, and describing how and in what ways his position has modified over time. The first six chapters marshal arguments that have been refined over 35 years for the conclusion that torture can never be justified in any actual circumstances whatsoever. The practice of torture has nothing significant in common with the ticking bomb scenario often used in its defence, and weak U.S. statutes have loop-holes for psychological torture of the kind now favoured by CIA in the 'war against terrorism'. The other sixteen chapters maintain that for as long as wars are in fact fought, it is morally urgent to limit specific destructive practices that cannot be prohibited. Two possible exceptions to the UN Charter's prohibition on all but defensive wars, humanitarian military intervention and preventive war to eliminate WMD, are evaluated; and one possible exception to the principle of discrimination, Michael Walzer's 'supreme emergency', is sharply criticized. Two other fundamental issues about the rules for the conduct of war receive extensive controversial treatment. The first is the rules to limit the bombing of dual-use infrastructure, with a focus on alternative interpretations of the principle of proportionality that limits 'collateral damage'. The second is the moral status of the laws of war as embodied in International Humanitarian Law. It is argued that the current philosophical critique of IHL by Jeff McMahan focused on individual moral liability to attack is an intellectual dead-end and that the morally best rules are international laws that are the same for all fighters.Examining real cases, including U.S. bombing of Iraq in 1991, the Clinton Administration decision not to intervene in the 1994 Rwandan genocide, NATO bombing of Serbia in 1999, and CIA torture after 9/11 and its alternatives, this book is highly accessible to general readers who are interested in the ethical status of American political life, especially foreign policy. (shrink)

The inversion principle for logical rules expresses a relationship between introduction and elimination rules for logical constants. Hallnäs & Schroeder-Heister proposed the principle of definitional reflection, which embodies basic ideas of inversion in the more general context of clausal definitions. For the context of admissibility statements, this has been further elaborated by Schroeder-Heister . Using the framework of definitional reflection and its admissibility interpretation, we show that, in the sequent calculus of minimal propositional logic, the left (...) introduction rules are admissible when the right introduction rules are taken as the definitions of the logical constants and vice versa. This generalizes the well-known relationship between introduction and elimination rules in natural deduction to the framework of the sequent calculus. (shrink)

On the basis of Martin-Löf’s meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in type theory by Ladyman and Presnell.

The inversion principle for logical rules expresses a relationship between introduction and elimination rules for logical constants. Hallnäs & Schroeder-Heister proposed the principle of definitional reflection, which embodies basic ideas of inversion in the more general context of clausal definitions. For the context of admissibility statements, this has been further elaborated by Schroeder-Heister. Using the framework of definitional reflection and its admissibility interpretation, we show that, in the sequent calculus of minimal propositional logic, the left introduction (...) rules are admissible when the right introduction rules are taken as the definitions of the logical constants and vice versa. This generalizes the well-known relationship between introduction and elimination rules in natural deduction to the framework of the sequent calculus. (shrink)

Go back to An-fang, the Peace Square at An-Fang, the Beginning Place at An-Fang, where all things start (… ) An-Fang was near a city, the only living city with a pre-atomic name (… ) The headquarters of the People Programmer was at An-Fang, and there the mistake happened: A ruby trembled. Two tourmaline nets failed to rectify the laser beam. A diamond noted the error. Both the error and the correction went into the general computer. Cordwainer SmithThe Dead (...) Lady of Clown Town, 1964. (shrink)

Proof-theoretic semantics is an inferentialist theory of meaning originally developed in a unilateral framework. Its extension to bilateral systems opens both opportunities and problems. The problems are caused especially by Coordination Principles (a kind of rule that is not present in unilateral systems) and mismatches between rules for assertion and rules for rejection. In this paper, a solution is proposed for two major issues: the availability of a reduction procedure for tonk and the existence of harmonious rules (...) for the paradoxical zero-ary connective \(\bullet\). The solution is based on a reinterpretation of bilateral rules as complex rules, that is, rules that introduce or eliminate connectives in a subordinate position. Looking at bilateral rules from this perspective, the problems faced by bilateralism can be seen as special cases of general problems of complex systems, which have been already analyzed in the literature. In the end, a comparison with other proposed solutions underlines the need for further investigation in order to complete the picture of bilateral proof-theoretic semantics. (shrink)

We introduce, in a general setting, an ‘‘analytic’’ version of standard equational calculi of combinatory logic. Analyticity lies on the one side in the fact that these calculi are characterized by the presence of combinatory introduction rules in place of combinatory axioms, and on the other side in that the transitivity rule proves to be eliminable. Apart from consistency, which follows immediately, we discuss other almost direct consequences of analyticity and the main transitivity elimination theorem; in particular (...) the Church−Rosser and the leftmostreduction theorems for the associated notions of reduction. The last two sections deal with analytic combinatory calculi with the extensionality rule added. Here, as far as the elimination of transitivity is concerned, we have only partial results, which unfortunately do not cover, at present, full CL + Ext. Yet, they are sufficient to prove the decidability of weaker combinatory calculi with extensionality, including e.g. BCK + Ext. (shrink)

We present a cut-free sequent calculus for a class of first-order theories in negation normal form which include coherent and co-coherent theories alike. All structural rules, including cut, are admissible.

The paper studies the extension of harmony and stability, major themes in proof-theoretic semantics, from single-conclusion natural-deduction systems to multiple -conclusions natural-deduction, independently of classical logic. An extension of the method of obtaining harmoniously-induced general elimination rules from given introduction rules is suggested, taking into account sub-structurality. Finally, the reductions and expansions of the multiple -conclusions natural-deduction representation of classical logic are formulated.

The idea of an ?inversion principle?, and the name itself, originated in the work of Paul Lorenzen in the 1950s, as a method to generate new admissible rules within a certain syntactic context. Some fifteen years later, the idea was taken up by Dag Prawitz to devise a strategy of normalization for natural deduction calculi (this being an analogue of Gentzen's cut-elimination theorem for sequent calculi). Later, Prawitz used the inversion principle again, attributing it with a semantic role. (...) Still working in natural deduction calculi, he formulated a general type of schematic introduction rules to be matched ? thanks to the idea supporting the inversion principle ? by a corresponding general schematic Elimination rule. This was an attempt to provide a solution to the problem suggested by the often quoted note of Gentzen. According to Gentzen ?it should be possible to display the elimination rules as unique functions of the corresponding introduction rules on the basis of certain requirements?. Many people have since worked on this topic, which can be appropriately seen as the birthplace of what are now referred to as ?general elimination rules?, recently studied thoroughly by Sara Negri and Jan von Plato. In this study, we retrace the main threads of this chapter of proof-theoretical investigation, using Lorenzen's original framework as a general guide. (shrink)

In this paper, we provide a general setting under which results of normalization of proof trees such as, for instance, the logicality result in equational reasoning and the cut-elimination property in sequent or natural deduction calculi, can be unified and generalized. This is achieved by giving simple conditions which are sufficient to ensure that such normalization results hold, and which can be automatically checked since they are syntactical. These conditions are based on basic properties of elementary combinations of (...) inference rules which ensure that the induced global proof tree transformation processes do terminate. (shrink)

Developing early results of Prawitz, Tennant proposed a criterion for an expression to count as a paradox in the framework of Gentzen’s natural deduction: paradoxical expressions give rise to non-normalizing derivations. Two distinct kinds of cases, going back to Crabbé and Tennant, show that the criterion overgenerates, that is, there are derivations which are intuitively non-paradoxical but which fail to normalize. Tennant’s proposed solution consists in reformulating natural deduction elimination rules in general form. Developing intuitions of Ekman (...) we show that the adoption of general rules has the consequence of hiding redundancies within derivations. Once reductions to get rid of the hidden redundancies are devised, it is clear that the adoption of general elimination rules offers no remedy to the overgeneration of the Prawitz–Tennant analysis. In this way, we indirectly provide further support for a solution to one of the two overgeneration cases developed in previous work. (shrink)

Inductive characterizations of the sets of terms, the subset of strongly normalizing terms and normal forms are studied in order to reprove weak and strong normalization for the simply-typed λ-calculus and for an extension by sum types with permutative conversions. The analogous treatment of a new system with generalized applications inspired by generalized elimination rules in natural deduction, advocated by von Plato, shows the flexibility of the approach which does not use the strong computability/candidate style à la Tait (...) and Girard. It is also shown that the extension of the system with permutative conversions by η-rules is still strongly normalizing, and likewise for an extension of the system of generalized applications by a rule of ``immediate simplification''. By introducing an infinitely branching inductive rule the method even extends to Gödel's T. (shrink)

A constructivisation of the cut-elimination proof for sequent calculi for classical, intuitionistic and minimal infinitary logics with geometric rules—given in earlier work by the second author—is presented. This is achieved through a procedure where the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. The proof of admissibility of the structural rules is made ordinal-free by introducing a new well-founded relation based on a notion of embeddability of derivations. (...) Additionally, conservativity for classical over intuitionistic/minimal logic for the seven (finitary) Glivenko sequent classes is here shown to hold also for the corresponding infinitary classes. (shrink)

The main result of this paper is a normalizing system of natural deduction for the full language of intuitionistic linear logic. No explicit weakening or contraction rules for -formulas are needed. By the systematic use of general elimination rules a correspondence between normal derivations and cut-free derivations in sequent calculus is obtained. Normalization and the subformula property for normal derivations follow through translation to sequent calculus and cut-elimination.

The article presents a full proof‐theoretic semantics for natural deduction based on an extended inversion principle: the elimination rule for an operator q may invert the introduction rule for q, but also vice versa, the introduction rule for a connective q may invert the elimination rule for q. Such an inversion—extending Prawitz' concept of inversion—gives the following theorem: Inversion for two rules of operator q (intro rule, elim rule) exists iff a reduction of a maximum formula for (...) q exists. The inversion theorem is specified to two logics, Lambek calculus (LC) and intuitionistic linear logic (ILL), with four propositional connectives: two multiplicatives (implication and conjunction) and two additives (conjunction and disjunction), with two quantifiers and two modals. LC is defined by using elimination rules by composition. ILL is defined by using usual general elimination rules. Elimination rules by composition are an exciting alternative to general elimination rules; in some cases, they do not need permutations. (shrink)

We extend natural deduction for first-order logic (FOL) by introducing diagrams as components of formal proofs. From the viewpoint of FOL, we regard a diagram as a deductively closed conjunction of certain FOL formulas. On the basis of this observation, we first investigate basic heterogeneous logic (HL) wherein heterogeneous inference rules are defined in the styles of conjunction introduction and elimination rules of FOL. By examining what is a detour in our heterogeneous proofs, we discuss that an (...) elimination-introduction pair of rules constitutes a redex in our HL, which is opposite the usual redex in FOL. In terms of the notion of a redex, we prove the normalization theorem for HL, and we give a characterization of the structure of heterogeneous proofs. Every normal proof in our HL consists of applications of introduction rules followed by applications of elimination rules, which is also opposite the usual form of normal proofs in FOL. Thereafter, we extend the basic HL by extending the heterogeneous rule in the style of general elimination rules to include a wider range of heterogeneous systems. (shrink)

This paper proves the strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. Using them, this paper also proves the strong normalization of classical natural deduction with general elimination rules for implication and conjunction, and their permutative conversions. This paper also proves that natural deduction can be embedded into natural deduction with general elimination rules, strictly preserving proof normalization.

This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none of its deduced steps contains a term of the formn(n(t)) for some term t, where n denotes negation. The first question asks for conditions on the hypotheses that, if satisfied, guarantee the existence of a double-negation-free proof when the conclusion is free of double negation. The second question asks about the existence (...) of an axiom system for classical propositional calculus whose use, for theorems with a conclusion free of double negation, guarantees the existence of a double-negation-free proof. After giving conditions that answer the first question, we answer the second question by focusing on the Lukasiewicz three-axiom system. We then extend our studies to infinite-valued sentential calculus and to intuitionistic logic and generalize the notion of being double-negation free. The double-negation proofs of interest rely exclusively on the inference rule condensed detachment, a rule that combines modus ponens with an appropriately general rule of substitution. The automated reasoning program Otter played an indispensable role in this study. (shrink)

An (n, k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical systems with (n, k)-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion (...) of coherence to characterize strong cutelimination in such systems. We show that the following properties of a canonical system G with arbitrary (n, k)-ary quantifiers are equivalent: (i) G is coherent, (ii) G admits strong cut-elimination, and (iii) G has a strongly characteristic two-valued generalized non-deterministic matrix. (shrink)

. The term inversion principle goes back to Lorenzen who coined it in the early 1950s. It was later used by Prawitz and others to describe the symmetric relationship between introduction and elimination inferences in natural deduction, sometimes also called harmony. In dealing with the invertibility of rules of an arbitrary atomic production system, Lorenzen’s inversion principle has a much wider range than Prawitz’s adaptation to natural deduction. It is closely related to definitional reflection, which is a principle (...) for reasoning on the basis of rule-based atomic definitions, proposed by Hallnäs and Schroeder-Heister. After presenting definitional reflection and the inversion principle, it is shown that the inversion principle can be formally derived from definitional reflection, when the latter is viewed as a principle to establish admissibility. Furthermore, the relationship between definitional reflection and the inversion principle is investigated on the background of a universalization principle, called the ω- principle, which allows one to pass from the set of all defined substitution instances of a sequent to the sequent itself. (shrink)

In this paper we provide a proof theoretical investigation of logical argumentation, where arguments are represented by sequents, conflicts between arguments are represented by sequent elimination rules, and deductions are made by dynamic proof systems extending standard sequent calculi. The idea is to imitate argumentative movements in which certain claims are introduced or withdrawn in the presence of counter-claims. This is done by a dynamic evaluation of sequences of sequents, in which the latter are considered ‘derived’ or ‘not (...) derived’ according to the content of the sequence. We show that decisive conclusions of such a process correspond to well-accepted consequences of the underlying argumentation framework. The outcome is therefore a general and modular proof-theoretical approach for paraconsistent and non-monotonic reasoning with argumentation systems. (shrink)

In mainstream Anglo-American philosophy, the relation between cognition and community has been defined primarily in terms of the generalization of the mathematical function, especially as a model for the nature of rules, which thus come to be under-stood as algorithms. This leads to the elimination of both the reflexive, synthesizing subject, and the intrinsic communal-historical nature of argumentation and belief-formation. Against this approach, I follow R.G. Collingwood’s hitherto unrecognized strategy in his Essay on Metaphysics and argue that the (...) relation of cognition and community is better understood by way of the ancient and forgotten model of creedal rules of faith or trust. These will be shown to have the logical form of first person performative rules of faith or trust that generate third person declaratives or proposi-tions, and so constitute the possibility conditions for an argumentational logic of question and answer. They restore the synthetic subject, for they are not algorithms but reflexive and interpretive formulae; they are communally constituted and so historically saturated; and they reinstate an ontological theory of truth as disclosure, with coherence and comprehensiveness as its criteria. In these respects, as Collingwood saw, the creedal model provides a fresh interpretation of the historicality of argumentation and redefines the relation of cognition and community in terms of the interdependence of faith and reason. (shrink)

In this paper, we deal with a relationship among the law of excluded middle, the double negation elimination and the independence of premiss rule ) for intuitionistic predicate logic. After giving a general machinery, we give, as corollaries, several examples of extensions of \ and \ which are closed under \ but do not derive the independence of premiss axiom.

One lists the distinct pairs of categorical premises formulable via only the positive terms, S,P,M, by constructing a six by six matrix obtained by pairing the six categorical P-premises, A, O, A, O, where P* ∈ {P,P′}, with the six, similar, categorical S-premises. One shows how five rules of valid syllogism, select only 15 distinct PCPs that entail logical consequences belonging to the set L+: = {A, O, A, E, O, I}. The choice of admissible LCs can be regarded (...) as a condition separated from the conditions contained in the RofVS: the usual eight PCPs that generate valid syllogisms are obtained when the only admissible LCs belong to the set L: = {A, E, O, I} and no existential imports are addressed. A 64 PCP-matrix obtains when both PCPs and LCs may contain indefinite terms—the positive, S,P,M, terms, and their complementary sets, S′,P′, M′, in the universe of discourse, U, called the negative terms. Now one can accept eight LCs: A, I, where P* ∈ {P,P′}, S* ∈ {S,S′}, and there are 32 conclusive PCPs, entailing precise, “one partitioning subset of U” LCs. The four rules of conclusive syllogisms predict the less precise LCs, left after eliminating the middle term from the exact LCs. The RofCS also predict that the other 32 PCPs of the 64 PCP-matrix are non-conclusive. The RofVS and the RofCS are generalized, and arguments are given, for also accepting as valid syllogisms the conclusive syllogisms formulable via positive terms which entail the LCs A and O. (shrink)

The distribution of the flap allophone [ɾ] of American English, along with the other allophones of /t/,[t h,t =, ʔ, t] has been accounted for in various formal frameworks by assuming a number of different abstract mechanisms and entities. The desirability or usefulness of these formalisms is not at issue in the present paper. Instead, a computationally explicit model of categorization is used (Skousen 1989, 1992) in order to account for the distribution of the allophones of /t/ without recourse to (...) such formalisms. The simulations that were carried out suggest that they are not needed because analogy to surface apparent variables such as phones and word boundaries is sufficient to predict allophony. In analogy, the particular allophone of /t/ (i.e. [ɾ, t h, t =, ʔ, t]) that appears in a given context is determined on the basis of similarity to stored exemplars in the mental lexicon. From an acquisitional standpoint, categorization by analogy to stored exemplars dispenses with the need for rule induction although it does suggest that speakers group functionally related sounds into mental categories, a process that is influenced to a great deal by orthography. Analogy also explains the stochastic nature of linguistic performance. In the present study, 3,719 tokens of the allophones of the phoneme /t/ were extracted from the TIMIT corpus and constitute the database from which analogs were chosen. The variables used included the three phones or boundaries on either side of /t/, and the stress of the syllables preceding and following /t/. The model proves quite successful in predicting the correct allophone, and the errors made are generally possible alternative pronunciations (e.g. moun[ʔ]ain, moun[t h ]ain). The success rate changes little when only small sub-samples of the database are incorporated. In addition, exemplar-modeling is found to be quite robust because even when a feature such as stress is eliminated, (a feature which is critical in most rule approaches), allophony is still highly predictable. (shrink)

The paper begins with a conceptual discussion of Michael Dummett's proof-theoretic justification of deduction or proof-theoretic semantics, which is based on what we might call Gentzen's thesis: 'the introductions constitute, so to speak, the "definitions" of the symbols concerned, and the eliminations are in the end only consequences thereof, which could be expressed thus: In the elimination of a symbol, the formula in question, whose outer symbol it concerns, may only "be used as that which it means on the (...) basis of the introduction of this symbol".' The intuitive philosophical content of Dummett's notions of harmony and stability is that harmony obtains if the grounds for asserting a proposition match the consequences of accepting it, and stability obtains if the converse also holds. Rules of inference define the meanings of a logical constant they govern if and only if they are stable. Gentzen observed that 'it should be possible to establish on the basis of certain requirements that the elimination rules are functions of the corresponding introduction rules.' One of the objectives of this paper is to specify such a function: I will specify a process by which it is possible to determine the elimination rules of logical constants from their introduction rules, and conversely, to determine the introduction rules from the elimination rules. I'll give the general forms of rules of inference and generalised reduction procedures for the normalisation of deduction. I'll give a formally precise characterisations of harmony and stability and show that deductions in logics that contain only constants governed by stable rules always normalise. (shrink)