[FOM] A NON-ARITHMETICAL CHARACTERIZATION OF G"ODEL'S FIRST INCOMPLETENESS THEOREM

[Steve Newberry]

                     A NON-ARITHMETICAL CHARACTERIZATION OF
                     G"ODEL'S FIRST INCOMPLETENESS THEOREM

                          by  R. Stephen Newberry

[Out of respect for the members of the FOM list, I have cut out the 
exposition of how G"odel encoded wffs of STT into Natural Numbers. I am 
using Henkin's General Models semantics, in which *all* models are 
significant, and assume as known the equivalence between STT and 
Second-order Predicate Logic [SOPL]. The ground domain is discrete, 
countable, and may be thought of as being either omega, or the set of all 
countable ordinals, or even as encompassing any arbitrary class of entities 
capable of being indexed by the elements of such ordinals.]

The title of this essay is a trifle misleading: G"odel's proofs made a 
statement about STT, but used only as much as was necessary to formalize 
PRA. His construction used a self-referential "diagonal" function, whereas 
I construct *nothing*, but merely point out *what is already there*. My 
results have nothing to say about PRA, but only about CLFO [Classical Logic 
of Finite Order -- AKA the Theory of Types]. No mention will be made of 
"arithmetization of syntax".

Insofar as this essay may contain any new insights, they will be due to the 
perspective gained through what I call "Paleolithic Model Theory", of which 
I now give a capsule overview:

All cwffs [closed wffs] of predicate logic are either ABSOLUTE or 
CONTINGENT. A cwff B  is *absolute* iff it is either a contradiction, or 
the negation of a contradiction, in which case it is called "u-valid" [a 
tautology]. B  is *contingent* iff it is not absolute. Absolute cwffs have 
well-defined truth values prior to and independent of interpretation, 
whereas contingent cwffs have indeterminate truth values prior to 
interpretation, and are *utterly* dependent for their evaluation upon 
interpretation.

[Note: Other writers have employed the words 'absolute' and 'contingent' 
somewhat differently than I do. Be warned!]

Every *contingent* cwff is unprovable in any simply-consistent classical 
logic, but SOME *contingent* cwffs are TRUE.

What distinguishes the *absolutely* true from the *contingently* true cwffs 
is that the absolutely true cwffs are LOGICALLY true, whereas the 
contingently true cwffs are FACTUALLY true, i.e., they pertain to questions 
of FACT rather than mere questions of syntactical structure. A rule of 
thumb is: If  B  is finitely valid [i.e., has no finite counter-models], 
then the recursively undecidable question of whether B  is FACTUALLY true 
can *only be solved by reflection*: If the truth of  B  depends upon ["is 
contingent upon"] some externality, then B  is not *absolutely* true. If 
the truth of B  depends only upon its internal structure, then it is 
absolutely true, tautological. [And you can take that to the bank!]

========================================================================

                   All sentences of CLFO may be partitioned on the basis
                   of whether or not they [or their duals] possess models
                   and, if so, whether or not they possess finite models.

========================================================================


Thus, a cwff B is u-valid [="Universally Valid"] iff its negation, ~B, 
possesses no models whatsoever. A cwff B is n-valid [="Factually Valid"] 
iff its negation, ~B, possesses at least one infinite model, but no finite 
models. A sentence B is k-valid iff B is valid on some finite domain and 
its negation ~B has at least one finite model. If B is realized on a 
domain, then that domain is designated as 'Dom(B)'.

An example of the latter: If  B  =df= "All natural numbers are 
less-than-or-equal to  13", then B is valid on the set {0,1,2, ... , 12, 
13} and ~B  ["There exists at least one natural number greater than 13"] 
has models on {14}, {14,15}, ... , {14,15, ...} i.e., has infinitely many 
finite models. Hence B  is k-valid, and  ~B  is (k+1)-satisfiable. This is 
an example of the

