[isabelle] Corrections of and amendments to prior publications on Goedel's First Incompleteness Theorem; Russell O'Connor's definitions for its proof in Peter B. Andrews' logic Q0; Comparison of the proofs by O'Connor and Paulson



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

________________________________________________________________________________

SampleProofTheoremV by Russell O'Connor
________________________________________________________________________________

[In the following, all occurrences of "substitueFormula" were replaced by "substituteFormula".]


[...] formal proof of a statement like

(1)   forall R exists r forall x   PRR1(R) -> [ Rx -> [ proofB[Sb(r,u,Z(x))] ] ]

but done in Q0 instead of informal mathematics.  However, to get us started we can just try proving a single instance of this more general theorem in Q0.

(2)  exists r forall x   PRR1([\x.x>1]) -> [ [\x.x>1]x -> [ proofB[Sb(r,u,Z(x))] ] ]

The sad bit is that this single instance is much much easier to prove directly than the general theorem is, so my proof of the single instance probably won't be too illuminating.

First, let me partially formalize statement (1) in Q0.

PRR1 : (Nat -> o) -> o
PRR1 := ... to be defined later ...

PR1isExpressible : o
PR1isExpressible
forall R : Nat -> o. PRR1(R) =>
  exists r \in FormulaSet. exists u \in Nat.
    forall x \in NatSet.
      (R x => proves RA (substituteFormula r (at u (natToTerm x)))) /\
      (~R x => proves RA (not (substituteFormula r (at u (natToTerm x)))))

(everything else should be defined [below])

The simpler instance is stated in Q0 as follows

GT1isExpressible : o
GT1isExpressible :=
  exists r \in FormulaSet. exists u \in Nat.
    forall x \in NatSet.
      (x > 1 => proves RA (substituteFormula r (at u x))) /\
      (~x > 1 => proves RA (not (substituteFormula r (at u (natToTerm x))))) /\

Unfortu[na]tely I've lopped off the PRR1 bit which is probably what inter[e]sted you, because now the proof is too easy.

Take r to be (some 1 (equal (var 0) (plus (var 1) (succ (succ zero)))))
Take u to be 0.
Let x be any value in NatSet.
We need to show that

(a) (x > 1) => proves RA (substituteFormula (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) (at 0 (natToTerm x))))
and
(b) ~(x < 1) => proves RA (not (substituteFormula (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) (at 0 (natToTerm x))))

First thing I'd like to note is that we can use the definition of substituteFormula to prove that

(substituteFormula (some 1 (equal (var 0) (plus (var 1) (succ (succ zero))))) (at 0 (natToTerm x))))
=
(some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero)))))

I also need a lemma that says
(forall x \in NatSet. freeVarTerm (natToTerm x) = empty)

This reduces our goal to

(a) (x > 1) => proves RA (some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero)))))
and
(b) ~(x < 1) => proves RA (not (some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero))))))

Let's do (b) first because it is easier. We know x \in NatSet and that ~(x < 1) holds.  So x = 0 or x = 1.

