Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Russell O'Connor's proof in Q0; Axiomatic Set Theory (ZFC) vs. Type Theory; "Is ZF a hack?" – Re: [Metamath] [FOM] proof assistants and foundations of mathematics

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Russell O'Connor's proof in Q0; Axiomatic Set Theory (ZFC) vs. Type Theory; "Is ZF a hack?" – Re: [Metamath] [FOM] proof assistants and foundations of mathematics


Chronological Thread 
  • From: Ken Kubota <mail AT kenkubota.de>
  • To: metamath AT googlegroups.com, coq-club AT inria.fr
  • Cc: Russell O'Connor <roconnor AT theorem.ca>, "Prof. Peter B. Andrews" <andrews AT cmu.edu>, Andrei Popescu <A.Popescu AT mdx.ac.uk>, Ondřej Kunčar <kuncar AT in.tum.de>
  • Subject: [Coq-Club] Russell O'Connor's proof in Q0; Axiomatic Set Theory (ZFC) vs. Type Theory; "Is ZF a hack?" – Re: [Metamath] [FOM] proof assistants and foundations of mathematics
  • Date: Mon, 6 Aug 2018 12:51:52 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT kenkubota.de; spf=Pass smtp.mailfrom=mail AT kenkubota.de; spf=None smtp.helo=postmaster AT plasma2.jpberlin.de
  • Ironport-phdr: 9a23:Jm99gx9oH+mo+/9uRHKM819IXTAuvvDOBiVQ1KB+0useIJqq85mqBkHD//Il1AaPAd2Fraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HSbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyaM+dwfr7GfdMCW2VOQtpRWSJGAoO5dYQPDuwBNvtco4Tyo1YCqB2zDhSuCuzy0D9FnmP50qIn3eohEw7I0g8uH9wQvnrTt9j6LrseUeWvwanI0TnObfVb0ir95ojSdRAhpOmBU7dufsrX1EIhEh7FgU6XqYz5JTyey+MAs22B4OphUeKikG0npB93ojis28cjkY7Jhp4PxVze6Cp23p84KNulQ0B1Zt6kFYFftyCcN4ZuWMwiWW5puCckyrEcvp67ZicKxIwoxx7YbPyHfIyI7Qz5WOmNJjd4gWppd6+4hxaz60Sgzff8Vsas3FZQsypJiN/MtnQV2xzU5MmHTvx9/kmk2TaO0QDc9PtEIV4umqbBLZ4u3KIwmoIJvkTFAyD2glv5jK6OdkUj4uin9f/nban7ppOGKo90iRnyPbg0lcy6G+g3KBQBU3KG+eS/0rDo4E73QK1Sg/Ayj6XVqo3WKMAYq6KjHQNY0pov5wyiAzqpzNgUhX0KIVxfdB6ZgYXlJ0vCLfL8APulnVihnjZmyvbbNbP7GJrNNGLMkLL5cLZ99UFczA0zwMhH55JQEL4BO/fzVVXvuNDCDB85Kxe7zPj9CNV514MeX3iDDbKHP6/KsF+I4PwgI/WUaYIRpTrxMeUp6vrtgHMjh1MQfbWl0YEKZH23AvhqO0CZbmDtgtcFH2cKpA0+TOnyhV2HSzFTZnKyUrk/5j4lDoKmDprDSZuqgLydxii3BIBZaX5eBlCWDXjob5mEW+sLaC+KPsBhlSUEWaG9RI8lyBGhrxT3y6FnL+rR4i0Xr4jv1Nlz5+3JlBE97yZ4D8qH0zLFcmdvg2ldQjY32Lx480lw1l6G2LR4wOFeDsFZ/PhTUw03HZHbyON+Bt/oXR/ZZZGCT1P1f9O9HDtkTs4t28RcJAFyAdK/lguF0C2tDLsY0beMAds4taXEw3/sO5VAzW3b3vwhk0U+WZkIcmK8gbNn7E7cAInGl0jfnKGvMqsG2zPVs2KO0WOLtV1YAzJ3BKDIQXkab1fWhdv+4UzGQrC0Dqk/KU1KzsvGYqBNc5jiiUhMbPblItXXJWyryEmqAhPd5b6KJKn3cWIB1W2JDUEFlygQ8HCFKAI5Gi7nr2+IX28mLk7mf065qbo2k3i8VEJhilzTNhwz5/+O4hcQwMekZbYW17MAtj0mrmwoTlWw2dHLAd2crkxtcfcFOI9v0BJ8zWvc8jdFENm4Nak72gwdfgJ0oknpyxwxBogSyZF3/kNv9xJ7LOej6H0Edz6c2sqpaKXTI3L39Urpabbc10va0dDQ9qpdsPk=

Dear José,

  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:


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
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?":
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]
(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]


Regards,

Ken

____________________________________________________


Am 05.08.2018 um 21:13 schrieb José Manuel Rodriguez Caballero <josephcmac AT gmail.com>:

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.


2018-08-05 6:41 GMT-04:00 Ken Kubota <mail AT kenkubota.de>:
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.
The proof in Q0 is available online as attachment to the posting here:

Quote:
// 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)


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.

Quote:
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]

____________________________________________________


--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe AT googlegroups.com.
To post to this group, send email to metamath AT googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.



  • [Coq-Club] Russell O'Connor's proof in Q0; Axiomatic Set Theory (ZFC) vs. Type Theory; "Is ZF a hack?" – Re: [Metamath] [FOM] proof assistants and foundations of mathematics, Ken Kubota, 08/06/2018

Archive powered by MHonArc 2.6.18.

Top of Page