scholarly journals The normalization theorem for extended natural deduction

2017 ◽  
Vol 101 (115) ◽  
pp. 75-98
Author(s):  
Mirjana Borisavljevic
Keyword(s):  
Natural Deduction ◽  
Standard System ◽  
Cut Elimination ◽  
Normalization Theorem

The normalization theorem for the system of extended natural deduction will be proved as a consequence of the cut-elimination theorem, by using the connections between the system of extended natural deduction and a standard system of sequents.

Gentzen's Proof of Normalization for Natural Deduction

2008 ◽  
Vol 14 (2) ◽  
pp. 240-257 ◽  
Author(s):  
Jan von Plato
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Direct Proof ◽  
Cut Elimination ◽  
Doctoral Thesis ◽  
Detailed Proof ◽  
Normalization Theorem ◽  
The One ◽  
The Right ◽  
Special Case

AbstractGentzen writes in the published version of his doctoral thesis Untersuchungen über das logische Schliessen (Investigations into logical reasoning) that he was able to prove the normalization theorem only for intuitionistic natural deduction, but not for classical. To cover the latter, he developed classical sequent calculus and proved a corresponding theorem, the famous cut elimination result. Its proof was organized so that a cut elimination result for an intuitionistic sequent calculus came out as a special case, namely the one in which the sequents have at most one formula in the right, succedent part. Thus, there was no need for a direct proof of normalization for intuitionistic natural deduction. The only traces of such a proof in the published thesis are some convertibilities, such as when an implication introduction is followed by an implication elimination [1934–35, II.5.13]. It remained to Dag Prawitz in 1965 to work out a proof of normalization. Another, less known proof was given also in 1965 by Andres Raggio.We found in February 2005 an early handwritten version of Gentzen's thesis, with exactly the above title, but with rather different contents: Most remarkably, it contains a detailed proof of normalization for what became the standard system of natural deduction. The manuscript is located in the Paul Bernays collection at the ETH-Zurichwith the signum Hs. 974: 271. Bernays must have gotten it well before the time of his being expelled from Göttingen on the basis of the racial laws in April 1933.

scholarly journals Normalization as a consequence of cut elimination

2009 ◽  
Vol 86 (100) ◽  
pp. 27-34
Author(s):  
Mirjana Borisavljevic
Keyword(s):  
Intuitionistic Logic ◽  
Natural Deduction ◽  
Cut Elimination ◽  
Deduction System ◽  
Normalization Theorem ◽  
Natural Deduction System

Pairs of systems, which consist of a system of sequents and a natural deduction system for some part of intuitionistic logic, are considered. For each of these pairs of systems the property that the normalization theorem is a consequence of the cut-elimination theorem is presented.

Normalization theorems for full first order classical natural deduction

1991 ◽  
Vol 56 (1) ◽  
pp. 129-149 ◽  
Author(s):  
Gunnar Stålmarck
Keyword(s):  
Normal Form ◽  
Natural Deduction ◽  
Full System ◽  
Strong Normalization ◽  
Logical Constants ◽  
Restricted Version ◽  
First Order ◽  
Form Theorem ◽  
Normalization Theorem ◽  
Normal Form Theorem

In this paper we prove the strong normalization theorem for full first order classical N.D. (natural deduction)—full in the sense that all logical constants are taken as primitive. We also give a syntactic proof of the normal form theorem and (weak) normalization for the same system.The theorem has been stated several times, and some proofs appear in the literature. The first proof occurs in Statman [1], where full first order classical N.D. (with the elimination rules for ∨ and ∃ restricted to atomic conclusions) is embedded in a system for second order (propositional) intuitionistic N.D., for which a strong normalization theorem is proved using strongly impredicative methods.A proof of the normal form theorem and (weak) normalization theorem occurs in Seldin [1] as an extension of a proof of the same theorem for an N.D.-system for the intermediate logic called MH.The proof of the strong normalization theorem presented in this paper is obtained by proving that a certain kind of validity applies to all derivations in the system considered.The notion “validity” is adopted from Prawitz [2], where it is used to prove the strong normalization theorem for a restricted version of first order classical N.D., and is extended to cover the full system. Notions similar to “validity” have been used earlier by Tait (convertability), Girard (réducibilité) and Martin-Löf (computability).In Prawitz [2] the N.D. system is restricted in the sense that ∨ and ∃ are not treated as primitive logical constants, and hence the deductions can only be seen to be “natural” with respect to the other logical constants. To spell it out, the strong normalization theorem for the restricted version of first order classical N.D. together with the well-known results on the definability of the rules for ∨ and ∃ in the restricted system does not imply the normalization theorem for the full system.

