[FOM] Non-Arithmetical "Godel" Incompleteness.

[Steve Newberry]

               Non-Arithmetical "Godel" Incompleteness.

                       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, because it  is the *only* 
semantics in which *all* models are regarded as being of equal 
significance, and assume as known the equivalence between STT and 
Second-order logic [SOL]. The ground domain is discrete, countable, and may 
be thought of as being any otherwise arbitrary set capable of being indexed 
by either omega, or by any initial segment of the set of all countable 
ordinals. The acronym 'CLFO' [Classical Logic of Finite Order] is used 
indifferently as a synonym for STT, and is understood to include 
Propositional Calculus as well as Quantifier/Predicate logic. The symbols 
'@', '/', 'w', '~',are used to denote "is an element of", "negation of (a 
dyadic infix operator)", "omega", and either "complement of (a domain)" or 
"negation of (a wff)". I shall indulge in an abuse of language by using the 
word 'model' as an abbreviation for "domain of realization."] *** '% x' 
denotes "Section number x" ***

[% 0:]
========================================================================

I have been advised that my use of logical terminology is not always in 
accord with standard usage, and that I will have more success in 
communicating if I make clear the definitions of all neologisms, and 
neologistic usages, and give some motivation for such locutions. 
Accordingly, let us begin:

Since the topic is classical logic, it might be well to begin with the

AXIOM OF DUAL-SYMMETRY: Dom(B) = ~Dom(~B), and Dom(~B) = ~Dom(B). ['Dom(B)' 
and 'Dom(~B)' denote the domains of realization of the sentences B,~B. 
A  "domain of realization" is understood to be a subset, *usually proper*, 
of the Ground Domain of individuals. If  B  has more than one domain of 
realization, then Dom(B) is the sequence of unit sets s.t. each such unit 
set is a domain of realization for B. It can, and often does, happen that 
both B,~B each are realized on infinitely many [different] finite domains: 
If  B  says that "All numbers are odd" then ~B  says that "There exist even 
numbers", and each is realized on an infinite number of finite domains.

'absolute' =df= "A (closed) well-formed-formula B is said to be ABSOLUTE 
iff B is either a contradiction or the negation of a contradiction."

'contingent' =df= "A (closed) well-formed-formula B is said to be 
CONTINGENT iff  B  is NOT either a contradiction or the negation of a 
contradiction." Thus B is contingent iff B is not absolute.

'tautology' =df= ***negation of a contradictory sentence*** of classical 
logic [of any order, finite or infinite], thus extending to 
predicate/quantifier logic the usage which was traditionally limited to 
Propositional Calculus. The reason for this is that the word 'valid' is 
currently used in several senses, of which at least one is not identical to 
the definition here given for 'tautology'. The adjectival form is 
"tautological".

'valid' =df= "true without exception on some domain 'Dom(B)' ", where B 
denotes the sentence under consideration). Thus, "B is valid on Dom(B)" is 
***identically equivalent*** to "~B is contradictory on Dom(B)." The reason 
for this specification is that the subject of this essay is a partition of 
ALL the (closed) well-formed-formulas of classical logic [of any order, 
finite or infinite], in terms of the domains of realization [i.e., validity 
or satisfaction] of complementary-pairs B,~B of such formulas.

'u-valid' =df= "Universally-valid, tautological, LOGICALLY true, provable."
My intention here is to convey the fact that each of the comma-delimited 
terms of the definiens is **logically synonymous** with every other such term.

'n-valid' =df= "valid on all-and-only FINITE domains, possessing an 
infinite counter-model, but no others, FACTUALLY true." The G"odel sentence 
"I am unprovable" is FACTUALLY true, because it IS unprovable.

'w-satisfiable' =df= "satisfiable on every domain isomorphic to omega."

'cwff', 'wff' =df= "(closed) well-formed-formula"

'counter-model' =df= model of the negation of a cwff.

[% 1:]
========================================================================

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  CLFO 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.

