0
$\begingroup$

Is there a formalization, which from a proof that a system includes enough arithmetic extracts an arithmetic sentence in the language of PA, which is not provable in the given system? Imagine the following, given representation of FOL+axioms of ZF, in let's say Coq/Agda, I can run the proof to obtain the independent sentence, of course after proving the assumptions on there existing enough arithmetic in ZF. Is there such a variant for Coq in Coq?

$\endgroup$
3
  • $\begingroup$ Re: "Is there a formalization, which from a proof that a system includes enough arithmetic extracts an arithmetic sentence in the language of PA, which is not provable in the given system?," the answer is very much yes - $Con(T)$ (or the original Godel sentence for $T$) is unprovable in $T$ whenever $T$ is consistent and interprets enough arithmetic, and producing $Con(T)$ from (a presentation of) $T$ is straightforward. We can even do better: via Rosser's trick we can write a sentence $R(T)$ which is independent of $T$ (there are consistent strong theories proving their own inconsistency) $\endgroup$ Commented Oct 10, 2019 at 18:14
  • $\begingroup$ But I'm not sure what "Is there such a variant for Coq in Coq?" means. $\endgroup$ Commented Oct 10, 2019 at 18:14
  • $\begingroup$ I realize I didnt reply for ages, I forgot about this question, I want to extract an unprovable sentence from within Coq for some formalization close to Coq. $\endgroup$
    – Ilk
    Commented Mar 5, 2020 at 15:42

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.