recursive inseparability of the two Gödelnumber-sets: theorems and 'anti-theorems' of EA
$begingroup$
Here again one of my more or less basic proof-theoretic questions, working through Girards monograph from '87.
This is about exercise 1.5.10. - "recursive inseparability", on page 80.
It is this:
Let A and B be disjoint recursively enumerable subsets of $mathbb{N}$; A and B are called $textit{recursively inseparable}$ if and only if there is no recursive subset C of $mathbb{N}$ such that $A subset C, B subset complement{C}$.
Show that the sets $A= {x mid Thm_{EA}[x]}$ and $B= {x mid Thm_{EA}[langle 13, x rangle]}$ are recursively inseparable.
[Remark: So A is the set of the Gödelnumbers of the theorems of EA, and B is the set of the Gödelnumbers of formulae such that the negations of these formulae are theorems of EA. (13 is the Gödelnumber of the negation sign).]
So there shall be no subset C of the natural numbers such that C and its complement 'divide' A and B from each other, in the sense that the theorem-numbers are part of C and the formula-numbers, when the negated formula is a theorem, are part of C's complement.
It might have something to do with Church's theorem:
Any extension T of EA in the language of EA is either undecidable or inconsistent.
Here 'decidable' means that the set of the Gödelnumbers of the theorems of T is recursive, that is there is a recursive function that 'says yes' (say, = 0) on the theorem-numbers and 'says no' ( = 1) on any non-theorem-number.
We may assume that EA is consistent, I think, cause otherwise any formula is a theorem, and A and B are just the same, so they are not even disjoint.
I guess if there was such a C we could construct a recursive function for A, the set of theorem-numbers, contradicting Church's theorem. Because then we'd already have a recursive function 'sort of dividing' A from B, we'd only have to figure out a way in which this function can be alternated to 'deal properly' with the numbers that are not in A neither in B.
Regards and Thanks,
Ettore
logic recursion proof-theory meta-math
asked Dec 10 '18 at 9:45
EttoreEttore
989
$endgroup$
add a comment |
$begingroup$
Here again one of my more or less basic proof-theoretic questions, working through Girards monograph from '87.
This is about exercise 1.5.10. - "recursive inseparability", on page 80.
It is this:
Let A and B be disjoint recursively enumerable subsets of $mathbb{N}$; A and B are called $textit{recursively inseparable}$ if and only if there is no recursive subset C of $mathbb{N}$ such that $A subset C, B subset complement{C}$.
Show that the sets $A= {x mid Thm_{EA}[x]}$ and $B= {x mid Thm_{EA}[langle 13, x rangle]}$ are recursively inseparable.
[Remark: So A is the set of the Gödelnumbers of the theorems of EA, and B is the set of the Gödelnumbers of formulae such that the negations of these formulae are theorems of EA. (13 is the Gödelnumber of the negation sign).]
So there shall be no subset C of the natural numbers such that C and its complement 'divide' A and B from each other, in the sense that the theorem-numbers are part of C and the formula-numbers, when the negated formula is a theorem, are part of C's complement.
It might have something to do with Church's theorem:
Any extension T of EA in the language of EA is either undecidable or inconsistent.
Here 'decidable' means that the set of the Gödelnumbers of the theorems of T is recursive, that is there is a recursive function that 'says yes' (say, = 0) on the theorem-numbers and 'says no' ( = 1) on any non-theorem-number.
We may assume that EA is consistent, I think, cause otherwise any formula is a theorem, and A and B are just the same, so they are not even disjoint.
I guess if there was such a C we could construct a recursive function for A, the set of theorem-numbers, contradicting Church's theorem. Because then we'd already have a recursive function 'sort of dividing' A from B, we'd only have to figure out a way in which this function can be alternated to 'deal properly' with the numbers that are not in A neither in B.
Regards and Thanks,
Ettore
logic recursion proof-theory meta-math
asked Dec 10 '18 at 9:45
EttoreEttore
989
$endgroup$
add a comment |
$begingroup$
Here again one of my more or less basic proof-theoretic questions, working through Girards monograph from '87.
This is about exercise 1.5.10. - "recursive inseparability", on page 80.
It is this:
Let A and B be disjoint recursively enumerable subsets of $mathbb{N}$; A and B are called $textit{recursively inseparable}$ if and only if there is no recursive subset C of $mathbb{N}$ such that $A subset C, B subset complement{C}$.
Show that the sets $A= {x mid Thm_{EA}[x]}$ and $B= {x mid Thm_{EA}[langle 13, x rangle]}$ are recursively inseparable.
[Remark: So A is the set of the Gödelnumbers of the theorems of EA, and B is the set of the Gödelnumbers of formulae such that the negations of these formulae are theorems of EA. (13 is the Gödelnumber of the negation sign).]
So there shall be no subset C of the natural numbers such that C and its complement 'divide' A and B from each other, in the sense that the theorem-numbers are part of C and the formula-numbers, when the negated formula is a theorem, are part of C's complement.
It might have something to do with Church's theorem:
Any extension T of EA in the language of EA is either undecidable or inconsistent.
Here 'decidable' means that the set of the Gödelnumbers of the theorems of T is recursive, that is there is a recursive function that 'says yes' (say, = 0) on the theorem-numbers and 'says no' ( = 1) on any non-theorem-number.
We may assume that EA is consistent, I think, cause otherwise any formula is a theorem, and A and B are just the same, so they are not even disjoint.
I guess if there was such a C we could construct a recursive function for A, the set of theorem-numbers, contradicting Church's theorem. Because then we'd already have a recursive function 'sort of dividing' A from B, we'd only have to figure out a way in which this function can be alternated to 'deal properly' with the numbers that are not in A neither in B.
Regards and Thanks,
Ettore
logic recursion proof-theory meta-math
asked Dec 10 '18 at 9:45
EttoreEttore
989
$endgroup$
Here again one of my more or less basic proof-theoretic questions, working through Girards monograph from '87.
This is about exercise 1.5.10. - "recursive inseparability", on page 80.
It is this:
Let A and B be disjoint recursively enumerable subsets of $mathbb{N}$; A and B are called $textit{recursively inseparable}$ if and only if there is no recursive subset C of $mathbb{N}$ such that $A subset C, B subset complement{C}$.
Show that the sets $A= {x mid Thm_{EA}[x]}$ and $B= {x mid Thm_{EA}[langle 13, x rangle]}$ are recursively inseparable.
[Remark: So A is the set of the Gödelnumbers of the theorems of EA, and B is the set of the Gödelnumbers of formulae such that the negations of these formulae are theorems of EA. (13 is the Gödelnumber of the negation sign).]
So there shall be no subset C of the natural numbers such that C and its complement 'divide' A and B from each other, in the sense that the theorem-numbers are part of C and the formula-numbers, when the negated formula is a theorem, are part of C's complement.
It might have something to do with Church's theorem:
Any extension T of EA in the language of EA is either undecidable or inconsistent.
Here 'decidable' means that the set of the Gödelnumbers of the theorems of T is recursive, that is there is a recursive function that 'says yes' (say, = 0) on the theorem-numbers and 'says no' ( = 1) on any non-theorem-number.
We may assume that EA is consistent, I think, cause otherwise any formula is a theorem, and A and B are just the same, so they are not even disjoint.
I guess if there was such a C we could construct a recursive function for A, the set of theorem-numbers, contradicting Church's theorem. Because then we'd already have a recursive function 'sort of dividing' A from B, we'd only have to figure out a way in which this function can be alternated to 'deal properly' with the numbers that are not in A neither in B.
Regards and Thanks,
Ettore
logic recursion proof-theory meta-math
logic recursion proof-theory meta-math
asked Dec 10 '18 at 9:45
EttoreEttore
989
asked Dec 10 '18 at 9:45
EttoreEttore
989
asked Dec 10 '18 at 9:45
EttoreEttore
989
asked Dec 10 '18 at 9:45
EttoreEttore
989
asked Dec 10 '18 at 9:45
EttoreEttore
989
989
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Already has an answer, even here on SE:
Show that a recursively inseparable pair of recursively enumerable sets exists
The idea lies in the diagonal lemma: The assumed separating set C can be represented by a formula $varphi$ in EA, which in turn is connected biconditionally in EA to a formula $tau$. This formula $tau$ has a Gödel number. If one asks oneself where this number might lay, in C or its complement, one gets a contradition either way.
answered Dec 10 '18 at 15:53
EttoreEttore
989
$endgroup$
1
$begingroup$
This method will work - we want to use the formula that says "I am not in $C$", I think. There is an alternative method: if $C$ is computable, contains $A$ and is disjoint from $B$, we can use $C$ to make a computable complete theory extending $A$, which contradicts the incompleteness theorems. Essentially, we put a formula into our complete theory if the conjunction of the formula and the formulas we have previously added is in $C$. In particular, no formula will ever be added which is inconsistent with $A$ and the previously added formulas.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:01
$begingroup$
Yes I think so too..or at least a formula that is provably equivalent to that. The other way is interesting, but it surprises me that this new theory is different, it sounds as if it doesn't change because the filled in formulae were already there before, but I guess I misunderstand. By the way, I also tried to complete the proof (part (iii)) in 'ordering between theories' - math.stackexchange.com/questions/3028361/…
$endgroup$
– Ettore
Dec 10 '18 at 16:25
1
$begingroup$
The issue is that the original theory was not complete, but with the method we can make a complete extension of it. $C$ is a kind of guide that allows us to avoid ever adding an inconsistency.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:27
1
$begingroup$
I think I can see...one goes on a search for the true unprovable formulae that lay in C, beyond A so to speak, and adds them as axioms, which then are infinite many I think.
$endgroup$
– Ettore
Dec 10 '18 at 16:41
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%2f3033704%2frecursive-inseparability-of-the-two-g%25c3%25b6delnumber-sets-theorems-and-anti-theorem%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
$begingroup$
Already has an answer, even here on SE:
Show that a recursively inseparable pair of recursively enumerable sets exists
The idea lies in the diagonal lemma: The assumed separating set C can be represented by a formula $varphi$ in EA, which in turn is connected biconditionally in EA to a formula $tau$. This formula $tau$ has a Gödel number. If one asks oneself where this number might lay, in C or its complement, one gets a contradition either way.
answered Dec 10 '18 at 15:53
EttoreEttore
989
$endgroup$
1
$begingroup$
This method will work - we want to use the formula that says "I am not in $C$", I think. There is an alternative method: if $C$ is computable, contains $A$ and is disjoint from $B$, we can use $C$ to make a computable complete theory extending $A$, which contradicts the incompleteness theorems. Essentially, we put a formula into our complete theory if the conjunction of the formula and the formulas we have previously added is in $C$. In particular, no formula will ever be added which is inconsistent with $A$ and the previously added formulas.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:01
$begingroup$
Yes I think so too..or at least a formula that is provably equivalent to that. The other way is interesting, but it surprises me that this new theory is different, it sounds as if it doesn't change because the filled in formulae were already there before, but I guess I misunderstand. By the way, I also tried to complete the proof (part (iii)) in 'ordering between theories' - math.stackexchange.com/questions/3028361/…
$endgroup$
– Ettore
Dec 10 '18 at 16:25
1
$begingroup$
The issue is that the original theory was not complete, but with the method we can make a complete extension of it. $C$ is a kind of guide that allows us to avoid ever adding an inconsistency.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:27
1
$begingroup$
I think I can see...one goes on a search for the true unprovable formulae that lay in C, beyond A so to speak, and adds them as axioms, which then are infinite many I think.
$endgroup$
– Ettore
Dec 10 '18 at 16:41
add a comment |
$begingroup$
Already has an answer, even here on SE:
Show that a recursively inseparable pair of recursively enumerable sets exists
The idea lies in the diagonal lemma: The assumed separating set C can be represented by a formula $varphi$ in EA, which in turn is connected biconditionally in EA to a formula $tau$. This formula $tau$ has a Gödel number. If one asks oneself where this number might lay, in C or its complement, one gets a contradition either way.
answered Dec 10 '18 at 15:53
EttoreEttore
989
$endgroup$
1
$begingroup$
This method will work - we want to use the formula that says "I am not in $C$", I think. There is an alternative method: if $C$ is computable, contains $A$ and is disjoint from $B$, we can use $C$ to make a computable complete theory extending $A$, which contradicts the incompleteness theorems. Essentially, we put a formula into our complete theory if the conjunction of the formula and the formulas we have previously added is in $C$. In particular, no formula will ever be added which is inconsistent with $A$ and the previously added formulas.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:01
$begingroup$
Yes I think so too..or at least a formula that is provably equivalent to that. The other way is interesting, but it surprises me that this new theory is different, it sounds as if it doesn't change because the filled in formulae were already there before, but I guess I misunderstand. By the way, I also tried to complete the proof (part (iii)) in 'ordering between theories' - math.stackexchange.com/questions/3028361/…
$endgroup$
– Ettore
Dec 10 '18 at 16:25
1
$begingroup$
The issue is that the original theory was not complete, but with the method we can make a complete extension of it. $C$ is a kind of guide that allows us to avoid ever adding an inconsistency.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:27
1
$begingroup$
I think I can see...one goes on a search for the true unprovable formulae that lay in C, beyond A so to speak, and adds them as axioms, which then are infinite many I think.
$endgroup$
– Ettore
Dec 10 '18 at 16:41
add a comment |
$begingroup$
Already has an answer, even here on SE:
Show that a recursively inseparable pair of recursively enumerable sets exists
The idea lies in the diagonal lemma: The assumed separating set C can be represented by a formula $varphi$ in EA, which in turn is connected biconditionally in EA to a formula $tau$. This formula $tau$ has a Gödel number. If one asks oneself where this number might lay, in C or its complement, one gets a contradition either way.
answered Dec 10 '18 at 15:53
EttoreEttore
989
$endgroup$
Already has an answer, even here on SE:
Show that a recursively inseparable pair of recursively enumerable sets exists
The idea lies in the diagonal lemma: The assumed separating set C can be represented by a formula $varphi$ in EA, which in turn is connected biconditionally in EA to a formula $tau$. This formula $tau$ has a Gödel number. If one asks oneself where this number might lay, in C or its complement, one gets a contradition either way.
answered Dec 10 '18 at 15:53
EttoreEttore
989
answered Dec 10 '18 at 15:53
EttoreEttore
989
answered Dec 10 '18 at 15:53
EttoreEttore
989
answered Dec 10 '18 at 15:53
EttoreEttore
989
989
1
$begingroup$
This method will work - we want to use the formula that says "I am not in $C$", I think. There is an alternative method: if $C$ is computable, contains $A$ and is disjoint from $B$, we can use $C$ to make a computable complete theory extending $A$, which contradicts the incompleteness theorems. Essentially, we put a formula into our complete theory if the conjunction of the formula and the formulas we have previously added is in $C$. In particular, no formula will ever be added which is inconsistent with $A$ and the previously added formulas.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:01
$begingroup$
Yes I think so too..or at least a formula that is provably equivalent to that. The other way is interesting, but it surprises me that this new theory is different, it sounds as if it doesn't change because the filled in formulae were already there before, but I guess I misunderstand. By the way, I also tried to complete the proof (part (iii)) in 'ordering between theories' - math.stackexchange.com/questions/3028361/…
$endgroup$
– Ettore
Dec 10 '18 at 16:25
1
$begingroup$
The issue is that the original theory was not complete, but with the method we can make a complete extension of it. $C$ is a kind of guide that allows us to avoid ever adding an inconsistency.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:27
1
$begingroup$
I think I can see...one goes on a search for the true unprovable formulae that lay in C, beyond A so to speak, and adds them as axioms, which then are infinite many I think.
$endgroup$
– Ettore
Dec 10 '18 at 16:41
add a comment |
1
$begingroup$
This method will work - we want to use the formula that says "I am not in $C$", I think. There is an alternative method: if $C$ is computable, contains $A$ and is disjoint from $B$, we can use $C$ to make a computable complete theory extending $A$, which contradicts the incompleteness theorems. Essentially, we put a formula into our complete theory if the conjunction of the formula and the formulas we have previously added is in $C$. In particular, no formula will ever be added which is inconsistent with $A$ and the previously added formulas.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:01
$begingroup$
Yes I think so too..or at least a formula that is provably equivalent to that. The other way is interesting, but it surprises me that this new theory is different, it sounds as if it doesn't change because the filled in formulae were already there before, but I guess I misunderstand. By the way, I also tried to complete the proof (part (iii)) in 'ordering between theories' - math.stackexchange.com/questions/3028361/…
$endgroup$
– Ettore
Dec 10 '18 at 16:25
1
$begingroup$
The issue is that the original theory was not complete, but with the method we can make a complete extension of it. $C$ is a kind of guide that allows us to avoid ever adding an inconsistency.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:27
1
$begingroup$
I think I can see...one goes on a search for the true unprovable formulae that lay in C, beyond A so to speak, and adds them as axioms, which then are infinite many I think.
$endgroup$
– Ettore
Dec 10 '18 at 16:41
1
1
$begingroup$
This method will work - we want to use the formula that says "I am not in $C$", I think. There is an alternative method: if $C$ is computable, contains $A$ and is disjoint from $B$, we can use $C$ to make a computable complete theory extending $A$, which contradicts the incompleteness theorems. Essentially, we put a formula into our complete theory if the conjunction of the formula and the formulas we have previously added is in $C$. In particular, no formula will ever be added which is inconsistent with $A$ and the previously added formulas.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:01
$begingroup$
This method will work - we want to use the formula that says "I am not in $C$", I think. There is an alternative method: if $C$ is computable, contains $A$ and is disjoint from $B$, we can use $C$ to make a computable complete theory extending $A$, which contradicts the incompleteness theorems. Essentially, we put a formula into our complete theory if the conjunction of the formula and the formulas we have previously added is in $C$. In particular, no formula will ever be added which is inconsistent with $A$ and the previously added formulas.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:01
$begingroup$
Yes I think so too..or at least a formula that is provably equivalent to that. The other way is interesting, but it surprises me that this new theory is different, it sounds as if it doesn't change because the filled in formulae were already there before, but I guess I misunderstand. By the way, I also tried to complete the proof (part (iii)) in 'ordering between theories' - math.stackexchange.com/questions/3028361/…
$endgroup$
– Ettore
Dec 10 '18 at 16:25
$begingroup$
Yes I think so too..or at least a formula that is provably equivalent to that. The other way is interesting, but it surprises me that this new theory is different, it sounds as if it doesn't change because the filled in formulae were already there before, but I guess I misunderstand. By the way, I also tried to complete the proof (part (iii)) in 'ordering between theories' - math.stackexchange.com/questions/3028361/…
$endgroup$
– Ettore
Dec 10 '18 at 16:25
1
1
$begingroup$
The issue is that the original theory was not complete, but with the method we can make a complete extension of it. $C$ is a kind of guide that allows us to avoid ever adding an inconsistency.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:27
$begingroup$
The issue is that the original theory was not complete, but with the method we can make a complete extension of it. $C$ is a kind of guide that allows us to avoid ever adding an inconsistency.
$endgroup$
– Carl Mummert
Dec 10 '18 at 16:27
1
1
$begingroup$
I think I can see...one goes on a search for the true unprovable formulae that lay in C, beyond A so to speak, and adds them as axioms, which then are infinite many I think.
$endgroup$
– Ettore
Dec 10 '18 at 16:41
$begingroup$
I think I can see...one goes on a search for the true unprovable formulae that lay in C, beyond A so to speak, and adds them as axioms, which then are infinite many I think.
$endgroup$
– Ettore
Dec 10 '18 at 16:41
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.
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%2f3033704%2frecursive-inseparability-of-the-two-g%25c3%25b6delnumber-sets-theorems-and-anti-theorem%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
