The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

Dear Members of the Research Community,

After a very fruitful debate with Russell O'Connor (who provided the proof of 
Goedel's First Incompleteness Theorem in Coq) I would like to correct and 
update some of my earlier publications.

Also, with the kind permission of Russell O'Connor, his definitions for 
carrying out Goedel's First Incompleteness Theorem in Peter B. Andrews' logic 
Q0, an improved variant of Church's type theory, including a sample proof for 
a 
case of theorem V, are attached at the end of this e-mail. Andrews' logic Q0 
is 
specified in [Andrews, 2002, pp. 210-215; Andrews, 1986, pp. 161-165]. A 
short 
description is available online at [Andrews, 2014]:
        
http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/#ForBasEqu

Finally, a comparison of the proofs of Goedel's First Incompleteness Theorem 
by 
Russell O'Connor (in Coq) and Lawrence C. Paulson (in Isabelle) is undertaken 
in order to foster the understanding of the proof. The type system 
implemented 
by O'Connor is particularly well suited for demonstrating the three different 
language levels in the proof.

Kind regards,

Ken Kubota


I. Corrections

1. The critique of a presentation of Goedel's First Incompleteness Theorem in 
my 2013 article [Kubota, 2013] applies to that particular presentation only, 
but not to the original publication of Goedel's First Incompleteness Theorem 
[Gödel, 1931]. Since the work with the criticized presentation is a standard 
work on higher-order logic, and the author of that work is usually extremely 
precise and accurate, I did not expect the criticized presentation to 
substantially differ from Goedel's original proof.

2. The hypothesis in my 2015 article [Kubota, 2015] that there is a 
significant 
difference in the results between axiomatic (Hilbert-style) deductive systems 
(called "object logics" in the article) and natural deduction systems (called 
"meta-logics" in the article) cannot be upheld.

In summary, although some presentations of Goedel's First Incompleteness 
Theorem fail, this doesn't seem to apply to Goedel's original proof, nor does 
it apply to the formalized (mechanized) proofs provided by Russell O'Connor 
(in 
Coq) and others. The result of the formal proof can be interpreted in the 
sense 
that there is a formula (having the form of a sentence) that is neither 
provable nor refutable, but calling this "incompleteness" depends on a 
specific 
philosophical view, the semantic approach (model theory). If one doesn't 
share 
the semantic view, Goedel's theorem, although it seems formally correct, 
doesn't have the philosophical relevance often associated with it.


II. Summary of the Proof


1. Mathematical (formal) part

a) Goedel begins with the introduction of a number of definitions supposed to 
represent the form of a mathematical proof using mathematical (arithmetic) 
means, up to the last definition "Bew" (for "beweisbare Formel", i.e., 
"provable formula").

b) In theorem V, Goedel shows that each relation R (with the property of 
being 
primitive recursive) is definable within the logistic system by syntactical 
means (i.e., provability) only, in other words, for each R, there is an r 
(with 
the free variables u_1, ..., u_n), such that
        R(x_1, ..., x_n) -> Bew(  Sb(r, u_1, Z(x_1), ..., u_n, Z(x_n))  )
where Z is the numeral function, which returns the number in the language of 
the embedded language when supplying a (natural) number of the logistic 
system 
in which the proof is undertaken.
The proof is of a rather technical nature and quite lengthy, and, 
unfortunately, in his presentation Goedel only sketched the idea. For an 
example, see the attached presentation by Russell O'Connor.

c) Newer presentations refer to a fixed-point theorem called the diagonal 
lemma 
(or diagonalization lemma), which is rather implicit in Goedel's original 
proof. It can be used to construe a formula with the form of a sentence (a 
boolean-valued well-formed formula with no free variables) g of the embedded 
language, such that (simplified)
        ~Bew(g)
and
        ~Bew(not g).

For an excellent introduction to the diagonal lemma, see [Raatikainen, 2015], 
available online at
        
http://plato.stanford.edu/archives/spr2015/entries/goedel-incompleteness/sup2.html

