Under the assumption that meaning conditions formally express the way in which a proposition is used, as outlined in Sect. 2, it is a bit more complicated to define the meaning conditions associated with a formal system with quantifiers than it is to define the meaning conditions associated with a quantifier-free formal system. In this section we shall study the notion of self-contradictory deductions in the formal system N−∃=, which is the fragment of N obtained by removing the symbols ∃ and

= and the inference schemata corresponding to these symbols from N. We shall also prove the following theorem.

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

Let A be any formula. To define the meaning conditions associated with the formal system N−∃= we shall informally consider ∀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−∃=.

A naïve way to give the meaning conditions associated with N−∃= is to add the following meaning conditions to the meaning conditions associated with N−∀∃=, where λ is assumed to have been added to the constructors of the syntax defining what the set of formal meanings to be assigned to formulas in deductions is, such that λm is a meaning for any meaning m.

D

m : A

λm : ∀xA ∀ D

λm :∀xA

m : A[t /x ] ∀

With meaning conditions given this way, we require that there is a one to one correspondence between the meaning of the premise and the conclusion both for ∀I inferences and for ∀E inferences. This condition is however too strong, if we consider ∀xA to represent the informally given infinitely long formula above, since the meaning conditions given for &E inferences does not require that there is a one to one correspondence between the meaning of the premise and the conclusion of an

&E inference. As an example, consider the following deduction.

[r ∈{y | A}& (r ∈{y |¬A}& C)] &E

r ∈{y |¬A}& C &E

r ∈{y |¬A}

∈E [r ∈{y |A}& (r ∈{y |¬A}& C)] &E

r ∈{y | A}

∈E

¬A[r/y] A[r/y]

⊃E

⊥ I

¬(r ∈ {y | A} & (r ∈ {y | ¬ A} & C))

This deduction is non-self-contradictory independently of which formulas A and C are. It is straightforward to assign meanings to the formula occurrences of the deduction above such that this assignment satisfies the meaning conditions. Assume that C is ∀x (r ∈ x ) and let us consider C to represent the informally given formula (r ∈ t1) & ((r ∈ t2) & ((r ∈ t3) & .. .)), where t1, t2, t3,... are all terms of the formal

system N−∃=. Then r ∈ {y | A} & (r ∈ {y | ¬ A} & C) and C informally represent the same formula. We have the following proof of ¬C, which from an informal point of view is another presentation of the deduction above.

[∀x(r ∈x)]

r ∈{y |¬A} ∀E

∈E [∀x(r ∈x)]

r ∈{y | A} ∀E

∈E

¬A[r/y] A[r/y] E

⊥ I ⊃

¬∀x (r ∈ x )

This deduction is self-contradictory if the meaning conditions are given as above.

We suggest the following definition of meaning conditions associated with 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, m + n and λx .m are meanings. The meaning conditions are the following and in addition the meaning conditions associated with the formal system N−∀∃=.

D

m : A

λx .m : ∀xA ∀ D

λx.m :∀xA m[n/x ] : A[t /x ] ∀

We have the restriction on the meaning variable, designated x , in the ∀I meaning condition schema that it may not occur free in any meaning assigned to an open assumption in D . This restriction excludes, for instance, the following decoration of a deduction.

λy.x :∀y(r ∈ y)

x :r ∈x ∀E

λx .x : ∀x (r ∈ x ) ∀I

Remember that the aim is to define the meaning conditions so that the meaning conditions express a constraint given by the meaning forced on a proposition given by an argument, in the sense of Sect. 2. Remember also that the meaning forced on a proposition given by an argument is arbitrary so far as what is considered to be known is arbitrary, when knowing only what kind of steps the steps of the argument are. We do not claim that the meaning conditions given are the only possible. The given meaning conditions express constraints which we judge as accurate.

We have chosen the constraint defined by the meaning conditions to be no more restrictive than what is necessary to prove Theorem 2. There are however reasons to consider further restrictions on the meaning conditions. Consider the deduction

m 1 : A

λx.x :∀xA ∀I

m2 : A ∀E

Assume that x does not occur free in A. Then the constraint defined by the meaning conditions can be strengthened so that m2 and m1 are required to be syntactically equal. More generally, if x occurs free in A we can strengthen the constraint defined by the meaning conditions so that, in an informal sense, if one “submeaning” of m2 and one “submeaning” of m1 “correspond” to the same subformula of A, and x does not occur free in this subformula, then these “submeanings” of m1 and m2, respectively, are required to be syntactically equal.

