[FOM] A NON-ARITHMETICAL CHARACTERIZATION OF G"ODEL'S FIRST INCOMPLETENESS THEOREM
Steve Newberry
stevnewb at ix.netcom.com
Sun May 18 14:06:14 EDT 2003
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).
========================================================================
More information about the FOM
mailing list