In order to use the least amount of prerequisites, one may consider Goedel's 
proof of the (simplified) formula
        ~Bew(g) /\ ~Bew(not g)
as a purely formal proof, where the definition of "Bew" is simply an 
abbreviation of a more complex number-theoretic well-formed formula.

However, for establishing the philosophical meaning associated with Goedel's 
First Incompleteness Theorem, namely incompleteness, two philosophical 
assumptions are necessary.


2. Philosophical part I: Correctness of definitions

The first philosophical assumption is the correspondence of the definitions 
up 
to "Bew" with the form of mathematical proofs. Although it is obvious that 
the 
definitions do establish a proper representation of mathematical proofs, this 
fact goes beyond the formal part. For example, a proof verification system 
(or 
proof assistant) may prove
        ~Bew(g) /\ ~Bew(not g)
as a formal theorem, showing that, given the definitions, this theorem can be 
obtained. But the software does not verify whether the definitions actually 
match the form of mathematical proofs; this task is left to the reader. 
Goedel 
himself emphasizes that the definability of (primitive) recursive relations 
in 
the system P is expressed by theorem V "_without_ reference to any 
interpretation of the formulas of P" [Gödel, 1931, p. 606, emphasis in the 
original].

Goedel speaks of yielding "an isomorphic image of the system PM in the domain 
of arithmetic, and all metamathematical arguments can just as well be carried 
out in this isomorphic image." [Gödel, 1931, p. 597, fn. 9] The isomorphism 
itself, however, can only be seen from top, from the meta-perspective, i.e., 
from outside of the logistic system in which the proof is undertaken. A 
direct 
reference of the formal system to its own propositions is not possible.

Accordingly, O'Connor distinguishes between a Goedel quote function and a 
Goedel numbering (or encoding) function, saying that propositions are 
"opaque". 
The Goedel numbering (or encoding) function "G isn't a function from 
propositions to natural numbers. It is supposed to be a function from 
*syntactic* formulas to natural numbers and the type of syntactic formulas is 
completely different from the type of propositions.  Computations over 
syntactic formulas can inspect the intension[al] structure of the formula, 
but 
propositions are opaque and no such computation is possible." [Russell 
O'Connor, e-mail to Ken Kubota, February 8, 2016]

The same consideration was made by the author when mentioning the 
"non-definability of the Goedel encoding function" previously at
        
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-January/msg00029.html

By verifying the definitions (which is not a purely mathematical / formal 
task) 
one then can reasonably state that "Bew" can be interpreted as "provable", 
and 
that there is a formula with the form of a sentence (a proposition with no 
free 
variables) that is neither provable nor refutable.


3. Philosophical part II: The semantic approach

Assuming
        1. the correctness of the formal proof, and
        2. the correctness of the definitions,
the result obtained so far is that a well-formed formula exists, or more 
specifically, a formula of the form of an arithmetic proposition exists, 
which 
can neither be proven nor refuted.

Following the semantic approach, according to which meaning is obtained by an 
interpretation in some kind of meta-theory, either "g" or "not g" must be 
true, 
hence there must be a true but unprovable theorem. This discrepancy between 
syntax (provability) and semantics (truth, meaning) is what is commonly 
called 
"incompleteness".

The implicit assumption made here and not discussed in the original 
publication 
of Goedel's First Incompleteness Theorem in [Gödel, 1931] is the use of the 
semantic approach (also called model-theoretic approach). In his completeness 
essay published a year earlier, Goedel already makes use of the 
model-theoretic 
approach in which semantic evaluation is performed by substitution at a 
meta-level, without explicitly pointing out the use of a specific 
philosophical 
assumption: "A formula of this kind is said to be valid (tautological) if a 
true proposition results from every substitution of specific propositions and 
functions for X, Y, Z, ... and F(x), G(x,y), ..., respectively [...]." 
[Gödel, 
1930, p. 584, fn. 3]

In order to speak of "incompleteness", an expectation of "completeness" is 
necessary, which is generally defined as the provability of all true 
propositions. Hence, incompleteness is only possible if semantics (meaning) 
differs from syntax, as is the case with model theory (the semantic approach).

