Partially verifiable logic
Are there any known or established or researched logics (not restricted to sequent logic) where the proof object
- Is not necessarily verifiable in every case whether the proof object is valid
- If it is verifiable, then it can be verified in finite time
The intention is that this logic would be more general than those restricted to primitive recursive computing models; for example, the proof of Godel's incompleteness theorem might not apply as usually presented.
logic
asked Sep 30 '17 at 18:16
DanielV
17.8k42754
|
show 2 more comments
Are there any known or established or researched logics (not restricted to sequent logic) where the proof object
- Is not necessarily verifiable in every case whether the proof object is valid
- If it is verifiable, then it can be verified in finite time
The intention is that this logic would be more general than those restricted to primitive recursive computing models; for example, the proof of Godel's incompleteness theorem might not apply as usually presented.
logic
asked Sep 30 '17 at 18:16
DanielV
17.8k42754
I may also ask this question on the cs stackexchange because they also have a very dedicated logic section.
– DanielV
Sep 30 '17 at 18:16
Have you looked into infinitary logic
– Rob Arthan
Sep 30 '17 at 22:58
There is also work on how the incompleteness theorem breaks down if you admit non-recursive axiom systems for number theory.
– Rob Arthan
Sep 30 '17 at 23:22
@RobArthan I haven't heard the term "infinitary logic" although I've seen the general concept discussed. The first sentence from wikipedia makes me hesitant though, "allows infinitely long statements and/or infinitely long proofs" would suggest a required computing model strictly stronger than Turing Machines. I would expect the proof object itself to be of finite size. Can you clarify what a "non-recursive axiom system" is? Does that mean "non primitive recursive" or a computing model strictly stronger than Turing Machines ?
– DanielV
Oct 1 '17 at 0:18
Every first-order theory comes with an axiom set. If that set is recursive (its members are decided by some program) then the incompleteness theorems apply to it. But even if the set is not recursive, as long as it is semi-recursive (there is a program that accepts exactly its members) or equivalently recursively enumerable (it is the range of a program taken as a partial function), then as described in my post the incompleteness theorems still apply to it! @RobArthan, you may be interested in it too. Another natural question is how much non-computability is needed to obtain a complete theory.
– user21820
Oct 4 '17 at 5:08
|
show 2 more comments
Are there any known or established or researched logics (not restricted to sequent logic) where the proof object
- Is not necessarily verifiable in every case whether the proof object is valid
- If it is verifiable, then it can be verified in finite time
The intention is that this logic would be more general than those restricted to primitive recursive computing models; for example, the proof of Godel's incompleteness theorem might not apply as usually presented.
logic
asked Sep 30 '17 at 18:16
DanielV
17.8k42754
Are there any known or established or researched logics (not restricted to sequent logic) where the proof object
- Is not necessarily verifiable in every case whether the proof object is valid
- If it is verifiable, then it can be verified in finite time
The intention is that this logic would be more general than those restricted to primitive recursive computing models; for example, the proof of Godel's incompleteness theorem might not apply as usually presented.
logic
logic
asked Sep 30 '17 at 18:16
DanielV
17.8k42754
asked Sep 30 '17 at 18:16
DanielV
17.8k42754
asked Sep 30 '17 at 18:16
DanielV
17.8k42754
asked Sep 30 '17 at 18:16
DanielV
17.8k42754
asked Sep 30 '17 at 18:16
DanielV
17.8k42754
17.8k42754
I may also ask this question on the cs stackexchange because they also have a very dedicated logic section.
– DanielV
Sep 30 '17 at 18:16
Have you looked into infinitary logic
– Rob Arthan
Sep 30 '17 at 22:58
There is also work on how the incompleteness theorem breaks down if you admit non-recursive axiom systems for number theory.
– Rob Arthan
Sep 30 '17 at 23:22
@RobArthan I haven't heard the term "infinitary logic" although I've seen the general concept discussed. The first sentence from wikipedia makes me hesitant though, "allows infinitely long statements and/or infinitely long proofs" would suggest a required computing model strictly stronger than Turing Machines. I would expect the proof object itself to be of finite size. Can you clarify what a "non-recursive axiom system" is? Does that mean "non primitive recursive" or a computing model strictly stronger than Turing Machines ?
– DanielV
Oct 1 '17 at 0:18
Every first-order theory comes with an axiom set. If that set is recursive (its members are decided by some program) then the incompleteness theorems apply to it. But even if the set is not recursive, as long as it is semi-recursive (there is a program that accepts exactly its members) or equivalently recursively enumerable (it is the range of a program taken as a partial function), then as described in my post the incompleteness theorems still apply to it! @RobArthan, you may be interested in it too. Another natural question is how much non-computability is needed to obtain a complete theory.
– user21820
Oct 4 '17 at 5:08
|
show 2 more comments
I may also ask this question on the cs stackexchange because they also have a very dedicated logic section.
– DanielV
Sep 30 '17 at 18:16
Have you looked into infinitary logic
– Rob Arthan
Sep 30 '17 at 22:58
There is also work on how the incompleteness theorem breaks down if you admit non-recursive axiom systems for number theory.
– Rob Arthan
Sep 30 '17 at 23:22
@RobArthan I haven't heard the term "infinitary logic" although I've seen the general concept discussed. The first sentence from wikipedia makes me hesitant though, "allows infinitely long statements and/or infinitely long proofs" would suggest a required computing model strictly stronger than Turing Machines. I would expect the proof object itself to be of finite size. Can you clarify what a "non-recursive axiom system" is? Does that mean "non primitive recursive" or a computing model strictly stronger than Turing Machines ?
– DanielV
Oct 1 '17 at 0:18
Every first-order theory comes with an axiom set. If that set is recursive (its members are decided by some program) then the incompleteness theorems apply to it. But even if the set is not recursive, as long as it is semi-recursive (there is a program that accepts exactly its members) or equivalently recursively enumerable (it is the range of a program taken as a partial function), then as described in my post the incompleteness theorems still apply to it! @RobArthan, you may be interested in it too. Another natural question is how much non-computability is needed to obtain a complete theory.
– user21820
Oct 4 '17 at 5:08
I may also ask this question on the cs stackexchange because they also have a very dedicated logic section.
– DanielV
Sep 30 '17 at 18:16
I may also ask this question on the cs stackexchange because they also have a very dedicated logic section.
– DanielV
Sep 30 '17 at 18:16
Have you looked into infinitary logic
– Rob Arthan
Sep 30 '17 at 22:58
Have you looked into infinitary logic
– Rob Arthan
Sep 30 '17 at 22:58
There is also work on how the incompleteness theorem breaks down if you admit non-recursive axiom systems for number theory.
– Rob Arthan
Sep 30 '17 at 23:22
There is also work on how the incompleteness theorem breaks down if you admit non-recursive axiom systems for number theory.
– Rob Arthan
Sep 30 '17 at 23:22
@RobArthan I haven't heard the term "infinitary logic" although I've seen the general concept discussed. The first sentence from wikipedia makes me hesitant though, "allows infinitely long statements and/or infinitely long proofs" would suggest a required computing model strictly stronger than Turing Machines. I would expect the proof object itself to be of finite size. Can you clarify what a "non-recursive axiom system" is? Does that mean "non primitive recursive" or a computing model strictly stronger than Turing Machines ?
– DanielV
Oct 1 '17 at 0:18
@RobArthan I haven't heard the term "infinitary logic" although I've seen the general concept discussed. The first sentence from wikipedia makes me hesitant though, "allows infinitely long statements and/or infinitely long proofs" would suggest a required computing model strictly stronger than Turing Machines. I would expect the proof object itself to be of finite size. Can you clarify what a "non-recursive axiom system" is? Does that mean "non primitive recursive" or a computing model strictly stronger than Turing Machines ?
– DanielV
Oct 1 '17 at 0:18
Every first-order theory comes with an axiom set. If that set is recursive (its members are decided by some program) then the incompleteness theorems apply to it. But even if the set is not recursive, as long as it is semi-recursive (there is a program that accepts exactly its members) or equivalently recursively enumerable (it is the range of a program taken as a partial function), then as described in my post the incompleteness theorems still apply to it! @RobArthan, you may be interested in it too. Another natural question is how much non-computability is needed to obtain a complete theory.
– user21820
Oct 4 '17 at 5:08
Every first-order theory comes with an axiom set. If that set is recursive (its members are decided by some program) then the incompleteness theorems apply to it. But even if the set is not recursive, as long as it is semi-recursive (there is a program that accepts exactly its members) or equivalently recursively enumerable (it is the range of a program taken as a partial function), then as described in my post the incompleteness theorems still apply to it! @RobArthan, you may be interested in it too. Another natural question is how much non-computability is needed to obtain a complete theory.
– user21820
Oct 4 '17 at 5:08
|
show 2 more comments
1 Answer
1
active
oldest
votes
From the comments it seems that you want proof objects that are finite, even if they are potentially unverifiable. In the generalized incompleteness theorem a general formal system is simply a proof verifier program $V$ that halts on every input and accepts (the code of) $(x,y)$ iff $x$ is a (valid) proof of $y$. Your proposal then naturally corresponds to the idea of relaxing the requirement on $V$ and allowing it to not halt on inputs that it does not accept. It turns out that your proposal will still fall to the generalized incompleteness theorems, and we will have incompleteness for "verifiable" instead of "provable". Namely, we have the following results for your system $S$ where we say that $S vdash P$ iff there is a verifiable proof of $P$ over $S$:
You will never be able to use such a system to construct a program that decides the truth value (according to the meta-system) of every arithmetical sentence (or equivalently every sentence about finite binary strings) correctly. This follows easily from the unsolvability of the halting problem.
If $S$ interprets PA$^-$ (equivalently TC) via a computable translation $ι$ of arithmetical sentences into $S$, and if $S nvdash ι(0=1)$, then there is some arithmetical sentence $P$ such that $S nvdash ι(P)$ and $S nvdash ι(neg P)$. The proof is the same as for the generalized incompleteness theorem linked above, except that $G$ performs the executions of $V$ in parallel, and so it does not matter that $V$ does not halt when it is unable to verify a proof. Indeed the stipulation that $V$ does halt when the proof can be verified is the crucial reason the proof works. Compared to (1), this requires $S$ to interpret PA$^-$, but does not care whether $S$ proves (the translation of) false arithmetical sentences. In other words, having mere arithmetical consistency is enough to force $S$ to be arithmetically incomplete, even if $S$ is arithmetically unsound.
As mentioned in this more recent post explaining the generalized incompleteness theorem, the computability-based proof relativizes easily. So even if the proof verifier uses an uncomputable oracle, as long as the system can reason about programs using that same oracle, it will suffer incompleteness.
By the way, see this post for further discussion of reasons for or against wanting a foundational system to interpret $PA^-$, and a self-verifying theory of arithmetic that escapes incompleteness.
Anyway your questions are very interesting! I enjoyed thinking about them!
answered Oct 3 '17 at 11:32
user21820
38.7k543153
My internet was down for a while. I'm going to take some time to read through this.
– DanielV
Oct 4 '17 at 6:39
@DanielV: Does my answer make sense? Feel free to ask to clarify any point. =)
– user21820
Oct 10 '17 at 16:20
@DanielV: I recently posted this, which is a relatively rigorous statement and proof of Godel's and Rosser's incompleteness theorems in computability terms, which should hence be easy for you to understand.
– user21820
Nov 13 '17 at 8:02
@DanielV: Hi! I just came across this post again, and decided to update my answer.
– user21820
Nov 27 '18 at 16:38
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%2f2451864%2fpartially-verifiable-logic%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
From the comments it seems that you want proof objects that are finite, even if they are potentially unverifiable. In the generalized incompleteness theorem a general formal system is simply a proof verifier program $V$ that halts on every input and accepts (the code of) $(x,y)$ iff $x$ is a (valid) proof of $y$. Your proposal then naturally corresponds to the idea of relaxing the requirement on $V$ and allowing it to not halt on inputs that it does not accept. It turns out that your proposal will still fall to the generalized incompleteness theorems, and we will have incompleteness for "verifiable" instead of "provable". Namely, we have the following results for your system $S$ where we say that $S vdash P$ iff there is a verifiable proof of $P$ over $S$:
You will never be able to use such a system to construct a program that decides the truth value (according to the meta-system) of every arithmetical sentence (or equivalently every sentence about finite binary strings) correctly. This follows easily from the unsolvability of the halting problem.
If $S$ interprets PA$^-$ (equivalently TC) via a computable translation $ι$ of arithmetical sentences into $S$, and if $S nvdash ι(0=1)$, then there is some arithmetical sentence $P$ such that $S nvdash ι(P)$ and $S nvdash ι(neg P)$. The proof is the same as for the generalized incompleteness theorem linked above, except that $G$ performs the executions of $V$ in parallel, and so it does not matter that $V$ does not halt when it is unable to verify a proof. Indeed the stipulation that $V$ does halt when the proof can be verified is the crucial reason the proof works. Compared to (1), this requires $S$ to interpret PA$^-$, but does not care whether $S$ proves (the translation of) false arithmetical sentences. In other words, having mere arithmetical consistency is enough to force $S$ to be arithmetically incomplete, even if $S$ is arithmetically unsound.
As mentioned in this more recent post explaining the generalized incompleteness theorem, the computability-based proof relativizes easily. So even if the proof verifier uses an uncomputable oracle, as long as the system can reason about programs using that same oracle, it will suffer incompleteness.
By the way, see this post for further discussion of reasons for or against wanting a foundational system to interpret $PA^-$, and a self-verifying theory of arithmetic that escapes incompleteness.
Anyway your questions are very interesting! I enjoyed thinking about them!
answered Oct 3 '17 at 11:32
user21820
38.7k543153
My internet was down for a while. I'm going to take some time to read through this.
– DanielV
Oct 4 '17 at 6:39
@DanielV: Does my answer make sense? Feel free to ask to clarify any point. =)
– user21820
Oct 10 '17 at 16:20
@DanielV: I recently posted this, which is a relatively rigorous statement and proof of Godel's and Rosser's incompleteness theorems in computability terms, which should hence be easy for you to understand.
– user21820
Nov 13 '17 at 8:02
@DanielV: Hi! I just came across this post again, and decided to update my answer.
– user21820
Nov 27 '18 at 16:38
add a comment |
From the comments it seems that you want proof objects that are finite, even if they are potentially unverifiable. In the generalized incompleteness theorem a general formal system is simply a proof verifier program $V$ that halts on every input and accepts (the code of) $(x,y)$ iff $x$ is a (valid) proof of $y$. Your proposal then naturally corresponds to the idea of relaxing the requirement on $V$ and allowing it to not halt on inputs that it does not accept. It turns out that your proposal will still fall to the generalized incompleteness theorems, and we will have incompleteness for "verifiable" instead of "provable". Namely, we have the following results for your system $S$ where we say that $S vdash P$ iff there is a verifiable proof of $P$ over $S$:
You will never be able to use such a system to construct a program that decides the truth value (according to the meta-system) of every arithmetical sentence (or equivalently every sentence about finite binary strings) correctly. This follows easily from the unsolvability of the halting problem.
If $S$ interprets PA$^-$ (equivalently TC) via a computable translation $ι$ of arithmetical sentences into $S$, and if $S nvdash ι(0=1)$, then there is some arithmetical sentence $P$ such that $S nvdash ι(P)$ and $S nvdash ι(neg P)$. The proof is the same as for the generalized incompleteness theorem linked above, except that $G$ performs the executions of $V$ in parallel, and so it does not matter that $V$ does not halt when it is unable to verify a proof. Indeed the stipulation that $V$ does halt when the proof can be verified is the crucial reason the proof works. Compared to (1), this requires $S$ to interpret PA$^-$, but does not care whether $S$ proves (the translation of) false arithmetical sentences. In other words, having mere arithmetical consistency is enough to force $S$ to be arithmetically incomplete, even if $S$ is arithmetically unsound.
As mentioned in this more recent post explaining the generalized incompleteness theorem, the computability-based proof relativizes easily. So even if the proof verifier uses an uncomputable oracle, as long as the system can reason about programs using that same oracle, it will suffer incompleteness.
By the way, see this post for further discussion of reasons for or against wanting a foundational system to interpret $PA^-$, and a self-verifying theory of arithmetic that escapes incompleteness.
Anyway your questions are very interesting! I enjoyed thinking about them!
answered Oct 3 '17 at 11:32
user21820
38.7k543153
My internet was down for a while. I'm going to take some time to read through this.
– DanielV
Oct 4 '17 at 6:39
@DanielV: Does my answer make sense? Feel free to ask to clarify any point. =)
– user21820
Oct 10 '17 at 16:20
@DanielV: I recently posted this, which is a relatively rigorous statement and proof of Godel's and Rosser's incompleteness theorems in computability terms, which should hence be easy for you to understand.
– user21820
Nov 13 '17 at 8:02
@DanielV: Hi! I just came across this post again, and decided to update my answer.
– user21820
Nov 27 '18 at 16:38
add a comment |
From the comments it seems that you want proof objects that are finite, even if they are potentially unverifiable. In the generalized incompleteness theorem a general formal system is simply a proof verifier program $V$ that halts on every input and accepts (the code of) $(x,y)$ iff $x$ is a (valid) proof of $y$. Your proposal then naturally corresponds to the idea of relaxing the requirement on $V$ and allowing it to not halt on inputs that it does not accept. It turns out that your proposal will still fall to the generalized incompleteness theorems, and we will have incompleteness for "verifiable" instead of "provable". Namely, we have the following results for your system $S$ where we say that $S vdash P$ iff there is a verifiable proof of $P$ over $S$:
You will never be able to use such a system to construct a program that decides the truth value (according to the meta-system) of every arithmetical sentence (or equivalently every sentence about finite binary strings) correctly. This follows easily from the unsolvability of the halting problem.
If $S$ interprets PA$^-$ (equivalently TC) via a computable translation $ι$ of arithmetical sentences into $S$, and if $S nvdash ι(0=1)$, then there is some arithmetical sentence $P$ such that $S nvdash ι(P)$ and $S nvdash ι(neg P)$. The proof is the same as for the generalized incompleteness theorem linked above, except that $G$ performs the executions of $V$ in parallel, and so it does not matter that $V$ does not halt when it is unable to verify a proof. Indeed the stipulation that $V$ does halt when the proof can be verified is the crucial reason the proof works. Compared to (1), this requires $S$ to interpret PA$^-$, but does not care whether $S$ proves (the translation of) false arithmetical sentences. In other words, having mere arithmetical consistency is enough to force $S$ to be arithmetically incomplete, even if $S$ is arithmetically unsound.
As mentioned in this more recent post explaining the generalized incompleteness theorem, the computability-based proof relativizes easily. So even if the proof verifier uses an uncomputable oracle, as long as the system can reason about programs using that same oracle, it will suffer incompleteness.
By the way, see this post for further discussion of reasons for or against wanting a foundational system to interpret $PA^-$, and a self-verifying theory of arithmetic that escapes incompleteness.
Anyway your questions are very interesting! I enjoyed thinking about them!
answered Oct 3 '17 at 11:32
user21820
38.7k543153
From the comments it seems that you want proof objects that are finite, even if they are potentially unverifiable. In the generalized incompleteness theorem a general formal system is simply a proof verifier program $V$ that halts on every input and accepts (the code of) $(x,y)$ iff $x$ is a (valid) proof of $y$. Your proposal then naturally corresponds to the idea of relaxing the requirement on $V$ and allowing it to not halt on inputs that it does not accept. It turns out that your proposal will still fall to the generalized incompleteness theorems, and we will have incompleteness for "verifiable" instead of "provable". Namely, we have the following results for your system $S$ where we say that $S vdash P$ iff there is a verifiable proof of $P$ over $S$:
You will never be able to use such a system to construct a program that decides the truth value (according to the meta-system) of every arithmetical sentence (or equivalently every sentence about finite binary strings) correctly. This follows easily from the unsolvability of the halting problem.
If $S$ interprets PA$^-$ (equivalently TC) via a computable translation $ι$ of arithmetical sentences into $S$, and if $S nvdash ι(0=1)$, then there is some arithmetical sentence $P$ such that $S nvdash ι(P)$ and $S nvdash ι(neg P)$. The proof is the same as for the generalized incompleteness theorem linked above, except that $G$ performs the executions of $V$ in parallel, and so it does not matter that $V$ does not halt when it is unable to verify a proof. Indeed the stipulation that $V$ does halt when the proof can be verified is the crucial reason the proof works. Compared to (1), this requires $S$ to interpret PA$^-$, but does not care whether $S$ proves (the translation of) false arithmetical sentences. In other words, having mere arithmetical consistency is enough to force $S$ to be arithmetically incomplete, even if $S$ is arithmetically unsound.
As mentioned in this more recent post explaining the generalized incompleteness theorem, the computability-based proof relativizes easily. So even if the proof verifier uses an uncomputable oracle, as long as the system can reason about programs using that same oracle, it will suffer incompleteness.
By the way, see this post for further discussion of reasons for or against wanting a foundational system to interpret $PA^-$, and a self-verifying theory of arithmetic that escapes incompleteness.
Anyway your questions are very interesting! I enjoyed thinking about them!
answered Oct 3 '17 at 11:32
user21820
38.7k543153
edited Nov 27 '18 at 16:37
answered Oct 3 '17 at 11:32
user21820
38.7k543153
answered Oct 3 '17 at 11:32
user21820
38.7k543153
answered Oct 3 '17 at 11:32
user21820
38.7k543153
38.7k543153
My internet was down for a while. I'm going to take some time to read through this.
– DanielV
Oct 4 '17 at 6:39
@DanielV: Does my answer make sense? Feel free to ask to clarify any point. =)
– user21820
Oct 10 '17 at 16:20
@DanielV: I recently posted this, which is a relatively rigorous statement and proof of Godel's and Rosser's incompleteness theorems in computability terms, which should hence be easy for you to understand.
– user21820
Nov 13 '17 at 8:02
@DanielV: Hi! I just came across this post again, and decided to update my answer.
– user21820
Nov 27 '18 at 16:38
add a comment |
My internet was down for a while. I'm going to take some time to read through this.
– DanielV
Oct 4 '17 at 6:39
@DanielV: Does my answer make sense? Feel free to ask to clarify any point. =)
– user21820
Oct 10 '17 at 16:20
@DanielV: I recently posted this, which is a relatively rigorous statement and proof of Godel's and Rosser's incompleteness theorems in computability terms, which should hence be easy for you to understand.
– user21820
Nov 13 '17 at 8:02
@DanielV: Hi! I just came across this post again, and decided to update my answer.
– user21820
Nov 27 '18 at 16:38
My internet was down for a while. I'm going to take some time to read through this.
– DanielV
Oct 4 '17 at 6:39
My internet was down for a while. I'm going to take some time to read through this.
– DanielV
Oct 4 '17 at 6:39
@DanielV: Does my answer make sense? Feel free to ask to clarify any point. =)
– user21820
Oct 10 '17 at 16:20
@DanielV: Does my answer make sense? Feel free to ask to clarify any point. =)
– user21820
Oct 10 '17 at 16:20
@DanielV: I recently posted this, which is a relatively rigorous statement and proof of Godel's and Rosser's incompleteness theorems in computability terms, which should hence be easy for you to understand.
– user21820
Nov 13 '17 at 8:02
@DanielV: I recently posted this, which is a relatively rigorous statement and proof of Godel's and Rosser's incompleteness theorems in computability terms, which should hence be easy for you to understand.
– user21820
Nov 13 '17 at 8:02
@DanielV: Hi! I just came across this post again, and decided to update my answer.
– user21820
Nov 27 '18 at 16:38
@DanielV: Hi! I just came across this post again, and decided to update my answer.
– user21820
Nov 27 '18 at 16:38
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%2f2451864%2fpartially-verifiable-logic%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
I may also ask this question on the cs stackexchange because they also have a very dedicated logic section.
– DanielV
Sep 30 '17 at 18:16
Have you looked into infinitary logic
– Rob Arthan
Sep 30 '17 at 22:58
There is also work on how the incompleteness theorem breaks down if you admit non-recursive axiom systems for number theory.
– Rob Arthan
Sep 30 '17 at 23:22
@RobArthan I haven't heard the term "infinitary logic" although I've seen the general concept discussed. The first sentence from wikipedia makes me hesitant though, "allows infinitely long statements and/or infinitely long proofs" would suggest a required computing model strictly stronger than Turing Machines. I would expect the proof object itself to be of finite size. Can you clarify what a "non-recursive axiom system" is? Does that mean "non primitive recursive" or a computing model strictly stronger than Turing Machines ?
– DanielV
Oct 1 '17 at 0:18
Every first-order theory comes with an axiom set. If that set is recursive (its members are decided by some program) then the incompleteness theorems apply to it. But even if the set is not recursive, as long as it is semi-recursive (there is a program that accepts exactly its members) or equivalently recursively enumerable (it is the range of a program taken as a partial function), then as described in my post the incompleteness theorems still apply to it! @RobArthan, you may be interested in it too. Another natural question is how much non-computability is needed to obtain a complete theory.
– user21820
Oct 4 '17 at 5:08