Suppose x = 0.  Then we have to prove
goal:  (proves RA (not (some 0 (equal (natToTerm 0) (plus (var 0) (succ (succ zero))))))

Using a lemma that natToTerm 0 = zero we can reduce this proving
goal:  (proves RA (not (some 0 (equal zero (plus (var 0) (succ (succ zero))))))

expanding the definition of some we get

goal:  (proves RA (not (not (all 0 (not (equal zero (plus (var 0) (succ (succ zero))))))))

Using a lemma that says that
forall f \in FormulaSet. (proves RA (not (not f)))=(proves RA f)

we can reduce this to showing

goal:  (proves RA (all 0 (not (equal zero (plus (var 0) (succ (succ zero))))))))

So we can reduce or goal to

goal:  (proves RA (not (equal zero (plus (var 0) (succ (succ zero)))))))

One of the formulas in LA is
all 1 (all 2 (impl (equal (var 1) (var 2))
    (impl (all 0 (not (equal zero (var 1))))
          (all 0 (not (equal zero (var 2)))))))

so we know that
(proves RA
  all 1 (all 2 (impl (equal (var 1) (var 2))
     (impl (all 0 (not (equal zero (var 1))))
           (all 0 (not (equal zero (var 2))))))))

from the universal instantiation lemma which says
forall f \in FormulaSet. forall n \in NatSet. forall t \in TermSet.
  proves RA (all n f) => proves RA (substituteFormula f (at n t))

we can conclude

(proves RA
  (impl (equal (succ (plus (var 0) (succ zero)))) (plus (var 0) (succ (succ zero))
    (impl (all 0 (not (equal zero (succ (plus (var 0) (succ zero)))
          (all 0 (not (equal zero (plus (var 0) (succ (succ zero)))

One of the axioms of RA is

(all 0 (all 1 (equal (plus (var 0) (succ (var 1))) (succ (plus (var 0) (var 1))))))

So by using the universal [i]nstantiation theorem we get
(proves RA (equal (plus (var 0) (succ (succ zero))) (succ (plus (var 0) (succ zero))))

We have another lemma that says
forall t \in TermSet. forall s \in TermSet.  (proves RA (equal t s))=(proves RA (equal s t))

which lets us deduce that
(proves RA (equal (succ (plus (var 0) (succ zero))) (plus (var 0) (succ (succ zero)))))

So by the modus ponens closure property that defines proves, we can conclude that

(proves RA
    (impl (all 0 (not (equal zero (succ (plus (var 0) (succ zero)))
          (all 0 (not (equal zero (plus (var 0) (succ (succ zero))))

Another axiom of RA is
 all 0 (not (equal (succ (var 0)) zero))

So that plus universal instantiation lets us show that

 (proves RA (not (equal (succ (plus (var 0) (succ zero))) zero)))

And another lemma that says
forall t \in TermSet. forall s \in TermSet.  (proves RA (not (equal t s)))=(proves RA (not (equal s t)))

so we can conclude that

(proves RA  (not (equal zero (succ (plus (var 0) (succ zero))))))

Buy the universal gen[er]alization lemma we conclude

(proves RA (all 0 (not (equal zero (succ (plus (var 0) (succ zero)))))))


Using the modus ponens closure property that defines proves we can conclude t[ha]t

(proves RA
          (all 0 (not (equal zero (plus (var 0) (succ (succ zero))))

which was our goal.

[...]

I'll let you do the case where x = 1.

Now back to part (a)

goal: (x > 1) => proves RA (some 0 (equal (natToTerm x) (plus (var 0) (succ (succ zero)))))

Assuming that x > 1 that means there is some y \in NatSet such that
x = S (S y)

So this reduces our goal to

goal: proves RA (some 0 (equal (natToTerm (S (S y))) (plus (var 0) (succ (succ zero)))))

We can prove that (natToTerm (S (S y))) = succ (succ (natToTerm y)), so our goal is further reduced to

goal: proves RA (some 0 (equal (succ (succ (natToTerm y))) (plus (var 0) (succ (succ zero)))))

[...] the rest of the p[r]oof [...] to basical[l]y goes like this:

You can show

(proves RA (equal (succ (succ (natToTerm y))) (plus (natToTerm y) (succ (succ zero))))

and from this you can prove taht

(proves RA (some 0 (equal (succ (succ (natToTerm y))) (plus (var 0) (succ (succ zero)))))

which is the desired result.

At some point you have to use induction on 'y' to do these sorts of proofs, but you might be able to get away without induction here because we were lucky.

________________________________________________________________________________

ExtendedIncompletenessInQ0 by Russell O'Connor
________________________________________________________________________________

// Define Computably Enumerable (aka recursively enumerable) predicates.
CESet : (Nat -> o) -> o
CESet := \p. exists f \in PRF2Set. p = (\n. exists m:Nat. 0 < f n m)

// Standard Model
  
interpT : (Nat -> Nat) -> Term -> Nat
interpT := \v. TermR_(Nat) v 0 (\t. S) (\t. \s. \n, \m. n + m) (\t. \s. \n. \m. n * m)

interpF : (Nat -> Nat) -> Formula -> o
interpF := \v. \f. FormulaR_((Nat -> Nat) -> o)
                     (\t. \s. \v. interpT v t = interpT v s)
                     (\v. F)
                     (\f. \g. \r. \s. \v. r v /\ s v)
                     (\f. \g. \r. \s. \v. r v => s v)
                     (\f. \n. \r. \s. \v. forall m \in NatSet. r (\x. if x = n then m else v x))

isTrue : Formula -> o
isTrue := \f. f \in FormulaSet /\ freeVarFormula f = empty /\ interpF (\x. x) f

// Statement of essential incompleteness of arithmetic
ExtendedEssentialIncompletenessOfRA : o
ExtendedEssentialIncompletenessOfRA := forall t : Theory. (t c= FormulaSet /\ RA c= proves t /\ (proves t) \in CESet) =>
  exists g \in FormulaSet. freeVarFormula g = empty /\
                           ((proves t g \/ proves t (not g)) => proves t = FormulaSet) /\
                           (~(isTrue g) => proves t = FormulaSet)

________________________________________________________________________________

PrimitiveRecursiveFunctions by Russell O'Connor
________________________________________________________________________________

// We will make use of some object of type Nat that are not in NatSet

top : Nat
top := \p : (i -> o). T

bottom : Nat
bottom := \p : (i -> o). F

// Lists of natural numbers are countable, so we code them with natural numbers.

// Type Definition
ListNat := nat

nil : ListNat
nil := 0

cons : Nat -> ListNat -> ListNat
cons := \x. \l. 1 + pair x l

ListNatSet : ListNat -> o
ListNatSet := \l. forall p : ListNat -> o. (p nil /\ forall n \in NatSet. forall k. p k => p (cons n k)) => p l

ListNatR_a : a -> (Nat -> ListNat -> a -> a) -> ListNat -> a
ListNatR_a := \n. \c. \r. iota x : a. forall w : ListNat -> a -> o.
  (w nil n /\
   (forall n \n NatSet. forall l : ListNat. forall y : a. w l y => w (cons n l) (c n l y))
  ) => w r x

length : ListNat -> Nat
length := ListNatR_(Nat) 0 (\h. \t. S)

// Returns an error, repres[en]ted by bottom, when passed nil
head : ListNat -> Nat
head := if (nil=l) then bottom else iota h : Nat. exists t \in ListNatSet. (cons h t)=l

// Returns an error, repres[en]ted by bottom, when passed nil
tail : ListNat -> ListNat
tail := if (nil=l) then bottom else iota t : ListNat. exists h \in NatSet. (cons h t)=l

allList : (Nat -> o) -> ListNat -> o
allList := \p. ListNatR_o T (\n. \l. \r. p n /\ r)

lookup : ListNat -> Nat -> Nat
lookup := ListNatR_(Nat -> Nat) (\n. bottom) (\h. \t. \r. \n. R (\m. \z. r m) h)

// A type for primitive recursive programs (source code)
// The number of primitive recursive programs is countable, so we will represent them with natural numbers.

// Type Definition
PrimRecProg := Nat

// Type Definition
ListPrimRecProg := ListNat

// the program that takes no input and outputs 0
zeroP : PrimRecProg
zeroP := 0

// the program that takes one input and outputs the successor of the input
succP : PrimRecProg
succP := 1

// the program that takes n inputs and returns the kth input.
piP : Nat -> Nat -> PrimRecProg
piP := \n. \k. 2 + 3*(pair n k)

// the composition of m programs each taking n inputs and with program taking m inputs to make a program that takes n inputs.
composeP : PrimRecProg -> ListPrimRecProg -> PrimRecProg
composeP := \p. \lp. 2 + 3*(pair n lp) + 1

// the combin[a]tion of one program taking n inputs (base case), f, and
// a second programming taking n + 2 inputs (recur[s]ive case), g, and
// combining them by primitive recursion to make a program, h, that takes n + 1 inputs.
// where h(0,x1,x2...xn) = f(x1,x2...xn) and h(S n,x1,x2...xn) = g(n,h(n,x1,x2...xn),x1,x2...xn)
primRecP : PrimRecProg -> PrimRecProg -> PrimRecProg
primRecP := \f. \g. 2 + 3*(pair f g) + 2

// Not all programs are well defined.  The combinators have to take the programs that have the correct number of parameters and such.
// Here we define the set of well formed programs accepting n inputs.

primRecProgSet : Nat -> PrimRecProg -> o
primRecProgSet := \n. \p. forall (w : Nat -> PrimRecProg -> o).
  (w 0 zeroP /\
   w 1 succP /\
   (forall n \in NatSet. forall k \in NatSet. k < n.  w n (pi n k)) /\
   (forall n \in NatSet. forall m \in NatSet. forall q : PrimRecProg. forall qs : ListPrimRecProg. (w m q /\ allList (w n) qs) => w n (composeP q qs)) /\
   (forall n \in NatSet. forall f : PrimRecProg. forall g : PrimRecProg. (w n f /\ w (S (S n)) g) => w (S n) (primRecP f g))
  ) => w n p

//Now we give semantics to primitive recursive programs by writing an interpreter for them.
//This inte[r]preter needs to produce functions that take n arguments for various n, but we cannot write this directly in Q0.
//We cheat by writing functions that operate on ListNat and expect n elements in the list.
//We make note of the arity of the function by returning the arity when passed the value "top" which is of type Nat, but isn't a member of NatSet.

interpret : PrimRecProg -> ListNat -> Nat
interpret := \p. \a. if (a = top) then (iota r : Nat. primRecProgSet r p) else (iota r : List -> Nat.
  forall w : PrimRecProg -> (List -> Nat) -> o.
    (w zeroP (\l. 0) /\
     w succP (\l. S (head l)) /\
     (forall n \in NatSet. forall k \in NatSet. k < n => w (piP n k) (\l. lookup l k)) /\
     (forall n \in NatSet. forall m \in NatSet. forall q \in primRecProgSet m. forall iq : ListNat -> Nat.
        forall qs : ListPrimRecProg. forall iqs : ListNat -> ListNat.
        (forall i \in NatSet. i < length qs => lookup qs i \in primRecProgSet n) =>
        (w q iq /\ (forall i \in NatSet. i < length qs => w (lookup qs i) (\l. lookup (iqs l) i))) =>
           w (composeP q qs) (\l. iq (iqs l))) /\
     (forall n \in NatSet. forall f \in primRecProgSet n. forall if : ListNat -> Nat.
        forall g \in primRecProgSet (S (S n)). forall ig : ListNat -> Nat.
        (w f if /\ w g ig) => w (primRecP f g) (\l. R (\n. \z. g (cons n (cons z (tail l)))) (f (tail l)) (head l)))
    ) => w p r) l
    
// Now we can state what it means for every primitive recursive function to be repre[se]n[ ]table by an arith[ ]metic formula.
PRFRepresentable : o
PRFRepr[e]sentable : forall n \in NatSet. forall p \in primRecProgSet n. exists f \in FormulaSet.
   (forall i \in NatSet. i \in freeVarFormula f => i < (S n)) /\
   (forall l \in ListNatSet. length l = n => forall y \in NatSet.
      (proves RA (substituteFormula f (\i. natToTerm (lookup (cons y l) i)))) <=> interpret p l=y)

// We can specialize the above general theorem to the case of Primitive Recursive Functions of 2 argume[nt]s
PRF2Set : (nat -> nat -> nat) -> o
PRF2Set := \f. exists p \in primRecProgSet 2. forall x \in NatSet. forall y \in NatSet. interpret p (cons x (cons y nill)) = f x y.

// We can state as a corollary of PRFRepr[e]sentable that every member of PRF2Set is representable by an arith[ ]metic formula.
PRF2Representable : o
PRF2Representable : forall f \in PRF2Set. exists f \in FormulaSet.
  (forall i \in NatSet. i \in freeVarFormula f => i < 3) /\
  (forall x \in NatSet. forall y \in NatSet. forall z \in NatSet.
    (proves RA (substituteFormula f (\i. natToTerm (if i=0 then z else if i=1 then x else if i=2 then y else 0)))) <=> f x y=z)

________________________________________________________________________________

IncompletenessOfArithmeticInQ0 by Russell O'Connor
________________________________________________________________________________

// Section: Primitive
// 'a' stands for any type

Q_a : a -> a -> o

iota : (i -> o) -> i

// Section: Logic

// Notation
A = B := Q A B

// Notation
A <=> B := Q_o A B

T : o
T := Q_o = Q_o

F : o
F := \x : o. T = \x : o. x

// Notation
forall x : a. A := (\x : a. T) = (\x : a. A)

// Notation
A /\ B := (\g : o -> o -> o. g T T) = (\g : o -> o -> o. g A B)

// Notation
A => B := A = (A /\ B)

// Notaton
~A := A = F

// Notation
A \/ B := ~(~A /\ ~B)

// Notation
exists x : a. A := ~(forall x : a. ~A)

// Notation
A =/= B := ~(A = B)

// Recursive Notation
iota x : i. A := iota (\x. A)
iota x : o. A := (\x. x) = (\x. A)
iota f : a -> b. A := \x : a. iota z : b. exists f : a -> b. A /\ f x = z

//Notation
if A then B else C := iota x. (A /\ x = B) \/ (~A /\ x = C)
  
// Section: sets / predicates

//Notation
A \in B := B A

//Notation
A \notin B := ~(A \in B)

//Notation
{A} := Q A

//Notation
A \intersect B := \x. x \in A /\ x \in B

//Notation
A \union B := \x. x \in B \/ x \in B

//Notation
A c= B := \x. x \in A => x \in B

//Notation
A \ B := A \intersect (\x. x \notin B)

//Notation (usually i occurs in A)
{ A | i <- B } := \x. exists i \in B. x = A

//Notation
forall x \in A. B := forall x. x \in A => B

//Notation
exists x \in A. B := exists x. x \in A /\ B

empty_a : a -> o
empty_a := \x. F

BigUnion_a : ((a -> o) -> o) -> a -> o
BigUnion_a := \p. \a. exists s \in p. a \in s

// Section: Natural numbers.

// Type defintion
Nat := (i -> o) -> o

0 : Nat
0 := Q (\x. F)

S : Nat -> Nat
S := \n. \p. exists x. p x /\ n (\y. y =/= x /\ p y)

NatSet : Nat -> o
NatSet := \n. forall p : Nat -> o. (p 0 /\ forall m : Nat. p m => p (S m)) => p n

R : (Nat -> Nat -> Nat) -> Nat -> Nat -> Nat
R := \h. \g. \n. iota m : Nat. forall w : Nat -> Nat -> o. (w 0 g /\ forall x : Nat. forall y : Nat. w x y => w (s x) (h x y)) => w n m

1 : Nat
1 := S 0

2 : Nat
2 := S 1

3 : Nat
3 := S 2

4 : Nat
4 := S 3

//Notation
A + B := R (\x. S) A B

//Notation
A * B := R (\x. \y. (A + y)) 0 B

triangle : Nat -> Nat
triangle := R (\x. \y. (S x) + y) 0

pair : Nat -> Nat -> Nat
pair := \n. \m. triangle (n + m) + m

//Notation
A <= B := exists n \in NatSet . A + n = B

//Notation
mu n. A := iota n : Nat. n \in NatSet /\ n \in A /\ forall m \in A. n <= m


// Section: Syntactic Logic

// Type defintion
Term := Nat

var : Nat -> Term
var := \n. 1 + 4*n

zero : Term
zero := 0

succ : Term -> Term
succ := \t. 1 + 4*t + 1

plus : Term -> Term -> Term
plus := \t. \s. 1 + 4*(pair t s) + 2

mult : Term -> Term -> Term
mult := \t. \s. 1 + 4*(pair t s) + 3

TermSet : Term -> o
TermSet := \t. forall p : Term -> o.
  ((forall n \in NatSet. p (var n)) /\
   p zero /\
   (forall t : Term. p t => p (succ t))
   (forall t : Term. forall s : Term. (p t /\ p s) => p (plus t s)) /\
   (forall t : Term. forall s : Term. (p t /\ p s) => p (mult t s))
  ) => p t

TermR_a : (Nat -> a) -> a -> (Term -> a -> a) -> (Term -> Term -> a -> a -> a) -> (Term -> Term -> a -> a -> a) -> Term -> a
TermR_a := \v. \z. \c. \p. \m. \r. iota x : a. forall w : Term -> a -> o.
 ((forall n \in NatSet. w (var n) (v n)) /\
  w zero z /\
  (forall t : Term. forall y : a. w t y => w (succ t) (c t y)) /\
  (forall t : Term. forall s : Term. forall y : a. forall z : a. (w t y /\ w s z) => w (plus t s) (p t s y z)) /\
  (forall t : Term. forall s : Term. forall y : a. forall z : a. (w t y /\ w s z) => w (mult t s) (m t s y z))
 ) => w r x
  
freeVarTerm : Term -> Nat -> o
freeVarTerm := TermR_(Nat -> o) (\n. {n}) empty (\t. \p. p) (\t. \s. \p. \q. p \union q) (\t. \s. \p. \q. p \union q)

subTerm : Term -> (Nat -> Term) -> Term
subTerm := \r. \l. TermR_(Term) l zero (\t. succ) (\t. \s. plus) (\t. \s. mult) r

at :: Nat -> Term -> Nat -> Term
at := \n. \t. \m. if m = n then t else (var m)

// Type definition
Formula := Nat

equal : Term -> Term -> Formula
equal := \t. \s. 1 + 4*(pair t s)

falsum : Formula
falsum := 0

conj : Formula -> Formula -> Formula
conj := \f. \g. 1 + 4*(pair f g) + 1

impl : Formula -> Formula -> Formula
impl := \f. \g. 1 + 4*(pair f g) + 2

all : Nat -> Formula -> Formula
all := \n. \f. 1 + 4*(pair n f) + 3

FormulaSet : Formula -> o
FormulaSet := \f. forall p : Formula -> o.
  ((forall t \in Term. forall s \in Term. p (equal t s)) /\
   p falsum /\
   (forall f : Formula. forall g : Formula. (p f /\ p g) => p (conj f g)) /\
   (forall f : Formula. forall g : Formula. (p f /\ p g) => p (impl f g)) /\
   (forall n \in NatSet. forall f : Formula. p f => p (all n f))
  ) => p f

not : Formula -> Formula
not := \f. impl f falsum

disj : Formula -> Formula -> Formula
disj := \f. \g. not (conj (not f) (not g))

iff : Formula -> Formula -> Formula
iff := \f. \g. conj (impl f g) (impl g f)

some : Nat -> Formula -> Formula
some := \n. \f. not (all n (not f))

FormulaR_a : (Term -> Term -> a) -> a -> (Formula -> Formula -> a -> a -> a) -> (Formula -> Formula -> a -> a -> a) -> (Formula -> Nat -> a -> a) -> Formula -> a
FormulaR_a := \e. \m. \c. \i. \l. \r. iota x : a. forall w : Formula -> a -> o.
   ((forall t \in TermSet. forall s \in TermSet. w (equal t s)) /\
    w falsum m /\
    (forall f : Formula. forall g : Formula. forall y : a. forall z : a. (w f y /\ w g z) => w (conj f g) (c f g y z)) /\
    (forall f : Formula. forall g : Formula. forall y : a. forall z : a. (w f y /\ w g z) => w (impl f g) (i f g y z)) /\
    (forall n \in NatSet. forall f : Formula. forall y : a. w f y => w (all n f) (l f n y))
   ) => w r x

freeVarFormula : Formula -> Nat -> o
freeVarFormula := FormulaR_(Nat -> o) (\t. \s. freeVarTerm t \union freeVarTerm s) empty (\f. \g. \p. \q. p \union q) (\f. \g. \p. \q. p \union q) (\f. \n. \p. p \ {n})

fresh : (Nat -> o) -> Nat
fresh := \p. mu x. ~p x

subFormula : Formula -> (Nat -> Term) -> Formula
subFormula := FormulaR_((Nat -> Term) -> Formula)
   (\t. \s. \l. equal (subTerm t l) (subTerm s l))
   (\l. falsum)
   (\f. \g. \r. \s. \l. conj (r l) (s l))
   (\f. \g. \r. \s. \l. impl (r l) (s l))
   (\f. \n. \r. \l. (\z. all z (r (\m. if m = n then var z else l m))) (fresh (BigUnion {freeVarTerm (l i) | i <- freeVarFormula f})))

// Type definition
Theory := Formula -> o

// Close a set of formulas under universal generalization.
gen :: (Formula -> o) -> Theory
gen := \q. \f. forall p : Formula -> o. (q c= p /\ (forall n \in NatSet. forall g : Formula. p g => p (all n g))) => p f

// Logical Axioms for syntactic formulas
LA : Theory
LA := gen (\f. (exists a \in FormulaSet. exists b \in FormulaSet. f = impl a (impl b a)) \/
               (exists a \in FormulaSet. exists b \in FormulaSet. exists c \in FormulaSet. f = impl (impl a (impl b c)) (impl (impl a b) (impl a c))) \/
               (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (conj a b) a) \/
               (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (conj a b) b) \/
               (exists a \in FormulaSet. exists b \in FormulaSet. f = impl a (impl b (conj a b))) \/
               (exists a \in FormulaSet. f = impl falsum a) \/
               (exists a \in FormulaSet. exists b \in FormulaSet. f = impl (impl (impl a b) a) a) \/
               (exists n \in NatSet. exists. a \in FormulaSet. exists t \in TermSet. f = impl (all n a) (subFormula a (at n t))) \/
               (exists n \in NatSet. exists. a \in FormulaSet. exists b \in FormulaSet. f = impl (all n (impl a b)) (impl (all n a) (all n b))) \/
               (exists n \in NatSet. exists. a \in FormulaSet. n \notin freeVarFormula a /\ f = impl a (all n a)) \/
               (exists n \in NatSet. f = equal (var n) (var n)) \/
               (exists n \in NatSet. exists m \in NatSet. exists z \in NatSet. exists a \in FormulaSet.
                     f = impl (equal (var n) (var m)) (impl (subFormula a (at z (var n))) (subFormula a (at z (var m))))))


// Close a set of formulas under modus ponens
proves : Theory -> Formula -> o
proves := \t. \f. forall p : Formula -> o. (t c= p /\ LA c= p /\ (forall f : Formula. forall g : Formula. (p f /\ p (impl f g)) => p g)) => p f

// Section Goedel

// Axioms of Robinson Arithmetic
RA : Theory
RA := \f. f = all 0 (not (equal (succ (var 0)) zero)) \/
          f = all 0 (all 1 (impl (equal (succ (var 0)) (succ (var 1))) (equal (var 0) (var 1)))) \/
          f = all 0 (or (equal (var 0) zero) (some 1 (equal (var 0) (succ (var 1)))))
          f = all 0 (equal (plus (var 0) zero) (var 0)) \/
          f = all 0 (all 1 (equal (plus (var 0) (succ (var 1))) (succ (plus (var 0) (var 1))))) \/
          f = all 0 (equal (mult (var 0) zero) zero) \/
          f = all 0 (all 1 (equal (mult (var 0) (succ (var 1))) (plus (mult (var 0) (var 1)) (var 0))))

natToTerm : Nat -> Term
natToTerm := R (\x. succ) zero

codeTerm : Term -> Nat
codeTerm : TermR_(Nat) (\n. 1 + 4*n) 0 (\t. \n. 1 + 4*n + 1) (\t. \s. \n. \m. 1 + 4*(pair n m) + 2) (\t. \s. \n. \m. 1 + 4*(pair n m) + 3)

codeFormula : Formula -> Nat
codeFormula : FormulaR_(Nat) (\t. \s. 1 + 4*(pair (codeTerm t) (codeTerm s))) 0 (\f. \g. \n. \m. 1 + 4*(pair n m) + 1) (\f. \g. \n. \m. 1 + 4*(pair n m) + 2) (\f. \n. \m. 1 + 4*(pair n m) + 3)

quotF : Formula -> Term
quotF := \f. natToTerm (codeFormula f)

expressableF : (Formula -> o) -> Theory -> o
expressableF := \p. \t. exists n \in NatSet. exists f \in FormulaSet.
   {n} = freeVarFormula f /\
   (forall m \in p => proves t (subFormula f (at n (quotF m)))) /\
   (forall m \in Formula. m \notin p => proves t (not (subFormula f (at n (quotF m)))))

// Statement of the diagona[l] lemma: https://en.wikipedia.org/wiki/Diagonal_lemma
diagonal_lemma : o
diagonal_lemma := forall t : Theory. (t c= FormulaSet /\ RA c= proves t) =>
                    forall n \in natSet. forall f \in FormulaSet. exists g \in FormulaSet.
		      freeVarFormula g = freeVarFormula f \ {n} /\
		         (proves t (iff g (subFormula f (at n (quotF g)))))

// Statement of essential incompleteness of (Robins[ ]on) arithmetic
EssentialIncompletenessOfRA : o
EssentialIncompletenessOfRA := forall t : Theory. (t c= FormulaSet /\ RA c= proves t /\ expressibleF t t) =>
                                 exists g \in FormulaSet. freeVarFormula g = empty /\
                                   ((proves t g \/ proves t (not g)) => proves t = FormulaSet)

________________________________________________________________________________





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.