A sequent calculus for type assignment

1977 ◽  
Vol 42 (1) ◽  
pp. 11-28 ◽  
Author(s):  
Jonathan P. Seldin
Keyword(s):  
Normal Form ◽  
Main Part ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
Cut Elimination ◽  
Type Assignment ◽  
Image Position ◽  
Atomic Type

The sequent calculus formulation (L-formulation) of the theory of functionality without the rules allowing for conversion of subjects of [3, §14E6] fails because the (cut) elimination theorem (ET) fails. This can be most easily seen by the fact that it is easy to prove in the systemandbut not (as is obvious if α is an atomic type [an F-simple])The error in the “proof” of ET in [14, §3E6], [3, §14E6], and [7, §9C] occurs in Stage 3, where it is implicitly assumed that if [x]X ≡ [x] Y then X ≡ Y. In the above counterexample, we have [x]x ≡ ∣ ≡ [x](∣x) but x ≢ ∣x. Since the formulation of [2, §9F] is not really satisfactory (for reasons stated in [3, §14E]), a new seguent calculus formulation is needed for the case in which the rules for subject conversions are not present. The main part of this paper is devoted to presenting such a formulation and proving it equivalent to the natural deduction formulation (T-formulation). The paper will conclude in §6 with some remarks on the result that every ob (term) with a type (functional character) has a normal form.The conventions and definitions of [3], especially of §12D and Chapter 14, will be used throughout the paper.

Gentzen's Proof Systems: Byproducts in a Work of Genius

2012 ◽  
Vol 18 (3) ◽  
pp. 313-367 ◽  
Author(s):  
Jan von Plato
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Central Component ◽  
Cut Elimination ◽  
Complete Class ◽  
Tree Form ◽  
Proof Systems ◽  
Set Up ◽  
Logical Calculi ◽  
Subformula Property

AbstractGentzen's systems of natural deduction and sequent calculus were byproducts in his program of proving the consistency of arithmetic and analysis. It is suggested that the central component in his results on logical calculi was the use of a tree form for derivations. It allows the composition of derivations and the permutation of the order of application of rules, with a full control over the structure of derivations as a result. Recently found documents shed new light on the discovery of these calculi. In particular, Gentzen set up five different forms of natural calculi and gave a detailed proof of normalization for intuitionistic natural deduction. An early handwritten manuscript of his thesis shows that a direct translation from natural deduction to the axiomatic logic of Hilbert and Ackermann was, in addition to the influence of Paul Hertz, the second component in the discovery of sequent calculus. A system intermediate between the sequent calculus LI and axiomatic logic, denoted LIG in unpublished sources, is implicit in Gentzen's published thesis of 1934–35. The calculus has half rules, half “groundsequents,” and does not allow full cut elimination. Nevertheless, a translation from LI to LIG in the published thesis gives a subformula property for a complete class of derivations in LIG. After the thesis, Gentzen continued to work on variants of sequent calculi for ten more years, in the hope to find a consistency proof for arithmetic within an intuitionistic calculus.

A normalization theorem for set theory

1988 ◽  
Vol 53 (3) ◽  
pp. 673-695 ◽  
Author(s):  
Sidney C. Bailin
Keyword(s):  
Set Theory ◽  
Natural Deduction ◽  
Inference Rule ◽  
Major Premise ◽  
Elimination Rule ◽  
Introduction Rule ◽  
Normalization Theorem ◽  
Image Position ◽  
Well Foundedness

