# Normal Deductions in a Fragment of N

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 *A*1*, A*2*,..., An* of formula occurrences in *D* such that: (1) *A*1 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 *A*1*, A*2*,..., 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 4** *Every branch in a normal deduction in* **N**−∃∨= *consists of an E -part followed by a (possibly empty) I -part.*

**Proposition 5** *A normal proof in* **N**−∃∨= *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 *E*1*,..., En* , where *n* ≥ 1, such that

*D* =⇒ *E*1 =⇒ *...* =⇒ *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* =⇒ *E*1 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* ]

=⇒

__ ____ __ __∃____x____A 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)