Self-contradictory Reasoning

Abstract

This paper concerns the characterization of paradoxical reasoning in terms of structures of proofs. The starting point is the observation that many paradoxes use self-reference to give a statement a double meaning and that this double meaning results in a contradiction. Continuing by constraining the concept of meaning by the inferences of a derivation “self-contradictory reasoning” is formalized as reasoning with statements that have a double meaning, or equivalently, cannot be given any meaning. The “meanings” derived this way are global for the argument as a whole. That is, they are not only constraints for each separate inference step of the argument. It is shown that the basic examples of paradoxes, the liar paradox and Russell’s paradox, are self-contradictory. Self-contradiction is not only a structure of paradoxes but is found also in proofs using self-reference. Self-contradiction is formalized in natural deduction systems for naïve set theory, and it is shown that self-contradiction is related to normalization. Non-normalizable deductions are self-contradictory.

This article is based on Chap. 5 of the author’s PhD thesis; see Ekman (1994) [2]. Definitions of elementary notions can be found in the Appendix below.

1 Introduction

Let us consider Russell’s paradox:

Let t be the set of all sets not containing themselves. Assume that t contains itself. Hence, by the definition of t, t does not contain itself. This contradicts the assumption that t contains itself and hence t does not contain itself. Since t does not contain itself, it follows from the definition of t that t contains itself. This is a contradiction.

Let us take a closer look at the part of Russell’s paradox that proves that t does not contain itself. Let $\mathscr {E_R}$ be this part of Russell’s paradox. We observe that the assumption that t contains itself is used twice in $\mathscr {E_R}$. We shall now distinguish the use of an assumption from how it is used. Let us therefore, to express that an assumption is used in an argument, say that the assumption occurs in an argument. Thus there are two occurrences of the assumption that t contains itself in $\mathscr {E_R}$. One of these two occurrences of the assumption that t contains itself is used together with the definition of t to derive that t does not contain itself. To contradict this last proposition the other occurrence of the assumption that t contains itself is used. Hence, there are two occurrences of the assumption that t contains itself in $\mathscr {E_R}$, and they are used in such a way that they contradict each other. In the last step of $\mathscr {E_R}$, the conclusion that t does not contain itself is drawn from the contradiction that the assumption that t contains itself leads to. In a sense the two occurrences of the assumption that t contains itself are identified in this step. Considering the two occurrences of the assumption that t contains itself as one and the same proposition, we have that there in $\mathscr {E_R}$ is a proposition which is used in two ways and that the two ways of using the proposition are incompatible.

A self-contradictory argument is, informally, an argument, as $\mathscr {E_R}$ above, in which there is a proposition which is used in two or more ways such that not all of the ways of using the proposition are compatible. In this article we aim to make those ideas more precise and formally express the notion of self-contradictory reasoning in some formal systems.

2 Meaning Conditions

The notion of a self-contradictory argument as introduced in the previous section is based on “the way in which a proposition is used in an argument.” In this section we aim at making it more precise what we mean by this, and we will outline how the notion of a self-contradictory argument will be formally expressed in the succeeding sections. Given an argument and a proposition of this argument we shall in the following consider the meaning forced on the proposition, by the steps of the argument. The meaning forced on a proposition, by the steps of the argument, expresses precisely the way in which the proposition is used in the argument.

Let us consider an example. Let $\mathscr {D}$ be the following argument: The wind is blowing because it’s snowing and the wind is blowing. Let A be the proposition it’s snowing and the wind is blowing and let B be the proposition the wind is blowing. Thus $\mathscr {D}$ consists of one step and A and B are the premise and the conclusion, respectively, of this step. If we forget about which propositions A and B represent we still know something about them by remembering what kind of step the inference of $\mathscr {D}$ is. That is, knowing only that the inference of $\mathscr {D}$ is of the kind that informally corresponds to one of the $\mathbin { \& }\mathrm {E}$ inference schemata in natural deduction for naïve set theory $\mathbf {N}$ (see Appendix below), we know that since A is the premise of the step, A is $A_1$ and $A_2$ for some propositions $A_1$ and $A_2$. Moreover, if A is $A_1$ and $A_2$ then B is $A_2$. The meaning forced on the propositions A and B by the inference of $\mathscr {D}$ is this knowledge about A and B given by the knowledge about what kind of step the inference of $\mathscr {D}$ is. Hence the meaning of the meaning forced on the proposition, by the steps of the argument depends on what is considered to be known, when knowing only what kind of steps the steps of the argument are.

