The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

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:

http://andreipopescu.uk/pdf/compr_IsabelleHOL_cons.pdf, p. 2

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

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

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, 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, p. 12

Regards,

Ken

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

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:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html

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)

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.

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]

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

--
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.