The Coq mailing list

[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

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

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?

Sent from my iPhone

On Aug 4, 2018, at 7:19 PM, Jan Burse <bursejan AT gmail.com> wrote:

Corr.: Typo
With or without proof assistent, you will still have theories T

Am Sonntag, 5. August 2018 01:13:47 UTC+2 schrieb Jan Burse:

Incompletness is not in contradiction of using a proof assistant.
With our without proof assistent, you will still have theories T
and theorems A, such that neither:

    T |- A

    - nor -

     T |- ~A

Most simple example of such a theory and theorem: T=empty
theory, and A=propositional variable p. Then you have neither:

      {} |- p

    - nor -
  
      {} |- ~p

Am Sonntag, 5. August 2018 00:59:56 UTC+2 schrieb José Manuel Rodriguez Caballero:

Petrus Abaelardus said: "The beginning of wisdom is found in doubting; by doubting we come to the question, and by seeking we may come upon the truth". 

This year, I hear several times, from different people, the following statements: "in community X we assume that proof assistant Y is consistent and everything that we mechanize in this proof assistant is considered true, if you don't believe in that, goodbye".

I like proof assistants for doing traditional mathematics (number theory, algebraic geometry, partial differential equations, measure theory, etc.), but I am not sure that some proof assistants could be used for foundations of mathematics, because they required their own foundation and if someone assume that "anything that my proof assistant verifies is true" the foundations of mathematics thinking dies.

 I'm almost convinced that MetaMath can be used for the foundation of mathematics, but I'm not so sure that Coq could be used for the same purpose. So, I would like to recommend people interested in this subject to read the following paper, from the point of view of the foundations of mathematics, and to reply if they are convinced of this proof of the "Essential Incompleteness of Arithmetic": https://arxiv.org/abs/cs/0505034

I'm not making a claim, I'm just sharing my doubts with people with more experience than me in foundations of mathematics.

Kind Regards,

Jose M.

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

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