In this paper we present a normalization theorem for a natural deduction formulation of Zermelo set theory. Our result gets around M. Crabbe's counterexample to normalizability (Hallnäs [3]) by adding an inference rule of the formand requiring that this rule be used wherever it is applicable. Alternatively, we can regard the result as pertaining to a modified notion of normalization, in which an inferenceis never considered reducible if A is T Є T, even if R is an elimination rule and the major premise of R is the conclusion of an introduction rule. A third alternative is to regard (1) as a derived rule: using the general well-foundedness rulewe can derive (1). If we regard (2) as neutral with respect to the normality of derivations (i.e., (2) counts as neither an introduction nor an elimination rule), then the resulting proofs are normal.

scholarly journals A short proof of the strong normalization of classical natural deduction with disjunction

2003 ◽  
Vol 68 (4) ◽  
pp. 1277-1288 ◽  
Author(s):  
René David ◽  
Karim Nour
Keyword(s):  
Natural Deduction ◽  
Elementary Proof ◽  
Short Proof ◽  
Cut Elimination ◽  
Strong Normalization ◽  
Elimination Procedure

AbstractWe give a direct, purely arithmetical and elementary proof of the strong normalization of the cut-elimination procedure for full (i.e., in presence of all the usual connectives) classical natural deduction.

scholarly journals Lambda terms for natural deduction, sequent calculus and cut elimination

2000 ◽  
Vol 10 (1) ◽  
pp. 121-134 ◽  
Author(s):  
HENK BARENDREGT ◽  
SILVIA GHILEZAN
Keyword(s):  
Normal Form ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
The Other ◽  
Cut Elimination ◽  
Simple Consequence ◽  
Type Assignment ◽  
Two Systems ◽  
The Many

It is well known that there is an isomorphism between natural deduction derivations and typed lambda terms. Moreover, normalising these terms corresponds to eliminating cuts in the equivalent sequent calculus derivations. Several papers have been written on this topic. The correspondence between sequent calculus derivations and natural deduction derivations is, however, not a one-one map, which causes some syntactic technicalities. The correspondence is best explained by two extensionally equivalent type assignment systems for untyped lambda terms, one corresponding to natural deduction (λN) and the other to sequent calculus (λL). These two systems constitute different grammars for generating the same (type assignment relation for untyped) lambda terms. The second grammar is ambiguous, but the first one is not. This fact explains the many-one correspondence mentioned above. Moreover, the second type assignment system has a ‘cut-free’ fragment (λLcf). This fragment generates exactly the typeable lambda terms in normal form. The cut elimination theorem becomes a simple consequence of the fact that typed lambda terms possess a normal form.

scholarly journals Cut-free Sequent Calculus and Natural Deduction for the Tetravalent Modal Logic

Studia Logica ◽  
2021 ◽  
Author(s):  
Martín Figallo
Keyword(s):  
Modal Logic ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
The Other ◽  
Cut Elimination ◽  
Modal Algebras ◽  
General Method

AbstractThe tetravalent modal logic ($${\mathcal {TML}}$$ TML ) is one of the two logics defined by Font and Rius (J Symb Log 65(2):481–518, 2000) (the other is the normal tetravalent modal logic$${{\mathcal {TML}}}^N$$ TML N ) in connection with Monteiro’s tetravalent modal algebras. These logics are expansions of the well-known Belnap–Dunn’s four-valued logic that combine a many-valued character (tetravalence) with a modal character. In fact, $${\mathcal {TML}}$$ TML is the logic that preserves degrees of truth with respect to tetravalent modal algebras. As Font and Rius observed, the connection between the logic $${\mathcal {TML}}$$ TML and the algebras is not so good as in $${{\mathcal {TML}}}^N$$ TML N , but, as a compensation, it has a better proof-theoretic behavior, since it has a strongly adequate Gentzen calculus (see Font and Rius in J Symb Log 65(2):481–518, 2000). In this work, we prove that the sequent calculus given by Font and Rius does not enjoy the cut-elimination property. Then, using a general method proposed by Avron et al. (Log Univ 1:41–69, 2006), we provide a sequent calculus for $${\mathcal {TML}}$$ TML with the cut-elimination property. Finally, inspired by the latter, we present a natural deduction system, sound and complete with respect to the tetravalent modal logic.

Sign in / Sign up

Export Citation Format

Share Document