Mixing
Does semantic inconsistency guarantee syntactic inconsistency?
$begingroup$
I'm wondering about the possibility of circumventing the problem of incompleteness posed by Roger Penrose in his book "Shadows of the Mind".
It occurred to me (and, Googling has revealed to me, others) that you can purchase a formal system's completeness as the price of consistency, if you adopt a paraconsistent logic and a "falsificationist" approach by which your aim is to find consistent subsets of all your enumerable propositions. This seems to me to be exactly what human beings are doing when they "intuit" the truth of the Gödelian sentence. I don't yet know enough about logic to fully develop the idea, however.
In particular, it seems to me that for a falsificationist approach to work, you need to have it such that $(Gamma models perp) rightarrow (Gamma vdash perp)$ in order to guarantee (or at least render highly probable) that you will eventually discover an inconsistency in your system, if it exists.
It seems that for any system with an effective procedure for determining if $Gamma models phi$ for some $phi$, the requirement is met since for a procedure to be "effective" it (caveat: seems to me) that it would have to be equivalent to some kind of syntactic manipulation of the formulae in $Gamma$.
In addition to a straightforward "yes", "no", "you're asking the wrong question", etc. style of answer I'd also highly appreciate links to the literature concerning work on the above problem specifically.
(EDIT) I've found another question which bears rather directly on this one, here: Gödel's Completeness Theorem and logical consequence
logic computability incompleteness
edited Apr 13 '17 at 12:20
Community♦
1
asked Jun 20 '15 at 11:56
Dion BridgerDion Bridger
926
$endgroup$
add a comment |
$begingroup$
I'm wondering about the possibility of circumventing the problem of incompleteness posed by Roger Penrose in his book "Shadows of the Mind".
It occurred to me (and, Googling has revealed to me, others) that you can purchase a formal system's completeness as the price of consistency, if you adopt a paraconsistent logic and a "falsificationist" approach by which your aim is to find consistent subsets of all your enumerable propositions. This seems to me to be exactly what human beings are doing when they "intuit" the truth of the Gödelian sentence. I don't yet know enough about logic to fully develop the idea, however.
In particular, it seems to me that for a falsificationist approach to work, you need to have it such that $(Gamma models perp) rightarrow (Gamma vdash perp)$ in order to guarantee (or at least render highly probable) that you will eventually discover an inconsistency in your system, if it exists.
It seems that for any system with an effective procedure for determining if $Gamma models phi$ for some $phi$, the requirement is met since for a procedure to be "effective" it (caveat: seems to me) that it would have to be equivalent to some kind of syntactic manipulation of the formulae in $Gamma$.
In addition to a straightforward "yes", "no", "you're asking the wrong question", etc. style of answer I'd also highly appreciate links to the literature concerning work on the above problem specifically.
(EDIT) I've found another question which bears rather directly on this one, here: Gödel's Completeness Theorem and logical consequence
logic computability incompleteness
edited Apr 13 '17 at 12:20
Community♦
1
asked Jun 20 '15 at 11:56
Dion BridgerDion Bridger
926
$endgroup$
add a comment |
$begingroup$
I'm wondering about the possibility of circumventing the problem of incompleteness posed by Roger Penrose in his book "Shadows of the Mind".
It occurred to me (and, Googling has revealed to me, others) that you can purchase a formal system's completeness as the price of consistency, if you adopt a paraconsistent logic and a "falsificationist" approach by which your aim is to find consistent subsets of all your enumerable propositions. This seems to me to be exactly what human beings are doing when they "intuit" the truth of the Gödelian sentence. I don't yet know enough about logic to fully develop the idea, however.
In particular, it seems to me that for a falsificationist approach to work, you need to have it such that $(Gamma models perp) rightarrow (Gamma vdash perp)$ in order to guarantee (or at least render highly probable) that you will eventually discover an inconsistency in your system, if it exists.
It seems that for any system with an effective procedure for determining if $Gamma models phi$ for some $phi$, the requirement is met since for a procedure to be "effective" it (caveat: seems to me) that it would have to be equivalent to some kind of syntactic manipulation of the formulae in $Gamma$.
In addition to a straightforward "yes", "no", "you're asking the wrong question", etc. style of answer I'd also highly appreciate links to the literature concerning work on the above problem specifically.
(EDIT) I've found another question which bears rather directly on this one, here: Gödel's Completeness Theorem and logical consequence
logic computability incompleteness
edited Apr 13 '17 at 12:20
Community♦
1
asked Jun 20 '15 at 11:56
Dion BridgerDion Bridger
926
$endgroup$
I'm wondering about the possibility of circumventing the problem of incompleteness posed by Roger Penrose in his book "Shadows of the Mind".
It occurred to me (and, Googling has revealed to me, others) that you can purchase a formal system's completeness as the price of consistency, if you adopt a paraconsistent logic and a "falsificationist" approach by which your aim is to find consistent subsets of all your enumerable propositions. This seems to me to be exactly what human beings are doing when they "intuit" the truth of the Gödelian sentence. I don't yet know enough about logic to fully develop the idea, however.
In particular, it seems to me that for a falsificationist approach to work, you need to have it such that $(Gamma models perp) rightarrow (Gamma vdash perp)$ in order to guarantee (or at least render highly probable) that you will eventually discover an inconsistency in your system, if it exists.
It seems that for any system with an effective procedure for determining if $Gamma models phi$ for some $phi$, the requirement is met since for a procedure to be "effective" it (caveat: seems to me) that it would have to be equivalent to some kind of syntactic manipulation of the formulae in $Gamma$.
In addition to a straightforward "yes", "no", "you're asking the wrong question", etc. style of answer I'd also highly appreciate links to the literature concerning work on the above problem specifically.
(EDIT) I've found another question which bears rather directly on this one, here: Gödel's Completeness Theorem and logical consequence
logic computability incompleteness
logic computability incompleteness
edited Apr 13 '17 at 12:20
Community♦
1
asked Jun 20 '15 at 11:56
Dion BridgerDion Bridger
926
edited Apr 13 '17 at 12:20
Community♦
1
asked Jun 20 '15 at 11:56
Dion BridgerDion Bridger
926
edited Apr 13 '17 at 12:20
Community♦
1
edited Apr 13 '17 at 12:20
Community♦
1
edited Apr 13 '17 at 12:20
Community♦
1
1
asked Jun 20 '15 at 11:56
Dion BridgerDion Bridger
926
asked Jun 20 '15 at 11:56
Dion BridgerDion Bridger
926
asked Jun 20 '15 at 11:56
Dion BridgerDion Bridger
926
926
add a comment |
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
This is the content of Godel's completeness theorem. $Tmodelsvarphi$ if and only if $Tvdashvarphi$, at least when we are discussing first-order logic. Note, by the way, that since there is no structure which satisfies $bot$, so writing $Tmodelsbot$ means by definition that $T$ has no models.
Interestingly, this is something which hinges on the axiom of choice. Namely, the proof of the completeness theorem uses the axiom of choice. To see how the implication you're interested in uses the axiom of choice, consider the case there exists a set $A$ which cannot be linearly ordered (something which strongly contradicts the axiom of choice).
Let $mathcal L_A$ is the language with constants ${c_amid ain A}$ and a binary relation symbol $<$. Now take $T$ to be the theory stating that $c_aneq c_b$ for $aneq b$ and $<$ is a linear ordering of the universe. This theory is finitely satisfiable, so it cannot prove $bot$; but it has no models since from a model of $T$ we obtain a linear ordering of $A$. (Note that the language here is uncountable, since $A$ is uncountable. If $cal L$ is a countable language in first-order logic, then the completeness theorem for $cal L$-theories is in fact "choice free". So for things like arithmetics we don't use the axiom of choice.)
Finally, let me point out that incompleteness here in the sense of Godelian sentences and Godel-Rosser sentences, have nothing to do with the completeness of the underlying logic, or the completeness/consistency of a theory. Those are different type of completeness (and lack thereof), and they should not be confused.
answered Jun 20 '15 at 12:05
Asaf Karagila♦Asaf Karagila
305k33435766
$endgroup$
$begingroup$
Very useful, thank you. The completeness theorem isn't very much talked about in the "popular" literature; which just goes to show that you should never try and form an opinion on the basis of non-technical literature! One thing that isn't clear to me from your answer is whether abandoning the requirement that your $T$ be consistent, as in paraconsistent logics, damages the proof of completeness. Presumably the axiom of choice holds for the logical constants of paraconsistent logics & thus the completeness proof follows?
$endgroup$
– Dion Bridger
Jun 20 '15 at 12:21
3
$begingroup$
If we restrict our attention to languages with a countable vocabulary, though (which is all we ever ought to need to model actual mathematical proofs), the completeness theorem doesn't require choice.
$endgroup$
– Henning Makholm
Jun 20 '15 at 12:21
$begingroup$
@Dion: Yeah, that's a good lesson for life!
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@Henning: That's a good point, I'll add it.
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@AsafKaragila Is there an easy way to see that in a failure of choice you can have a set with no linear orderings?
$endgroup$
– James
Jun 20 '15 at 12:33
|
show 3 more comments
$begingroup$
I would like to add another answer to this focussing on the case of countable languages, because that is the usual context of logic and also of the Penrose argument.
Indeed the question is asking about the Completeness Theorem ($vdash$ implies $models$) of First Order Logic, and whether it is always valid. In fact my own question asked about whether this theorem was constructive ie fully effective as I had been learning about Reverse Mathematics and the result that Completeness depended on a non-constructive axiom known as WKL (Weak Konig's Lemma). As your linked remark shows historic Logic literature has been confused about the relationship between $models$ and $vdash$. To summarise the reason:
First Order Logic can be formalised in a weak framework called RCA which captures computability. Many theorems (and meta-theorems) can be proven in RCA including the Soundness Theorem ($models$ implies $vdash$) of First Order Logic.
However Completeness requires WKL and is not provable in RCA.
An immediate consequence of this is that $models$ and $vdash$ are not interchangeable (unless one assumes WKL).
Another consequence is that if a theory is consistent it cannot be established constructively that it has a model. In fact the model building process does involve an element of choice, although the ZF Axiom of Choice is not involved. The choice principle involved is mentioned in the Reverse Mathematics book and called "Strong $Pi_{1}^{0}$ dependent choice" and is a (meta-)corollary of WKL.
However partial models can be built constructively (whose elements are either True or False), but extending this to all properties cannot be achieved. So for any such partial model there will exist a property p_k such that p_k(k) will map to {True,False} in our model, rather than to a specific truth value.
The fact that p_k(k) maps to {True,False} opens the door to 3-valued logics (in which p_k(k) is undefined) or to paraconsistent logics (in which p_k(k) is both True and False).
If one starts with a paraconsistent logic PL then it has also been argued that Godel's Incompleteness Theorem will not hold for PL (since its proof would require that inconsistency is impossible).
In the Penrose argument, in Artificial Intelligence and in Computer Science/Software Engineering more generally constructive logics are central, though 2-valuedness - although natural and desirable - cannot be guaranteed. In a sense it is the WKL axiom which introduces 2-valuedness across logic, but it does so non-constructively, leaving room for much further debate and investigation into this area.
answered Jan 18 at 13:51
Roy SimpsonRoy Simpson
338111
$endgroup$
$begingroup$
This comment has been extremely valuable to me, though I cannot remark on it in detail at present. Reverse mathematics looks extremely interesting. Thank you.
$endgroup$
– Dion Bridger
Jan 20 at 22: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%2f1332552%2fdoes-semantic-inconsistency-guarantee-syntactic-inconsistency%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
This is the content of Godel's completeness theorem. $Tmodelsvarphi$ if and only if $Tvdashvarphi$, at least when we are discussing first-order logic. Note, by the way, that since there is no structure which satisfies $bot$, so writing $Tmodelsbot$ means by definition that $T$ has no models.
Interestingly, this is something which hinges on the axiom of choice. Namely, the proof of the completeness theorem uses the axiom of choice. To see how the implication you're interested in uses the axiom of choice, consider the case there exists a set $A$ which cannot be linearly ordered (something which strongly contradicts the axiom of choice).
Let $mathcal L_A$ is the language with constants ${c_amid ain A}$ and a binary relation symbol $<$. Now take $T$ to be the theory stating that $c_aneq c_b$ for $aneq b$ and $<$ is a linear ordering of the universe. This theory is finitely satisfiable, so it cannot prove $bot$; but it has no models since from a model of $T$ we obtain a linear ordering of $A$. (Note that the language here is uncountable, since $A$ is uncountable. If $cal L$ is a countable language in first-order logic, then the completeness theorem for $cal L$-theories is in fact "choice free". So for things like arithmetics we don't use the axiom of choice.)
Finally, let me point out that incompleteness here in the sense of Godelian sentences and Godel-Rosser sentences, have nothing to do with the completeness of the underlying logic, or the completeness/consistency of a theory. Those are different type of completeness (and lack thereof), and they should not be confused.
answered Jun 20 '15 at 12:05
Asaf Karagila♦Asaf Karagila
305k33435766
$endgroup$
$begingroup$
Very useful, thank you. The completeness theorem isn't very much talked about in the "popular" literature; which just goes to show that you should never try and form an opinion on the basis of non-technical literature! One thing that isn't clear to me from your answer is whether abandoning the requirement that your $T$ be consistent, as in paraconsistent logics, damages the proof of completeness. Presumably the axiom of choice holds for the logical constants of paraconsistent logics & thus the completeness proof follows?
$endgroup$
– Dion Bridger
Jun 20 '15 at 12:21
3
$begingroup$
If we restrict our attention to languages with a countable vocabulary, though (which is all we ever ought to need to model actual mathematical proofs), the completeness theorem doesn't require choice.
$endgroup$
– Henning Makholm
Jun 20 '15 at 12:21
$begingroup$
@Dion: Yeah, that's a good lesson for life!
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@Henning: That's a good point, I'll add it.
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@AsafKaragila Is there an easy way to see that in a failure of choice you can have a set with no linear orderings?
$endgroup$
– James
Jun 20 '15 at 12:33
|
show 3 more comments
$begingroup$
This is the content of Godel's completeness theorem. $Tmodelsvarphi$ if and only if $Tvdashvarphi$, at least when we are discussing first-order logic. Note, by the way, that since there is no structure which satisfies $bot$, so writing $Tmodelsbot$ means by definition that $T$ has no models.
Interestingly, this is something which hinges on the axiom of choice. Namely, the proof of the completeness theorem uses the axiom of choice. To see how the implication you're interested in uses the axiom of choice, consider the case there exists a set $A$ which cannot be linearly ordered (something which strongly contradicts the axiom of choice).
Let $mathcal L_A$ is the language with constants ${c_amid ain A}$ and a binary relation symbol $<$. Now take $T$ to be the theory stating that $c_aneq c_b$ for $aneq b$ and $<$ is a linear ordering of the universe. This theory is finitely satisfiable, so it cannot prove $bot$; but it has no models since from a model of $T$ we obtain a linear ordering of $A$. (Note that the language here is uncountable, since $A$ is uncountable. If $cal L$ is a countable language in first-order logic, then the completeness theorem for $cal L$-theories is in fact "choice free". So for things like arithmetics we don't use the axiom of choice.)
Finally, let me point out that incompleteness here in the sense of Godelian sentences and Godel-Rosser sentences, have nothing to do with the completeness of the underlying logic, or the completeness/consistency of a theory. Those are different type of completeness (and lack thereof), and they should not be confused.
answered Jun 20 '15 at 12:05
Asaf Karagila♦Asaf Karagila
305k33435766
$endgroup$
$begingroup$
Very useful, thank you. The completeness theorem isn't very much talked about in the "popular" literature; which just goes to show that you should never try and form an opinion on the basis of non-technical literature! One thing that isn't clear to me from your answer is whether abandoning the requirement that your $T$ be consistent, as in paraconsistent logics, damages the proof of completeness. Presumably the axiom of choice holds for the logical constants of paraconsistent logics & thus the completeness proof follows?
$endgroup$
– Dion Bridger
Jun 20 '15 at 12:21
3
$begingroup$
If we restrict our attention to languages with a countable vocabulary, though (which is all we ever ought to need to model actual mathematical proofs), the completeness theorem doesn't require choice.
$endgroup$
– Henning Makholm
Jun 20 '15 at 12:21
$begingroup$
@Dion: Yeah, that's a good lesson for life!
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@Henning: That's a good point, I'll add it.
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@AsafKaragila Is there an easy way to see that in a failure of choice you can have a set with no linear orderings?
$endgroup$
– James
Jun 20 '15 at 12:33
|
show 3 more comments
$begingroup$
This is the content of Godel's completeness theorem. $Tmodelsvarphi$ if and only if $Tvdashvarphi$, at least when we are discussing first-order logic. Note, by the way, that since there is no structure which satisfies $bot$, so writing $Tmodelsbot$ means by definition that $T$ has no models.
Interestingly, this is something which hinges on the axiom of choice. Namely, the proof of the completeness theorem uses the axiom of choice. To see how the implication you're interested in uses the axiom of choice, consider the case there exists a set $A$ which cannot be linearly ordered (something which strongly contradicts the axiom of choice).
Let $mathcal L_A$ is the language with constants ${c_amid ain A}$ and a binary relation symbol $<$. Now take $T$ to be the theory stating that $c_aneq c_b$ for $aneq b$ and $<$ is a linear ordering of the universe. This theory is finitely satisfiable, so it cannot prove $bot$; but it has no models since from a model of $T$ we obtain a linear ordering of $A$. (Note that the language here is uncountable, since $A$ is uncountable. If $cal L$ is a countable language in first-order logic, then the completeness theorem for $cal L$-theories is in fact "choice free". So for things like arithmetics we don't use the axiom of choice.)
Finally, let me point out that incompleteness here in the sense of Godelian sentences and Godel-Rosser sentences, have nothing to do with the completeness of the underlying logic, or the completeness/consistency of a theory. Those are different type of completeness (and lack thereof), and they should not be confused.
answered Jun 20 '15 at 12:05
Asaf Karagila♦Asaf Karagila
305k33435766
$endgroup$
This is the content of Godel's completeness theorem. $Tmodelsvarphi$ if and only if $Tvdashvarphi$, at least when we are discussing first-order logic. Note, by the way, that since there is no structure which satisfies $bot$, so writing $Tmodelsbot$ means by definition that $T$ has no models.
Interestingly, this is something which hinges on the axiom of choice. Namely, the proof of the completeness theorem uses the axiom of choice. To see how the implication you're interested in uses the axiom of choice, consider the case there exists a set $A$ which cannot be linearly ordered (something which strongly contradicts the axiom of choice).
Let $mathcal L_A$ is the language with constants ${c_amid ain A}$ and a binary relation symbol $<$. Now take $T$ to be the theory stating that $c_aneq c_b$ for $aneq b$ and $<$ is a linear ordering of the universe. This theory is finitely satisfiable, so it cannot prove $bot$; but it has no models since from a model of $T$ we obtain a linear ordering of $A$. (Note that the language here is uncountable, since $A$ is uncountable. If $cal L$ is a countable language in first-order logic, then the completeness theorem for $cal L$-theories is in fact "choice free". So for things like arithmetics we don't use the axiom of choice.)
Finally, let me point out that incompleteness here in the sense of Godelian sentences and Godel-Rosser sentences, have nothing to do with the completeness of the underlying logic, or the completeness/consistency of a theory. Those are different type of completeness (and lack thereof), and they should not be confused.
answered Jun 20 '15 at 12:05
Asaf Karagila♦Asaf Karagila
305k33435766
edited Jun 20 '15 at 12:24
answered Jun 20 '15 at 12:05
Asaf Karagila♦Asaf Karagila
305k33435766
answered Jun 20 '15 at 12:05
Asaf Karagila♦Asaf Karagila
305k33435766
answered Jun 20 '15 at 12:05
Asaf Karagila♦Asaf Karagila
305k33435766
305k33435766
$begingroup$
Very useful, thank you. The completeness theorem isn't very much talked about in the "popular" literature; which just goes to show that you should never try and form an opinion on the basis of non-technical literature! One thing that isn't clear to me from your answer is whether abandoning the requirement that your $T$ be consistent, as in paraconsistent logics, damages the proof of completeness. Presumably the axiom of choice holds for the logical constants of paraconsistent logics & thus the completeness proof follows?
$endgroup$
– Dion Bridger
Jun 20 '15 at 12:21
3
$begingroup$
If we restrict our attention to languages with a countable vocabulary, though (which is all we ever ought to need to model actual mathematical proofs), the completeness theorem doesn't require choice.
$endgroup$
– Henning Makholm
Jun 20 '15 at 12:21
$begingroup$
@Dion: Yeah, that's a good lesson for life!
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@Henning: That's a good point, I'll add it.
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@AsafKaragila Is there an easy way to see that in a failure of choice you can have a set with no linear orderings?
$endgroup$
– James
Jun 20 '15 at 12:33
|
show 3 more comments
$begingroup$
Very useful, thank you. The completeness theorem isn't very much talked about in the "popular" literature; which just goes to show that you should never try and form an opinion on the basis of non-technical literature! One thing that isn't clear to me from your answer is whether abandoning the requirement that your $T$ be consistent, as in paraconsistent logics, damages the proof of completeness. Presumably the axiom of choice holds for the logical constants of paraconsistent logics & thus the completeness proof follows?
$endgroup$
– Dion Bridger
Jun 20 '15 at 12:21
3
$begingroup$
If we restrict our attention to languages with a countable vocabulary, though (which is all we ever ought to need to model actual mathematical proofs), the completeness theorem doesn't require choice.
$endgroup$
– Henning Makholm
Jun 20 '15 at 12:21
$begingroup$
@Dion: Yeah, that's a good lesson for life!
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@Henning: That's a good point, I'll add it.
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@AsafKaragila Is there an easy way to see that in a failure of choice you can have a set with no linear orderings?
$endgroup$
– James
Jun 20 '15 at 12:33
$begingroup$
Very useful, thank you. The completeness theorem isn't very much talked about in the "popular" literature; which just goes to show that you should never try and form an opinion on the basis of non-technical literature! One thing that isn't clear to me from your answer is whether abandoning the requirement that your $T$ be consistent, as in paraconsistent logics, damages the proof of completeness. Presumably the axiom of choice holds for the logical constants of paraconsistent logics & thus the completeness proof follows?
$endgroup$
– Dion Bridger
Jun 20 '15 at 12:21
$begingroup$
Very useful, thank you. The completeness theorem isn't very much talked about in the "popular" literature; which just goes to show that you should never try and form an opinion on the basis of non-technical literature! One thing that isn't clear to me from your answer is whether abandoning the requirement that your $T$ be consistent, as in paraconsistent logics, damages the proof of completeness. Presumably the axiom of choice holds for the logical constants of paraconsistent logics & thus the completeness proof follows?
$endgroup$
– Dion Bridger
Jun 20 '15 at 12:21
3
3
$begingroup$
If we restrict our attention to languages with a countable vocabulary, though (which is all we ever ought to need to model actual mathematical proofs), the completeness theorem doesn't require choice.
$endgroup$
– Henning Makholm
Jun 20 '15 at 12:21
$begingroup$
If we restrict our attention to languages with a countable vocabulary, though (which is all we ever ought to need to model actual mathematical proofs), the completeness theorem doesn't require choice.
$endgroup$
– Henning Makholm
Jun 20 '15 at 12:21
$begingroup$
@Dion: Yeah, that's a good lesson for life!
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@Dion: Yeah, that's a good lesson for life!
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@Henning: That's a good point, I'll add it.
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@Henning: That's a good point, I'll add it.
$endgroup$
– Asaf Karagila♦
Jun 20 '15 at 12:22
$begingroup$
@AsafKaragila Is there an easy way to see that in a failure of choice you can have a set with no linear orderings?
$endgroup$
– James
Jun 20 '15 at 12:33
$begingroup$
@AsafKaragila Is there an easy way to see that in a failure of choice you can have a set with no linear orderings?
$endgroup$
– James
Jun 20 '15 at 12:33
|
show 3 more comments
$begingroup$
I would like to add another answer to this focussing on the case of countable languages, because that is the usual context of logic and also of the Penrose argument.
Indeed the question is asking about the Completeness Theorem ($vdash$ implies $models$) of First Order Logic, and whether it is always valid. In fact my own question asked about whether this theorem was constructive ie fully effective as I had been learning about Reverse Mathematics and the result that Completeness depended on a non-constructive axiom known as WKL (Weak Konig's Lemma). As your linked remark shows historic Logic literature has been confused about the relationship between $models$ and $vdash$. To summarise the reason:
First Order Logic can be formalised in a weak framework called RCA which captures computability. Many theorems (and meta-theorems) can be proven in RCA including the Soundness Theorem ($models$ implies $vdash$) of First Order Logic.
However Completeness requires WKL and is not provable in RCA.
An immediate consequence of this is that $models$ and $vdash$ are not interchangeable (unless one assumes WKL).
Another consequence is that if a theory is consistent it cannot be established constructively that it has a model. In fact the model building process does involve an element of choice, although the ZF Axiom of Choice is not involved. The choice principle involved is mentioned in the Reverse Mathematics book and called "Strong $Pi_{1}^{0}$ dependent choice" and is a (meta-)corollary of WKL.
However partial models can be built constructively (whose elements are either True or False), but extending this to all properties cannot be achieved. So for any such partial model there will exist a property p_k such that p_k(k) will map to {True,False} in our model, rather than to a specific truth value.
The fact that p_k(k) maps to {True,False} opens the door to 3-valued logics (in which p_k(k) is undefined) or to paraconsistent logics (in which p_k(k) is both True and False).
If one starts with a paraconsistent logic PL then it has also been argued that Godel's Incompleteness Theorem will not hold for PL (since its proof would require that inconsistency is impossible).
In the Penrose argument, in Artificial Intelligence and in Computer Science/Software Engineering more generally constructive logics are central, though 2-valuedness - although natural and desirable - cannot be guaranteed. In a sense it is the WKL axiom which introduces 2-valuedness across logic, but it does so non-constructively, leaving room for much further debate and investigation into this area.
answered Jan 18 at 13:51
Roy SimpsonRoy Simpson
338111
$endgroup$
$begingroup$
This comment has been extremely valuable to me, though I cannot remark on it in detail at present. Reverse mathematics looks extremely interesting. Thank you.
$endgroup$
– Dion Bridger
Jan 20 at 22:38
add a comment |
$begingroup$
I would like to add another answer to this focussing on the case of countable languages, because that is the usual context of logic and also of the Penrose argument.
Indeed the question is asking about the Completeness Theorem ($vdash$ implies $models$) of First Order Logic, and whether it is always valid. In fact my own question asked about whether this theorem was constructive ie fully effective as I had been learning about Reverse Mathematics and the result that Completeness depended on a non-constructive axiom known as WKL (Weak Konig's Lemma). As your linked remark shows historic Logic literature has been confused about the relationship between $models$ and $vdash$. To summarise the reason:
First Order Logic can be formalised in a weak framework called RCA which captures computability. Many theorems (and meta-theorems) can be proven in RCA including the Soundness Theorem ($models$ implies $vdash$) of First Order Logic.
However Completeness requires WKL and is not provable in RCA.
An immediate consequence of this is that $models$ and $vdash$ are not interchangeable (unless one assumes WKL).
Another consequence is that if a theory is consistent it cannot be established constructively that it has a model. In fact the model building process does involve an element of choice, although the ZF Axiom of Choice is not involved. The choice principle involved is mentioned in the Reverse Mathematics book and called "Strong $Pi_{1}^{0}$ dependent choice" and is a (meta-)corollary of WKL.
However partial models can be built constructively (whose elements are either True or False), but extending this to all properties cannot be achieved. So for any such partial model there will exist a property p_k such that p_k(k) will map to {True,False} in our model, rather than to a specific truth value.
The fact that p_k(k) maps to {True,False} opens the door to 3-valued logics (in which p_k(k) is undefined) or to paraconsistent logics (in which p_k(k) is both True and False).
If one starts with a paraconsistent logic PL then it has also been argued that Godel's Incompleteness Theorem will not hold for PL (since its proof would require that inconsistency is impossible).
In the Penrose argument, in Artificial Intelligence and in Computer Science/Software Engineering more generally constructive logics are central, though 2-valuedness - although natural and desirable - cannot be guaranteed. In a sense it is the WKL axiom which introduces 2-valuedness across logic, but it does so non-constructively, leaving room for much further debate and investigation into this area.
answered Jan 18 at 13:51
Roy SimpsonRoy Simpson
338111
$endgroup$
$begingroup$
This comment has been extremely valuable to me, though I cannot remark on it in detail at present. Reverse mathematics looks extremely interesting. Thank you.
$endgroup$
– Dion Bridger
Jan 20 at 22:38
add a comment |
$begingroup$
I would like to add another answer to this focussing on the case of countable languages, because that is the usual context of logic and also of the Penrose argument.
Indeed the question is asking about the Completeness Theorem ($vdash$ implies $models$) of First Order Logic, and whether it is always valid. In fact my own question asked about whether this theorem was constructive ie fully effective as I had been learning about Reverse Mathematics and the result that Completeness depended on a non-constructive axiom known as WKL (Weak Konig's Lemma). As your linked remark shows historic Logic literature has been confused about the relationship between $models$ and $vdash$. To summarise the reason:
First Order Logic can be formalised in a weak framework called RCA which captures computability. Many theorems (and meta-theorems) can be proven in RCA including the Soundness Theorem ($models$ implies $vdash$) of First Order Logic.
However Completeness requires WKL and is not provable in RCA.
An immediate consequence of this is that $models$ and $vdash$ are not interchangeable (unless one assumes WKL).
Another consequence is that if a theory is consistent it cannot be established constructively that it has a model. In fact the model building process does involve an element of choice, although the ZF Axiom of Choice is not involved. The choice principle involved is mentioned in the Reverse Mathematics book and called "Strong $Pi_{1}^{0}$ dependent choice" and is a (meta-)corollary of WKL.
However partial models can be built constructively (whose elements are either True or False), but extending this to all properties cannot be achieved. So for any such partial model there will exist a property p_k such that p_k(k) will map to {True,False} in our model, rather than to a specific truth value.
The fact that p_k(k) maps to {True,False} opens the door to 3-valued logics (in which p_k(k) is undefined) or to paraconsistent logics (in which p_k(k) is both True and False).
If one starts with a paraconsistent logic PL then it has also been argued that Godel's Incompleteness Theorem will not hold for PL (since its proof would require that inconsistency is impossible).
In the Penrose argument, in Artificial Intelligence and in Computer Science/Software Engineering more generally constructive logics are central, though 2-valuedness - although natural and desirable - cannot be guaranteed. In a sense it is the WKL axiom which introduces 2-valuedness across logic, but it does so non-constructively, leaving room for much further debate and investigation into this area.
answered Jan 18 at 13:51
Roy SimpsonRoy Simpson
338111
$endgroup$
I would like to add another answer to this focussing on the case of countable languages, because that is the usual context of logic and also of the Penrose argument.
Indeed the question is asking about the Completeness Theorem ($vdash$ implies $models$) of First Order Logic, and whether it is always valid. In fact my own question asked about whether this theorem was constructive ie fully effective as I had been learning about Reverse Mathematics and the result that Completeness depended on a non-constructive axiom known as WKL (Weak Konig's Lemma). As your linked remark shows historic Logic literature has been confused about the relationship between $models$ and $vdash$. To summarise the reason:
First Order Logic can be formalised in a weak framework called RCA which captures computability. Many theorems (and meta-theorems) can be proven in RCA including the Soundness Theorem ($models$ implies $vdash$) of First Order Logic.
However Completeness requires WKL and is not provable in RCA.
An immediate consequence of this is that $models$ and $vdash$ are not interchangeable (unless one assumes WKL).
Another consequence is that if a theory is consistent it cannot be established constructively that it has a model. In fact the model building process does involve an element of choice, although the ZF Axiom of Choice is not involved. The choice principle involved is mentioned in the Reverse Mathematics book and called "Strong $Pi_{1}^{0}$ dependent choice" and is a (meta-)corollary of WKL.
However partial models can be built constructively (whose elements are either True or False), but extending this to all properties cannot be achieved. So for any such partial model there will exist a property p_k such that p_k(k) will map to {True,False} in our model, rather than to a specific truth value.
The fact that p_k(k) maps to {True,False} opens the door to 3-valued logics (in which p_k(k) is undefined) or to paraconsistent logics (in which p_k(k) is both True and False).
If one starts with a paraconsistent logic PL then it has also been argued that Godel's Incompleteness Theorem will not hold for PL (since its proof would require that inconsistency is impossible).
In the Penrose argument, in Artificial Intelligence and in Computer Science/Software Engineering more generally constructive logics are central, though 2-valuedness - although natural and desirable - cannot be guaranteed. In a sense it is the WKL axiom which introduces 2-valuedness across logic, but it does so non-constructively, leaving room for much further debate and investigation into this area.
answered Jan 18 at 13:51
Roy SimpsonRoy Simpson
338111
answered Jan 18 at 13:51
Roy SimpsonRoy Simpson
338111
answered Jan 18 at 13:51
Roy SimpsonRoy Simpson
338111
answered Jan 18 at 13:51
Roy SimpsonRoy Simpson
338111
338111
$begingroup$
This comment has been extremely valuable to me, though I cannot remark on it in detail at present. Reverse mathematics looks extremely interesting. Thank you.
$endgroup$
– Dion Bridger
Jan 20 at 22:38
add a comment |
$begingroup$
This comment has been extremely valuable to me, though I cannot remark on it in detail at present. Reverse mathematics looks extremely interesting. Thank you.
$endgroup$
– Dion Bridger
Jan 20 at 22:38
$begingroup$
This comment has been extremely valuable to me, though I cannot remark on it in detail at present. Reverse mathematics looks extremely interesting. Thank you.
$endgroup$
– Dion Bridger
Jan 20 at 22:38
$begingroup$
This comment has been extremely valuable to me, though I cannot remark on it in detail at present. Reverse mathematics looks extremely interesting. Thank you.
$endgroup$
– Dion Bridger
Jan 20 at 22: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.
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%2f1332552%2fdoes-semantic-inconsistency-guarantee-syntactic-inconsistency%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
