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)
________________________________________________________________________________
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