But the semantic approach itself is a specific philosophical view and not 
inherent in mathematics. If one, like the author, does not share the semantic 
approach, but a purely syntactic approach, such that meaning in mathematics 
is 
obtained by syntactical inference only (and the few rules of inference have 
their legitimation in philosophy, outside of formal logic and mathematics), 
then by definition there is no distinction between syntax and semantics.

In summary, if one assumes the philosophical assumption of the semantic 
approach, then there is mathematical (arithmetic) incompleteness. But if one 
doesn't, Goedel's First Incompleteness Theorem only shows that there is a 
formula with the form of a well-formed (arithmetic) proposition which is 
neither provable nor refutable, but may also be considered meaningless. Not 
every well-formed formula (proposition) necessarily has to have a meaning, if 
one doesn't follow the semantic approach. "Mathematics is liquid" is 
grammatically correct, but nonsense. In philosophy, it is a well-established 
fact that sentences may have the (outward) form of a meaningful proposition 
without being meaningful.

Hence, without the philosophical assumption of the semantic view or a similar 
approach, Goedel's First Incompleteness Theorem loses its philosophical 
significance.


III. The Proofs by Russell O'Connor (in Coq) and Lawrence C. Paulson (in 
Isabelle)

A particularly elegant formulation of Goedel's First Incompleteness Theorem 
was 
presented by Russell O'Connor using the proof assistant Coq, as he takes 
advantage of "type safety by coding using an inductive type" [Russell 
O'Connor, 
e-mail to Ken Kubota, February 13, 2016], such that all three language levels 
use a different type. A short description is given in [O'Connor, 2006] 
available online at
        http://arxiv.org/pdf/cs/0505034v2.pdf
The formal proof is available at
        http://www.lix.polytechnique.fr/coq/pylons/contribs/view/Goedel/trunk

O'Connor uses different types for the three different levels of language:
L1: type "prop"
L2: type "Formula" (which may contain expressions of type "Term")
L3: type "nat"

The first language level (L1) is the language in which the proof is 
undertaken, 
expressed by propositions (type "prop").
The second language level (L2) is the embedded logic to be represented, 
expressed by syntactic formulae (type "Formula").
The third language level (L3) are the Goedel numbers obtained by encoding 
syntactic formulae (L2) using the Goedel numbering (or encoding) function, 
expressed by natural numbers (type "nat").

For example, the elimination of the implication can be expressed by
"Lemma impE :
forall (T : System) (f g : Formula),
SysPrf T (impH g f) -> SysPrf T g -> SysPrf T f."
        
http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.LNN.html
with the predicate "SysPrf" corresponding to Goedel's "Bew", expressing the 
provability of a L2 formula p in a theory T by "SysPrf T p".

The L1 expression is: "forall (T : System) (f g : Formula), SysPrf T (impH g 
f) 
-> SysPrf T g -> SysPrf T f".
A L2 expression is: "impH g f" (which would be written as "g -> f" at the L1 
level).

The Goedel numbering (or encoding) function accepts an argument of L2, and 
returns a number of L3:
"Fixpoint codeFormula (f : Formula) : nat :=
 match f with
 | fol.equal t1 t2 => cPair 0 (cPair (codeTerm t1) (codeTerm t2))
 | fol.impH f1 f2 => cPair 1 (cPair (codeFormula f1) (codeFormula f2))
 | fol.notH f1 => cPair 2 (codeFormula f1)
 | fol.forallH n f1 => cPair 3 (cPair n (codeFormula f1))
 | fol.atomic R ts => cPair (4+(codeR R)) (codeTerms _ ts)
 end."
        
http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.code.html

The numeral function accepts a number of L3 and returns the corresponding 
term 
that can be part of a L2 formula:
"Fixpoint natToTerm (n : nat) : Term :=
 match n with
 | O => Zero
 | S m => Succ (natToTerm m)
 end."
        
http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.LNN.html
For example, the number 3 is mapped to Succ(Succ(Succ(Zero))).