Axiom of Dual-Symmetry: [Read '@' as "element of" ] Dom(~B) =df= ~Dom(B). 
The most interesting example of this is when B is n-valid: Dom(B) @ < {0}, 
{1}, {2}, ... > and Dom(~B) = ~Dom(B) = omega - < (0}, {1}, {2}, ... >. 
This can be best understood by noting that omega =df= U < {0}, {1}, {2}, 
...> and interpreting 'omega - <{0}, {1}, {2}, ... >' as denoting the 
actual, completed limit ordinal omega as a sort of hard shell or 
impenetrable surface of a hollow sphere. The idea being that ~B is NOT 
realized on any proper subset of  w. [It's as if the idea of open and 
closed sets were applicable to w.]

This partition applies with equal force to sentences of Second Order 
Predicate Logic [SOPL] and on up through the entire panoply of higher-order 
predicate logics [CLFO]. A sentence of Predicate Logic, of any order is 
either consistent or not. If it  *is* consistent then it possesses at least 
one model, and of those models, either at least one is finite, or not. The 
criterion of "possessing a finite model" is semi-decidable: If a finite 
model exists, it can always be found in finitely many steps. If no finite 
model exists, there is (in general) no finitary process by which 
non-existence can be decided. This *fact* defines a partition on the set of 
all sentences of Predicate Logic (of any order) as follows:

All sentences of FOPL, SOPL and CLFO necessarily fall into one of the three 
blocks of the following partition:

        {U} contains all-and-only the u-valid sentences and their negations;
        {N} contains all-and-only the n-valid sentences and their negations;
        {K} contains all-and-only the k-valid sentences and their negations.

{U} is coextensive with the class of absolute cwffs, and the blocks {N} and 
{K} comprise the class of contingent cwffs.

             *** All the "true-but-unprovable" cwffs live in {N}.***

[The concepts of 'absolute' and 'contingent', together with this partition 
and the Axiom of Dual-Symmetry provide the foundation of what I call 
"Paleolithic Model Theory".]

So far as I'm aware, the only time [prior to the publication of G"odel's 
Incompleteness Proof ] that the phenomenon of  n-validity was mentioned in 
the literature was in Leopold L"owenheim's 1915 paper ON POSSIBILITIES IN 
THE CALCULUS OF RELATIVES [which, as noted above in the discussion of the 
Completeness Theorem for FOPL, played a significant role in G"odel's 
Completeness Proof.]

Although L"owenheim's paper was couched in the language of the 
Boole-Schroeder Calculus of Relatives, the contents translate over to FOPL, 
and in the first section of the paper L"owenheim presents [the Calculus of 
Relatives counterpart of] the partition introduced at the beginning of this 
paper. L"owenheim gives the three blocks as, "An identical equation" 
[corresponding to u-validity], "A fleeing equation" [corresponding to 
n-validity], and "A halting equation" [corresponding to k-validity], 
although no mention is made of the duals. G"odel *may* have read 
L"owenheim's paper, as part of his preparation for the Completeness of 
FOPL, as well as the corrected and extended version of Skolem 1920, and if 
so, the novelty of the "Fleeing equations" surely must have stuck in his mind.

========================================================================

G"odel's Completeness theorem treated the question of the completeness 
[semi-decidability] of First Order Predicate Logic [FOPL] by showing that, 
for any proposition B of  FOPL, the meta-proposition, "B  is u-valid 
[defined above] if-and-only-if  B  is provable in FOPL" is equivalent to 
the meta-proposition, "B  is either refutable [demonstrably inconsistent] 
or  B  is satisfiable on a finite or denumerably infinite ground domain." 
He then presented a version of Thoralf Skolem's proof of the latter 
meta-proposition, which was derived from L"owenheim's 1915 paper ON 
POSSIBILITIES IN THE CALCULUS OF RELATIVES. Result: All u-valid sentences 
of FOPL are provable within the system.

Leon Henkin, [Journal of Symbolic Logic, Vol. 15, 1950] proved that the 
equivalence of the two meta-propositions mentioned above holds for CLFO as 
well as for FOPL. Hence, CLFO is complete for u-validity.

In terms of the  U + N + K partition above, G"odel's Completeness Theorem 
can then be re-stated as:"If  B  is in  {U} then either  B or ~B can be 
proven in FOPL". As I demonstrate below, G"odel's Incompleteness Theorem 
can be restated as: "If  B  is in {N} then either  B  or  ~B  is 
true-but-unprovable in classical CLFO".