In the previous section, “a self-contradictory argument” was explained to be an argument in which there is a proposition which is used in two or more ways such that not all of the ways of using the proposition are compatible. In this section “the meaning forced on a proposition, by the steps of the argument” expresses precisely the way in which the proposition is used in the argument. Hence, we can explain what “a self-contradictory argument” is by saying that it is an argument such that the steps of the argument force several meanings on one of the propositions of the argument and that not all of these meanings are compatible. Yet another way to put this is to say that an argument is self-contradictory if and only if the steps of the argument force an ambiguous meaning on one of the propositions of the argument. Note that, as is clear from the example above, the meaning forced on a proposition by an argument is not an interpretation of the proposition but a constraint on how it may be interpreted.

Now we change to how to formally express “a self-contradictory argument.” Let us by the meaning of a proposition mean an interpretation of the proposition. For instance, the wind is blowing is the meaning of the proposition B in the example above. Let A be a formula occurrence in a deduction in some formal system. To denote that A has a certain meaning, m say, we decorate A with m. More precisely, we shall write m : A to denote that A has the meaning m. We use these decorations to define meaning conditions. Meaning conditions are formal representations of the constraints given by the meaning forced on a proposition by an argument. For every formal system considered in this article we shall do the following. We shall define what the set of formal meanings is for decorating the formulas in deductions in the formal system and we shall give the meaning conditions associated with the formal system. Thus, through the meaning conditions we formally define what is informally described by “the way in which a proposition is used in an argument.” By an assignment of meanings to the formulas in a deduction we mean a decoration of all of the formulas in the deduction. That a meaning is assigned to a formula means that the formula has been decorated with the meaning. The meaning conditions are given as constraints on the decorations, by formal meanings, of the formulas in the deductions. As an example let us consider, in the formal system $\mathbf {N}$, a deduction consisting of an $\mathbin {\supset }\mathrm {E}$ inference, $\alpha$ say. Let X, Y and Z be the major premise, the minor premise and the conclusion, respectively, of $\alpha$. Let $m_x$, $m_y$ and $m_z$ denote some meanings assigned to X, Y and Z, respectively. We decorate the formulas in the deduction as follows.

Reasoning in the same way as in the previous example, we know that since X is the major premise of an $\mathbin {\supset }\mathrm {E}$ inference, X must be $X_1 \mathbin {\supset }X_2$ for some propositions $X_1$ and $X_2$. We express this constraint by requiring the meaning $m_x$ to be $m \Rightarrow n$ for some meanings m and n, where thus $\Rightarrow$ means “implies that.” Moreover we require $m_y$ to be m and $m_z$ to be n. Thus, $m_x$ may not be it’s snowing and the wind is blowing. However $m_y$ may be it’s snowing and the wind is blowing and $m_z$ may be the wind is blowing. In this case $m_x$ must be it’s snowing and the wind is blowing implies that the wind is blowing. We express meaning conditions given for any $\mathbin {\supset }\mathrm {E}$ inference in any deduction in the formal system $\mathbf {N}$ by the schema

Hence the meaning condition for the major premise A of an $\mathbin {\supset }\mathrm {E}$ inference is that A must have the meaning $m \Rightarrow n$ for some meanings m and n. Moreover, the meanings of the major premise, the minor premise and the conclusion respectively must have the relation to each other expressed by the schema. The notion of a self-contradictory deduction in a formal system is defined as follows.

Definition 1

Assume that $\mathbf {F}$ is a formal system. Assume that the set of formal meanings for decorating the formulas in the deductions in $\mathbf {F}$ are defined, and assume that the meaning conditions associated with the formal system are given in some way. Then a deduction $\mathscr {D}$ in $\mathbf {F}$ is self-contradictory if there is no assignment of formal meanings to the formulas in $\mathscr {D}$ such that this assignment satisfies the meaning conditions.

The meaning conditions, as we shall give them, are related to the inversion principle of Prawitz. In Prawitz (1965) [6] we can read the following.

Observe that an elimination rule is, in a sense, the inverse of the corresponding introduction rule: by an application of an elimination rule one essentially only restores what had already been established if the major premise of the application was inferred by an application of an introduction rule.

We may say that, for a given deduction, the constraint expressed by the meaning conditions is an attempt to make the inversion principle global, in the deduction. But this attempt is successful if and only if the deduction is not self-contradictory, since otherwise there is no assignment of formal meanings to the formulas in the deduction such that this assignment satisfies the meaning conditions.