Examples:
.P & ~P. and .P v ~P. have truth-values which are independent of 
interpretation.
.P & ~Q. and .P v ~Q. have no truth-values prior to interpretation.

The same remarks apply if the propositional variables are replaced by 
predicate expressions P(x), Q(x).

  [% 2:]
========================================================================

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

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

Let us now develop the idea outlined in FACT : The first block of the 
partition is the home of the absolute cwffs, call it  {U} for 
Universally  TRUE or Universally  FALSE.

B @ {U} iff one of B,~B has no models whatsoever, i.e., is contradictory. 
We adopt the convention that the contradictory cwff is denoted by '~B' and 
the tautology by 'B'. This accords with the definition of tautology as the 
negation of a contradiction: [Since we are in CLFO, the rule of 
double-negation holds, and  ~~B = B.]

Clearly, {U} contains all-and-only the *absolute* cwffs. Since the 
criterion for inclusion
in {U} is that one-and-only-one of the complementary pair B,~B has a model, 
then the criterion for inclusion in the *contingent* block *must* be that 
BOTH B,~B  have models; just for the moment, let us denote the contingent 
block as '{NK}'.

Referring again to FACT, we now inquire as to the possession of  *finite* 
models, and discover that the contingent block {NK} spontaneously divides, 
amoeba-like, into two blocks, {N} and {K}, where B @ {N} iff 
one-and-only-one of B,~B possesses a *finite* model; and adopt the 
convention that the possessor of one or more finite models is denoted 
by  'B' and the other, which has *no* finite models [but does have an 
infinite model!], is denoted by '~B'. {N} will be seen to be a VERY 
INTERESTING collection of cwffs! But first, let us finish by defining the 
last block of the UNK partition:

B @ {K} iff BOTH members of the complementary pair have finite models, and 
if one member
is realized on only finitely many finite domains, then it is denoted as 
'B', whereas
'~B' denotes the complementary member which is realized on infinitely many 
finite domains.
That there must be such follows from the Axiom of Dual-Symmetry [vide 
supra]. Indeed, we
CAN further partition {K} into {K'}, {K"} on the criterion of whether only 
one, or both,
of B,~B possess infinitely many finite models; but in this essay we shall 
restrict our attention to the coarser division, UNK. Let us now meet the

[% 3:] Axiom of Completeness: All cwffs of CLFO are provable iff they are 
tautologies. [L"owenheim, G"odel, Henkin]

Now this raises an interesting question: We know that, by the Axiom of 
Completeness, all cwffs of CLFO are Unprovable iff they are either 
contradictory or contingent, but the famous theorem of G"odel (1931) tells 
us that at least *some* of these [contingent] cwffs are TRUE in the 
Standard model! Clearly, none of these cwffs can be members of  either  {U} 
or {K}, hence {N} is the only place remaining for TRUE but contingent 
sentences to reside.

An approximate, but useful, restatement of G"odel's First Incompleteness 
theorem might be the following:

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

Recall the definition of  {N}: B has finite realizations, ~B does not. 
Since  ~B  is not contradictory [~B /@ {U}] then ~B must have a model, and 
since  ~B  has no finite realizations, that model must be infinite, which 
fact is frequently recognized in the literature by referring to such cwffs 
as "axioms of infinity". Some of these have primary interpretations which 
formalize one of the several definitions of infinite set in terms of 
mappings, others merely describe processes or relations which can only 
exist on *completed* infinite sets, e.g., '<'.

People who have difficulty in conceiving of such sets have a corresponding 
difficulty in conceiving of the  ~B  sentences as being significant; and 
many others, [who evidently are altogether comfortable with 
completed-infinite sets, even to the extent of non-denumerably infinite 
sets], dismiss the  ~B  cwffs as being "non-standard" and therefore irrelevant.

In any case, it is clear that these strange cwffs are VERY CLOSE to being 
contradictory. One might say that they are "asymptotically" close to being 
contradictory, and, by dual-symmetry, that tells us that the  ~~B [=B] 
cwffs are "asymptotically" close to being u-valid. And in fact, we have a 
special designation for these "quasi-tautological" cwffs:

[% 4:]
        ***B is n-valid. iff B  has no finite counter-models,
        but does have at least one infinite counter-model.***

      ***A true sentence living in {U} is u-valid and provable and
       a 'true' sentence living in {N} is n-valid and unprovable.***

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

What distinguishes the *absolutely* true from the *contingently* true cwffs 
is that the absolutely true cwffs are only LOGICALLY true, whereas the 
contingently true cwffs are FACTUALLY true, i.e., they are contingent upon 
questions of actual 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 or not  B  is FACTUALLY true 
[as opposed to merely being LOGICALLY true] can either *only be solved by 
thought* [if Factual], or by producing a formal proof of B [if Logical]. If 
the truth of  B  depends upon ["is contingent upon"] some externality, some 
actual fact of  the Real World, then B  is not *absolutely* true, and *must 
therefore be
n-valid*. If the truth of B  depends only upon its internal syntactical 
structure, then
it is absolutely true, tautological, and in CLFO, provable.

Summarizing the  UNK partition: 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 BOTH B,~B  have at least one finite model. If B 
is realized on a domain, then that domain is designated as 'Dom(B)'.

Material Implication Theorem:

:B => C. and .C is contingent: => :B is either contradictory or contingent. 
& .Dom(B) is a subset of Dom(C):

Corollary: u-valid(B) & contingent(C). => .~.B => C: no, not ever, never.

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

[% 5:] The  UNK partition applies with equal force to sentences of Second 
Order logic [SOL] and on up through the entire panoply of higher-order 
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 FOL, SOL 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".]

[% 6:]
========================================================================

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 FOL, 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 FOL, 
and in the first section of the paper L"owenheim presents [the Calculus of 
Relatives counterpart of] the  UNK partition introduced above. 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 
FOL, and if he did,, 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 logic [FOL] by showing that, for any 
proposition B  of  FOL, the meta-proposition, "B  is u-valid [defined 
above] if-and-only-if  B  is provable in FOL" 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 FOL 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 FOL. Hence, CLFO is complete for u-validity.

Axiom of Completeness: All cwffs of CLFO are provable iff they are 
tautologies.
[L"owenheim, G"odel, Henkin]

In terms of the  UNK 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 FOL".
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 CLFO".

A rather 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.

[% 7:]
========================================================================

Let us now return to the partition:

All sentences of FOL, SOL 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, [assuming simple consistency of 
G"odel's system P], we *really do know* that  G, ~G aren't in that block,

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 CERTAINLY 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 G"odel's system P 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. REMEMBER it!]

But G *is* true, because being valid on every finite ground domain entails 
also being satisfiable on the infinite union of the fundamental sequence of 
finite models, and the conjunction of these two conditions is equivalent to 
the definition of n-validity, which is *as close to absolute Truth* as it 
is *possible* for any non-tautological proposition to *get*!

                  [This also merits some reflection.]

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

     THIS WOULD BE A GOOD TIME FOR A COFFEE BREAK , OR A PIT STOP

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

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 FOL 
and was first published by Kurt Sch"utte, in 1934, as a demonstration that 
the "E-A-E prefix class" of
FOL 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 FOL 
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 negation of  KS is just:

       ~.(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 !!!

So FOL is just as incomplete as SOL, and for the same reason.

[Clearly, both KS and ~KS are consistent, and must therefore have models. 
Question: Are either KS or  ~KS true in the Standard model? If yes, which 
one? Why that one?.]

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 SOL.

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

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

which is the negation of an infinity axiom  [~.(Ax,Ey)[ x < y ].] and hence,

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

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].

[% 8:]
========================================================================

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-ROMANTICIZE the theorem. *****

[% 9:]
========================================================================

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, and 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).

[% 10:]
========================================================================