A large literature has arisen about this theorem; some of it rather 
smacking of mythology, in which it is more or less taken as axiomatic that 
true-but-undecidable sentences must necessarily be constructed in the 
manner that G"odel employed, or at least be self-referential, and that 
there is some sort of mysterious characteristic about the class of 
true-but-undecidable sentences. I shall comment on this in the sequel.

========================================================================

Let us now return to the partition:

All sentences of FOPL, SOPL and CLFO necessarily fall into one of the three 
blocks of the following partition:

         {U} contains all-and-only the u-valid sentences and their negations;
         {N} contains all-and-only the n-valid sentences and their negations;
         {K} contains all-and-only the k-valid sentences and their negations.

So now we ask, into *which* block of the partition does G fit? Clearly not 
into {U}, for that would mean that G,~G are (respectively) universally 
valid and absolutely contradictory, and we *really do know* that  G, ~G 
aren't in that block, [assuming the simple consistency of STT.]

Similarly, if G,~G were to fall into {K} , then there would have to be 
values of p , call them p' and  p" such that NotProve(p',q) is true 
and  ~[NotProve(p",q)] is true, which would mean that STT was both 
CERTAINLY simply-inconsistent and POSSIBLY omega-inconsistent. [For any 
given particular value of  p , if the sentence is true, then the truth of 
the sentence is effectively provable because of the primitive recursiveness 
of the relation NotProve( p,q).]

The only block left that  *permits* us to believe STT is BOTH simply AND 
omega-consistent is {N}.

        Hence, we have that  G is  n-valid, and that  ~G has an infinite model.

========================================================================


So now we see that  G is unprovable, *not merely* because of G"odel's 
self-referential construction, but *also* because the UNINTERPRETED 
proposition is  NOT  u-valid ! And the fact that STT would be shown to be 
inconsistent if it were to prove G ,

           **would also follow from proving ANY OTHER NON u-valid proposition**

             [Chew on THAT awhile. Roll it around in your mouth. Taste it.]

But G *is* true, because being valid on every finite ground domain is as 
close to Truth as it is possible for any non-tautological proposition to 
get! [This also merits some reflection.]

The shortest and simplest axiom of infinity that I know of in a "pure" 
logic [i.e., one without any defined constants such as '=' or '<' ] is 
expressible in FOPL and was first published by Kurt Sch"utte, in 1934, as a 
demonstration that the "E-A-E prefix class" of FOPL was undecidable. The 
elegance and economy of this proposition, which employs only three F.O. 
quantifiers, one dyadic-predicate and four literals, suggests to me 
that  Sch"utte knew *exactly* what he was doing, and started off with a 
FOPL definition of a non-reflexive, transitive relation [think "<" or ">"] 
and then trimmed it down to the final form.

(Ax)[~P(x,x) & .(Ey)[P(x,y) & .(Az)[P(y,z) => P(x,z)].].]. - - - - - - - - 
- - - - - - KS

has no finite models. The n-valid dual of  KS results from negation:

~.(Ax)[~P(x,x) & .(Ey)[P(x,y) & .(Az)[P(y,z) => P(x,z) ].].].

which, after a little judicious re-arranging, yields

~.[(Ax,Ey)[P(x,y) & .(Az)[P(y,z) => P(x,z)].] & ~(Ex)P(x,x).].

which is equivalent to

[.(Ax)(Ey)[P(x,y) & .(Az)[P(y,z) => P(x,z)].]. => (Ex)P(x,x).].

"If the relation P is transitive, then it is also reflexive w.r.t. at least 
one element of its domain",

                        which is n-valid,

and just as true [semantically], and just as unprovable [syntactically] as 
G"odel's self-referential construction G !!!

Moreover, by simply prefixing the second-order universal quantifier "(AP)" 
to the last formula, we obtain a correspondingly short and simple 
constructive proof of the "undecidability" [semi-decidability] of SOPL.

In an "applied" logic, i.e., having one or more operator or relation 
constants, e.g., '<', the shortest "true-but-unprovable" cwff that I know of is

                             ~.(Ax,Ey)[ x < y ].

which is the negation of an infinity axiom [omega-satisfiable, but no 
finite models] and hence,

                             .(Ex,Ay)[x >= y].

                 "(Every non-empty set) has a greatest element.)"

which is n-valid, true and unprovable.

If you object to the *Implicitness* of  "(Every non-empty set)", then 
rewrite it as

                    .(Ex,Ay)[.S(x) & S(y). => x >= y].

========================================================================

None of this detracts, *or is intended* to detract, from the beauty and 
great importance of G"odel's magnificent work. As I remarked above, prior 
to G"odel, no one except L"owenheim seems to have even *noticed the 
existence* of n-valid cwffs.

            ***** It IS, however, *intended* to DE-MYSTIFY the theorem. *****

One further note: The statement that "SOPL [second-order predicate logic] 
is not even semi-decidable" is *misleading*: While it is true that there 
are cwffs of  SOPL which are TRUE IN THE STANDARD MODEL that are not 
syntactically derivable from the axioms, this is *not* a comment about the 
"inadequacy of the axiomatization", but rather about *a  fundamental flaw* 
in the concept of "truth in the standard model": It *includes* as true in 
the standard model all cwffs which although *not provable* in a finitary 
logic, become provable by implicit recourse to "the axiom of infinite 
induction", commonly referred to as "the omega rule". This applies to the 
set of all n-valid cwffs, and indeed was formulated to achieve just that 
purpose. An inevitable concomitant of such a  convention is to exclude all 
"infinity-axioms" from the standard model by the simple device of 
stipulating that infinite counter-models are "non-standard" and therefore 
irrelevant. It is by  **this** maneuver that it is then claimed that "truth 
in the standard model" captures categoricity: For now, all those other 
models which had prevented, e.g., Peano Arithmetic, from being categorical 
are simply MANDATED to be, in effect, non-existent. Standard Model 
semantics obtains omega-completeness by declaring that infinite 
counter-models *just don't matter*. This is

                       "truth-by-gentleman's-agreement",

and has very little relevance to the Algebra of Logic known as the 
Classical Logic of Finite Order [A.K.A. Theory of Types] in which it is 
possible to  *actually determine by finite calculation* whether a given 
conclusion validly follows from a given (set of) premiss(es). That, after 
all, was the entire justification for the existence of Mathematical Logic 
in the first place.

One last thing: If theories which have no finite models [e.g., PA] are to 
be true in the Standard Model, then the "(Ax)[S(x) /= 0]" axiom [or 
equivalent] has to be either dropped or negated. If negated, then 
"(Ex)[S(x) = 0]" presents us with a FINITE inaccessible cardinal. [Check 
out Tarski's definition!] Strict finitists should *love* this.

Confusion on the question of completeness in higher-order logic has arisen 
because of the unprovability of G in SOPL. Since G is not u-valid, that 
leaves SOPL (as well as STT) in the same decidability class as FOPL: All 
are semi-decidable for u-validity. If  G, being True (on account of being 
n-valid), is to be regarded as a  **proper candidate** for proof in SOPL, 
then, of course, it would appear that "SOPL is not even semi-decidable"; 
but then, by the same reasoning, the *same* remark would apply to FOPL, 
since n-valid sentences **are not provable there either.**

========================================================================

Finally, we conclude with the

General Undecidabiity Theorem: A finitary formal deductive system S , in 
which all and only the u-valid wffs of  S  are provable need satisfy only 
the following two additional criteria in order to be "undecidable" [i.e., 
semi-decidable]:

(1) The negation ~B  (of a wff B of  S) such that  B  has an infinite 
model, but no finite models, is valid on every finite non-empty ground domain.

(2) There is at least one wff B of  S  such that either  B  or  ~B  has an 
infinite, but no finite model.

If a finitary formal deductive system in which all and only the u-valid 
cwffs of the system are provable, additionally meets the above two 
criteria, then the system is simply consistent and "undecidable" in the 
sense of being at most semi-decidable, and is omega-incomplete, in the 
sense of Tarski, [citation].

NOTE: Proof: (1) rules out "freak" systems that might be constructed to 
provide that the negation of an axiom of infinity is only satisfiable on 
the empty domain, and at the same time provides the n-valid negation of the 
axiom of infinity provided by (2).

========================================================================