The Curry-Howard interpretation may resemble what designates meanings in the meaning conditions. However, the similarity is only superficial. In general, it is not the case that the assignment of Curry-Howard interpretations to the formula occurrences in a deduction satisfies the meaning conditions. Since the Curry-Howard interpretation is just a representation of an argument, there are always Curry-Howard interpretations of the formula occurrences in a deduction, but there need not be an assignment of formal meanings to the formulas in the deduction such that this assignment satisfies the meaning conditions.

3 The Liar Paradox

In this section we shall study the liar paradox as an example of a self-contradictory argument. The liar paradox is the following.

Let P be the sentence “This sentence is false.” That is, P is the sentence “P is false.” Assume P. Hence, by the definition of P, P is false. This contradicts the assumption P, and hence P is false. Since P is false, P follows from the definition of P. This is a contradiction.

This argument is very similar to Russell’s paradox. Below we present the formal system $\mathbf {FP}$, specially designed for a formal presentation of the liar paradox. The language of $\mathbf {FP}$ is the set of formulas, where $\mathord {\perp }$ and P are formulas, and if A and B are formulas, then $A \mathbin {\supset }B$ is a formula; $\lnot A$ is defined to be $A \mathbin {\supset }\mathord {\perp }$. The inference schemata of $\mathbf {FP}$ are the following.

The liar paradox is formally represented by the following deduction $\mathscr {G}$,

The set of formal meanings to be assigned to formulas in deductions in the formal system $\mathbf {FP}$ is inductively defined as follows. The meaning variable x is a meaning, and if m and n are meanings, then pm and $m \Rightarrow n$ are meanings. We may interpret the meanings as follows: $m \Rightarrow n$ means “m implies that n,” and pm means “This sentence is false,” where “This” refers to the sentence expressed by m. The meaning conditions associated with the formal system $\mathbf {FP}$ are the following.

Now assume that there is an assignment of formal meanings to the formulas in the deduction $\mathscr {F}$ above such that this assignment satisfies the meaning conditions.

Assume that m is the meaning of the minor premise P of the $\mathbin {\supset }\mathrm {E}$ inference and that n is the meaning of the conclusion $\mathord {\perp }$ of the $\mathbin {\supset }\mathrm {E}$ inference. Then, by the conditions above we conclude that the meaning of the premise P of the $\mathrm {PE}$ inference must be $p(m \Rightarrow n)$.

The condition given for the $\mathbin {\supset }\mathrm {I}$ inference schema requires both of the formulas cancelled at the $\mathbin {\supset }\mathrm {I}$ inference in $\mathscr {F}$ to have the same meaning. However, no matter how we choose m and n the meanings m and $p(m \Rightarrow n)$ are not the same. Hence, there is no assignment of formal meanings to the formulas in $\mathscr {F}$ such that this assignment satisfies the meaning conditions. Hence, $\mathscr {F}$ is self-contradictory.

4 Self-contradictory Reasoning in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$

Let $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ be the fragment of $\mathbf {N}$ obtained by removing the symbols $\mathord {\forall }$, $\mathord {\exists }$ and $=$ and the inference schemata corresponding to these symbols from $\mathbf {N}$. In this section we shall study the notion of self-contradictory deductions in the formal system $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$. We shall also prove the following theorem.

Theorem 1

Every non-self-contradictory deduction in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ is normalizable.

In this section and the two succeeding ones we shall use the terminology of Ekman (1994) [2, Sect. 3.1], see Appendix below. Hence, by “normalizable” in Theorem 1 we mean normalizable as defined in Ekman (1994) [2, Sect. 3.1], see Appendix below. As in the formal system $\mathbf {FP}$, m and n denote meanings.

Assume that A is a formula such that there is no normal proof of A in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$. Then, by Proposition 3.1.4 in Ekman (1994) [2] there is no normalizable proof of A in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$. Hence by Theorem 1 every proof of A is self-contradictory. Since there is no normal proof of $\mathord {\perp }$ in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ it follows that every paradox in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ is self-contradictory, if by paradox we mean a proof of $\mathord {\perp }$. In Ekman (1994) [2, Sect. 2.1] it is shown that there is no normal proof of the formula $t \notin u$, where t is the term defined by

Hence, every proof of $t \notin u$ in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ is self-contradictory. In Ekman (1994) [2, Sect. 2.1] also a proof, named Crabbe’s counterexample (see Crabbé (1974) [1]), of the formula $t \notin u$ is presented. This proof is a proof in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ and hence Crabbe’s counterexample is a self-contradictory proof. It is also argued in Ekman (1994) [2, Sect. 2.1] that Crabbe’s counterexample expresses a correct argument in $\mathbf {ZF}$. Hence the formula $t \notin u$, or the proposition that informally corresponds to $t \notin u$, serves as an example of a proposition provable in $\mathbf {ZF}$, but only by self-contradictory proofs, unless we use proof principles not expressible in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$.

