<p>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?</p>

CC BY-SA 4.0
2019-10-10T18:14:01.250Z
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)
Noah Schweber
CC BY-SA 4.0
2019-10-10T18:14:22.243Z
But I'm not sure what "Is there such a variant for Coq in Coq?" means.
Noah Schweber
CC BY-SA 4.0
2020-03-05T15:42:20.543Z
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.
Ilk
<reference-request><fl.formal-languages>
Incompleteness and term extraction
Ilk
# Incompleteness and term extraction

(Asked by: username_0 on 2019-10-09)

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?

**Tags:** reference-request, fl.formal-languages

> **Comments:**
> **username_1**: 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)  
> **username_1**: But I'm not sure what "Is there such a variant for Coq in Coq?" means.  
> **username_0**: 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.  

---

## 0 answers

