The meaning conditions associated with N−= are defined by adding to the meaning conditions associated with N−∃= some constraints given by informally considering

∃xA to represent the informally given infinitely long formula A[t1/x ]∨ ( A[t2/x ]∨

( A[t3/x ]∨.. .)), where t1, t2, t3,... are all terms of the formal system N−=. The set of

formal meanings to be assigned to formulas in deductions in the formal system N−=

is inductively defined as follows. The meaning variable x and false are meanings, and if m and n are meanings, then Em, m ⇒ n, m ∧ n, λx .m and μx .m are meanings.

The meaning conditions associated with the formal system N−= are the following, and in addition the meaning conditions associated with the formal system N−∃=.

[m : A]

D D E

m[n/x]: A[t/x]

μx .m : ∃xA ∃I μx.m :∃xA n :C

n : C ∃E

We have the restriction on the meaning variable designated x in the ∃E meaning condition schema that neither may it occur free in the meaning designated n assigned to the subsequent premise of the ∃E nor may it occur free in any meaning assigned to an open assumption of the deduction of the subsequent premise E other than the open assumption designated A.

Theorem 3Every non-self-contradictory deduction inN−= is normalizable.

Let PR be the formal system with the same language as N−=, obtained by removing the ∈-inferences from N. We have the following result concerning PR.

Proof Let D be any given deduction in PR. We shall define an assignment of formal meanings to the formulas in D such that this assignment satisfies the meaning conditions. This assignment is defined by decorating every formula occurrence A in D with the formal meaning A◦, where ◦ is a function from the set of formulas of PR to the set of formal meanings to be assigned to formulas in deductions in the formal

system N−=. The bijection ◦ is defined as follows.

We present the system N of natural deduction for naïve set theory. The syntactic categories of the language of N are

1. Variables, x , y, z

2. Terms, r, s, t, u, v,w

3. Formulas, A, B, C,...

The language of N is the set of terms and formulas, inductively defined as follows. Variables x , y and z are terms, and if A is a formula, then {x | A} is a term. If r and s are terms, then r = s and r ∈ s are formulas, and if A and B are formulas, then A ⊃ B, A & B, ∀x A, A ∨ B and ∃xA are formulas; ⊥ is also a formula. The symbols used in the language of a formal system are the primitive symbols of that formal system. In addition to the primitive symbols of N, we shall use the following defined symbols

¬ A ≡ A ⊃⊥

r ∈/ s ≡ ¬(r ∈ s)

We use D , E , F ,... to denote deductions. The deductions in N are defined by the following inference schemata.

D

A[t/x]

t ∈ {x | A} ∈I

[ A] D

t ∈{x | A}

A[t /x ] ∈E

D

⊥ E

A

D D E

B A ⊃ B ⊃I A⊃B A

B ⊃

D E D D

A B &I

A & B A& B &E

A A& B &E

B

D

A

∀xA ∀I

D D

∀xA A[t /x ]

D ∀E [ A]

E

A[t/x]

∃xA ∃I ∃xA C C

[ A1] ∃E

[ A2]

D D D E F

A A ∨ B ∨I

[x ∈ r ] B A ∨ B ∨I

[y ∈ t ] A1 ∨A2 C C

C ∨E

D E D E D E

x ∈t y ∈r

r = t =I r =t A [r/x]

A[t /x ] =E r =t A [t/x]

A[r/x ] =E

An inference is an application of an inference schema. An atomic formula is a formula that cannot be the conclusion of an introduction inference. In an elimination inference the leftmost premise is the major premise and all other premises, if there are any, are the minor premises. A proof is a deduction without open assumptions. A subdeduction is defined to be an occurrence of a subdeduction in a deduction.

The variable x in the ∀I and ∃E schemata and the variables x and y in the =I

schema designate eigenvariables of inferences. We require that the eigenvariables occurring in a deduction D are syntactically distinguished from each other and from variables with free non-eigenvariable occurrences in D .

For a treatment of the basic concepts of natural deduction the reader is referred to Gentzen (1969) [3] and Prawitz (1965, 1971) [6, 7].

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