Let F be a formal system. We consider a fragment of F to be a formal system obtained from F by removing some primitive symbols and the corresponding inference schemata. To begin with we look at normal deductions in the formal system obtained by removing the symbols ∃, ∨ and = and the inference schemata corresponding to these symbols from N. We let N−∃∨= denote this formal system.

In addition to the uniqueness of names of eigenvariables we have restrictions on deductions concerning the scopes of eigenvariables. The scope of an eigenvariable in a deduction D is the subdeduction of D in which the eigenvariable is defined. The scope of an eigenvariable of an ∀I inference is the premise deduction of the inference. We have the restriction on deductions that an eigenvariable of an inference may not occur free in any open assumption in the scope of the eigenvariable other than assumptions cancelled at the inference.

Definition 2 In N−∃∨= a cut is formula occurrence which is both the conclusion of an introduction inference and the major premise of an elimination inference. A normal deduction is a deduction containing no cut.

Definition 3 A branch in a deduction D is a sequence A1, A2,..., An of formula occurrences in D such that: (1) A1 is an assumption. (2) For each i such that 1 ≤ i < n, Ai stands immediately above Ai +1 and Ai is not the minor premise of an elimination inference. (3) An is the end formula of the deduction or the minor premise of an elimination inference. An E -part of a branch is a sequence of consecutive formulas of the branch, none of which is the conclusion of an introduction inference. An I -part of a branch is a sequence of consecutive formulas of the branch, all of which are the conclusions of introduction inferences. A main branch is a branch A1, A2,..., An , with An as the end formula of the deduction. An E -main branch is a main branch consisting only of an E-part. Note that there cannot be more than one E-main branch in a deduction.

If a formula occurrence in a deduction in N−∃∨= is a minor premise of an elimination inference then this formula occurrence is the minor premise of an ⊃E inference. The reason that the phrase the minor premise of an elimination inference is used in the definition of a branch above is to make the definition applicable to deductions in other formal systems, where it is not the case that a minor premise of an elimination inference always is the minor premise of an ⊃E inference.

Proposition 4Every branch in a normal deduction inN−∃∨= consists of an E -part followed by a (possibly empty) I -part.

Proposition 5A normal proof inN−∃∨= has an introduction inference as its last inference.

Reductions of Deductions in N−=

We use D =⇒ E to denote that D reduces to the deduction E . If there is a deduction E such that D =⇒ E then D is reducible. D reduces in zero steps to itself. If there are deductions E1,..., En , where n ≥ 1, such that

D =⇒ E1 =⇒ ... =⇒ En

then D reduces in n steps to the deduction En . Hence, the two phrases D reduces in one step to E and D reduces to E have the same meaning. If there is an n ≥ 0 and a deduction E such that D reduces in n steps to E , and E is not reducible, then D is normalizable. If there is no infinite family {Ei }, i = 1, 2, 3,... of deductions such that D =⇒ E1 and Ei =⇒ Ei +1, for i ≥ 1, then D is strongly normalizable.

The relation =⇒ is defined inductively, by the schemata below. Notice that a deduction is reducible only if it has a cut and that the reduction defined removes the cut.

Epsilon reduction Imply reduction

D [ A] E

A[t/x]

t ∈{x | A} ∈I =⇒ D

A[t /x ] D A

B E =⇒

⊃ D

A[t /x ] ∈E A⊃B A

B ⊃

I

I F =

B C ∨E C

Exist reduction For all reduction

D

A[t/x]

∃I [ A]

E D

A[t /x ]

=⇒ D

A

∀I D [t /x ]

=⇒

∃xA C

C ∃ E [t /x ]

C∀xA A[t /x ] ∀ A[t /x ]

For two further reductions (Left Compose and Subderivation) see Ekman (1994) [2, Sect. 4.1].

Propositional Logic

Propositional logic is the formal system P obtained by removing the symbols ∈, ∀, ∃ and = and the inference schemata corresponding to these symbols from N. The formal system P does not have any term variables but instead propositional variables. The language of P is the set of formulas, inductively defined as follows. The propositional variables P, Q, R and ⊥ are formulas, and if A and B are formulas, then A ⊃ B, A & B and A ∨ B are formulas.

A branch in a deduction in P is defined as a branch in a deduction in N−∃∨=. The notion of a cut in a deduction in P and the notion of a normal deduction in P is defined as in N−=. The definitions of an E-part of a branch, an I-part of a branch, a main branch and an E-main branch are the same for a branch in a deduction in N as for a branch in a deduction in N−∃∨=.

References

1. Crabbé, M.: Non-normalisation de la théorie de Zermelo. logic-center.be/ Publications/Bibliotheque/contreexemple.pdf (sketch of the result presented at the Proof Theory Symposium held in Kiel in 1974)

2. Ekman, J.: Normal proofs in set theory. Ph.D. thesis, Department of Computing Science, University of Göteborg (1994)

3. Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39, 176210, 405-431 (1934/35) (English translation in: The Collected Papers of Gerhard Gentzen (Szabo, M.E. (ed.). Amsterdam, North Holland (1969), pp. 68-131)

4. Girard, J.-Y.: Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium, pp. 63-92. North-Holland, Amsterdam (1971)

5. Martin-Löf, P.: Hauptsatz for the theory of species. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium, pp. 217-233. North-Holland, Amsterdam (1971)

6. Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell, Stockholm (1965). Reprinted Dover Publ., Mineola 2006

7. Prawitz, D.: Ideas and results in proof theory. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium (Oslo 1970), pp. 235–307. North-Holland, Amsterdam (1971)

Found a mistake? Please highlight the word and press Shift + Enter