Are there any statements $phi$ where “$vdash phi$ or $vdash neg phi$” was shown nonconstructively?
up vote
0
down vote
favorite
I am wondering if there is an example of a statement $phi$ in the language of some formal system $T$ satisfying (1-4):
$phi$ was shown to not be independent of $T$ (i.e. it was proved that $T vdash phi$ or $T vdash neg phi$)- The proof in (1) was nonconstructive: it was initially (or still) unknown which of {$phi, neg phi$} was a theorem of $T$.
$phi$ was not clearly $Delta_0$ (any bounded statement like "there is no odd perfect number less than 10↑↑↑10" has a (possibly long) proof/disproof).
$phi$ was not part of some class of statements $C$ that were shown by some algorithm to be decidable. (For instance, any statement in Presburger arithmetic or ACF/RCF which we know to be decidable by a quantifier elimination algorithm).
$T$ is r.e.
logic examples-counterexamples proof-theory
asked Nov 16 at 19:58
Morgan Sinclaire
163
|
show 2 more comments
up vote
0
down vote
favorite
I am wondering if there is an example of a statement $phi$ in the language of some formal system $T$ satisfying (1-4):
$phi$ was shown to not be independent of $T$ (i.e. it was proved that $T vdash phi$ or $T vdash neg phi$)- The proof in (1) was nonconstructive: it was initially (or still) unknown which of {$phi, neg phi$} was a theorem of $T$.
$phi$ was not clearly $Delta_0$ (any bounded statement like "there is no odd perfect number less than 10↑↑↑10" has a (possibly long) proof/disproof).
$phi$ was not part of some class of statements $C$ that were shown by some algorithm to be decidable. (For instance, any statement in Presburger arithmetic or ACF/RCF which we know to be decidable by a quantifier elimination algorithm).
$T$ is r.e.
logic examples-counterexamples proof-theory
asked Nov 16 at 19:58
Morgan Sinclaire
163
1
As stated, the answer is yes and here's a rather silly example: Let $T$ be the theory of the constructible universe $L$ (in some fixed universe $V$ such that $T$ exists) and let $phi$ be Riemann's hypothesis. Since $T$ is complete, we have $T vdash phi$ or $T vdash neg phi$. But we don't yet know which one it is.
– Stefan Mesken
Nov 16 at 20:04
Yes, I thought I forgot a non-triviality condition: $T$ should be r.e. I think that fixes that class of examples?
– Morgan Sinclaire
Nov 16 at 20:35
1
Not really. We know that there is a finite subtheory $T'$ of $T$ that decides Riemann's hypothesis.
– Stefan Mesken
Nov 16 at 20:36
Yeah, but for that finite subtheory, we know exactly which way it decides RH. We want an example of a theory $T$ where we don't know which way $T$ decides $phi$, just that it does. Unless we have access to the theory of $L$ I don't see how to recursively enumerate any $T'$ as you've described it. Unless I'm misunderstanding?
– Morgan Sinclaire
Nov 16 at 20:56
The point is we don't know how $T'$ decides RH (only that it decides RH in the same way as $T$). And we do have access to $T$ and $T'$. The latter, being finite, is trivially r.e.
– Stefan Mesken
Nov 16 at 21:00
|
show 2 more comments
up vote
0
down vote
favorite
up vote
0
down vote
favorite
I am wondering if there is an example of a statement $phi$ in the language of some formal system $T$ satisfying (1-4):
$phi$ was shown to not be independent of $T$ (i.e. it was proved that $T vdash phi$ or $T vdash neg phi$)- The proof in (1) was nonconstructive: it was initially (or still) unknown which of {$phi, neg phi$} was a theorem of $T$.
$phi$ was not clearly $Delta_0$ (any bounded statement like "there is no odd perfect number less than 10↑↑↑10" has a (possibly long) proof/disproof).
$phi$ was not part of some class of statements $C$ that were shown by some algorithm to be decidable. (For instance, any statement in Presburger arithmetic or ACF/RCF which we know to be decidable by a quantifier elimination algorithm).
$T$ is r.e.
logic examples-counterexamples proof-theory
asked Nov 16 at 19:58
Morgan Sinclaire
163
I am wondering if there is an example of a statement $phi$ in the language of some formal system $T$ satisfying (1-4):
$phi$ was shown to not be independent of $T$ (i.e. it was proved that $T vdash phi$ or $T vdash neg phi$)- The proof in (1) was nonconstructive: it was initially (or still) unknown which of {$phi, neg phi$} was a theorem of $T$.
$phi$ was not clearly $Delta_0$ (any bounded statement like "there is no odd perfect number less than 10↑↑↑10" has a (possibly long) proof/disproof).
$phi$ was not part of some class of statements $C$ that were shown by some algorithm to be decidable. (For instance, any statement in Presburger arithmetic or ACF/RCF which we know to be decidable by a quantifier elimination algorithm).
$T$ is r.e.
logic examples-counterexamples proof-theory
logic examples-counterexamples proof-theory
asked Nov 16 at 19:58
Morgan Sinclaire
163
asked Nov 16 at 19:58
Morgan Sinclaire
163
edited Nov 16 at 22:25
asked Nov 16 at 19:58
Morgan Sinclaire
163
asked Nov 16 at 19:58
Morgan Sinclaire
163
asked Nov 16 at 19:58
Morgan Sinclaire
163
163
1
As stated, the answer is yes and here's a rather silly example: Let $T$ be the theory of the constructible universe $L$ (in some fixed universe $V$ such that $T$ exists) and let $phi$ be Riemann's hypothesis. Since $T$ is complete, we have $T vdash phi$ or $T vdash neg phi$. But we don't yet know which one it is.
– Stefan Mesken
Nov 16 at 20:04
Yes, I thought I forgot a non-triviality condition: $T$ should be r.e. I think that fixes that class of examples?
– Morgan Sinclaire
Nov 16 at 20:35
1
Not really. We know that there is a finite subtheory $T'$ of $T$ that decides Riemann's hypothesis.
– Stefan Mesken
Nov 16 at 20:36
Yeah, but for that finite subtheory, we know exactly which way it decides RH. We want an example of a theory $T$ where we don't know which way $T$ decides $phi$, just that it does. Unless we have access to the theory of $L$ I don't see how to recursively enumerate any $T'$ as you've described it. Unless I'm misunderstanding?
– Morgan Sinclaire
Nov 16 at 20:56
The point is we don't know how $T'$ decides RH (only that it decides RH in the same way as $T$). And we do have access to $T$ and $T'$. The latter, being finite, is trivially r.e.
– Stefan Mesken
Nov 16 at 21:00
|
show 2 more comments
1
As stated, the answer is yes and here's a rather silly example: Let $T$ be the theory of the constructible universe $L$ (in some fixed universe $V$ such that $T$ exists) and let $phi$ be Riemann's hypothesis. Since $T$ is complete, we have $T vdash phi$ or $T vdash neg phi$. But we don't yet know which one it is.
– Stefan Mesken
Nov 16 at 20:04
Yes, I thought I forgot a non-triviality condition: $T$ should be r.e. I think that fixes that class of examples?
– Morgan Sinclaire
Nov 16 at 20:35
1
Not really. We know that there is a finite subtheory $T'$ of $T$ that decides Riemann's hypothesis.
– Stefan Mesken
Nov 16 at 20:36
Yeah, but for that finite subtheory, we know exactly which way it decides RH. We want an example of a theory $T$ where we don't know which way $T$ decides $phi$, just that it does. Unless we have access to the theory of $L$ I don't see how to recursively enumerate any $T'$ as you've described it. Unless I'm misunderstanding?
– Morgan Sinclaire
Nov 16 at 20:56
The point is we don't know how $T'$ decides RH (only that it decides RH in the same way as $T$). And we do have access to $T$ and $T'$. The latter, being finite, is trivially r.e.
– Stefan Mesken
Nov 16 at 21:00
1
1
As stated, the answer is yes and here's a rather silly example: Let $T$ be the theory of the constructible universe $L$ (in some fixed universe $V$ such that $T$ exists) and let $phi$ be Riemann's hypothesis. Since $T$ is complete, we have $T vdash phi$ or $T vdash neg phi$. But we don't yet know which one it is.
– Stefan Mesken
Nov 16 at 20:04
As stated, the answer is yes and here's a rather silly example: Let $T$ be the theory of the constructible universe $L$ (in some fixed universe $V$ such that $T$ exists) and let $phi$ be Riemann's hypothesis. Since $T$ is complete, we have $T vdash phi$ or $T vdash neg phi$. But we don't yet know which one it is.
– Stefan Mesken
Nov 16 at 20:04
Yes, I thought I forgot a non-triviality condition: $T$ should be r.e. I think that fixes that class of examples?
– Morgan Sinclaire
Nov 16 at 20:35
Yes, I thought I forgot a non-triviality condition: $T$ should be r.e. I think that fixes that class of examples?
– Morgan Sinclaire
Nov 16 at 20:35
1
1
Not really. We know that there is a finite subtheory $T'$ of $T$ that decides Riemann's hypothesis.
– Stefan Mesken
Nov 16 at 20:36
Not really. We know that there is a finite subtheory $T'$ of $T$ that decides Riemann's hypothesis.
– Stefan Mesken
Nov 16 at 20:36
Yeah, but for that finite subtheory, we know exactly which way it decides RH. We want an example of a theory $T$ where we don't know which way $T$ decides $phi$, just that it does. Unless we have access to the theory of $L$ I don't see how to recursively enumerate any $T'$ as you've described it. Unless I'm misunderstanding?
– Morgan Sinclaire
Nov 16 at 20:56
Yeah, but for that finite subtheory, we know exactly which way it decides RH. We want an example of a theory $T$ where we don't know which way $T$ decides $phi$, just that it does. Unless we have access to the theory of $L$ I don't see how to recursively enumerate any $T'$ as you've described it. Unless I'm misunderstanding?
– Morgan Sinclaire
Nov 16 at 20:56
The point is we don't know how $T'$ decides RH (only that it decides RH in the same way as $T$). And we do have access to $T$ and $T'$. The latter, being finite, is trivially r.e.
– Stefan Mesken
Nov 16 at 21:00
The point is we don't know how $T'$ decides RH (only that it decides RH in the same way as $T$). And we do have access to $T$ and $T'$. The latter, being finite, is trivially r.e.
– Stefan Mesken
Nov 16 at 21:00
|
show 2 more comments
active
oldest
votes
active
oldest
votes
active
oldest
votes
active
oldest
votes
active
oldest
votes
draft saved
draft discarded
draft saved
draft discarded
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3001580%2fare-there-any-statements-phi-where-vdash-phi-or-vdash-neg-phi-was%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
1
As stated, the answer is yes and here's a rather silly example: Let $T$ be the theory of the constructible universe $L$ (in some fixed universe $V$ such that $T$ exists) and let $phi$ be Riemann's hypothesis. Since $T$ is complete, we have $T vdash phi$ or $T vdash neg phi$. But we don't yet know which one it is.
– Stefan Mesken
Nov 16 at 20:04
Yes, I thought I forgot a non-triviality condition: $T$ should be r.e. I think that fixes that class of examples?
– Morgan Sinclaire
Nov 16 at 20:35
1
Not really. We know that there is a finite subtheory $T'$ of $T$ that decides Riemann's hypothesis.
– Stefan Mesken
Nov 16 at 20:36
Yeah, but for that finite subtheory, we know exactly which way it decides RH. We want an example of a theory $T$ where we don't know which way $T$ decides $phi$, just that it does. Unless we have access to the theory of $L$ I don't see how to recursively enumerate any $T'$ as you've described it. Unless I'm misunderstanding?
– Morgan Sinclaire
Nov 16 at 20:56
The point is we don't know how $T'$ decides RH (only that it decides RH in the same way as $T$). And we do have access to $T$ and $T'$. The latter, being finite, is trivially r.e.
– Stefan Mesken
Nov 16 at 21:00