The final result is:
"Theorem Goedel'sIncompleteness1st :
wConsistent T ->
exists f : Formula,
  ~ SysPrf T f /\
  ~ SysPrf T (notH f) /\ (forall v : nat, ~ In v (freeVarFormula LNN f))."
        
http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.goedel1.html

So if the theory is (omega-)consistent, then a proposition exists (that does 
not contain any free variables) which is neither provable nor refutable.


Another formulation of Goedel's First Incompleteness Theorem was presented by 
Lawrence C. Paulson using the Isabelle proof assistant software. Descriptions 
are given in [Paulson, 2014] and [Paulson, 2015], linked at
        http://www.cl.cam.ac.uk/~lp15/papers/Formath/
and available online at
        http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic-mine.pdf
        http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf
The formal proof is available at
        https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/

The proof by Paulson is carried out in his proof assistant software Isabelle, 
which is implemented as a logical framework (a meta-logic), such that a 
fourth 
language level (the meta-logic) is involved. On the basis of this meta-logic 
(Isabelle/Pure), different object logics can be implemented such as set 
theory 
(Isabelle/ZF) or type theory (Isabelle/HOL).

Hence, the four language levels of Paulson's proof are:
L0: type "prop" of Isabelle/Pure (the logical framework / meta-logic)
L1: type "bool" of Isabelle/HOL (the object logic)
L2: type "fm" (for formula) of HF set theory (which may contain expressions 
of 
type "tm")
L3: type "tm" (for term) of HF set theory

However, since the purpose of the logical framework or meta-logic (L0) is 
only 
the implementation of several object logics such as the type theory / 
higher-order logic HOL (L1), the meta-logic has no significance, and for the 
purpose of verifying Goedel's proof and comparing its different formulations, 
one may abstract from (i.e., ignore) it. The proof could be carried out 
within 
a direct implementation of HOL (without a logical framework / meta-logic) 
also.

Particularly misleading to those not familiar with the Isabelle software can 
be 
the turnstile symbol (⊢) as defined by Paulson in the context of Goedel's 
proof 
only:
"inductive hfthm :: "fm set => fm => bool" (infixl "⊢" 55)"
        
https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/SyntaxN.html
The turnstile is introduced as an infix operator in a L1 expression, 
accepting 
a set of L2 formulae as first (left) operand, and a L2 formula as second 
(right) operand, denoting the predicate hfthm (for theorem of HF set theory) 
defined inductively directly afterwards. Usually in literature (e.g., 
[Andrews, 
2002]), the right operand is an expression of the main language (L1), such 
that 
the turnstile is an operator of the metamathematical level (which one would 
have to place at L0, although it would functionally differ from a logical 
framework).

Paulson's Goedel numbering (or encoding) function does not return numbers, 
but 
type "tm" (for term) of L3, which are more likely to be confused with L2:

"class quot =
 fixes quot :: "'a => tm"  ("⌈_⌉")

instantiation tm :: quot
begin
 definition quot_tm :: "tm => tm"
   where "quot_tm t = quot_dbtm (trans_tm [] t)"

 instance ..
end

[...]

instantiation fm :: quot
begin
 definition quot_fm :: "fm => tm"
   where "quot_fm A = quot_dbfm (trans_fm [] A)"

 instance ..
end"
        
https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/Coding.html

Paulson: "It is essential to remember that [in Paulson's formulation of the 
proof] Gödel encodings are terms (having type tm), not sets or numbers."
        http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 16)

The final result is:
"text{*Gödel's first incompleteness theorem: If consistent, our theory is 
incomplete.*}
theorem Goedel_I:
 assumes "¬ {} ⊢ Fls"
 obtains δ where "{} ⊢ δ IFF Neg (PfP ⌈δ⌉)"  "¬ {} ⊢ δ"  "¬ {} ⊢ Neg δ"  
                 "eval_fm e δ"  "ground_fm δ" "
        
https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/Goedel_I.html

