Ken Kubota
2018-08-06 10:51:52 UTC
Dear José,
But since the prerequisites used in Goedel's proof are rather simple (basic number theory
and primitive recursive functions, as far as I can recall) the proof in Coq shouldn't be affected
if one would modify the Coq foundations in order to remove any hypothetical inconsistency in Coq.
Moreover, Russell's (Russell O'Connor's) proof in Coq is quite handmade with little automation,
which means that the chance of having taken advantage of a hypothetical inconsistency of Coq
is quite low, as it is just the formalization of a proof already presented on paper.
(Your argument would be stronger for Larry Paulson's formalization of Goedel's proof in Isabelle,
where automation is more powerful than in Coq, I believe).
So while from a very theoretical point of view a proof in a possibly inconsistent system is
of less reliability, from a practical point of view this is of little significance in this case.
Even the recent inconsistency in Isabelle/HOL was discovered only be directly exploiting
the weakness using an expression combining both self-reference and negation:
http://andreipopescu.uk/pdf/compr_IsabelleHOL_cons.pdf <http://andreipopescu.uk/pdf/compr_IsabelleHOL_cons.pdf>, p. 2
http://owlofminerva.net/kubota/r0-faq/ <http://owlofminerva.net/kubota/r0-faq/>
Commenting on the ongoing discussion in the Metamath group, I share the view that ZF/ZFC
is insufficient. The point is that ZFC is not the result of systematically trying to solve the problem of
Russell's (Bertrand Russell's) antinomy, which is caused by type violations as discussed here:
The two characteristics of an antinomy: self-reference and negation
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html>
In order to avoid the antinomy, the adequate solution is to make the restrictions explicit, but not
in the form of hypotheses (conditionals), but with the syntactic means of the language,
i.e., shaping the grammar of the formal language properly.
This is what Bertrand Russell did with the invention of type theory: drawing a clear line between
formulae that should be expressible, and those that shouldn't (since they cause inconsistency),
by preserving the dependencies within the formal language (the syntax).
The white-list approach of ZFC is clearly arbitrary (covering most mathematics used at that time)
and not a systematic approach.
Freek has written a paper "Is ZF a hack?":
http://www.cs.ru.nl/F.Wiedijk/zfc-etc/zfc-etc.pdf <http://www.cs.ru.nl/F.Wiedijk/zfc-etc/zfc-etc.pdf>
I didn't have the chance yet to read it completely, but I definitely agree with the essay's title.
This to some degree coincides with Zermelo's own view:
"Under these circumstances there is at this point nothing left for us to do but to proceed in the
opposite direction and, starting from set theory as it is historically given [...]."
[Zermelo, 1967, p. 200, emphasis as in the original, first published in German in 1908]
http://www.owlofminerva.net/files/fom.pdf <http://www.owlofminerva.net/files/fom.pdf>, p. 13
(Note the formulation "historically given".)
Heijenoort expressed it similarly:
"One response to the challenge was Russellâs theory of types [...]. Another, coming at almost
the same time, was Zermeloâs axiomatization of set theory. The two responses are extremely different;
the former is a far-reaching theory of great significance for logic and even ontology, while the latter is
an immediate answer to the pressing needs of the working mathematician.â [Heijenoort, 1967c, p. 199]
http://www.owlofminerva.net/files/fom.pdf <http://www.owlofminerva.net/files/fom.pdf>, p. 12
Regards,
Ken
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>
Could be possible - in principle - that Coq is inconsistent whereas Q0 is consistent?
This is, of course, in principle possible.But since the prerequisites used in Goedel's proof are rather simple (basic number theory
and primitive recursive functions, as far as I can recall) the proof in Coq shouldn't be affected
if one would modify the Coq foundations in order to remove any hypothetical inconsistency in Coq.
Moreover, Russell's (Russell O'Connor's) proof in Coq is quite handmade with little automation,
which means that the chance of having taken advantage of a hypothetical inconsistency of Coq
is quite low, as it is just the formalization of a proof already presented on paper.
(Your argument would be stronger for Larry Paulson's formalization of Goedel's proof in Isabelle,
where automation is more powerful than in Coq, I believe).
So while from a very theoretical point of view a proof in a possibly inconsistent system is
of less reliability, from a practical point of view this is of little significance in this case.
Even the recent inconsistency in Isabelle/HOL was discovered only be directly exploiting
the weakness using an expression combining both self-reference and negation:
http://andreipopescu.uk/pdf/compr_IsabelleHOL_cons.pdf <http://andreipopescu.uk/pdf/compr_IsabelleHOL_cons.pdf>, p. 2
http://owlofminerva.net/kubota/r0-faq/ <http://owlofminerva.net/kubota/r0-faq/>
Commenting on the ongoing discussion in the Metamath group, I share the view that ZF/ZFC
is insufficient. The point is that ZFC is not the result of systematically trying to solve the problem of
Russell's (Bertrand Russell's) antinomy, which is caused by type violations as discussed here:
The two characteristics of an antinomy: self-reference and negation
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html>
In order to avoid the antinomy, the adequate solution is to make the restrictions explicit, but not
in the form of hypotheses (conditionals), but with the syntactic means of the language,
i.e., shaping the grammar of the formal language properly.
This is what Bertrand Russell did with the invention of type theory: drawing a clear line between
formulae that should be expressible, and those that shouldn't (since they cause inconsistency),
by preserving the dependencies within the formal language (the syntax).
The white-list approach of ZFC is clearly arbitrary (covering most mathematics used at that time)
and not a systematic approach.
Freek has written a paper "Is ZF a hack?":
http://www.cs.ru.nl/F.Wiedijk/zfc-etc/zfc-etc.pdf <http://www.cs.ru.nl/F.Wiedijk/zfc-etc/zfc-etc.pdf>
I didn't have the chance yet to read it completely, but I definitely agree with the essay's title.
This to some degree coincides with Zermelo's own view:
"Under these circumstances there is at this point nothing left for us to do but to proceed in the
opposite direction and, starting from set theory as it is historically given [...]."
[Zermelo, 1967, p. 200, emphasis as in the original, first published in German in 1908]
http://www.owlofminerva.net/files/fom.pdf <http://www.owlofminerva.net/files/fom.pdf>, p. 13
(Note the formulation "historically given".)
Heijenoort expressed it similarly:
"One response to the challenge was Russellâs theory of types [...]. Another, coming at almost
the same time, was Zermeloâs axiomatization of set theory. The two responses are extremely different;
the former is a far-reaching theory of great significance for logic and even ontology, while the latter is
an immediate answer to the pressing needs of the working mathematician.â [Heijenoort, 1967c, p. 199]
http://www.owlofminerva.net/files/fom.pdf <http://www.owlofminerva.net/files/fom.pdf>, p. 12
Regards,
Ken
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>
Dear Ken,
Could be possible - in principle - that Coq is inconsistent whereas Q0 is consistent?
If this is true, then a proof in the incompleteness of arithmetic in Coq is not the same as such a proof in Q0.
Regards,
José M.
The prerequisites used in this proof are rather simple, such that it can be expressed in many other formal languages, too.
Russell was so kind and translated his proof into the language of Peter Andrewsâ logic Q0.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html>
// 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)
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html>
Jan's example provided below is slightly problematic, since he uses a simple propositional variable, which is not an arithmetic formula.
In particular, the formula that is neither provable nor refutable (g) doesnât have any free variables ("freeVarFormula g = empty").
See also the same condition "(forall v : nat, ~ In v (freeVarFormula LNT f))" in section 6.1 at https://arxiv.org/pdf/cs/0505034v2.pdf <https://arxiv.org/pdf/cs/0505034v2.pdf>.
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].
"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]
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html>
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
Visit this group at https://groups.google.com/group/metamath <https://groups.google.com/group/metamath>.
For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.
Could be possible - in principle - that Coq is inconsistent whereas Q0 is consistent?
If this is true, then a proof in the incompleteness of arithmetic in Coq is not the same as such a proof in Q0.
Regards,
José M.
I will formulate my question in a more concrete way: Is a metamath-proof of incompleteness of PA the same as a Coq-proof of the same result, from the point of view of foundations of mathematics?
Basically, yes.The prerequisites used in this proof are rather simple, such that it can be expressed in many other formal languages, too.
Russell was so kind and translated his proof into the language of Peter Andrewsâ logic Q0.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html>
// 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)
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html>
Jan's example provided below is slightly problematic, since he uses a simple propositional variable, which is not an arithmetic formula.
In particular, the formula that is neither provable nor refutable (g) doesnât have any free variables ("freeVarFormula g = empty").
See also the same condition "(forall v : nat, ~ In v (freeVarFormula LNT f))" in section 6.1 at https://arxiv.org/pdf/cs/0505034v2.pdf <https://arxiv.org/pdf/cs/0505034v2.pdf>.
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].
"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]
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html>
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
Visit this group at https://groups.google.com/group/metamath <https://groups.google.com/group/metamath>.
For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.