The variables of the language of $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ will also be used to denote meaning variables. The set of formal meanings to be assigned to formulas in deductions in the formal system $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ is inductively defined as follows. The meaning variable x and $false$ are meanings, and if m and n are meanings, then $\epsilon m$, $m \Rightarrow n$, $m \mathbin {\wedge }n$ and $m + n$ are meanings. The meaning conditions associated with the formal system $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ are the following.

Let $\mathscr {D}$ and $\mathscr {E}$ be two deductions in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ such that $\mathscr {D}$ is non-self-contradictory, $\theta$ is an assignment of formal meanings to the formula occurrences in $\mathscr {D}$ such that this assignment satisfies the meaning conditions and $\mathscr {D} \Longrightarrow \mathscr {E}$ (i.e., $\mathscr {D}$ reduces to $\mathscr {E}$; see Appendix for the definition of reductions of deductions). Then we let $a(\theta ,\mathscr {E},\mathscr {D})$ denote the assignment of formal meanings to the formula occurrences in $\mathscr {E}$ given by considering every formula occurrence in $\mathscr {E}$ to correspond to a formula occurrence in $\mathscr {D}$ and assigning the same meaning to the formula occurrence in $\mathscr {E}$ as the meaning assigned to the corresponding formula occurrence in $\mathscr {D}$. If $\mathscr {D}$ reduces to $\mathscr {E}$ via an epsilon reduction, then the deduction $\mathscr {D}$, with its formula occurrences decorated by $\theta$ has the form

In this case $\mathscr {E}$, with its formula occurrences decorated by $a(\theta ,\mathscr {E},\mathscr {D})$, is the following deduction

If $\mathscr {D}$ reduces to $\mathscr {E}$ via an imply reduction, then $\mathscr {D}$, with its formula occurrences decorated by $\theta$, has the form

In this case $\mathscr {E}$, with its formula occurrences decorated by $a(\theta ,\mathscr {E},\mathscr {D})$, is the deduction

For all other cases of the kind of reduction that takes $\mathscr {D}$ to $\mathscr {E}$, $a(\theta ,\mathscr {E},\mathscr {D})$ is defined similarly.

Lemma 1

If a deduction $\mathscr {D}$ is non-self-contradictory and $\mathscr {D}$ reduces to $\mathscr {E}$, then also the deduction $\mathscr {E}$ is non-self-contradictory.

Proof

Let $\theta$ be an assignment of formal meanings to the formula occurrences in $\mathscr {D}$ such that this assignment satisfies the meaning conditions. Then $a(\theta ,\mathscr {E},\mathscr {D})$ is an assignment of formal meanings to the formula occurrences in $\mathscr {E}$ such that this assignment satisfies the meaning conditions.$\square$

Let the formal system $\mathbf {P}$ of propositional logic be given as in the Appendix below. We assume that there is at least one propositional variable P in the language of $\mathbf {P}$. Let $^*$ be the function from the set of meanings to be assigned to formulas in deductions in the formal system $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ onto the set of formulas of $\mathbf {P}$, defined as follows.

We extend $^*$ to a function from the set of sets of meanings to be assigned to formulas in deductions in the formal system $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ onto the set of sets of formulas of $\mathbf {P}$ by letting $\varGamma ^*$ denote the set of formulas $A^*$ such that A belongs to $\varGamma$, for all sets of meanings to be assigned to formulas in deductions in the formal system $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$.

We extend $^*$ once more, to a function from the set of non-self-contradictory deductions in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ to the set of deductions in $\mathbf {P}$. If $\mathscr {D}$ is a deduction in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ consisting of the open assumption m : A, then $\mathscr {D}^*$ is the open assumption $m^*$:

Observe that there is no open assumption of the form $\mathord {\perp }\mathbin {\supset }\mathord {\perp }$ in $\mathscr {D}^*$, cancelled at the $\mathbin {\supset }\mathrm {I}$ inference, in the deduction to the right above.

For all other cases of the end inference of a deduction $\mathscr {D}$, the definition of $\mathscr {D}^*$ commutes with the definition of deduction. For instance, for the case that an $\mathbin {\supset }\mathrm {I}$ is the last inference of a deduction, we have the following clause defining the image under $^*$ of this deduction:

Proposition 1

Assume that $\mathscr {D}$ is a non-self-contradictory deduction, $\theta$ is an assignment of formal meanings to the formula occurrences in $\mathscr {D}$ such that this assignment satisfies the meaning conditions and $\mathscr {D} \Longrightarrow \mathscr {E}$. Let $\mathscr {D}$ also denote the deduction obtained from $\mathscr {D}$ by decorating the formula occurrences in $\mathscr {D}$ with $\theta$. Let $\mathscr {E}$ also denote the deduction obtained from $\mathscr {E}$ by decorating the formula occurrences in $\mathscr {E}$ with $a(\theta ,\mathscr {E},\mathscr {D})$. Then $\mathscr {D}^* \Longrightarrow \mathscr {E}^*$.

Since $\mathbf {P}$ is strongly normalizable (see Prawitz (1965) [6]), we have Theorem 1 as a consequence of Proposition 1.

5 Self-contradictory Reasoning in $\mathbf {N}_{-\mathord {\exists }=}$

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 $\mathbf {N}_{-\mathord {\exists }=}$, which is the fragment of $\mathbf {N}$ obtained by removing the symbols $\mathord {\exists }$ and $=$ and the inference schemata corresponding to these symbols from $\mathbf {N}$. We shall also prove the following theorem.

Theorem 2

Every non-self-contradictory deduction in $\mathbf {N}_{-\mathord {\exists }=}$ is normalizable.

Let A be any formula. To define the meaning conditions associated with the formal system $\mathbf {N}_{-\mathord {\exists }=}$ we shall informally consider $\mathord {\forall }x A$ to represent the informally given infinitely long formula $A[t_1/x] \mathbin { \& }(A[t_2/x] \mathbin { \& }(A[t_3/x] \mathbin { \& }\ldots ))$, where $t_1,t_2,t_3,\ldots$ are all terms of the formal system $\mathbf {N}_{-\mathord {\exists }=}$.

A naïve way to give the meaning conditions associated with $\mathbf {N}_{-\mathord {\exists }=}$ is to add the following meaning conditions to the meaning conditions associated with $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$, where $\lambda$ 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 $\lambda m$ is a meaning for any meaning m.

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 $\mathord {\forall }\mathrm {I}$ inferences and for $\mathord {\forall }\mathrm {E}$ inferences. This condition is however too strong, if we consider $\mathord {\forall }x A$ to represent the informally given infinitely long formula above, since the meaning conditions given for $\mathbin { \& }\mathrm {E}$ inferences does not require that there is a one to one correspondence between the meaning of the premise and the conclusion of an $\mathbin { \& }\mathrm {E}$ inference. As an example, consider the following deduction.

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 $\mathord {\forall }x (r \in x)$ and let us consider C to represent the informally given formula $(r \in t_1) \mathbin { \& }((r \in t_2) \mathbin { \& }((r \in t_3) \mathbin { \& }\ldots ))$, where $t_1,t_2,t_3,\ldots$ are all terms of the formal system $\mathbf {N}_{-\mathord {\exists }=}$. Then $r \in \{y \mid A\} \mathbin { \& }(r \in \{y \mid \lnot A\} \mathbin { \& }C)$ and C informally represent the same formula. We have the following proof of $\lnot C$, which from an informal point of view is another presentation of the deduction above.

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 $\mathbf {N}_{-\mathord {\exists }=}$. The set of formal meanings to be assigned to formulas in deductions in the formal system $\mathbf {N}_{-\mathord {\exists }=}$ is inductively defined as follows. The meaning variable x and $false$ are meanings, and if m and n are meanings, then $\epsilon m$, $m \Rightarrow n$, $m \mathbin {\wedge }n$, $m + n$ and $\lambda x.m$ are meanings. The meaning conditions are the following and in addition the meaning conditions associated with the formal system $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$.

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

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

