Skip to main content
MathOverflow

Return to Answer

added year of reference
Source Link
user44143
user44143

You can ask the same question about arithmetical theories, and the answer may be illuminating.

For most arithmetical examples, when we can establish provability non-constructively, we can also establish it constructively within a few years.

See Jeremy Avigad's 1998 talk on Semantic Methods in Proof Theory. That has examples like:

Theorem. $B\Sigma_{k+1}$ is $\Pi_{k+2}$-conservative over $I\Sigma_k$. Original proofs by Paris and Friedman (independently) were semantic. Sieg offered the first proof-theoretic proof.

He surveys semantic methods for establishing provability, and in every case he mentions a syntactic method to the same end.

The one contrary example I see in his talk is the Paris-Harrington statement, whose unprovability in PA is established only semantically.

So for arithmetical theories, it is rare and usually temporary for theorems to be shown provable only in a non-constructive metatheory. I don't have good data on whether the same pattern holds for geometric theories with topos-theoretic metatheories; perhaps others do, or perhaps it remains to be seen.

You can ask the same question about arithmetical theories, and the answer may be illuminating.

For most arithmetical examples, when we can establish provability non-constructively, we can also establish it constructively within a few years.

See Jeremy Avigad's talk on Semantic Methods in Proof Theory. That has examples like:

Theorem. $B\Sigma_{k+1}$ is $\Pi_{k+2}$-conservative over $I\Sigma_k$. Original proofs by Paris and Friedman (independently) were semantic. Sieg offered the first proof-theoretic proof.

He surveys semantic methods for establishing provability, and in every case he mentions a syntactic method to the same end.

The one contrary example I see in his talk is the Paris-Harrington statement, whose unprovability in PA is established only semantically.

So for arithmetical theories, it is rare and usually temporary for theorems to be shown provable only in a non-constructive metatheory. I don't have good data on whether the same pattern holds for geometric theories with topos-theoretic metatheories; perhaps others do, or perhaps it remains to be seen.

You can ask the same question about arithmetical theories, and the answer may be illuminating.

For most arithmetical examples, when we can establish provability non-constructively, we can also establish it constructively within a few years.

See Jeremy Avigad's 1998 talk on Semantic Methods in Proof Theory. That has examples like:

Theorem. $B\Sigma_{k+1}$ is $\Pi_{k+2}$-conservative over $I\Sigma_k$. Original proofs by Paris and Friedman (independently) were semantic. Sieg offered the first proof-theoretic proof.

He surveys semantic methods for establishing provability, and in every case he mentions a syntactic method to the same end.

The one contrary example I see in his talk is the Paris-Harrington statement, whose unprovability in PA is established only semantically.

So for arithmetical theories, it is rare and usually temporary for theorems to be shown provable only in a non-constructive metatheory. I don't have good data on whether the same pattern holds for geometric theories with topos-theoretic metatheories; perhaps others do, or perhaps it remains to be seen.

Source Link
user44143
user44143

You can ask the same question about arithmetical theories, and the answer may be illuminating.

For most arithmetical examples, when we can establish provability non-constructively, we can also establish it constructively within a few years.

See Jeremy Avigad's talk on Semantic Methods in Proof Theory. That has examples like:

Theorem. $B\Sigma_{k+1}$ is $\Pi_{k+2}$-conservative over $I\Sigma_k$. Original proofs by Paris and Friedman (independently) were semantic. Sieg offered the first proof-theoretic proof.

He surveys semantic methods for establishing provability, and in every case he mentions a syntactic method to the same end.

The one contrary example I see in his talk is the Paris-Harrington statement, whose unprovability in PA is established only semantically.

So for arithmetical theories, it is rare and usually temporary for theorems to be shown provable only in a non-constructive metatheory. I don't have good data on whether the same pattern holds for geometric theories with topos-theoretic metatheories; perhaps others do, or perhaps it remains to be seen.