Paulson's definition of the turnstile symbol (⊢) corresponds to O'Connor's 
predicate "SysPrf", which allows to express provability of L2 sentences 
within 
L1.
Paulson's definition of the predicate "PfP" corresponds to O'Connor's 
predicate 
"codeSysPf", which allows to express provability of L3 sentences within L2.

The statement "{} ⊢ δ IFF Neg (PfP ⌈δ⌉)" is an instance of the diagonal lemma 
using the construction "not provable" ("Neg (PfP [...])") as the lemma's 
property, which corresponds to that in O'Connor's definition of G:
"Definition G := let (a,_) := FixPointLNN (notH codeSysPf) 0 in a."
        
http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.goedel1.html

The statements "¬ {} ⊢ δ" and "¬ {} ⊢ Neg δ" express that neither the 
proposition nor its negation are provable. The turnstile (⊢) denotes a 
predicate defined on the basis of the language of the logic in which the 
proof 
is undertaken.

In contrast to O'Connor, Paulson also performs a semantic evaluation:
The statement "eval_fm e δ" says that the proposition evaluates to true.

The statement "ground_fm δ" ensures, like in O'Connor's proof, that the 
proposition does not contain any free variables.


Despite Paulson's claim that "the availability of this formal proof (which 
can 
be surveyed by anybody who has a suitable computer and a copy of the Isabelle 
software) can help to demystify the incompleteness theorems"
        http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic-mine.pdf 
(p. 1)
his presentation has a number of disadvantages. In order to fully understand 
Paulson's proof, including the language levels and the type system involved, 
Paulson's articles are insufficient. Especially the description of the type 
system of both meta-logic and object logic is fragmented into a number of 
occurrences across various documentation files of the software, making it 
extremely tedious to obtain all the information necessary to fully understand 
the formalized (mechanized) proof for anyone who is not very familiar with 
the 
proof assistant software used, even with advanced knowledge in formalizing 
(mechanizing) proofs. Not only would one expect a short introduction into the 
language levels, including the type system involved, but the articles 
concentrate on technical implementation details rather than the basic idea of 
the proof. The type "tm" occurs at two different language levels (L2 and L3), 
resulting in a higher ambiguity. The notation would require introduction, as 
a 
predicate is written as a symbol. Intermediary results, such as an instance 
of 
the diagonal lemma, and the additional semantic evaluation make the final 
result less readable in comparison to O'Connor's, who focuses on the 
non-provability and non-refutability of the proposition like Goedel in his 
original proof in theorem VI [cf. Gödel, 1931, p. 607 ff.].

Moreover, the formulation of the diagonal lemma is given as a special 
instance 
only, but not in the general form. Due to the "elimination of the 
pseudo-function K_i"
        http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 23)
his formulation of the diagonal lemma (and its application in Goedel's First 
Incompleteness Theorem) lacks the explicit use of the numeral function, 
yielding the following formulation:
"lemma diagonal:
 obtains δ where "{} ⊢ δ IFF α(i::=⌈δ⌉)"  "supp δ = supp α - {atom i}" "
        
https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/Goedel_I.html