In the following we shall not assume this last restriction to be added. Of course, if Theorem 2 holds without this restriction added to the restrictions of the meaning conditions, then this theorem also is true with this restriction added.

All meaning condition schemata except the ⊥E meaning condition schema define

a relation between the meanings assigned to the premises and the conclusion of the inference. We can interpret this as follows: use of the ⊥E inference schema says that nothing more is known about how the premise of an ⊥E inference is derived other than that it is the premise of an ⊥E inference. Instead of having ⊥ primitively given in N we can define it by ∀x (r ∈ x ), where r is an arbitrary term. We then have the

⊥E inference schema as a derived schema, derived as follows, where x is supposed to be chosen so that x does not occur free in A.

λx.Ex :∀x(r ∈x)

Em :r ∈{x | A} ∀E

m : A ∈E

Then if we also take false to be defined by λx .Ex we have the ⊥E meaning condition schema as a derived meaning condition schema, derived from the meaning condition schemata ∀E and ∈E.

Lemma 2If a deduction D is non-self-contradictory and D reduces to E then also the deduction E is non-self-contradictory.

The proof of Theorem 2 is similar to the proof of Theorem 1. To prove Theorem 1 we define a function ∗ from the set of non-self-contradictory deductions in N−∀∃= to the set of deductions in P. To prove Theorem 2 we shall instead defined a function

∗ from the set of non-self-contradictory deductions in N−∃= to the set of deductions

in P2, where P2 denotes the formal system of second order propositional logic. The

language of P2 is the set of formulas, inductively defined as follows. The propositional variables X, X1, X2,... and ⊥ are formulas, and if A and B are formulas, then A⊃ B, A & B, A ∨ B and ∀XA are formulas. The ⊥, ⊃, & and ∨ inference schemata are

the same for P2 as for the formal system N . The ∀ inference schemata for P2

are the following. D

A

∀XA ∀I D

∀XA A[B/ X ] ∀

We have the restriction on deductions in P2 that the variable designated X in the ∀I schema may not occur free in any open assumption in the deduction designated D . The reduction rules for deductions in P2 are the same as the reduction

rules for deductions in N−∃= except that the substitution of a term for a variable in the ∀-reduction in N corresponds, in P2, to a substitution of a proposition for a propositional variable. We presuppose that the set of variables of N−∃= and the set of propositional variables of P2 have the same cardinality. Hence there is a one

to one correspondence, ∗ say, between the set of variables of N−∃= and the set of

propositional variables of P2. For any variable x of N we let the propositional

variable X of P2 denote x ∗. The function ∗ from the set of meanings to be assigned

2

to formulas in deductions in the formal system N−∃= onto the set of formulas of P

The function ∗ is extended to a function from the set of sets of meanings to be assigned to formulas in deductions in the formal system N−∃= onto the set of sets of formulas of P2 by letting Γ ∗ denote the set of formulas A∗ such that A belongs to Γ , for all sets Γ of meanings to be assigned to formulas in deductions in the formal system

N−∃=. In a similar way as in Sect. 4 we extend ∗ once more, to a function from the

set of non-self-contradictory deductions in N to the set of deductions in P2. To define this function we add the following clauses to the definition of the function ∗

in Sect. 4.

I D

m : A

λx .m : ∀xA

I D ∗

∀I ≡

∗ D ∗

m∗

∀Xm∗ ∀I

D ∗

λx.m :∀xA m[n/x ] : A[t /x ] ∀ ≡ ∀Xm∗

m∗[n∗/ X ] ∀

The definition of a(θ, E , D ), given in Sect. 4, extends from deductions in N−∀∃= to deductions in N−∃= by defining a(θ, E , D ) also in the case D reduces to E via an ∀ reduction. This is done in a similar way as for the other cases of the kind of reduction that takes D to E .

Proposition 2Assume that D is a non-self-contradictory deduction, θ is an assignment of formal meanings to the formula occurrences in D such that this assignment satisfies the meaning conditions and D =⇒ E . Let D also denote the deduction obtained from D by decorating the formula occurrences in D with θ . Let E also

denote the deduction obtained from E by decorating the formula occurrences in E

with a(θ, E , D ). Then D ∗ =⇒ E ∗.

From Girard (1971) [4] it is known that deductions in P2 are strongly normalizable; see also Martin-Löf (1971) [5]. From this together with Proposition 2, Theorem 2 follows.

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