◄ Index 
◄
Main essay
PA is instantiationally and arithmetically complete,
but algorithmically incomplete
An interpretation of Gödelian incompleteness under
Church’s Thesis that leads to a link between formal logic and computability
Bhupinder Singh Anand[1]
(A
.pdf file of this essay before the current update is available at http://arXiv.org/abs/math/0507044)
We
define instantiational and algorithmic completeness for a formal language, and
arithmetical completeness for Peano Arithmetic. We show that, in the presence
of Church’s Thesis, an interpretation of Gödelian incompleteness is that Peano Arithmetic is instantiationally complete, but
algorithmically incomplete. We then postulate a Provability Thesis that links
Peano Arithmetic and effective algorithmic computability - just as Church's
Thesis links Recursive Arithmetic and effective instantiational computability -
under which PA is arithmetically complete.
1. Introduction: Interpreting universal quantification
An issue that, sooner or later, seems to obfuscate every philosophical discussion on the relationship between formal logic and computability, and one which seems to lie also at the root of most foundational ambiguities, is the equivocal, semantic, interpretation of universal quantification (i.e., of unqualified generalisation).
In other words, from a foundational perspective, standard interpretations of classical theory do not provide an unambiguous answer to the question:
Can we unequivocally interpret a universally quantified formula of a language L under an interpretation M?
2. Differentiating instantiational and algorithmic
Tarskian satisfiability
We begin by noting that Tarski's definitions of the satisfiability and truth of the formulas of a formal language, say L, under an interpretation, say M, can be qualified to differentiate between at least two, essentially different, methods of assigning, for instance, the valuation TRUE to a predicate of M, by appeal to definitions such as the following[2]:
(i) Effective instantiational satisfiability: A predicate, say R(x), of an interpretation M, of a language L, is effectively satisfiable instantiationally if, and only if, given any element s in the domain D of the interpretation M, there is always some effective[3] method, say T(s), of determining that R(s) is satisfied under the interpretation M;
(ii) Effective algorithmic satisfiability: A predicate, say R(x), of an interpretation M, of a language L, is effectively satisfiable algorithmically if, and only if, there is some effective method, say UT, such that, given any element s in the domain D of the interpretation M, UT effectively determines that R(s) is satisfied under the interpretation M.
Now, if R(x) is the interpretation in M of an L-formula, [R(x)][4], then (i) is satisfied if, for every s in D, [R(s)] is provable[5] in L, and L is assumed to be sound[6]. Similarly, (ii) is satisfied if [(Ax)R(x)] is provable in such an L.
Further, although every algorithmically satisfiable predicate of M is instantiationally satisfiable in M, Gödel has shown ([Go31a], p25(1)[7]) - by a constructive and intuitionistically unobjectionable meta-argument - that there are instances when [R(x)] is instantiationally provable in L[8] if L is a consistent Peano Arithmetic, so (i) holds; but [(Ax)R(x)] is not provable in L, so (ii) may not hold.
It follows that (i) and (ii) cannot be assumed equivalent without qualification.
3. Differentiating instantiational and algorithmic
Tarskian truth
This suggests that, if we treat (i) as corresponding to the classical definition of Tarskian truth in M, which we may denote symbolically by |=M [(Ax)R(x)], then we can treat (ii) as the definition of a qualified, algorithmic, Tarskian truth in M - which we may denote symbolically by ||=M [(Ax)R(x)].
So we can, without loss of generality, symbolically express the distinction between instantiational Tarskian truth, and algorithmic Tarskian truth, in an interpretation M, by defining:
(1) |=M [(Ax)R(x)] <=> (i);
and:
(2) ||=M [(Ax)R(x)] <=> (ii);
where:
(3) ||=M [(Ax)R(x)] => |=M [(Ax)R(x)];
but the following does not always hold:
(4) |=M [(Ax)R(x)] => ||=M [(Ax)R(x)].
4. Defining instantiational and algorithmic
provability
We can, then, define:
(iii) Instantiational provability: An instantiationally Tarskian-true predicate, R(…)[9], of an interpretation, say M, of a formal language, say L, is instantiationally provable in L if, and only if, R(…) is the interpretation of an L-formula, [R(…)], and every instantiation of R(…) in M is the interpretation of an L-provable formula.
(iv) Algorithmic provability: An algorithmically Tarskian-true predicate, R(…), of an interpretation, say M, of a formal language, say L, is algorithmically provable in L if, and only if, R(…) is the interpretation of an L-formula, [R(…)], and [(A…)R(…)] is provable in L.
5. Defining instantiational and algorithmic
completeness
We can also define, further:
Instantiational completeness: A language L is instantiationally complete with respect to an interpretation M if, and only if, every instantiationally Tarskian-true predicate, R(…), of M is instantiationally equivalent to a predicate, R'(…), of M, every instantiation of which is the interpretation in M of an L-provable formula.
Algorithmic completeness: A language L is algorithmically complete with respect to an interpretation M if, and only if, every algorithmically Tarskian-true predicate, R(…), of M is provable in L.
We now show the significance of the above definitions, by considering the particular case where L is a consistent first-order Peano Arithmetic, and M its standard interpretation.
6. Differentiating between instantiational and
algorithmic effective computability in Church’s Thesis
Now, a standard expression of Church’s Thesis is:
Church’s Thesis: A (partial) number-theoretic function is effectively computable if, and only if, it is (partial) recursive.
If we, again, differentiate between instantiational and algorithmic computability, we can either interpret the above as asserting the, weaker, equivalence:
or, the stronger identity (which implies the above equivalence):
7. Is first-order Peano Arithmetic instantiationally
complete with respect to its standard interpretation?
Now, by the Instantiational Church’s Thesis, every instantiationally Tarskian-true predicate, R(…), of M is instantiationally equivalent to a recursive relation, R'(…), of M that, treated as a Boolean function, always evaluates as TRUE.
By Gödel’s Theorems V and VII [Go31a][10], it follows that there is, thus, a PA-formula, [R''(…)], such that its standard interpretation in M, the arithmetical relation R''(…), is instantiationally equivalent, in M, to R'(…), and, hence, to R(…); and every instantiation of R''(…) in M is the standard interpretation of a PA-provable formula.
It follows that:
Meta-theorem 1: The Instantiational Church’s Thesis implies that first-order Peano Arithmetic is instantiationally complete with respect to its standard interpretation.
Thus, the
The Thesis, essentially, postulates that any arbitrary property that holds instantionally under the standard interpretation of Peano’s second-order Induction Axiom is instantiationally equivalent to a recursive relation in the interpretation.
It follows that:
Corollary 1.1: The
The question arises: How do we
interpret Gödelian incompleteness in
the presence of the
8. Is Peano Arithmetic algorithmically complete with
respect to its standard interpretation?
Now, Peano Arithmetic would, further, be algorithmically complete with respect to its standard interpretation, M, if, and only if, every algorithmically Tarskian-true predicate, R(…), of M were provable in PA.
In the Appendix we show, however, that this is not the case, since Gödel’s Tarskian-true primitive recursive predicate, ~xB(Sb(p 19|Z(p)))[11] - which is algorithmic by definition - is not the standard interpretation of any of its representations in Gödel’s formal system P (and the argument remains valid for any first-order Peano Arithmetic).
We thus have:
Meta-theorem 2: First-order Peano Arithmetic is not algorithmically complete with respect to its standard interpretation, M.
So, in the presence of the
9. Is Peano Arithmetic algorithmically complete with
respect to the Arithmetical part of M?
We define:
Arithmetic completeness: An Arithmetic, A, is arithmetically complete with respect to its standard interpretation, M, if, and only if, every algorithmically Tarskian-true arithmetical predicate, R(…), of M is provable in A.
The question arises: Is PA arithmetically complete?
Now, it seems reasonable, and intuitively unobjectionable, to assume that, if there is an algorithm such that every instantiation of an arithmetical predicate, R(…), is effectively decidable as Tarskian-true in M, then there must be a corresponding PA-proof sequence for the formula, [R(…)].
We may formally define this assertion as a:
Provability Thesis: Every algorithmically Tarskian-true arithmetical predicate, R(…), is provable in PA.
It follows that:
Meta-theorem 3: The Provability Thesis implies that first-order Peano Arithmetic is arithmetically complete with respect to its standard interpretation, M.
10. Is the Provability Thesis effectively
verifiable?
The question arises: Is the Provability Thesis effectively verifiable?
Now, if it were always effectively decidable in M whether or not an arbitrary number-theoretic relation is algorithmically Tarskian-true - i.e., it is effectively satisfied algorithmically in the sense of (ii) - then, assuming Church’s Thesis, it would follow that Turing’s Halting Problem would be decidable by a Turing machine.
Since this is not the case, it follows that the Provability Thesis, like Church’s Thesis, may not be effectively verifiable.
11. Soundness
Now, standard interpretations of classical logic define the following semantic meta-implication as an instance of the property of the ‘soundness’ of PA:
(5) |-PA [(Ax)R(x)] => |=M [(Ax)R(x)].
Further, standard interpretations of classical theory show that the converse meta-implication, |=M [(Ax)R(x)] => |-PA [(Ax)R(x)], does not necessarily hold - a consequence of Tarski's Theorem that arithmetical truth cannot be defined arithmetically ([Me64], Corollary 3.38, p151).
The Provability Thesis is, thus, an attempt to offer a possible answer to the question: Can, and if so, when, does the converse hold?
It is the postulation that, if R(x) is an arithmetical predicate, then, in the sense of (2):
(6) ||=M [(Ax)R(x)] => |-PA [(Ax)R(x)]
The detailed consequences of such a postulation are beyond the immediate intent, and scope, of the subject of this essay.
12. Some consequences of postulating a Provability
Thesis for PA
However, we note, briefly, that, if we postulate a Provability Thesis for Peano Arithmetic, then:
(a) we would interpret Gödel’s reasoning as showing that, whereas (ii) implies (i), the converse does not always hold;
(b) Peano Arithmetic would be ω-inconsistent[12] - and, so, Gödel’s Theorem VI [Go31a], and its consequences, would hold vacuously[13]:
According to the Provability Thesis, there is no algorithm for determining that, given any natural number n in the standard interpretation M of PA, R(n) holds in M, although R(n) is true in M for every natural number n, and [R(n)] is provable in PA for every numeral [n].
Since mere addition of [(Ax)R(x)] as an axiom to PA would not entail the introduction of an algorithm in M for determining that, given any natural number n, R(n) holds in M, it follows that PA+[(Ax)R(x)] would be inconsistent under the standard interpretation.
It follows that, if PA is consistent, then [(Ax)R(x)] would not be independent of the axioms of PA. Hence, since Gödel’s reasoning implies that [(Ax)R(x)] is not provable in a consistent PA, [~(Ax)R(x)] must be PA-provable[14].
Since [R(x)] is provable in PA whenever we substitute any numeral [n] for the variable [x], it would, then, follow that PA would be consistent, but not ω-consistent.
(c) the intuitionist objection to concluding that the provability of [(Ex)R'(x)] in PA always implies the existence of some s, in M, such that R'(s) holds in M, would be vindicated if PA is ω-inconsistent; and Rosser’s proof of undecidability would fail:
Since [(Ex)R'(x)] is simply an abbreviation of [~(Ax)~R'(x)], under the Provability Thesis, the PA provability of [~(Ax)~R'(x)] is the meta-assertion that there is no algorithm in M for determining that, given any natural number n, ~R'(n) holds in M.
However, if PA is ω-inconsistent, we may have that [~(Ax)~R'(x)] is PA-provable, and also that [~R(x)] is provable in PA whenever we substitute any numeral [n] for the variable [x].
Hence we may not conclude from the PA provability of [~(Ax)~R'(x)] that there is always some s, in M, such that R'(s) holds in M.
Now Rosser’s proof - that his proposition, say [(Ax)R*(x)], can be shown to be undecidable in PA without assuming ω-consistency - assumes that, from the premise [~(Ax)R*(x)] in PA, we may conclude the existence of some natural number s in M such that ~R*(s) holds in M. However, under the Provability Thesis, such an assumption may be invalid.
(d) the Turing Thesis would no longer hold, since, if [(Ax)G(x)] represents Gödel’s undecidable proposition, then the arithmetical predicate G(n), treated as a Boolean function, would be an instantiationally (assumed effectively) computable function that would not, however, be Turing-computable;
(e) consequently, strictly speaking[15], G(n) would be in the complexity class NP, but not in P;
(f) Hilbert's proposed ω-rule could, then, be
viewed as also an attempt at a complete, semantic, definition of provability
for Peano Arithmetic.
13. Significance of a Provability Thesis
Now, the Provability Thesis, is, essentially, the assertion that a PA formula is provable if, and only if, any one of its interpretations is Tarskian-decidable algorithmically, in the sense of (ii) above.
The significance of such a link between formal provability and computability emerges when it is seen in a broader perspective, where we note that:
(a) The Instantiational Church's Thesis (which is implied by the standard form of Church's Thesis, although the converse does not hold) builds an iff bridge between instantiational (assumed effective) computability and Recursive Arithmetic;
eg., A number-theoretic predicate R(x), is instantiationally (assumed effectively) decidable for every natural number value of x if, and only if, R(x) is instantiationally (assumed effectively) equivalent to a recursive predicate Q(x).
(b) Hilbert & Bernays Representation Theorem, and its converse, together, build an iff bridge between Recursive Arithmetic and Peano Arithmetic;
eg., A number-theoretic predicate Q(x) is recursive if, and only if, Q(x) is representable in PA when treated as a Boolean function.
(c) The Church-Turing Theorem builds an iff bridge between Recursive Arithmetic and Turing computability;
eg., A number-theoretic predicate Q(x) is recursive if, and only if, Q(x), treated as a Boolean function, is total and Turing-computable.
(d) Markov algorithms build an iff bridge between Turing computability and algorithmic computability.
eg., A number-theoretic predicate Q(x), treated as a Boolean function, is Turing-computable if, and only if, Q(x), treated as a Boolean function, is partially Markov-computable.
However:
(e) Soundness merely builds an only-if bridge between Peano Arithmetic and Turing (algorithmic) computability;
eg., [R(x)] is a PA-provable formula only if, under the standard interpretation of PA, the interpreted arithmetical predicate, R(n), treated as a Boolean function, is Turing-computable as TRUE for any given natural number n.
whilst:
(f) The Provability Thesis complements, and completes, the concept of Soundness in arithmetic by building an iff bridge between Peano Arithmetic and Turing (algorithmic) computability.
eg., [R(x)] is a PA-provable formula if, and only if, under the standard interpretation of PA, the interpreted arithmetical predicate, R(n), treated as a Boolean function, is Turing-computable as TRUE for any given natural number n.
14. Conclusion
We have shown that Church’s Thesis implies that a first-order Peano Arithmetic is instantiationally complete, in the sense that it completely formalises Dedekind’s Peano Postulates with respect to Tarskian-truth.
We have shown, further, that, in the presence of Church’s Thesis, the Gödelian incompleteness of a Peano Arithmetic is, essentially, the assertion that the Arithmetic is not algorithmically complete with respect to its standard interpretation, M.
We have, then, defined a Provability Thesis that complements, and completes, the concept of Soundness in arithmetic - by building an iff bridge between Peano Arithmetic and Turing (algorithmic) computability - under which PA is also arithmetically complete.
We have also briefly indicated how the consequences of such a Thesis - whose detailed consideration lies beyond the intent and scope of the present investigation - may be significant for standard interpretations of classical theory.
Appendix
Unless
specified otherwise, we generally follow the notation introduced by Mendelson
in his English translation of Gödel’s 1931 paper [Go31a];
however, for convenience of exposition, we refer to it as Gödel’s notation. Two
notable exceptions: we use the notation “(Ax)”, whose classical, standard, interpretation is “for
all x”, to denote Gödel’s
special symbol for Generalisation; the successor symbol is denoted by “S”,
instead of by “f”.
Following
Gödel (cf. [Go31a],
footnote 13), we use square brackets to indicate that the expression [(Ax)], including square brackets, only denotes the
uninterpreted string[16] named[17] within the brackets. Thus, [(Ax)] is not part of the formal system P, and would be
replaced by Gödel’s special symbolism for Generalisation wherever it occurs.
Following
Gödel’s definitions of well-formed formulas[18], we note that juxtaposing the string [(Ax)] and the formula[19] [F(x)] is the formula [(Ax)F(x)],
juxtaposing the symbol [~] and the formula [F] is the formula [~F],
and juxtaposing the symbol [v] between the formulas [F] and [G]
is the formula [FvG].
The
number-theoretic functions and relations in the following are defined
explicitly by Gödel [Go31a]. The formulas are defined
implicitly by his reasoning.
Preliminary
Definitions
We take
P to be Gödel’s formal system[20], and define ([Go31a], Theorem VI, p24-25):
(i) Q(x, y) as
Gödel’s recursive relation ~xB(Sb(y 19|Z(y)))[21].
(ii) [R(x, y)] as a
formula that represents Q(x, y) in the formal
system P.
(iii) q as the Gödel-number[22] of the formula [R(x, y)] of P.
(iv) p as the Gödel-number of the formula [(Ax)R(x, y)][23] of P.
(v) [p] as the numeral that represents the natural number p in P.
(vi) r as the Gödel-number of the formula [R(x, p)] of P.
(vii) 17Genr as the Gödel-number of the formula [(Ax)R(x, p)] of P.
(viii) Neg(17Genr)[24] as the Gödel-number of the formula [~(Ax)R(x, p)] of P.
(ix) R(x, y) as the standard interpretation of the formula [R(x, y)] of P.
Meta-theorem 2[25]: There is a recursive relation that is not the
standard representation of any of its representations in P.
Proof: We
consider Gödel’s primitive recursive relation ~xB(Sb(y 19|Z(y))).
(a) We assume
that every recursive number-theoretic function or relation is the standard
interpretation of at least one of its formal representations in P[26].
(b) There
is, thus, some P-formula [~xB(Sb(y 19|Z(y)))] whose
standard interpretation is the primitive recursive relation ~xB(Sb(y 19|Z(y)))[27].
(c) Now,
in every model M[28] (cf. [Me64], p192-3) of P, we can also interpret[29]:
(i) the
integer 0 as the interpretation of the symbol “0”;
(ii) the
successor operation as the interpretation of the successor function “'”;
(iii) addition
and multiplication as the interpretations of “+” and “.”;
(iv) the
interpretation of the predicate letter = as the identity relation.
(d) Since
the numerals of P interpret as a sub-domain of every model M of P, the natural
numbers are, then, a sub-domain of every M.
(e) Further,
by the hypothesis (a), all of Gödel’s 45 primitive recursive functions
and relations ([Go31a],
p17-22) are also, then, mirrored in every model M of P, and the P-formula, [~xB(Sb(p 19|Z(p)))], always interprets as the M-relation ~xB(Sb(p 19|Z(p))), where [p] is the
numeral that represents the natural number p in P, and p is the Gödel-number of [(Ax)~xB(Sb(y 19|Z(y)))].
(f) Hence,
in every model M of P, the relation ~xB(Sb(p 19|Z(p))) holds in M if, and only if, x is a M-number that is not the Gödel-number of a proof
of [(Ax)~xB(Sb(p 19|Z(p)))] in P.
(g) Further,
since the Gödel-number of a proof of [(Ax)~xB(Sb(p 19|Z(p)))] in P
is necessarily a natural number, ~xB(Sb(p 19|Z(p))) holds in every model M of P if x is an M-number that is not a natural number.
(h) Now,
Gödel has shown (cf. [Go31a], Theorem VI) that ~xB(Sb(p 19|Z(p))) holds over the domain of the natural numbers.
(i) It
follows that ~xB(Sb(p 19|Z(p))) is
satisfied by all x in every
model M of P.
(j) Hence,
the P-formula [(Ax)~xB(Sb(p 19|Z(p)))] is true (cf. [Me64], p51) in every model M of P, and, by
Gödel’s Completeness Theorem ([Me64], Corollary 2.14, p68), [(Ax)~xB(Sb(p 19|Z(p)))] is
P-provable.
However, since Gödel has shown that [(Ax)~xB(Sb(p 19|Z(p)))] is not P-provable (cf. [Go31a], Theorem VI), we conclude that assumption (a) does not hold. This proves the theorem.
References
[Go31a] Gödel,
Kurt. 1931. On formally undecidable propositions of Principia Mathematica
and related
[Me64] Mendelson,
Elliott. 1964. Introduction to Mathematical Logic. Van Norstrand,
(Created:
