n-consistency - provability/truth of $Sigma^0_n$ and $Pi^0_{n+1}$ -formulas; n-consistent extensions, etc.
$begingroup$
I am facing difficulties with the following exercise.
(It is 1.5.9. from 'proof theory and logical complexity', Girard, '87)
(i) T is $textbf{n-consistent} (n>0)$ if any $Sigma^0_n$ - theorem A of T, A closed, is true.
Show that if T is n-consistent, then all closed $Pi^0_{n+1}$ -theorems of T are true.
Show that n-consistency of T is a $Pi^0_{n+1}$ -formula, when T is prim. rec.
(ii) Assume that T is n-consistent; form a theory U by adding to T all true closed $Pi^0_{n}$ -formulas. If T is prim. rec., show that $Thm_U$ is $Sigma^0_{n+1}$. (Hint: define first a $Pi^0_n$ -formula $Val^0_n$ such that if A is $Pi^0_n$ and closed, $Val^0_n[overline{ ulcorner A urcorner}] leftrightarrow A.$ )
[Remark: I guess he means $truth$ of $Val^0_n[overline{ ulcorner A urcorner}] leftrightarrow A.$ , not provability in T or U.]
I am probably shortly going to add (iii) and (iv).
Idea for (i):
I think the first thing to show in (i) is pretty clear.
If one is given a $Pi^0_{n+1}$ -theorem B, then B[t] is provable for any t. (t takes the place of the first variable). But B[t] is a closed $Sigma^0_n$ -theorem, hence it is true - for any t. So B is true.
The second thing to show may work with induction on n, but it's a wild guess. I'm not even sure what he means by n-consistency "being" a such and such formula, what formula exactly does he have in mind?
Also I am not sure if/how the system is able to tell whether a formula is $Sigma^0_n$ or not.
Thanks,
Ettore
PS: I left a link on mathoverflow also:
https://mathoverflow.net/questions/319285/n-consistency-provability-truth-of-sigma0-n-and-pi0-n1-formulas-n
logic proof-theory incompleteness meta-math provability
asked Dec 14 '18 at 18:40
EttoreEttore
1019
$endgroup$
|
show 1 more comment
$begingroup$
I am facing difficulties with the following exercise.
(It is 1.5.9. from 'proof theory and logical complexity', Girard, '87)
(i) T is $textbf{n-consistent} (n>0)$ if any $Sigma^0_n$ - theorem A of T, A closed, is true.
Show that if T is n-consistent, then all closed $Pi^0_{n+1}$ -theorems of T are true.
Show that n-consistency of T is a $Pi^0_{n+1}$ -formula, when T is prim. rec.
(ii) Assume that T is n-consistent; form a theory U by adding to T all true closed $Pi^0_{n}$ -formulas. If T is prim. rec., show that $Thm_U$ is $Sigma^0_{n+1}$. (Hint: define first a $Pi^0_n$ -formula $Val^0_n$ such that if A is $Pi^0_n$ and closed, $Val^0_n[overline{ ulcorner A urcorner}] leftrightarrow A.$ )
[Remark: I guess he means $truth$ of $Val^0_n[overline{ ulcorner A urcorner}] leftrightarrow A.$ , not provability in T or U.]
I am probably shortly going to add (iii) and (iv).
Idea for (i):
I think the first thing to show in (i) is pretty clear.
If one is given a $Pi^0_{n+1}$ -theorem B, then B[t] is provable for any t. (t takes the place of the first variable). But B[t] is a closed $Sigma^0_n$ -theorem, hence it is true - for any t. So B is true.
The second thing to show may work with induction on n, but it's a wild guess. I'm not even sure what he means by n-consistency "being" a such and such formula, what formula exactly does he have in mind?
Also I am not sure if/how the system is able to tell whether a formula is $Sigma^0_n$ or not.
Thanks,
Ettore
PS: I left a link on mathoverflow also:
https://mathoverflow.net/questions/319285/n-consistency-provability-truth-of-sigma0-n-and-pi0-n1-formulas-n
logic proof-theory incompleteness meta-math provability
asked Dec 14 '18 at 18:40
EttoreEttore
1019
$endgroup$
2
$begingroup$
There is a truth predicate $T_n$ for $Sigma_n^0$ sentences, and of course you have a provability predicate and a "this sentence is $Sigma_n^0$" predicate. The $n$-consistency statement "any $Sigma_n^0$ sentence that is provable is true" can be expressed in terms of these three predicates.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 18:50
1
$begingroup$
I didn't see you said you weren't sure about the "this formula is $Sigma_n^0$" predicate. A formula having less than or equal to $n$ nestings of $exists-forall$ blocks is a syntactical property that can be decided by parsing the formula... it is recursive. Being provably equivalent to such a sentence is just a statement about such an equivalence proof existing.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 19:44
$begingroup$
thanks @spaceisdarkgreen! I will think about it and try something out a bit...I thought it should be possible to tell whether $Sigma^0_n$ or not, so I more or less believed it from the beginning, but do not clearly see before my eyes how this is realized/works, but that is not terribly important. Maybe I will also need the HBL-derivability conditions? I wouldn't have thought about the truth predicate, I only recall that the general truth predicate does not exist by tarski's theorem..
$endgroup$
– Ettore
Dec 15 '18 at 8:47
$begingroup$
In that case I guess our formula would be something like $forall x (Sigma^0_n (x) land exists y Pr(x,y) rightarrow Tr_n(x))$. But why is it $Pi^0_{n+1}$?
$endgroup$
– Ettore
Dec 15 '18 at 11:15
1
$begingroup$
The truth predicate for $Sigma_n$ sentences is itself $Sigma_n.$ The other two are $Sigma_1$.
$endgroup$
– spaceisdarkgreen
Dec 15 '18 at 22:28
|
show 1 more comment
$begingroup$
I am facing difficulties with the following exercise.
(It is 1.5.9. from 'proof theory and logical complexity', Girard, '87)
(i) T is $textbf{n-consistent} (n>0)$ if any $Sigma^0_n$ - theorem A of T, A closed, is true.
Show that if T is n-consistent, then all closed $Pi^0_{n+1}$ -theorems of T are true.
Show that n-consistency of T is a $Pi^0_{n+1}$ -formula, when T is prim. rec.
(ii) Assume that T is n-consistent; form a theory U by adding to T all true closed $Pi^0_{n}$ -formulas. If T is prim. rec., show that $Thm_U$ is $Sigma^0_{n+1}$. (Hint: define first a $Pi^0_n$ -formula $Val^0_n$ such that if A is $Pi^0_n$ and closed, $Val^0_n[overline{ ulcorner A urcorner}] leftrightarrow A.$ )
[Remark: I guess he means $truth$ of $Val^0_n[overline{ ulcorner A urcorner}] leftrightarrow A.$ , not provability in T or U.]
I am probably shortly going to add (iii) and (iv).
Idea for (i):
I think the first thing to show in (i) is pretty clear.
If one is given a $Pi^0_{n+1}$ -theorem B, then B[t] is provable for any t. (t takes the place of the first variable). But B[t] is a closed $Sigma^0_n$ -theorem, hence it is true - for any t. So B is true.
The second thing to show may work with induction on n, but it's a wild guess. I'm not even sure what he means by n-consistency "being" a such and such formula, what formula exactly does he have in mind?
Also I am not sure if/how the system is able to tell whether a formula is $Sigma^0_n$ or not.
Thanks,
Ettore
PS: I left a link on mathoverflow also:
https://mathoverflow.net/questions/319285/n-consistency-provability-truth-of-sigma0-n-and-pi0-n1-formulas-n
logic proof-theory incompleteness meta-math provability
asked Dec 14 '18 at 18:40
EttoreEttore
1019
$endgroup$
I am facing difficulties with the following exercise.
(It is 1.5.9. from 'proof theory and logical complexity', Girard, '87)
(i) T is $textbf{n-consistent} (n>0)$ if any $Sigma^0_n$ - theorem A of T, A closed, is true.
Show that if T is n-consistent, then all closed $Pi^0_{n+1}$ -theorems of T are true.
Show that n-consistency of T is a $Pi^0_{n+1}$ -formula, when T is prim. rec.
(ii) Assume that T is n-consistent; form a theory U by adding to T all true closed $Pi^0_{n}$ -formulas. If T is prim. rec., show that $Thm_U$ is $Sigma^0_{n+1}$. (Hint: define first a $Pi^0_n$ -formula $Val^0_n$ such that if A is $Pi^0_n$ and closed, $Val^0_n[overline{ ulcorner A urcorner}] leftrightarrow A.$ )
[Remark: I guess he means $truth$ of $Val^0_n[overline{ ulcorner A urcorner}] leftrightarrow A.$ , not provability in T or U.]
I am probably shortly going to add (iii) and (iv).
Idea for (i):
I think the first thing to show in (i) is pretty clear.
If one is given a $Pi^0_{n+1}$ -theorem B, then B[t] is provable for any t. (t takes the place of the first variable). But B[t] is a closed $Sigma^0_n$ -theorem, hence it is true - for any t. So B is true.
The second thing to show may work with induction on n, but it's a wild guess. I'm not even sure what he means by n-consistency "being" a such and such formula, what formula exactly does he have in mind?
Also I am not sure if/how the system is able to tell whether a formula is $Sigma^0_n$ or not.
Thanks,
Ettore
PS: I left a link on mathoverflow also:
https://mathoverflow.net/questions/319285/n-consistency-provability-truth-of-sigma0-n-and-pi0-n1-formulas-n
logic proof-theory incompleteness meta-math provability
logic proof-theory incompleteness meta-math provability
asked Dec 14 '18 at 18:40
EttoreEttore
1019
asked Dec 14 '18 at 18:40
EttoreEttore
1019
edited Dec 22 '18 at 14:32
Ettore
asked Dec 14 '18 at 18:40
EttoreEttore
1019
asked Dec 14 '18 at 18:40
EttoreEttore
1019
asked Dec 14 '18 at 18:40
EttoreEttore
1019
1019
2
$begingroup$
There is a truth predicate $T_n$ for $Sigma_n^0$ sentences, and of course you have a provability predicate and a "this sentence is $Sigma_n^0$" predicate. The $n$-consistency statement "any $Sigma_n^0$ sentence that is provable is true" can be expressed in terms of these three predicates.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 18:50
1
$begingroup$
I didn't see you said you weren't sure about the "this formula is $Sigma_n^0$" predicate. A formula having less than or equal to $n$ nestings of $exists-forall$ blocks is a syntactical property that can be decided by parsing the formula... it is recursive. Being provably equivalent to such a sentence is just a statement about such an equivalence proof existing.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 19:44
$begingroup$
thanks @spaceisdarkgreen! I will think about it and try something out a bit...I thought it should be possible to tell whether $Sigma^0_n$ or not, so I more or less believed it from the beginning, but do not clearly see before my eyes how this is realized/works, but that is not terribly important. Maybe I will also need the HBL-derivability conditions? I wouldn't have thought about the truth predicate, I only recall that the general truth predicate does not exist by tarski's theorem..
$endgroup$
– Ettore
Dec 15 '18 at 8:47
$begingroup$
In that case I guess our formula would be something like $forall x (Sigma^0_n (x) land exists y Pr(x,y) rightarrow Tr_n(x))$. But why is it $Pi^0_{n+1}$?
$endgroup$
– Ettore
Dec 15 '18 at 11:15
1
$begingroup$
The truth predicate for $Sigma_n$ sentences is itself $Sigma_n.$ The other two are $Sigma_1$.
$endgroup$
– spaceisdarkgreen
Dec 15 '18 at 22:28
|
show 1 more comment
2
$begingroup$
There is a truth predicate $T_n$ for $Sigma_n^0$ sentences, and of course you have a provability predicate and a "this sentence is $Sigma_n^0$" predicate. The $n$-consistency statement "any $Sigma_n^0$ sentence that is provable is true" can be expressed in terms of these three predicates.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 18:50
1
$begingroup$
I didn't see you said you weren't sure about the "this formula is $Sigma_n^0$" predicate. A formula having less than or equal to $n$ nestings of $exists-forall$ blocks is a syntactical property that can be decided by parsing the formula... it is recursive. Being provably equivalent to such a sentence is just a statement about such an equivalence proof existing.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 19:44
$begingroup$
thanks @spaceisdarkgreen! I will think about it and try something out a bit...I thought it should be possible to tell whether $Sigma^0_n$ or not, so I more or less believed it from the beginning, but do not clearly see before my eyes how this is realized/works, but that is not terribly important. Maybe I will also need the HBL-derivability conditions? I wouldn't have thought about the truth predicate, I only recall that the general truth predicate does not exist by tarski's theorem..
$endgroup$
– Ettore
Dec 15 '18 at 8:47
$begingroup$
In that case I guess our formula would be something like $forall x (Sigma^0_n (x) land exists y Pr(x,y) rightarrow Tr_n(x))$. But why is it $Pi^0_{n+1}$?
$endgroup$
– Ettore
Dec 15 '18 at 11:15
1
$begingroup$
The truth predicate for $Sigma_n$ sentences is itself $Sigma_n.$ The other two are $Sigma_1$.
$endgroup$
– spaceisdarkgreen
Dec 15 '18 at 22:28
2
2
$begingroup$
There is a truth predicate $T_n$ for $Sigma_n^0$ sentences, and of course you have a provability predicate and a "this sentence is $Sigma_n^0$" predicate. The $n$-consistency statement "any $Sigma_n^0$ sentence that is provable is true" can be expressed in terms of these three predicates.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 18:50
$begingroup$
There is a truth predicate $T_n$ for $Sigma_n^0$ sentences, and of course you have a provability predicate and a "this sentence is $Sigma_n^0$" predicate. The $n$-consistency statement "any $Sigma_n^0$ sentence that is provable is true" can be expressed in terms of these three predicates.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 18:50
1
1
$begingroup$
I didn't see you said you weren't sure about the "this formula is $Sigma_n^0$" predicate. A formula having less than or equal to $n$ nestings of $exists-forall$ blocks is a syntactical property that can be decided by parsing the formula... it is recursive. Being provably equivalent to such a sentence is just a statement about such an equivalence proof existing.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 19:44
$begingroup$
I didn't see you said you weren't sure about the "this formula is $Sigma_n^0$" predicate. A formula having less than or equal to $n$ nestings of $exists-forall$ blocks is a syntactical property that can be decided by parsing the formula... it is recursive. Being provably equivalent to such a sentence is just a statement about such an equivalence proof existing.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 19:44
$begingroup$
thanks @spaceisdarkgreen! I will think about it and try something out a bit...I thought it should be possible to tell whether $Sigma^0_n$ or not, so I more or less believed it from the beginning, but do not clearly see before my eyes how this is realized/works, but that is not terribly important. Maybe I will also need the HBL-derivability conditions? I wouldn't have thought about the truth predicate, I only recall that the general truth predicate does not exist by tarski's theorem..
$endgroup$
– Ettore
Dec 15 '18 at 8:47
$begingroup$
thanks @spaceisdarkgreen! I will think about it and try something out a bit...I thought it should be possible to tell whether $Sigma^0_n$ or not, so I more or less believed it from the beginning, but do not clearly see before my eyes how this is realized/works, but that is not terribly important. Maybe I will also need the HBL-derivability conditions? I wouldn't have thought about the truth predicate, I only recall that the general truth predicate does not exist by tarski's theorem..
$endgroup$
– Ettore
Dec 15 '18 at 8:47
$begingroup$
In that case I guess our formula would be something like $forall x (Sigma^0_n (x) land exists y Pr(x,y) rightarrow Tr_n(x))$. But why is it $Pi^0_{n+1}$?
$endgroup$
– Ettore
Dec 15 '18 at 11:15
$begingroup$
In that case I guess our formula would be something like $forall x (Sigma^0_n (x) land exists y Pr(x,y) rightarrow Tr_n(x))$. But why is it $Pi^0_{n+1}$?
$endgroup$
– Ettore
Dec 15 '18 at 11:15
1
1
$begingroup$
The truth predicate for $Sigma_n$ sentences is itself $Sigma_n.$ The other two are $Sigma_1$.
$endgroup$
– spaceisdarkgreen
Dec 15 '18 at 22:28
$begingroup$
The truth predicate for $Sigma_n$ sentences is itself $Sigma_n.$ The other two are $Sigma_1$.
$endgroup$
– spaceisdarkgreen
Dec 15 '18 at 22:28
|
show 1 more comment
0
active
oldest
votes
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%2f3039763%2fn-consistency-provability-truth-of-sigma0-n-and-pi0-n1-formulas-n%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
0
active
oldest
votes
0
active
oldest
votes
active
oldest
votes
active
oldest
votes
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.
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%2f3039763%2fn-consistency-provability-truth-of-sigma0-n-and-pi0-n1-formulas-n%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
2
$begingroup$
There is a truth predicate $T_n$ for $Sigma_n^0$ sentences, and of course you have a provability predicate and a "this sentence is $Sigma_n^0$" predicate. The $n$-consistency statement "any $Sigma_n^0$ sentence that is provable is true" can be expressed in terms of these three predicates.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 18:50
1
$begingroup$
I didn't see you said you weren't sure about the "this formula is $Sigma_n^0$" predicate. A formula having less than or equal to $n$ nestings of $exists-forall$ blocks is a syntactical property that can be decided by parsing the formula... it is recursive. Being provably equivalent to such a sentence is just a statement about such an equivalence proof existing.
$endgroup$
– spaceisdarkgreen
Dec 14 '18 at 19:44
$begingroup$
thanks @spaceisdarkgreen! I will think about it and try something out a bit...I thought it should be possible to tell whether $Sigma^0_n$ or not, so I more or less believed it from the beginning, but do not clearly see before my eyes how this is realized/works, but that is not terribly important. Maybe I will also need the HBL-derivability conditions? I wouldn't have thought about the truth predicate, I only recall that the general truth predicate does not exist by tarski's theorem..
$endgroup$
– Ettore
Dec 15 '18 at 8:47
$begingroup$
In that case I guess our formula would be something like $forall x (Sigma^0_n (x) land exists y Pr(x,y) rightarrow Tr_n(x))$. But why is it $Pi^0_{n+1}$?
$endgroup$
– Ettore
Dec 15 '18 at 11:15
1
$begingroup$
The truth predicate for $Sigma_n$ sentences is itself $Sigma_n.$ The other two are $Sigma_1$.
$endgroup$
– spaceisdarkgreen
Dec 15 '18 at 22:28