Assume that x does not occur free in A. Then the constraint defined by the meaning conditions can be strengthened so that $m_2$ and $m_1$ 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 $m_2$ and one “submeaning” of $m_1$ “correspond” to the same subformula of A, and x does not occur free in this subformula, then these “submeanings” of $m_1$ and $m_2$, 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 $\mathord {\perp }\mathrm {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 $\mathord {\perp }\mathrm {E}$ inference schema says that nothing more is known about how the premise of an $\mathord {\perp }\mathrm {E}$ inference is derived other than that it is the premise of an $\mathord {\perp }\mathrm {E}$ inference. Instead of having $\mathord {\perp }$ primitively given in $\mathbf {N}$ we can define it by $\mathord {\forall }x (r \in x)$, where r is an arbitrary term. We then have the $\mathord {\perp }\mathrm {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.

Then if we also take $false$ to be defined by $\lambda x.\epsilon x$ we have the $\mathord {\perp }\mathrm {E}$ meaning condition schema as a derived meaning condition schema, derived from the meaning condition schemata $\mathord {\forall }\mathrm {E}$ and $\mathord {\in } \mathrm {E}$.

Lemma 2

If a deduction $\mathscr {D}$ is non-self-contradictory and $\mathscr {D}$ reduces to $\mathscr {E}$ then also the deduction $\mathscr {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 $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ to the set of deductions in $\mathbf {P}$. To prove Theorem 2 we shall instead defined a function $^*$ from the set of non-self-contradictory deductions in $\mathbf {N}_{-\mathord {\exists }=}$ to the set of deductions in $\mathbf {P^2}$, where $\mathbf {P^2}$ denotes the formal system of second order propositional logic. The language of $\mathbf {P^2}$ is the set of formulas, inductively defined as follows. The propositional variables $X,X_1,X_2,\ldots$ and $\mathord {\perp }$ are formulas, and if A and B are formulas, then $A \mathbin {\supset }B$, $A \mathbin { \& }B$, $A \mathbin {\vee }B$ and $\mathord {\forall }X A$ are formulas. The $\mathord {\perp }, \mathbin {\supset }, \mathbin { \& }$ and $\mathbin {\vee }$ inference schemata are the same for $\mathbf {P^2}$ as for the formal system $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$. The $\mathord {\forall }$ inference schemata for $\mathbf {P^2}$ are the following.

We have the restriction on deductions in $\mathbf {P^2}$ that the variable designated X in the $\mathord {\forall }\mathrm {I}$ schema may not occur free in any open assumption in the deduction designated $\mathscr {D}$. The reduction rules for deductions in $\mathbf {P^2}$ are the same as the reduction rules for deductions in $\mathbf {N}_{-\mathord {\exists }=}$ except that the substitution of a term for a variable in the $\mathord {\forall }$-reduction in $\mathbf {N}_{-\mathord {\exists }=}$ corresponds, in $\mathbf {P^2}$, to a substitution of a proposition for a propositional variable. We presuppose that the set of variables of $\mathbf {N}_{-\mathord {\exists }=}$ and the set of propositional variables of $\mathbf {P^2}$ have the same cardinality. Hence there is a one to one correspondence, $^{*}$ say, between the set of variables of $\mathbf {N}_{-\mathord {\exists }=}$ and the set of propositional variables of $\mathbf {P^2}$. For any variable x of $\mathbf {N}_{-\mathord {\exists }=}$ we let the propositional variable X of $\mathbf {P^2}$ denote $x^{*}$. The function $^*$ from the set of meanings to be assigned to formulas in deductions in the formal system $\mathbf {N}_{-\mathord {\exists }=}$ onto the set of formulas of $\mathbf {P^2}$ is defined as follows.

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 $\mathbf {N}_{-\mathord {\exists }=}$ onto the set of sets of formulas of $\mathbf {P^2}$ by letting $\varGamma ^*$ denote the set of formulas $A^*$ such that A belongs to $\varGamma$, for all sets $\varGamma$ of meanings to be assigned to formulas in deductions in the formal system $\mathbf {N}_{-\mathord {\exists }=}$. In a similar way as in Sect. 4 we extend $^*$ once more, to a function from the set of non-self-contradictory deductions in $\mathbf {N}_{-\mathord {\exists }=}$ to the set of deductions in $\mathbf {P^2}$. To define this function we add the following clauses to the definition of the function $^*$ in Sect. 4.

The definition of $a(\theta ,\mathscr {E},\mathscr {D})$, given in Sect. 4, extends from deductions in $\mathbf {N}_{-\mathord {\forall }\mathord {\exists }=}$ to deductions in $\mathbf {N}_{-\mathord {\exists }=}$ by defining $a(\theta ,\mathscr {E},\mathscr {D})$ also in the case $\mathscr {D}$ reduces to $\mathscr {E}$ via an $\mathord {\forall }$ reduction. This is done in a similar way as for the other cases of the kind of reduction that takes $\mathscr {D}$ to $\mathscr {E}$.

Proposition 2

Assume that $\mathscr {D}$ is a non-self-contradictory deduction, $\theta$ is an assignment of formal meanings to the formula occurrences in $\mathscr {D}$ such that this assignment satisfies the meaning conditions and $\mathscr {D} \Longrightarrow \mathscr {E}$. Let $\mathscr {D}$ also denote the deduction obtained from $\mathscr {D}$ by decorating the formula occurrences in $\mathscr {D}$ with $\theta$. Let $\mathscr {E}$ also denote the deduction obtained from $\mathscr {E}$ by decorating the formula occurrences in $\mathscr {E}$ with $a(\theta ,\mathscr {E},\mathscr {D})$. Then $\mathscr {D}^* \Longrightarrow \mathscr {E}^*$.

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

6 Self-contradictory Reasoning in $\mathbf {N}_{-=}$

The meaning conditions associated with $\mathbf {N}_{-=}$ are defined by adding to the meaning conditions associated with $\mathbf {N}_{-\mathord {\exists }=}$ some constraints given by informally considering $\mathord {\exists }x A$ to represent the informally given infinitely long formula $A[t_1/x] \mathbin {\vee }(A[t_2/x] \mathbin {\vee }(A[t_3/x] \mathbin {\vee }\ldots ))$, where $t_1,t_2,t_3,\ldots$ are all terms of the formal system $\mathbf {N}_{-=}$. The set of formal meanings to be assigned to formulas in deductions in the formal system $\mathbf {N}_{-=}$ is inductively defined as follows. The meaning variable x and $false$ are meanings, and if m and n are meanings, then $\epsilon m$, $m \Rightarrow n$, $m \mathbin {\wedge }n$, $\lambda x.m$ and $\mu x.m$ are meanings. The meaning conditions associated with the formal system $\mathbf {N}_{-=}$ are the following, and in addition the meaning conditions associated with the formal system $\mathbf {N}_{-\mathord {\exists }=}$.

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

Theorem 3

Every non-self-contradictory deduction in $\mathbf {N}_{-=}$ is normalizable.

Let $\mathbf {PR}$ be the formal system with the same language as $\mathbf {N}_{-=}$, obtained by removing the $\in$-inferences from $\mathbf {N}$. We have the following result concerning $\mathbf {PR}$.

Proposition 3

Every deduction in $\mathbf {PR}$ is non-self-contradictory.

Proof

Let $\mathscr {D}$ be any given deduction in $\mathbf {PR}$. We shall define an assignment of formal meanings to the formulas in $\mathscr {D}$ such that this assignment satisfies the meaning conditions. This assignment is defined by decorating every formula occurrence A in $\mathscr {D}$ with the formal meaning $A^\circ$, where $^\circ$ is a function from the set of formulas of $\mathbf {PR}$ to the set of formal meanings to be assigned to formulas in deductions in the formal system $\mathbf {N}_{-=}$. The bijection $^\circ$ is defined as follows.

Appendix

1.1 Naïve Set Theory

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

• 1. Variables,   x, y, z

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

• 3. Formulas,   $A,B,C,\ldots$

The language of $\mathbf {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 \mid A\}$ is a term. If r and s are terms, then $r = s$ and $r \in s$ are formulas, and if A and B are formulas, then $A \mathbin {\supset }B$, $A \mathbin { \& }B$, $\mathord {\forall }x A$, $A \mathbin {\vee }B$ and $\mathord {\exists }x A$ are formulas; $\mathord {\perp }$ 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 $\mathbf {N}$, we shall use the following defined symbols

We use $\mathscr {D},\mathscr {E},\mathscr {F},\ldots$ to denote deductions. The deductions in $\mathbf {N}$ are defined by the following inference schemata.

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 $\mathord {\forall }\mathrm {I}$ and $\mathord {\exists }\mathrm {E}$ schemata and the variables x and y in the $\mathord {=}\mathrm {I}$ schema designate eigenvariables of inferences. We require that the eigenvariables occurring in a deduction $\mathscr {D}$ are syntactically distinguished from each other and from variables with free non-eigenvariable occurrences in $\mathscr {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].

1.2 Normal Deductions in a Fragment of $\mathbf {N}$

Let $\mathbf {F}$ be a formal system. We consider a fragment of $\mathbf {F}$ to be a formal system obtained from $\mathbf {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 $\mathord {\exists }$, $\mathbin {\vee }$ and $=$ and the inference schemata corresponding to these symbols from $\mathbf {N}$. We let $\mathbf {N}_{-\mathord {\exists }\mathbin {\vee }=}$ 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 $\mathscr {D}$ is the subdeduction of $\mathscr {D}$ in which the eigenvariable is defined. The scope of an eigenvariable of an $\mathord {\forall }\mathrm {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 $\mathbf {N}_{-\mathord {\exists }\mathbin {\vee }=}$ 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 $\mathscr {D}$ is a sequence $A_1,A_2,\ldots ,A_n$ of formula occurrences in $\mathscr {D}$ such that: (1) $A_1$ is an assumption. (2) For each i such that $1 \le i < n$, $A_i$ stands immediately above $A_{i+1}$ and $A_i$ is not the minor premise of an elimination inference. (3) $A_n$ 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,\ldots ,A_n$, with $A_n$ as the end formula of the deduction. An E-main branch is a main branch consisting only of an $\mathrm {E}$-part. Note that there cannot be more than one $\mathrm {E}$-main branch in a deduction.

If a formula occurrence in a deduction in $\mathbf {N}_{-\mathord {\exists }\mathbin {\vee }=}$ is a minor premise of an elimination inference then this formula occurrence is the minor premise of an $\mathbin {\supset }\mathrm {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 $\mathbin {\supset }\mathrm {E}$ inference.

Proposition 4

Every branch in a normal deduction in $\mathbf {N}_{-\mathord {\exists }\mathbin {\vee }=}$ consists of an E-part followed by a (possibly empty) I-part.

Proposition 5

A normal proof in $\mathbf {N}_{-\mathord {\exists }\mathbin {\vee }=}$ has an introduction inference as its last inference.

1.3 Reductions of Deductions in $\mathbf {N}_{-=}$

We use $\mathscr {D} \Longrightarrow \mathscr {E}$ to denote that $\mathscr {D}$ reduces to the deduction $\mathscr {E}$. If there is a deduction $\mathscr {E}$ such that $\mathscr {D} \Longrightarrow \mathscr {E}$ then $\mathscr {D}$ is reducible. $\mathscr {D}$ reduces in zero steps to itself. If there are deductions $\mathscr {E}_1,\ldots ,\mathscr {E}_n$, where $n \ge 1$, such that

$$\begin{aligned} \mathscr {D} \Longrightarrow \mathscr {E}_1 \Longrightarrow \ldots \Longrightarrow \mathscr {E}_n \end{aligned}$$

then $\mathscr {D}$ reduces in n steps to the deduction $\mathscr {E}_n$. Hence, the two phrases $\mathscr {D}$ reduces in one step to $\mathscr {E}$ and $\mathscr {D}$ reduces to $\mathscr {E}$ have the same meaning. If there is an $n \ge 0$ and a deduction $\mathscr {E}$ such that $\mathscr {D}$ reduces in n steps to $\mathscr {E}$, and $\mathscr {E}$ is not reducible, then $\mathscr {D}$ is normalizable. If there is no infinite family $\{\mathscr {E}_i\}$, $i = 1,2,3,\ldots$ of deductions such that $\mathscr {D} \Longrightarrow \mathscr {E}_1$ and $\mathscr {E}_i \Longrightarrow \mathscr {E}_{i+1}$, for $i \ge 1$, then $\mathscr {D}$ is strongly normalizable.

The relation $\Longrightarrow$ 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.

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

1.4 Propositional Logic

Propositional logic is the formal system $\mathbf {P}$ obtained by removing the symbols $\in , \mathord {\forall }, \mathord {\exists }$ and $=$ and the inference schemata corresponding to these symbols from $\mathbf {N}$. The formal system $\mathbf {P}$ does not have any term variables but instead propositional variables. The language of $\mathbf {P}$ is the set of formulas, inductively defined as follows. The propositional variables P, Q, R and $\mathord {\perp }$ are formulas, and if A and B are formulas, then $A \mathbin {\supset }B$, $A \mathbin { \& }B$ and $A \mathbin {\vee }B$ are formulas.

A branch in a deduction in $\mathbf {P}$ is defined as a branch in a deduction in $\mathbf {N}_{-\mathord {\exists }\mathbin {\vee }=}$. The notion of a cut in a deduction in $\mathbf {P}$ and the notion of a normal deduction in $\mathbf {P}$ is defined as in $\mathbf {N}_{-=}$. The definitions of an $\mathrm {E}$-part of a branch, an $\mathrm {I}$-part of a branch, a main branch and an $\mathrm {E}$-main branch are the same for a branch in a deduction in $\mathbf {N}$ as for a branch in a deduction in $\mathbf {N}_{-\mathord {\exists }\mathbin {\vee }=}$.