◄ Index                                                                                                                                      ◄ Main essay

 

An arguable addition to the standard Deduction Theorems of first order theories

Bhupinder Singh Anand[1]

(A .pdf file of this essay before the current update is available at http://arXiv.org/abs/math.LO/0502502)

We consider an arguable addition to the standard Deduction Theorems of first order theories.

Contents[2]

 

1.  Introduction

 

2.  A standard Deduction Theorem

 

2.1 A number-theoretic corollary

2.2 An extended Deduction Theorem

 

3.  An additional Deduction Theorem

 

4.  Conclusion

 

Appendix 1: A model-theoretic proof of Corollary 2.1

 

Appendix 2: Gödel’s reasoning and Corollary 2.1

 

References

1.  Introduction

We first review, in Meta-theorem 1, the proof of a standard Deduction Theorem - ([T], [A])|-K [B] if, and only if, [T]|-K [A => B] (cf. [Me64], Corollary 2.6, p61) - of classical[3], first-order, theories, where an explicit deduction of [B][4] from ([T], [A]) is known.

We then show, in Corollary 1.2, that, assuming Church’s Thesis, Meta-theorem 1 can be constructively extended to cases where, ([T], [A])|-K [B] is established meta-mathematically, assuming the consistency of ([T], [A]), but where an explicit deduction of [B] from ([T], [A]) is not known.

We finally argue, in Meta-theorem 2, that:

([T], [A])|-K [B] holds if, and only if, [T]|-K [B] holds when we assume [T]|-K [A].

(In other words, that [B] is a deduction from ([T], [A]) in K if, and only if, whenever [A][5] is a hypothetical deduction from [T] in K, [B] is a deduction from [T] in K.)

2.  A standard Deduction Theorem

The following is, essentially, Mendelson’s proof of a standard Deduction Theorem ([Me64], p61, Proposition 2.4 and Corollary 2.6) of an arbitrary first order theory K:

Meta-theorem 1: If [T] is a set of well-formed formulas of an arbitrary first order theory K, and if [A] is a closed well-formed formula of K, and if ([T], [A])|-K [B], then [T]|-K [A => B][6].

Proof: Let <[B1], [B2], ..., [Bn]> be a deduction of [B] from ([T], [A]) in K.

Then, by definition, [Bn] is [B] and, for each i, either [Bi] is an axiom of K, or [Bi] is in [T], or [Bi] is [A], or [Bi] is a direct consequence by some rules of inference of K of some of the preceding well-formed formulas in the sequence.

We now show, by induction, that [T]|-K [A => Bi] for each i =< n. As inductive hypothesis, we assume that the proposition is true for all deductions of length less than n.

(i)      If [Bi] is an axiom, or belongs to [T], then [T]|-K [A => Bi], since [Bi => (A => Bi)] is an axiom of K.

(ii)     If [Bi] is [A], then [T]|-K [A => Bi], since [T]|-K [A => A].

(iii)    If there exist j, k less than i such that [Bk] is [Bj => Bi], then, by the inductive hypothesis, [T]|-K [A => Bj], and [T]|-K [A => (Bj => Bi)]. Hence, [T]|-K [A => Bi].

(iv)    Finally, suppose there is some j < i such that [Bi] is [(Ax)Bi], where x is a variable in K. By hypothesis, [T]|-K [A => Bj]. Since x is not a free variable of [A], we have that [(Ax)(A => Bj) => (A => (Ax)Bj] is PA-provable. Since [T]|-K [A => Bj], it follows by Generalisation that [T]|-K [(Ax)(A => Bj)], and so [T]|-K [A => (Ax)Bj], i.e. [T]|-K [A => Bi].

This completes the induction, and Meta-theorem 1 follows as the special case where i = n. ¶[7]

2.1  A number-theoretic corollary

Now, Gödel has defined ([Go31], p22, Definition 45(6)) a primitive recursive number-theoretic relation xB(K, [T])y that holds if, and only if, x is the Gödel-number of a deduction from T of the K-formula whose Gödel-number is y.

We thus have:

Corollary 1.1[8]: If the Gödel-number of the well-formed K-formula [B] is b, and that of the well-formed K-formula [A => B] is c, then Meta-theorem 1 holds if, and only if[9]:

(Ex)xB(K, [T], [A])b => (Ez)zB(K, [T])c

2.2  An extended Deduction Theorem

We next consider the meta-proposition:

Corollary 1.2: If we assume Church’s Thesis[10], then Meta-theorem 1 holds even if the premise ([T], [A])|-K [B] is established meta-mathematically, assuming the consistency of ([T], [A]), but a deduction <[B1], [B2], ..., [Bn]> of [B] from ([T], [A]) in K is not known explicitly.

Proof: Since Gödel’s number-theoretic relation xB(K, [T])y is primitive recursive, it follows that, if we assume Church’s Thesis - which implies that a number-theoretic relation is decidable if, and only if, it is recursive - we can effectively determine some finite natural number n for which the assertion nB(K, [T], [A])b holds, where the Gödel-number of the well-formed K-formula [B] is b.

Since n would then, by definition, be the Gödel-number of a deduction <[B1], [B2], ..., [Bn]> of [B] from ([T], [A]) in K, we may thus constructively conclude, from the meta-mathematically determined assertion ([T], [A])|-K [B], that some deduction <[B1], [B2], ..., [Bn]> of [B] from ([T], [A]) in K can, indeed, be effectively determined. Meta-theorem 1 follows. ¶

3.  An additional Deduction Theorem

We, finally, argue that:

Meta-theorem 2: If K is an arbitrary first order theory, and if [A] is a closed well-formed formula of K, then ([T], [A])|-K [B] holds if, and only if, [T]|-K [B] holds when we assume that [T]|-K [A] holds.

Proof: First, if there is a deduction <[B1], [B2], ..., [Bn]> of [B] from ([T], [A]) in K, and there is a deduction, <[A1], [A2], ..., [Am]>, of [A] from [T] in K, then <[A1], [A2], ..., [Am], [B1], [B2], ..., [Bn]> is a deduction of [B] from [T] in K. Hence, if ([T], [A])|-K [B] holds, then [T]|-K [B] holds when we assume [T]|-K [A].

Second, if there is a deduction <[B1], [B2], ..., [Bn]> of [B] from [T] in K, then we have, trivially, that, if [T]|-K [B] holds when we assume [T]|-K [A], then ([T], [A])|-K [B] holds.

Last, we assume that there is no deduction, <[B1], [B2], ..., [Bn]>, of [B] from [T] in K. If, now, [T]|-K' [B] holds when we assume that [T]|-K' [A] holds in any extension K' of K, then, if we assume that there is a sequence <[A1], [A2], ..., [Am]> of well-formed K'-formulas such that [Am] is [A] and, for each m >= i >= 1, either [Ai] is an axiom of K', or [Ai] is in [T], or [Ai] is a direct consequence by some rules of inference of K' of some of the preceding well-formed formulas in the sequence, then it follows from our hypothesis[11] that we can show, by induction on the deduction length n, that there is a sequence <[B1], [B2], ..., [Bn]> of well-formed K-formulas such that [B1] is [A][12], [Bn] is [B] and, for each i > 1, either [Bi] is an axiom of K, or [Bi] is in [T], or [Bi] is a direct consequence by some rules of inference of K of some of the preceding well-formed formulas in the sequence.

In other words, if there is a deduction, <[A1], [A2], ..., [Am]>, of [A] from [T] in K', then, by our hypothesis, <[A], [B2], ..., [Bn]> is a deduction of [B] from ([T], [A]) in K'. By definition, it follows that <[A], [B2], ..., [Bn]> is, then, a deduction of [B] from ([T], [A]) in K. We thus have that, if [T]|-K [B] holds when we assume [T]|-K [A], then ([T], [A])|-K [B] holds.  This completes the proof. ¶

In view of Corollary 1.2, we thus have:

Corollary 2.1: If we assume Church’s Thesis, and if [A] is a closed well-formed formula of K, then we may conclude that [T]|-K ([A] => [B]) holds if [T]|-K [B] holds when we assume [T]|-K [A].[13]

We note that, in the notation of Corollary 1.1, if the Gödel-number of the well-formed K-formula [A] is a, then Corollary 2.1 holds if, and only if[14]:

Corollary 2.2: ((Ex)xB(K, [T])a  => (Eu)uB(K, [T])b) => (Ez)zB(K, [T])c.

4.  Conclusion

We have argued that Meta-theorem 2 is a valid Deduction Theorem of any first order theory. However, standard interpretations of Gödel’s reasoning and conclusions are inconsistent with the consequences of this Meta-theorem in an arbitrary first order theory[15]. Hence, in the absence of constructive, and intuitionistically unobjectionable, reasons for denying the applicability of the Meta-theorem, and of its Corollary 2.1, to a first order theory, such interpretations ought not to be considered as definitive.

Appendix 1: A model-theoretic proof of Corollary 2.1

We note that there is a model-theoretic proof of Corollary 2.1. The case [T]|-K [B] is straightforward.

If [T]|-K [B] does not hold, then, as noted in Meta-theorem 2, if [T]|-K [B] holds when we assume [T]|-K [A], then there is a sequence <[B1], [B2], ..., [Bn]> of well-formed K-formulas such that [B1] is [A], [Bn] is [B] and, for each i > 1, either [Bi] is an axiom of K, or [Bi] is in [T], or [Bi] is a direct consequence by some rules of inference of K of some of the preceding well-formed formulas in the sequence.

(We note that if [T] is the set of well-formed K-formulas {[T1], [T2], ..., [Tl]} then ([T] & [A]) denotes the well-formed K-formula [T1 & T2 & ..., Tl & A], and, (T & A) denotes its interpretation in M, i.e., T1 & T2 & ..., Tl & A.)

If, now, any well-formed formula in ([T], [A]) is false under an interpretation M of K, then (T & A) => B is vacuously true in M.

If, however, all the well-formed formulas in ([T], [A]) are true under interpretation in M, then the sequence <[B1], [B2], ..., [Bn]> interprets as a deduction in M, since the interpretation preserves the axioms and rules of inference of K (cf. [Me64], p57). Thus [B] is true in M, and so is (T & A) => B.

In other words, we cannot have ([T], [A]) true, and [B] false, under interpretation in M, as this would imply that there is some extension K' of K in which [T]|-K' [A], but not [T]|-K' [B]; this would contradict our hypothesis, which implies that, in any extension K' of K in which we have [T]|-K' [A], we also have [T]|-K' [B].

Hence, (T & A) => B is true in all models of K. By a consequence of Gödel’s Completeness Theorem for an arbitrary first order theory ([Me64], p68, Corollary 2.15(a)), it follows that |-K ([T] & [A]) => [B]); and, ipso facto, that [T]|-K ([A] => [B]).

Appendix 2: Gödel’s reasoning and Corollary 2.1

In his seminal 1931 paper [Go31], Gödel meta-mathematically argues that, assuming any formal system of Peano Arithmetic, PA, is simply consistent, we can define an “undecidable” PA-proposition, [(Ax)R(x)], such that (cf. [Go31], #1, p25):

If [(Ax)R(x)] is PA-provable, then [~(Ax)R(x)] is PA-provable.[16]

Now, by Corollary 2.1, it should follow that:

 [(Ax)R(x) => ~(Ax)R(x)] is PA-provable,

and, therefore, that:

[~(Ax)R(x)] is PA-provable.

Since Gödel also proved that, if PA is assumed simply consistent, then [R(n)] is PA-provable for any, given, natural number n, Corollary 2.1 implies that PA is omega-inconsistent.

(We note that Gödel defined a first order theory K as omega-consistent if, and only if, for every well-formed formula [F(x)] of K, if |-K[F(n)] for every numeral [n], then it is not the case that |-K(Ex)F(x) (cf. [Me64], p142; see also [Go31], p23-24).

However, this conclusion is inconsistent with standard interpretations of Gödel’s reasoning, which, first, assert both [(Ax)R(x)] and [~(Ax)R(x)] as PA-unprovable, and, second, assume that PA can be omega-consistent[17]. Such interpretations, therefore, implicitly deny that the PA-provability of [~(Ax)R(x)] can be inferred from the above meta-argument; ipso facto, they imply that Corollary 2.1 is false.

References

[Ch37]    Church, A. 1937. Introduction to Mathematical Logic. Dover, New York.

[Go31]    Gödel, Kurt. 1931. On formally undecidable propositions of Principia Mathematica and related systems I. Translated by Elliott Mendelson. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York.

[Me64]   Mendelson, Elliott. 1964. Introduction to Mathematical Logic. Van Norstrand, Princeton. 

[Sh67]     Shoenfield, J. R. 1967. Mathematical Logic. Association for Symbolic Logic, Urbana.

(Updated: Monday 13th September 2004 3:31:36 AM IST by re@alixcomsi.com)

 

◄ Index           ▲ Top of page


[1] The author is an independent scholar. E-mail: re@alixcomsi.com; anandb@vsnl.com.

 

[2] Key words: Arithmetic, Church, classical, computable, constructive, deduction, effective, expressible, finite, formal, formula, function, Gödel, interpretation, meta-assertion, meta-theorem, natural number, number-theoretic, numeral, Peano, primitive, proof, recursive, relation, satisfiable, sequence, standard, truth, undecidable.

 

[3] We take Mendelson [Me64] as representative, in the area that it covers, of standard expositions of classical, first order, logic.

 

[4] We use square brackets to differentiate between a formal expression [F] and its interpretation “F”, where we follow Mendelson’s definition of an interpretation M of a formal theory K, and of the interpretation of a formula of K under M ([Me64], p49, §2). For instance, we use [n] to denote the numeral in K whose standard interpretation is the natural number n.

 

[5] For the purposes of this essay, we assume everywhere that [T] is an abbreviation for a finite set of K-formulas {[T1], [T2], ... [Tl]}, whereas [A], [B], ... are closed well-formed formulas of K. We note, also, that “[A] & [B]” and “[A & B]” denote the same K-formula.

 

[6] The converse is trivially true (cf. [Sh67], p33).

 

[7] We use the symbol “¶” as an end-of-proof marker.

 

[8] We note that Corollary 1.1 and Corollary 2.2 may be essentially different number-theoretic assertions, which, in the absence of a formal proof, cannot be assumed to be equivalent.

 

[9] We note that this symbolically expresses a meta-equivalence in a recursive arithmetic RA, based on a semantic interpretation of the definition of the primitive recursive relation xB(K, [T])y; it is not a K-formula.

 

[10] Church’s Thesis: A number-theoretic function is effectively computable if, and only if, it is recursive ([Me64], p147, footnote). We appeal explicitly to Church’s Thesis here to avoid implicitly assuming that every recursive relation is algorithmically decidable.

 

[11] That [T]|-K [A] holds.

 

[12] [A] is, thus, the hypothesis in the sequence; it is the only well-formed K-formula in the sequence that is not an axiom of K, not in [T], and not a direct consequence of the axioms of K by any rules of inference of K.

 

[13] We give a model-theoretic proof of Corollary 2.1 in the Appendix.

 

[14] We note that this, too, is not a K-formula, but a semantic meta-equivalence, based on the definition of the primitive recursive relation xB(K, [T])y.

 

[15] See Appendix 2.

 

[16] Gödel essentially argues, number-theoretically, that, if the Gödel-number of [(Ax)R(x)] is 17Genr, and if this formula is PA-provable, then the PA-formula whose Gödel-number is Neg(17Genr), i.e., [~(Ax)R(x)], is also PA-provable if PA is assumed simply consistent.

 

[17] We note that Gödel’s Incompleteness Theorems assume significance only if we presume that the arithmetic, in which they are derived, can be omega-consistent (cf. [Go31], p23-24)