Only the encoding function (⌈...⌉) is explicit in Paulson's formulation, 
whereas in O'Connor's formulation not only the Goedel encoding function 
(codeFormula), but also the numeral function (natToTermLNT) is present:
"Lemma FixPointLNT :
forall (A : Formula) (v : nat),
{B : Formula |
  SysPrf PA
    (iffH B (substituteFormula LNT A v (natToTermLNT (codeFormula B)))) /\ 
[...]"
        
http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.fixPoint.html

Without crediting Wikipedia with scientific credibility, we shall take 
advantage of the symbolic notation used for the Goedel encoding function (#) 
and the numeral function (°):
"Then T proves [...] p <-> F(°#(p)), which is the desired result." [The Greek 
character 'psi' was replaced by 'p'.]
        
https://en.wikipedia.org/w/index.php?title=Diagonal_lemma&oldid=702789841#Proof

In both cases quoted above, first the Goedel numbering or encoding function 
(#/codeFormula), then the numeral function (°/natToTermLNT) is applied.


IV. Possible Objections to the Formalized (Mechanized) Proofs

Due to their nature, formalized (mechanized), i.e., computer verified proofs 
are unlikely to contain mistakes. But two conceptual issues require 
discussion, 
as they are tacitly assumed.

1. The semantic approach (model theory)

Some proof assistants use methods of inference that rely on the semantic 
approach, specifically on the notion of satisfiability. These methods include 
resolution, which regularly makes use of unification and skolemization. If 
one 
does not share the semantic approach, but wants to rely on syntactical 
inference only, some skepticism may arise against theorems obtained by using 
these methods.

However, since no unexpected results are known by the use of the current 
proof 
assistants, most likely an equivalent method exists by which the results can 
be 
obtained using syntactical means only.

2. The introduction of types with the Backus-Naur form (BNF)

Most of the current proof assistants allow the introduction of mathematical 
types by use of the Backus-Naur form (BNF), which in computer science is the 
method of specifying an element of a formal language corresponding to 
inductive 
definitions in mathematics.

For example, O'Connor defines the type of syntactic formulae "Formula" as 
follows:
"Inductive Formula : Set :=
 | equal : Term -> Term -> Formula
 | atomic : forall r : Relations L, Terms (arity L (inl _ r)) -> Formula
 | impH : Formula -> Formula -> Formula
 | notH : Formula -> Formula
 | forallH : nat -> Formula -> Formula."
        
http://www.lix.polytechnique.fr/coq/pylons/contribs/files/Goedel/trunk/Goedel.fol.html

In an e-mail to the author, Paulson, who designed the Isabelle proof 
assistant 
software, basically argued that newer type systems should be more expressive 
than Church's simple type theory which uses combinations of iota (i) and 
omicron (o) only. Although this is, of course, correct, the explanation is 
not 
sufficient for justifying this specific mode, namely BNF, of type 
introduction. 
The legitimacy of mathematical types depends on logical properties. For 
example, types must not be empty, since otherwise the logistic system is 
rendered inconsistent. Thus, the use of the Backus-Naur form, which 
historically was introduced to specify grammars, is not appropriate for 
replacing mathematical reasoning. Types were invented by Bertrand Russell in 
order to avoid the paradoxes and therefore have logical properties (e.g., 
being 
non-empty) which should be subject to proof, but not be a matter of arbitrary 
declaration.

Nevertheless, other means may be used to express the same, such that the use 
of 
the Backus-Naur form is not essential to the proofs obtained by it.


V. Some Remarks on the Semantic Approach

In his article "The Semantic or Model-Theoretic View of Theories and 
Scientific 
Realism" available online at
        http://www3.nd.edu/~achakra1/downloads/semantic_view.pdf
Anjan Chakravartty emphasizes that according to the syntactic view, a theory 
"is identified with a particular linguistic formulation" [Chakravartty, 2001, 
p. 325]. In contrast, the semantic view aims at "independence on behalf of 
theories from language" [Chakravartty, 2001, p. 326].

Obviously, Paulson and his Isabelle software follow the semantic approach. In 
his essays describing the proof [Paulson, 2014; Paulson, 2015], the semantic 
approach remains a tacit assumption given as granted, as the notion of 
incompleteness depends on it. On the basis of Isabelle's logical framework 
Isabelle/Pure, variants of both axiomatic set theory and type theory, i.e., a 
formulation of Zermelo-Fraenkel set theory (Isabelle/ZF) and a polymorphic 
version of Church's simple type theory (Isabelle/HOL), are implemented 
without 
opting or showing preference for one.

In some sense, O'Connor is more careful, as he doesn't refer to the general 
notion of incompleteness, but only to "arithmetic incompleteness" or 
"essential 
incompleteness of [...] the language of arithmetic" [O'Connor, 2006, p. 15]. 
The problem reduces to a very specific phenomenon:
"Goedel's theorem is more than the exist[ ]ance of a wff of type 'o' that is 
neither provable nor refutable.  That goal is easy
((iota x : Nat . F) = 0) : o
This wff above is neither provable nor refutable in Q0 (or both provable and 
refutable in the unlikely case Q0 is inconsistent.)
The point of the incompleteness theorem is that there is an *arith[ ]metic* 
formula that is neither provable nor refutable, specifically a Pi1 arithmetic 
formula." [Russell O'Connor, e-mail to Ken Kubota, February 19, 2016]

"The emphasis on syntactical inference exists already hidden in the œuvre of 
Andrews. After stating that the semantic approach is only 'appealing' (but 
not 
definitely necessary), he then suggests to 'focus on trying to understand 
what 
there is about the syntactic structures of theorems that makes them valid.' 
'[S]imply checking each line of a truth table is not really very 
enlightening' 
[Andrews, 1989, pp. 257 f.]." [Kubota, 2013, p. 15]


VI. Acknowledgements

I would like to thank Russell O'Connor for providing the attached definitions 
and the sample proof as well as for granting permission for publication, for 
our interesting discussion, and for granting permission for the quotes used 
in 
this article to be published.


References

Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type 
Theory: To Truth Through Proof. Orlando: Academic Press.

Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type 
Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: 
Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: 
10.1007/978-94-015-9934-4.

Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia 
of 
Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at 
http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/ (July 
2, 
2016).

Chakravartty, Anjan (2001), "The Semantic or Model-Theoretic View of Theories 
and Scientific Realism". In: Synthese 127, pp. 325-345. DOI: 
10.1023/A:1010359521312. Available online at 
http://www3.nd.edu/~achakra1/downloads/semantic_view.pdf (June 30, 2016).

Gödel, Kurt (1930), "The completeness of the axioms of the functional 
calculus 
of logic". In: Heijenoort, Jean van, ed. (1967), From Frege to Gödel: A 
Source 
Book in Mathematical Logic, 1879-1931. Cambridge, Massachusetts: Harvard 
University Press, pp. 582-591.

Gödel, Kurt (1931), "On formally undecidable propositions of Principia 
mathematica and related systems I". In: Heijenoort, Jean van, ed. (1967), 
From 
Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Cambridge, 
Massachusetts: Harvard University Press, pp. 596-616.

Kubota, Ken (2013), On Some Doubts Concerning the Formal Correctness of 
Gödel's 
Incompleteness Theorem. Berlin: Owl of Minerva Press. ISBN 978-3-943334-04-3. 
DOI: 10.4444/100.101. See: http://dx.doi.org/10.4444/100.101

Kubota, Ken (2015), Gödel Revisited. Some More Doubts Concerning the Formal 
Correctness of Gödel's Incompleteness Theorem. Berlin: Owl of Minerva Press. 
ISBN 978-3-943334-06-7. DOI: 10.4444/100.102. See: 
http://dx.doi.org/10.4444/100.102

O'Connor, Russell (2006), "Essential Incompleteness of Arithmetic Verified by 
Coq" (2nd version). Available online at http://arxiv.org/pdf/cs/0505034v2.pdf 
(June 29, 2016). DOI: 10.1007/11541868_16.

Paulson, Lawrence C. (2014), "A Machine-Assisted Proof of Gödel's 
Incompleteness Theorems for the Theory of Hereditarily Finite Sets". In: 
Review 
of Symbolic Logic 7, pp. 484-498. DOI: 10.1017/S1755020314000112. Available 
online at http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic-mine.pdf 
(June 30, 2016).

Paulson, Lawrence C. (2015), "A Mechanised Proof of Gödel's Incompleteness 
Theorems using Nominal Isabelle". In: Journal of Automated Reasoning 55, pp. 
1-37. DOI: 10.1007/s10817-015-9322-8. Available online at 
http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (June 30, 2016).

Raatikainen, Panu (2015), "Supplement: The Diagonalization Lemma". In: 
Stanford 
Encyclopedia of Philosophy (Spring 2015 Edition). Ed. by Edward N. Zalta. 
Available online at 
http://plato.stanford.edu/archives/spr2015/entries/goedel-incompleteness/sup2.html
 
(June 30, 2016).

____________________

Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100