Ordering between formal theories by provability of consistency
I am studying proof theory with Girard's monograph from '87 ('proof theory and logical complexity').
1.5.6. is an exercise called 'ordering between theories'.
It reads as follows:
" (i) Let $textbf{G}$ be the set of all primitive recursive extensions of $textbf{EA}$ containing $textbf{PRA}$; define the following relation of $textbf{G}$:
$$ textbf{T} < textbf{U} $$
if and only if $$
textbf{U} vdash (Con(textbf{T})) $$
and show that < is irreflexive and transitive: < is a strict order.
(ii) Is it possible to have $textbf{T}, textbf{U} in textbf{G},textbf{T} vdash (Con(textbf{U})) ,textbf{U} vdash (Con(textbf{T})) $?
(iii) If $ textbf{T} < textbf{U} $ and $textbf{T} vdash A$, with $A$ a closed $Pi^0_1$ -formula, show that $textbf{U} vdash A$."
I think (ii) is quite obviously impossible, since then by transitivity we would have a theory proving its own consistency, which is impossible by the second incompleteness theorem.
But I don't know how to deal with the transitivity from (i) or how to deal with (iii).
Thanks,
Ettore
logic proof-theory incompleteness meta-math
asked Dec 6 at 11:13
Ettore
798
|
show 8 more comments
I am studying proof theory with Girard's monograph from '87 ('proof theory and logical complexity').
1.5.6. is an exercise called 'ordering between theories'.
It reads as follows:
" (i) Let $textbf{G}$ be the set of all primitive recursive extensions of $textbf{EA}$ containing $textbf{PRA}$; define the following relation of $textbf{G}$:
$$ textbf{T} < textbf{U} $$
if and only if $$
textbf{U} vdash (Con(textbf{T})) $$
and show that < is irreflexive and transitive: < is a strict order.
(ii) Is it possible to have $textbf{T}, textbf{U} in textbf{G},textbf{T} vdash (Con(textbf{U})) ,textbf{U} vdash (Con(textbf{T})) $?
(iii) If $ textbf{T} < textbf{U} $ and $textbf{T} vdash A$, with $A$ a closed $Pi^0_1$ -formula, show that $textbf{U} vdash A$."
I think (ii) is quite obviously impossible, since then by transitivity we would have a theory proving its own consistency, which is impossible by the second incompleteness theorem.
But I don't know how to deal with the transitivity from (i) or how to deal with (iii).
Thanks,
Ettore
logic proof-theory incompleteness meta-math
asked Dec 6 at 11:13
Ettore
798
1
Here is a hint that may help with transitivity ($W < T$ and $T < U$ implies $W < U$). We are assuming that these theories include PRA. So, for example, if $lnot text{Con}(W)$ then every one of these theories proves $lnot text{Con}(W)$. Remember $text{Con}(W)$ is $lnot ulcorner W vdash 0 = 1urcorner$. Moreover, if $W vdash 0 = 1$ then $U vdash ulcorner T vdash ulcorner W vdash 0 = 1urcorner urcorner $. This is because there is a primitive recursive function that takes a $W$ derivation of $0 = 1$ to a $T$ derivation of $ulcorner W vdash 0 = 1urcorner$.
– Carl Mummert
Dec 6 at 11:59
1
I should have written $T < W$ and $U < T$ implies $U <W$ to match the rest of my comment.
– Carl Mummert
Dec 6 at 14:43
1
Con(W) is a $Pi^0_1$ statement, but you are circling around the right idea. If $lnot text{Con}(U)$ then $T$ would prove $lnot text{Con}(U)$. What we want is the formalization of that: $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$.
– Carl Mummert
Dec 6 at 19:22
1
I was imagining a proof by contradiction in $W$ - show that, within $W$, $lnot text{Con}(U)$ leads to a contradiction, because $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$, and also $T > U$ leads to $W vdash ulcorner T vdash text{Con}(U)urcorner$ , and from $ulcorner T vdash text{Con}(U)urcorner$ and $ulcorner T vdash lnot text{Con}(U)$, $W$ can prove $lnot text{Con}(T)$.
– Carl Mummert
Dec 7 at 2:25
1
I think it will be a similar argument - $lnot A$ is $Sigma^0_1$, so $U vdash lnot A to ulcorner T vdash lnot Aurcorner$. If you like, you would be welcome to write an answer in the answer box below (rather in the question box) to record it for others.
– Carl Mummert
Dec 7 at 12:40
|
show 8 more comments
I am studying proof theory with Girard's monograph from '87 ('proof theory and logical complexity').
1.5.6. is an exercise called 'ordering between theories'.
It reads as follows:
" (i) Let $textbf{G}$ be the set of all primitive recursive extensions of $textbf{EA}$ containing $textbf{PRA}$; define the following relation of $textbf{G}$:
$$ textbf{T} < textbf{U} $$
if and only if $$
textbf{U} vdash (Con(textbf{T})) $$
and show that < is irreflexive and transitive: < is a strict order.
(ii) Is it possible to have $textbf{T}, textbf{U} in textbf{G},textbf{T} vdash (Con(textbf{U})) ,textbf{U} vdash (Con(textbf{T})) $?
(iii) If $ textbf{T} < textbf{U} $ and $textbf{T} vdash A$, with $A$ a closed $Pi^0_1$ -formula, show that $textbf{U} vdash A$."
I think (ii) is quite obviously impossible, since then by transitivity we would have a theory proving its own consistency, which is impossible by the second incompleteness theorem.
But I don't know how to deal with the transitivity from (i) or how to deal with (iii).
Thanks,
Ettore
logic proof-theory incompleteness meta-math
asked Dec 6 at 11:13
Ettore
798
I am studying proof theory with Girard's monograph from '87 ('proof theory and logical complexity').
1.5.6. is an exercise called 'ordering between theories'.
It reads as follows:
" (i) Let $textbf{G}$ be the set of all primitive recursive extensions of $textbf{EA}$ containing $textbf{PRA}$; define the following relation of $textbf{G}$:
$$ textbf{T} < textbf{U} $$
if and only if $$
textbf{U} vdash (Con(textbf{T})) $$
and show that < is irreflexive and transitive: < is a strict order.
(ii) Is it possible to have $textbf{T}, textbf{U} in textbf{G},textbf{T} vdash (Con(textbf{U})) ,textbf{U} vdash (Con(textbf{T})) $?
(iii) If $ textbf{T} < textbf{U} $ and $textbf{T} vdash A$, with $A$ a closed $Pi^0_1$ -formula, show that $textbf{U} vdash A$."
I think (ii) is quite obviously impossible, since then by transitivity we would have a theory proving its own consistency, which is impossible by the second incompleteness theorem.
But I don't know how to deal with the transitivity from (i) or how to deal with (iii).
Thanks,
Ettore
logic proof-theory incompleteness meta-math
logic proof-theory incompleteness meta-math
asked Dec 6 at 11:13
Ettore
798
asked Dec 6 at 11:13
Ettore
798
edited Dec 9 at 10:43
asked Dec 6 at 11:13
Ettore
798
asked Dec 6 at 11:13
Ettore
798
asked Dec 6 at 11:13
Ettore
798
798
1
Here is a hint that may help with transitivity ($W < T$ and $T < U$ implies $W < U$). We are assuming that these theories include PRA. So, for example, if $lnot text{Con}(W)$ then every one of these theories proves $lnot text{Con}(W)$. Remember $text{Con}(W)$ is $lnot ulcorner W vdash 0 = 1urcorner$. Moreover, if $W vdash 0 = 1$ then $U vdash ulcorner T vdash ulcorner W vdash 0 = 1urcorner urcorner $. This is because there is a primitive recursive function that takes a $W$ derivation of $0 = 1$ to a $T$ derivation of $ulcorner W vdash 0 = 1urcorner$.
– Carl Mummert
Dec 6 at 11:59
1
I should have written $T < W$ and $U < T$ implies $U <W$ to match the rest of my comment.
– Carl Mummert
Dec 6 at 14:43
1
Con(W) is a $Pi^0_1$ statement, but you are circling around the right idea. If $lnot text{Con}(U)$ then $T$ would prove $lnot text{Con}(U)$. What we want is the formalization of that: $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$.
– Carl Mummert
Dec 6 at 19:22
1
I was imagining a proof by contradiction in $W$ - show that, within $W$, $lnot text{Con}(U)$ leads to a contradiction, because $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$, and also $T > U$ leads to $W vdash ulcorner T vdash text{Con}(U)urcorner$ , and from $ulcorner T vdash text{Con}(U)urcorner$ and $ulcorner T vdash lnot text{Con}(U)$, $W$ can prove $lnot text{Con}(T)$.
– Carl Mummert
Dec 7 at 2:25
1
I think it will be a similar argument - $lnot A$ is $Sigma^0_1$, so $U vdash lnot A to ulcorner T vdash lnot Aurcorner$. If you like, you would be welcome to write an answer in the answer box below (rather in the question box) to record it for others.
– Carl Mummert
Dec 7 at 12:40
|
show 8 more comments
1
Here is a hint that may help with transitivity ($W < T$ and $T < U$ implies $W < U$). We are assuming that these theories include PRA. So, for example, if $lnot text{Con}(W)$ then every one of these theories proves $lnot text{Con}(W)$. Remember $text{Con}(W)$ is $lnot ulcorner W vdash 0 = 1urcorner$. Moreover, if $W vdash 0 = 1$ then $U vdash ulcorner T vdash ulcorner W vdash 0 = 1urcorner urcorner $. This is because there is a primitive recursive function that takes a $W$ derivation of $0 = 1$ to a $T$ derivation of $ulcorner W vdash 0 = 1urcorner$.
– Carl Mummert
Dec 6 at 11:59
1
I should have written $T < W$ and $U < T$ implies $U <W$ to match the rest of my comment.
– Carl Mummert
Dec 6 at 14:43
1
Con(W) is a $Pi^0_1$ statement, but you are circling around the right idea. If $lnot text{Con}(U)$ then $T$ would prove $lnot text{Con}(U)$. What we want is the formalization of that: $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$.
– Carl Mummert
Dec 6 at 19:22
1
I was imagining a proof by contradiction in $W$ - show that, within $W$, $lnot text{Con}(U)$ leads to a contradiction, because $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$, and also $T > U$ leads to $W vdash ulcorner T vdash text{Con}(U)urcorner$ , and from $ulcorner T vdash text{Con}(U)urcorner$ and $ulcorner T vdash lnot text{Con}(U)$, $W$ can prove $lnot text{Con}(T)$.
– Carl Mummert
Dec 7 at 2:25
1
I think it will be a similar argument - $lnot A$ is $Sigma^0_1$, so $U vdash lnot A to ulcorner T vdash lnot Aurcorner$. If you like, you would be welcome to write an answer in the answer box below (rather in the question box) to record it for others.
– Carl Mummert
Dec 7 at 12:40
1
1
Here is a hint that may help with transitivity ($W < T$ and $T < U$ implies $W < U$). We are assuming that these theories include PRA. So, for example, if $lnot text{Con}(W)$ then every one of these theories proves $lnot text{Con}(W)$. Remember $text{Con}(W)$ is $lnot ulcorner W vdash 0 = 1urcorner$. Moreover, if $W vdash 0 = 1$ then $U vdash ulcorner T vdash ulcorner W vdash 0 = 1urcorner urcorner $. This is because there is a primitive recursive function that takes a $W$ derivation of $0 = 1$ to a $T$ derivation of $ulcorner W vdash 0 = 1urcorner$.
– Carl Mummert
Dec 6 at 11:59
Here is a hint that may help with transitivity ($W < T$ and $T < U$ implies $W < U$). We are assuming that these theories include PRA. So, for example, if $lnot text{Con}(W)$ then every one of these theories proves $lnot text{Con}(W)$. Remember $text{Con}(W)$ is $lnot ulcorner W vdash 0 = 1urcorner$. Moreover, if $W vdash 0 = 1$ then $U vdash ulcorner T vdash ulcorner W vdash 0 = 1urcorner urcorner $. This is because there is a primitive recursive function that takes a $W$ derivation of $0 = 1$ to a $T$ derivation of $ulcorner W vdash 0 = 1urcorner$.
– Carl Mummert
Dec 6 at 11:59
1
1
I should have written $T < W$ and $U < T$ implies $U <W$ to match the rest of my comment.
– Carl Mummert
Dec 6 at 14:43
I should have written $T < W$ and $U < T$ implies $U <W$ to match the rest of my comment.
– Carl Mummert
Dec 6 at 14:43
1
1
Con(W) is a $Pi^0_1$ statement, but you are circling around the right idea. If $lnot text{Con}(U)$ then $T$ would prove $lnot text{Con}(U)$. What we want is the formalization of that: $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$.
– Carl Mummert
Dec 6 at 19:22
Con(W) is a $Pi^0_1$ statement, but you are circling around the right idea. If $lnot text{Con}(U)$ then $T$ would prove $lnot text{Con}(U)$. What we want is the formalization of that: $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$.
– Carl Mummert
Dec 6 at 19:22
1
1
I was imagining a proof by contradiction in $W$ - show that, within $W$, $lnot text{Con}(U)$ leads to a contradiction, because $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$, and also $T > U$ leads to $W vdash ulcorner T vdash text{Con}(U)urcorner$ , and from $ulcorner T vdash text{Con}(U)urcorner$ and $ulcorner T vdash lnot text{Con}(U)$, $W$ can prove $lnot text{Con}(T)$.
– Carl Mummert
Dec 7 at 2:25
I was imagining a proof by contradiction in $W$ - show that, within $W$, $lnot text{Con}(U)$ leads to a contradiction, because $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$, and also $T > U$ leads to $W vdash ulcorner T vdash text{Con}(U)urcorner$ , and from $ulcorner T vdash text{Con}(U)urcorner$ and $ulcorner T vdash lnot text{Con}(U)$, $W$ can prove $lnot text{Con}(T)$.
– Carl Mummert
Dec 7 at 2:25
1
1
I think it will be a similar argument - $lnot A$ is $Sigma^0_1$, so $U vdash lnot A to ulcorner T vdash lnot Aurcorner$. If you like, you would be welcome to write an answer in the answer box below (rather in the question box) to record it for others.
– Carl Mummert
Dec 7 at 12:40
I think it will be a similar argument - $lnot A$ is $Sigma^0_1$, so $U vdash lnot A to ulcorner T vdash lnot Aurcorner$. If you like, you would be welcome to write an answer in the answer box below (rather in the question box) to record it for others.
– Carl Mummert
Dec 7 at 12:40
|
show 8 more comments
1 Answer
1
active
oldest
votes
$textbf{(Sketch of a) proof of transitivity (i):}$
We may suppose that $W$ is consistent, for if it is inconsistent it proves anything.
Assume $W vdash Thm_U(0=1)$ - we're after a contradiction $in$ $W$.
We have $W vdash Thm_U(0=1) rightarrow Thm_T(Thm_U(0=1))$.
This is an instance of theorem 1.4.7., that is the formalization of 1.3.4. (iii).
Hence $W vdash Thm_T(Thm_U(0=1))$.
Since $T vdash neg Thm_U(0=1)$, also $W vdash neg Thm_U(0=1)$.
It think this is because if the statement is provable in some theory extending EA, it is provalbe in $any$ theory extending EA, but I am not sure.
So: $W vdash Thm_T(neg Thm_U(0=1))$.
It think that should be possible for any theory T, as long as T is prim.rec.
Now, I guess it is not difficult to see that, although not sure about the precise way how to do it, from $W vdash Thm_T(neg Thm_U(0=1))$ and $W vdash Thm_T(Thm_U(0=1))$, it follows that $W vdash Thm_T (0=1)$.
But we already know from the beginning that $W vdash neg Thm_T (0=1)$.
So we get a contradiction in $W$ by assumption of $W vdash Thm_U(0=1)$, thus we get $W vdash neg Thm_U(0=1)$.
It seems to me that a lack of my understanding comes from not really knowing what the provability predicate is able to do. It seems to me that my textbook didn't clarify these things very explicitly, or at least I didn't notice. Specifically the predicate was never used for different theories at the same time (in this intricated way).
$textbf{Now an offer for a proof of (iii):}$
We head for a contradiction within $U$.
Suppose $U vdash neg A$.
$neg A$ is a $Sigma^0_1$ -sentence, since $A$ is a $Pi^0_1$ -sentence.
Hence by theorem 1.4.7. (1.3.4. (iii) within PRA) $U vdash neg A rightarrow Thm_T(neg A)$, as $U$ contains PRA and $T$ extends EA, and thus $U vdash Thm_T(neg A)$.
But since $T vdash A$, also $U vdash Thm_T(A)$ by theorem 1.3.4., as long as $T$ is any prim. rec. theory and $U$ extends EA, since $Thm_T(A)$ is a true $Sigma$ -sentence.
So by $U vdash Thm_T(neg A)$ and $U vdash Thm_T(A)$ also $U vdash Thm_T(neg A land A)$, that is $U vdash Thm_T(0=1)$.
But we have as a premise that $U vdash neg Thm_T(0=1)$.
So we derived a contradiction in U from $U vdash neg A$.
So $U vdash A$.
answered Dec 9 at 10:42
Ettore
798
1
For $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$, we have assumed $U <T$ so $T vdash lnot text{Thm}_U(0=1)$ and we have $T vdash lnot text{Thm}_U(0=1)$ implies $text{EA} vdash text{Thm}_T(lnot text{Thm}_U(0=1))$. So we don't need to show or assume $W vdash lnot text{Thm}_U(0=1)$.
– Carl Mummert
Dec 11 at 14:40
1
For the next part, the key point is that if $T$ is any primitive recursive theory and $phi$ is any sentence in the language, there is a primitive recursive function that takes two inputs - a $T$-proof of $phi$ and a $T$-proof of $lnot phi$ - and returns a $T$-proof of $0=1$. The exact function depends on the formal deduction system being used, but the overall structure is to prove the tautology $phi to (lnotphi to 0=1)$ and then use modus ponens twice.
– Carl Mummert
Dec 11 at 14:42
1
Since $W$ extends PRA, if there is a primitive recursive procedure that takes a proof of one kind to a proof of a second kind, then the provability predicate of $W$ will be closed under that operation. For example $W vdash [text{Thm}_T(phi) land text{Thm}_T(psi)] to text{Thm}_T(phi land psi)$.This is because we obtain the proof of $phi land psi$ by doing a straightforward (primitive recursive) manipulation of the proofs of $phi$ and $psi$, which does not depend on what those proofs look like.
– Carl Mummert
Dec 11 at 14:45
I think I understand. In your first comment you mean $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$ in the end instead right? As for Thm, so one could say that a primitive recursive function allows W to calculate proof-Gödelnumbers from other proof-Gödelnumbers for T without really needing to 'touch' the proofs or the provability of intermediate steps themselves.
– Ettore
Dec 11 at 16:59
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
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%2f3028361%2fordering-between-formal-theories-by-provability-of-consistency%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$textbf{(Sketch of a) proof of transitivity (i):}$
We may suppose that $W$ is consistent, for if it is inconsistent it proves anything.
Assume $W vdash Thm_U(0=1)$ - we're after a contradiction $in$ $W$.
We have $W vdash Thm_U(0=1) rightarrow Thm_T(Thm_U(0=1))$.
This is an instance of theorem 1.4.7., that is the formalization of 1.3.4. (iii).
Hence $W vdash Thm_T(Thm_U(0=1))$.
Since $T vdash neg Thm_U(0=1)$, also $W vdash neg Thm_U(0=1)$.
It think this is because if the statement is provable in some theory extending EA, it is provalbe in $any$ theory extending EA, but I am not sure.
So: $W vdash Thm_T(neg Thm_U(0=1))$.
It think that should be possible for any theory T, as long as T is prim.rec.
Now, I guess it is not difficult to see that, although not sure about the precise way how to do it, from $W vdash Thm_T(neg Thm_U(0=1))$ and $W vdash Thm_T(Thm_U(0=1))$, it follows that $W vdash Thm_T (0=1)$.
But we already know from the beginning that $W vdash neg Thm_T (0=1)$.
So we get a contradiction in $W$ by assumption of $W vdash Thm_U(0=1)$, thus we get $W vdash neg Thm_U(0=1)$.
It seems to me that a lack of my understanding comes from not really knowing what the provability predicate is able to do. It seems to me that my textbook didn't clarify these things very explicitly, or at least I didn't notice. Specifically the predicate was never used for different theories at the same time (in this intricated way).
$textbf{Now an offer for a proof of (iii):}$
We head for a contradiction within $U$.
Suppose $U vdash neg A$.
$neg A$ is a $Sigma^0_1$ -sentence, since $A$ is a $Pi^0_1$ -sentence.
Hence by theorem 1.4.7. (1.3.4. (iii) within PRA) $U vdash neg A rightarrow Thm_T(neg A)$, as $U$ contains PRA and $T$ extends EA, and thus $U vdash Thm_T(neg A)$.
But since $T vdash A$, also $U vdash Thm_T(A)$ by theorem 1.3.4., as long as $T$ is any prim. rec. theory and $U$ extends EA, since $Thm_T(A)$ is a true $Sigma$ -sentence.
So by $U vdash Thm_T(neg A)$ and $U vdash Thm_T(A)$ also $U vdash Thm_T(neg A land A)$, that is $U vdash Thm_T(0=1)$.
But we have as a premise that $U vdash neg Thm_T(0=1)$.
So we derived a contradiction in U from $U vdash neg A$.
So $U vdash A$.
answered Dec 9 at 10:42
Ettore
798
1
For $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$, we have assumed $U <T$ so $T vdash lnot text{Thm}_U(0=1)$ and we have $T vdash lnot text{Thm}_U(0=1)$ implies $text{EA} vdash text{Thm}_T(lnot text{Thm}_U(0=1))$. So we don't need to show or assume $W vdash lnot text{Thm}_U(0=1)$.
– Carl Mummert
Dec 11 at 14:40
1
For the next part, the key point is that if $T$ is any primitive recursive theory and $phi$ is any sentence in the language, there is a primitive recursive function that takes two inputs - a $T$-proof of $phi$ and a $T$-proof of $lnot phi$ - and returns a $T$-proof of $0=1$. The exact function depends on the formal deduction system being used, but the overall structure is to prove the tautology $phi to (lnotphi to 0=1)$ and then use modus ponens twice.
– Carl Mummert
Dec 11 at 14:42
1
Since $W$ extends PRA, if there is a primitive recursive procedure that takes a proof of one kind to a proof of a second kind, then the provability predicate of $W$ will be closed under that operation. For example $W vdash [text{Thm}_T(phi) land text{Thm}_T(psi)] to text{Thm}_T(phi land psi)$.This is because we obtain the proof of $phi land psi$ by doing a straightforward (primitive recursive) manipulation of the proofs of $phi$ and $psi$, which does not depend on what those proofs look like.
– Carl Mummert
Dec 11 at 14:45
I think I understand. In your first comment you mean $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$ in the end instead right? As for Thm, so one could say that a primitive recursive function allows W to calculate proof-Gödelnumbers from other proof-Gödelnumbers for T without really needing to 'touch' the proofs or the provability of intermediate steps themselves.
– Ettore
Dec 11 at 16:59
add a comment |
$textbf{(Sketch of a) proof of transitivity (i):}$
We may suppose that $W$ is consistent, for if it is inconsistent it proves anything.
Assume $W vdash Thm_U(0=1)$ - we're after a contradiction $in$ $W$.
We have $W vdash Thm_U(0=1) rightarrow Thm_T(Thm_U(0=1))$.
This is an instance of theorem 1.4.7., that is the formalization of 1.3.4. (iii).
Hence $W vdash Thm_T(Thm_U(0=1))$.
Since $T vdash neg Thm_U(0=1)$, also $W vdash neg Thm_U(0=1)$.
It think this is because if the statement is provable in some theory extending EA, it is provalbe in $any$ theory extending EA, but I am not sure.
So: $W vdash Thm_T(neg Thm_U(0=1))$.
It think that should be possible for any theory T, as long as T is prim.rec.
Now, I guess it is not difficult to see that, although not sure about the precise way how to do it, from $W vdash Thm_T(neg Thm_U(0=1))$ and $W vdash Thm_T(Thm_U(0=1))$, it follows that $W vdash Thm_T (0=1)$.
But we already know from the beginning that $W vdash neg Thm_T (0=1)$.
So we get a contradiction in $W$ by assumption of $W vdash Thm_U(0=1)$, thus we get $W vdash neg Thm_U(0=1)$.
It seems to me that a lack of my understanding comes from not really knowing what the provability predicate is able to do. It seems to me that my textbook didn't clarify these things very explicitly, or at least I didn't notice. Specifically the predicate was never used for different theories at the same time (in this intricated way).
$textbf{Now an offer for a proof of (iii):}$
We head for a contradiction within $U$.
Suppose $U vdash neg A$.
$neg A$ is a $Sigma^0_1$ -sentence, since $A$ is a $Pi^0_1$ -sentence.
Hence by theorem 1.4.7. (1.3.4. (iii) within PRA) $U vdash neg A rightarrow Thm_T(neg A)$, as $U$ contains PRA and $T$ extends EA, and thus $U vdash Thm_T(neg A)$.
But since $T vdash A$, also $U vdash Thm_T(A)$ by theorem 1.3.4., as long as $T$ is any prim. rec. theory and $U$ extends EA, since $Thm_T(A)$ is a true $Sigma$ -sentence.
So by $U vdash Thm_T(neg A)$ and $U vdash Thm_T(A)$ also $U vdash Thm_T(neg A land A)$, that is $U vdash Thm_T(0=1)$.
But we have as a premise that $U vdash neg Thm_T(0=1)$.
So we derived a contradiction in U from $U vdash neg A$.
So $U vdash A$.
answered Dec 9 at 10:42
Ettore
798
1
For $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$, we have assumed $U <T$ so $T vdash lnot text{Thm}_U(0=1)$ and we have $T vdash lnot text{Thm}_U(0=1)$ implies $text{EA} vdash text{Thm}_T(lnot text{Thm}_U(0=1))$. So we don't need to show or assume $W vdash lnot text{Thm}_U(0=1)$.
– Carl Mummert
Dec 11 at 14:40
1
For the next part, the key point is that if $T$ is any primitive recursive theory and $phi$ is any sentence in the language, there is a primitive recursive function that takes two inputs - a $T$-proof of $phi$ and a $T$-proof of $lnot phi$ - and returns a $T$-proof of $0=1$. The exact function depends on the formal deduction system being used, but the overall structure is to prove the tautology $phi to (lnotphi to 0=1)$ and then use modus ponens twice.
– Carl Mummert
Dec 11 at 14:42
1
Since $W$ extends PRA, if there is a primitive recursive procedure that takes a proof of one kind to a proof of a second kind, then the provability predicate of $W$ will be closed under that operation. For example $W vdash [text{Thm}_T(phi) land text{Thm}_T(psi)] to text{Thm}_T(phi land psi)$.This is because we obtain the proof of $phi land psi$ by doing a straightforward (primitive recursive) manipulation of the proofs of $phi$ and $psi$, which does not depend on what those proofs look like.
– Carl Mummert
Dec 11 at 14:45
I think I understand. In your first comment you mean $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$ in the end instead right? As for Thm, so one could say that a primitive recursive function allows W to calculate proof-Gödelnumbers from other proof-Gödelnumbers for T without really needing to 'touch' the proofs or the provability of intermediate steps themselves.
– Ettore
Dec 11 at 16:59
add a comment |
$textbf{(Sketch of a) proof of transitivity (i):}$
We may suppose that $W$ is consistent, for if it is inconsistent it proves anything.
Assume $W vdash Thm_U(0=1)$ - we're after a contradiction $in$ $W$.
We have $W vdash Thm_U(0=1) rightarrow Thm_T(Thm_U(0=1))$.
This is an instance of theorem 1.4.7., that is the formalization of 1.3.4. (iii).
Hence $W vdash Thm_T(Thm_U(0=1))$.
Since $T vdash neg Thm_U(0=1)$, also $W vdash neg Thm_U(0=1)$.
It think this is because if the statement is provable in some theory extending EA, it is provalbe in $any$ theory extending EA, but I am not sure.
So: $W vdash Thm_T(neg Thm_U(0=1))$.
It think that should be possible for any theory T, as long as T is prim.rec.
Now, I guess it is not difficult to see that, although not sure about the precise way how to do it, from $W vdash Thm_T(neg Thm_U(0=1))$ and $W vdash Thm_T(Thm_U(0=1))$, it follows that $W vdash Thm_T (0=1)$.
But we already know from the beginning that $W vdash neg Thm_T (0=1)$.
So we get a contradiction in $W$ by assumption of $W vdash Thm_U(0=1)$, thus we get $W vdash neg Thm_U(0=1)$.
It seems to me that a lack of my understanding comes from not really knowing what the provability predicate is able to do. It seems to me that my textbook didn't clarify these things very explicitly, or at least I didn't notice. Specifically the predicate was never used for different theories at the same time (in this intricated way).
$textbf{Now an offer for a proof of (iii):}$
We head for a contradiction within $U$.
Suppose $U vdash neg A$.
$neg A$ is a $Sigma^0_1$ -sentence, since $A$ is a $Pi^0_1$ -sentence.
Hence by theorem 1.4.7. (1.3.4. (iii) within PRA) $U vdash neg A rightarrow Thm_T(neg A)$, as $U$ contains PRA and $T$ extends EA, and thus $U vdash Thm_T(neg A)$.
But since $T vdash A$, also $U vdash Thm_T(A)$ by theorem 1.3.4., as long as $T$ is any prim. rec. theory and $U$ extends EA, since $Thm_T(A)$ is a true $Sigma$ -sentence.
So by $U vdash Thm_T(neg A)$ and $U vdash Thm_T(A)$ also $U vdash Thm_T(neg A land A)$, that is $U vdash Thm_T(0=1)$.
But we have as a premise that $U vdash neg Thm_T(0=1)$.
So we derived a contradiction in U from $U vdash neg A$.
So $U vdash A$.
answered Dec 9 at 10:42
Ettore
798
$textbf{(Sketch of a) proof of transitivity (i):}$
We may suppose that $W$ is consistent, for if it is inconsistent it proves anything.
Assume $W vdash Thm_U(0=1)$ - we're after a contradiction $in$ $W$.
We have $W vdash Thm_U(0=1) rightarrow Thm_T(Thm_U(0=1))$.
This is an instance of theorem 1.4.7., that is the formalization of 1.3.4. (iii).
Hence $W vdash Thm_T(Thm_U(0=1))$.
Since $T vdash neg Thm_U(0=1)$, also $W vdash neg Thm_U(0=1)$.
It think this is because if the statement is provable in some theory extending EA, it is provalbe in $any$ theory extending EA, but I am not sure.
So: $W vdash Thm_T(neg Thm_U(0=1))$.
It think that should be possible for any theory T, as long as T is prim.rec.
Now, I guess it is not difficult to see that, although not sure about the precise way how to do it, from $W vdash Thm_T(neg Thm_U(0=1))$ and $W vdash Thm_T(Thm_U(0=1))$, it follows that $W vdash Thm_T (0=1)$.
But we already know from the beginning that $W vdash neg Thm_T (0=1)$.
So we get a contradiction in $W$ by assumption of $W vdash Thm_U(0=1)$, thus we get $W vdash neg Thm_U(0=1)$.
It seems to me that a lack of my understanding comes from not really knowing what the provability predicate is able to do. It seems to me that my textbook didn't clarify these things very explicitly, or at least I didn't notice. Specifically the predicate was never used for different theories at the same time (in this intricated way).
$textbf{Now an offer for a proof of (iii):}$
We head for a contradiction within $U$.
Suppose $U vdash neg A$.
$neg A$ is a $Sigma^0_1$ -sentence, since $A$ is a $Pi^0_1$ -sentence.
Hence by theorem 1.4.7. (1.3.4. (iii) within PRA) $U vdash neg A rightarrow Thm_T(neg A)$, as $U$ contains PRA and $T$ extends EA, and thus $U vdash Thm_T(neg A)$.
But since $T vdash A$, also $U vdash Thm_T(A)$ by theorem 1.3.4., as long as $T$ is any prim. rec. theory and $U$ extends EA, since $Thm_T(A)$ is a true $Sigma$ -sentence.
So by $U vdash Thm_T(neg A)$ and $U vdash Thm_T(A)$ also $U vdash Thm_T(neg A land A)$, that is $U vdash Thm_T(0=1)$.
But we have as a premise that $U vdash neg Thm_T(0=1)$.
So we derived a contradiction in U from $U vdash neg A$.
So $U vdash A$.
answered Dec 9 at 10:42
Ettore
798
edited Dec 9 at 12:48
answered Dec 9 at 10:42
Ettore
798
answered Dec 9 at 10:42
Ettore
798
answered Dec 9 at 10:42
Ettore
798
798
1
For $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$, we have assumed $U <T$ so $T vdash lnot text{Thm}_U(0=1)$ and we have $T vdash lnot text{Thm}_U(0=1)$ implies $text{EA} vdash text{Thm}_T(lnot text{Thm}_U(0=1))$. So we don't need to show or assume $W vdash lnot text{Thm}_U(0=1)$.
– Carl Mummert
Dec 11 at 14:40
1
For the next part, the key point is that if $T$ is any primitive recursive theory and $phi$ is any sentence in the language, there is a primitive recursive function that takes two inputs - a $T$-proof of $phi$ and a $T$-proof of $lnot phi$ - and returns a $T$-proof of $0=1$. The exact function depends on the formal deduction system being used, but the overall structure is to prove the tautology $phi to (lnotphi to 0=1)$ and then use modus ponens twice.
– Carl Mummert
Dec 11 at 14:42
1
Since $W$ extends PRA, if there is a primitive recursive procedure that takes a proof of one kind to a proof of a second kind, then the provability predicate of $W$ will be closed under that operation. For example $W vdash [text{Thm}_T(phi) land text{Thm}_T(psi)] to text{Thm}_T(phi land psi)$.This is because we obtain the proof of $phi land psi$ by doing a straightforward (primitive recursive) manipulation of the proofs of $phi$ and $psi$, which does not depend on what those proofs look like.
– Carl Mummert
Dec 11 at 14:45
I think I understand. In your first comment you mean $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$ in the end instead right? As for Thm, so one could say that a primitive recursive function allows W to calculate proof-Gödelnumbers from other proof-Gödelnumbers for T without really needing to 'touch' the proofs or the provability of intermediate steps themselves.
– Ettore
Dec 11 at 16:59
add a comment |
1
For $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$, we have assumed $U <T$ so $T vdash lnot text{Thm}_U(0=1)$ and we have $T vdash lnot text{Thm}_U(0=1)$ implies $text{EA} vdash text{Thm}_T(lnot text{Thm}_U(0=1))$. So we don't need to show or assume $W vdash lnot text{Thm}_U(0=1)$.
– Carl Mummert
Dec 11 at 14:40
1
For the next part, the key point is that if $T$ is any primitive recursive theory and $phi$ is any sentence in the language, there is a primitive recursive function that takes two inputs - a $T$-proof of $phi$ and a $T$-proof of $lnot phi$ - and returns a $T$-proof of $0=1$. The exact function depends on the formal deduction system being used, but the overall structure is to prove the tautology $phi to (lnotphi to 0=1)$ and then use modus ponens twice.
– Carl Mummert
Dec 11 at 14:42
1
Since $W$ extends PRA, if there is a primitive recursive procedure that takes a proof of one kind to a proof of a second kind, then the provability predicate of $W$ will be closed under that operation. For example $W vdash [text{Thm}_T(phi) land text{Thm}_T(psi)] to text{Thm}_T(phi land psi)$.This is because we obtain the proof of $phi land psi$ by doing a straightforward (primitive recursive) manipulation of the proofs of $phi$ and $psi$, which does not depend on what those proofs look like.
– Carl Mummert
Dec 11 at 14:45
I think I understand. In your first comment you mean $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$ in the end instead right? As for Thm, so one could say that a primitive recursive function allows W to calculate proof-Gödelnumbers from other proof-Gödelnumbers for T without really needing to 'touch' the proofs or the provability of intermediate steps themselves.
– Ettore
Dec 11 at 16:59
1
1
For $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$, we have assumed $U <T$ so $T vdash lnot text{Thm}_U(0=1)$ and we have $T vdash lnot text{Thm}_U(0=1)$ implies $text{EA} vdash text{Thm}_T(lnot text{Thm}_U(0=1))$. So we don't need to show or assume $W vdash lnot text{Thm}_U(0=1)$.
– Carl Mummert
Dec 11 at 14:40
For $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$, we have assumed $U <T$ so $T vdash lnot text{Thm}_U(0=1)$ and we have $T vdash lnot text{Thm}_U(0=1)$ implies $text{EA} vdash text{Thm}_T(lnot text{Thm}_U(0=1))$. So we don't need to show or assume $W vdash lnot text{Thm}_U(0=1)$.
– Carl Mummert
Dec 11 at 14:40
1
1
For the next part, the key point is that if $T$ is any primitive recursive theory and $phi$ is any sentence in the language, there is a primitive recursive function that takes two inputs - a $T$-proof of $phi$ and a $T$-proof of $lnot phi$ - and returns a $T$-proof of $0=1$. The exact function depends on the formal deduction system being used, but the overall structure is to prove the tautology $phi to (lnotphi to 0=1)$ and then use modus ponens twice.
– Carl Mummert
Dec 11 at 14:42
For the next part, the key point is that if $T$ is any primitive recursive theory and $phi$ is any sentence in the language, there is a primitive recursive function that takes two inputs - a $T$-proof of $phi$ and a $T$-proof of $lnot phi$ - and returns a $T$-proof of $0=1$. The exact function depends on the formal deduction system being used, but the overall structure is to prove the tautology $phi to (lnotphi to 0=1)$ and then use modus ponens twice.
– Carl Mummert
Dec 11 at 14:42
1
1
Since $W$ extends PRA, if there is a primitive recursive procedure that takes a proof of one kind to a proof of a second kind, then the provability predicate of $W$ will be closed under that operation. For example $W vdash [text{Thm}_T(phi) land text{Thm}_T(psi)] to text{Thm}_T(phi land psi)$.This is because we obtain the proof of $phi land psi$ by doing a straightforward (primitive recursive) manipulation of the proofs of $phi$ and $psi$, which does not depend on what those proofs look like.
– Carl Mummert
Dec 11 at 14:45
Since $W$ extends PRA, if there is a primitive recursive procedure that takes a proof of one kind to a proof of a second kind, then the provability predicate of $W$ will be closed under that operation. For example $W vdash [text{Thm}_T(phi) land text{Thm}_T(psi)] to text{Thm}_T(phi land psi)$.This is because we obtain the proof of $phi land psi$ by doing a straightforward (primitive recursive) manipulation of the proofs of $phi$ and $psi$, which does not depend on what those proofs look like.
– Carl Mummert
Dec 11 at 14:45
I think I understand. In your first comment you mean $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$ in the end instead right? As for Thm, so one could say that a primitive recursive function allows W to calculate proof-Gödelnumbers from other proof-Gödelnumbers for T without really needing to 'touch' the proofs or the provability of intermediate steps themselves.
– Ettore
Dec 11 at 16:59
I think I understand. In your first comment you mean $W vdash text{Thm}_T(lnot text{Thm}_U(0=1))$ in the end instead right? As for Thm, so one could say that a primitive recursive function allows W to calculate proof-Gödelnumbers from other proof-Gödelnumbers for T without really needing to 'touch' the proofs or the provability of intermediate steps themselves.
– Ettore
Dec 11 at 16:59
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
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%2f3028361%2fordering-between-formal-theories-by-provability-of-consistency%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
Here is a hint that may help with transitivity ($W < T$ and $T < U$ implies $W < U$). We are assuming that these theories include PRA. So, for example, if $lnot text{Con}(W)$ then every one of these theories proves $lnot text{Con}(W)$. Remember $text{Con}(W)$ is $lnot ulcorner W vdash 0 = 1urcorner$. Moreover, if $W vdash 0 = 1$ then $U vdash ulcorner T vdash ulcorner W vdash 0 = 1urcorner urcorner $. This is because there is a primitive recursive function that takes a $W$ derivation of $0 = 1$ to a $T$ derivation of $ulcorner W vdash 0 = 1urcorner$.
– Carl Mummert
Dec 6 at 11:59
1
I should have written $T < W$ and $U < T$ implies $U <W$ to match the rest of my comment.
– Carl Mummert
Dec 6 at 14:43
1
Con(W) is a $Pi^0_1$ statement, but you are circling around the right idea. If $lnot text{Con}(U)$ then $T$ would prove $lnot text{Con}(U)$. What we want is the formalization of that: $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$.
– Carl Mummert
Dec 6 at 19:22
1
I was imagining a proof by contradiction in $W$ - show that, within $W$, $lnot text{Con}(U)$ leads to a contradiction, because $W vdash lnot text{Con}(U) to ulcorner T vdash lnot text{Con}(U)urcorner$, and also $T > U$ leads to $W vdash ulcorner T vdash text{Con}(U)urcorner$ , and from $ulcorner T vdash text{Con}(U)urcorner$ and $ulcorner T vdash lnot text{Con}(U)$, $W$ can prove $lnot text{Con}(T)$.
– Carl Mummert
Dec 7 at 2:25
1
I think it will be a similar argument - $lnot A$ is $Sigma^0_1$, so $U vdash lnot A to ulcorner T vdash lnot Aurcorner$. If you like, you would be welcome to write an answer in the answer box below (rather in the question box) to record it for others.
– Carl Mummert
Dec 7 at 12:40