Show that $Sigma vdashvarphi$ if and only if $Sigma,cup {negvarphi}$ is inconsistent.
I am stuck at the following problem:
Let $varphi$ be a sentence in a predicate calculus $T$ and $Sigma$ a set of sentences in $T$. Show that $Sigma vdashvarphi$ if and only if $Sigma,cup {negvarphi}$ is inconsistent.
My attempt:
$(Leftarrow)$ Suppose $Sigma,cup {negvarphi}$ is inconsistent, then there exists a formula $psi$ such that $Sigma,cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$.
$(Rightarrow)$ Suppose $Sigma vdashvarphi$. Then, since every theorem of predicate calculus is logically valid, $varphi$ is logically valid. Then $negvarphi$ is not satisfiable.
WTS:
$Sigma,cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$
$Sigma,cup {negvarphi}$ is inconsistent
logic first-order-logic predicate-logic proof-theory hilbert-calculus
|
show 3 more comments
I am stuck at the following problem:
Let $varphi$ be a sentence in a predicate calculus $T$ and $Sigma$ a set of sentences in $T$. Show that $Sigma vdashvarphi$ if and only if $Sigma,cup {negvarphi}$ is inconsistent.
My attempt:
$(Leftarrow)$ Suppose $Sigma,cup {negvarphi}$ is inconsistent, then there exists a formula $psi$ such that $Sigma,cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$.
$(Rightarrow)$ Suppose $Sigma vdashvarphi$. Then, since every theorem of predicate calculus is logically valid, $varphi$ is logically valid. Then $negvarphi$ is not satisfiable.
WTS:
$Sigma,cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$
$Sigma,cup {negvarphi}$ is inconsistent
logic first-order-logic predicate-logic proof-theory hilbert-calculus
Can you use soundness and completeness theorems?
– Taroccoesbrocco
Nov 27 at 13:37
We used these in propositional logic, but we haven't seen them so far in first order logic
– Leyla Alkan
Nov 27 at 13:41
Actually "every theorem of predicate calculus is logically valid" is soundness..
– Leyla Alkan
Nov 27 at 13:45
See also the post Prove that if $Gamma cup { lnot varphi }$ is inconsistent, then ...
– Mauro ALLEGRANZA
Nov 27 at 15:06
2
@MauroALLEGRANZA - I don't agree that the question is a duplicate of that one. Here the question is about both directions of the equivalence, not only one direction.
– Taroccoesbrocco
Nov 27 at 15:40
|
show 3 more comments
I am stuck at the following problem:
Let $varphi$ be a sentence in a predicate calculus $T$ and $Sigma$ a set of sentences in $T$. Show that $Sigma vdashvarphi$ if and only if $Sigma,cup {negvarphi}$ is inconsistent.
My attempt:
$(Leftarrow)$ Suppose $Sigma,cup {negvarphi}$ is inconsistent, then there exists a formula $psi$ such that $Sigma,cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$.
$(Rightarrow)$ Suppose $Sigma vdashvarphi$. Then, since every theorem of predicate calculus is logically valid, $varphi$ is logically valid. Then $negvarphi$ is not satisfiable.
WTS:
$Sigma,cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$
$Sigma,cup {negvarphi}$ is inconsistent
logic first-order-logic predicate-logic proof-theory hilbert-calculus
I am stuck at the following problem:
Let $varphi$ be a sentence in a predicate calculus $T$ and $Sigma$ a set of sentences in $T$. Show that $Sigma vdashvarphi$ if and only if $Sigma,cup {negvarphi}$ is inconsistent.
My attempt:
$(Leftarrow)$ Suppose $Sigma,cup {negvarphi}$ is inconsistent, then there exists a formula $psi$ such that $Sigma,cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$.
$(Rightarrow)$ Suppose $Sigma vdashvarphi$. Then, since every theorem of predicate calculus is logically valid, $varphi$ is logically valid. Then $negvarphi$ is not satisfiable.
WTS:
$Sigma,cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$
$Sigma,cup {negvarphi}$ is inconsistent
logic first-order-logic predicate-logic proof-theory hilbert-calculus
logic first-order-logic predicate-logic proof-theory hilbert-calculus
edited Nov 27 at 14:46
Taroccoesbrocco
5,05761839
5,05761839
asked Nov 27 at 13:26
Leyla Alkan
1,5691723
1,5691723
Can you use soundness and completeness theorems?
– Taroccoesbrocco
Nov 27 at 13:37
We used these in propositional logic, but we haven't seen them so far in first order logic
– Leyla Alkan
Nov 27 at 13:41
Actually "every theorem of predicate calculus is logically valid" is soundness..
– Leyla Alkan
Nov 27 at 13:45
See also the post Prove that if $Gamma cup { lnot varphi }$ is inconsistent, then ...
– Mauro ALLEGRANZA
Nov 27 at 15:06
2
@MauroALLEGRANZA - I don't agree that the question is a duplicate of that one. Here the question is about both directions of the equivalence, not only one direction.
– Taroccoesbrocco
Nov 27 at 15:40
|
show 3 more comments
Can you use soundness and completeness theorems?
– Taroccoesbrocco
Nov 27 at 13:37
We used these in propositional logic, but we haven't seen them so far in first order logic
– Leyla Alkan
Nov 27 at 13:41
Actually "every theorem of predicate calculus is logically valid" is soundness..
– Leyla Alkan
Nov 27 at 13:45
See also the post Prove that if $Gamma cup { lnot varphi }$ is inconsistent, then ...
– Mauro ALLEGRANZA
Nov 27 at 15:06
2
@MauroALLEGRANZA - I don't agree that the question is a duplicate of that one. Here the question is about both directions of the equivalence, not only one direction.
– Taroccoesbrocco
Nov 27 at 15:40
Can you use soundness and completeness theorems?
– Taroccoesbrocco
Nov 27 at 13:37
Can you use soundness and completeness theorems?
– Taroccoesbrocco
Nov 27 at 13:37
We used these in propositional logic, but we haven't seen them so far in first order logic
– Leyla Alkan
Nov 27 at 13:41
We used these in propositional logic, but we haven't seen them so far in first order logic
– Leyla Alkan
Nov 27 at 13:41
Actually "every theorem of predicate calculus is logically valid" is soundness..
– Leyla Alkan
Nov 27 at 13:45
Actually "every theorem of predicate calculus is logically valid" is soundness..
– Leyla Alkan
Nov 27 at 13:45
See also the post Prove that if $Gamma cup { lnot varphi }$ is inconsistent, then ...
– Mauro ALLEGRANZA
Nov 27 at 15:06
See also the post Prove that if $Gamma cup { lnot varphi }$ is inconsistent, then ...
– Mauro ALLEGRANZA
Nov 27 at 15:06
2
2
@MauroALLEGRANZA - I don't agree that the question is a duplicate of that one. Here the question is about both directions of the equivalence, not only one direction.
– Taroccoesbrocco
Nov 27 at 15:40
@MauroALLEGRANZA - I don't agree that the question is a duplicate of that one. Here the question is about both directions of the equivalence, not only one direction.
– Taroccoesbrocco
Nov 27 at 15:40
|
show 3 more comments
3 Answers
3
active
oldest
votes
If you are allowed to use soundness and completeness theorems (which hold not only in propositional logic but also in first-order logic), the proof is quite easy.
$Leftarrow$: Suppose $Sigma cup {negvarphi}$ is inconsistent, then there exists a formula $psi$ such that $Sigma cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$.
By soundness theorem, $Sigma cup {negvarphi} models psi$ and $Sigma cup {negvarphi}models negpsi$, which means that every model of $Sigma cup {negvarphi}$ satisfies both $psi$ and $lnot psi$. Now, by definition, there is no structure in first-order logic that satisfies a formula and its negation.
Therefore, there is no model of $Sigma cup {negvarphi}$, which means that every model of $Sigma$ is a model of $varphi$ as well, i.e. $Sigma models varphi$.
According to completeness theorem, $Sigma vdash varphi$.
$Rightarrow:$ Suppose $Sigma vdash varphi$. Then, $Sigma cup {lnot varphi} vdash varphi$, according to the weakening property (which holds in any deduction system for "traditional logics").
But $Sigma cup {negvarphi} vdash lnot varphi$ as well, since $lnot varphi in Sigma cup {negvarphi}$. Hence, $Sigma cup {negvarphi}$ is inconsistent. $qquadsquare$
Note the your use of the soundness theorem in your original post is not correct, or at least not well-written: according to soundness theorem, $Sigma vdash varphi$ does not imply that $varphi$ is logically valid (a formula is logically valid iff every structure satisfies it), but it implies that every model of $Sigma$ satisfies $varphi$ (it is possible that $Sigma$ has no models and $varphi$ is unsatisfiable as well).
Roughly, weakening property says that if you can prove something starting from some hypothesis $Sigma$, you can prove it even when you add more hypotheses to $Sigma$.
If you are not allowed to use soundness and correctness theorems, the proof of ($Leftarrow$) is slightly more technical and it depends on the deduction system and the inference rules you are allowed to use. This means that soundness and completeness theorems are not necessary to prove ($Leftarrow$) but they simplify the proof and also they "universalize" the proof, in the sense that by appealing to these theorems the proof of ($Leftarrow$) does not depend explicitly on the deduction system and the inference rules you are allowed to use.
Anyway, if the deduction system you are using is Hilbert system with the axiom $(lnot varphi to lnot psi) to ((lnot varphi to psi) to varphi)$ (as the systems described in Mendelson's book, pp. 35 and 69 for propositional and first order logic, respectively), you can easily prove $(Leftarrow)$ as described in this post, without appealing to the semantic notions involved in soundess and completeness theorems.
I understood the first one, but I don't know if it's okay for us to use weakening property, since we didn't cover it in class
– Leyla Alkan
Nov 27 at 14:19
@LeylaAlkan - Which deduction system are you using? I guess you are using Hilbert system and if it is so, weakening is a trivial property which follows immediately from the definition of derivation in such a system.
– Taroccoesbrocco
Nov 27 at 14:20
What do you mean by deduction system? We are basically following Mendelson's book
– Leyla Alkan
Nov 27 at 14:26
@LeylaAlkan - Yes, it is also called Hilbert system. The first property of this system proved in Mendelson's book is exactly weakening (p. 35, point 1).
– Taroccoesbrocco
Nov 27 at 14:30
add a comment |
Suppose $Sigma vdash varphi$. Trivially $negvarphi vdash negvarphi$. So $Sigma, negvarphi vdash varphi land negvarphi$. Therefore $Sigma, negvarphi vdash bot$, so $Sigma, negvarphi$ is (syntactically) inconsistent.
Suppose $Sigma, negvarphi$ is (syntactically) inconsistent, i.e. $Sigma, negvarphi vdash bot$. Then $Sigma vdash negvarphi to bot$. Whence $Sigma vdash negnegvarphi$. Whence, classically, $Sigma vdash varphi$.
There are some details you'll need to fill in depending on the proof-system that you have available (the one that defines the relation symbolized by '$vdash$'). But you won't need to appeal to soundness and completeness if syntactic consistency is in question. All you need are some simple properties of the relevant proof system.
If semantic consistency is in question then, yes, you'll need the soundness and completeness results that link the syntactic and semantic notions. But is very important for questions like this to be clear which notion of consistency is in question. (Your single turnstile is conventionally the sign for the syntactic proof relation, so this naturally goes along with the notion of syntactic consistency -- classically, not proving $bot$, or not proving an explicit contradiction, or not proving every sentence.)
add a comment |
Neither for $Leftarrow$ nor for $Rightarrow$ is it necessery to involve semantics. The exact derivations depend on the particular deduction system you are using, but the general structure will be as follows.
For $Leftarrow$, continue with deriving $Sigma cup { lnot phi } vdash psi land lnot psi$. Therefore $Sigma vdash lnot phi to (psi land lnot psi)$. So $Sigma vdash lnot lnot phi$ and therefore $Sigma vdash phi$.
For $Rightarrow$, you already have $Sigma vdash phi$ and therefore also $Sigma cap { lnot phi } vdash phi$. Of course, also $Sigma cup { lnot phi } vdash lnot phi$. Together you can use this to derive $Sigma cup { lnot phi } vdash psi$ for an arbitrary $psi$.
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%2f3015764%2fshow-that-sigma-vdash-varphi-if-and-only-if-sigma-cup-neg-varphi-i%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
If you are allowed to use soundness and completeness theorems (which hold not only in propositional logic but also in first-order logic), the proof is quite easy.
$Leftarrow$: Suppose $Sigma cup {negvarphi}$ is inconsistent, then there exists a formula $psi$ such that $Sigma cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$.
By soundness theorem, $Sigma cup {negvarphi} models psi$ and $Sigma cup {negvarphi}models negpsi$, which means that every model of $Sigma cup {negvarphi}$ satisfies both $psi$ and $lnot psi$. Now, by definition, there is no structure in first-order logic that satisfies a formula and its negation.
Therefore, there is no model of $Sigma cup {negvarphi}$, which means that every model of $Sigma$ is a model of $varphi$ as well, i.e. $Sigma models varphi$.
According to completeness theorem, $Sigma vdash varphi$.
$Rightarrow:$ Suppose $Sigma vdash varphi$. Then, $Sigma cup {lnot varphi} vdash varphi$, according to the weakening property (which holds in any deduction system for "traditional logics").
But $Sigma cup {negvarphi} vdash lnot varphi$ as well, since $lnot varphi in Sigma cup {negvarphi}$. Hence, $Sigma cup {negvarphi}$ is inconsistent. $qquadsquare$
Note the your use of the soundness theorem in your original post is not correct, or at least not well-written: according to soundness theorem, $Sigma vdash varphi$ does not imply that $varphi$ is logically valid (a formula is logically valid iff every structure satisfies it), but it implies that every model of $Sigma$ satisfies $varphi$ (it is possible that $Sigma$ has no models and $varphi$ is unsatisfiable as well).
Roughly, weakening property says that if you can prove something starting from some hypothesis $Sigma$, you can prove it even when you add more hypotheses to $Sigma$.
If you are not allowed to use soundness and correctness theorems, the proof of ($Leftarrow$) is slightly more technical and it depends on the deduction system and the inference rules you are allowed to use. This means that soundness and completeness theorems are not necessary to prove ($Leftarrow$) but they simplify the proof and also they "universalize" the proof, in the sense that by appealing to these theorems the proof of ($Leftarrow$) does not depend explicitly on the deduction system and the inference rules you are allowed to use.
Anyway, if the deduction system you are using is Hilbert system with the axiom $(lnot varphi to lnot psi) to ((lnot varphi to psi) to varphi)$ (as the systems described in Mendelson's book, pp. 35 and 69 for propositional and first order logic, respectively), you can easily prove $(Leftarrow)$ as described in this post, without appealing to the semantic notions involved in soundess and completeness theorems.
I understood the first one, but I don't know if it's okay for us to use weakening property, since we didn't cover it in class
– Leyla Alkan
Nov 27 at 14:19
@LeylaAlkan - Which deduction system are you using? I guess you are using Hilbert system and if it is so, weakening is a trivial property which follows immediately from the definition of derivation in such a system.
– Taroccoesbrocco
Nov 27 at 14:20
What do you mean by deduction system? We are basically following Mendelson's book
– Leyla Alkan
Nov 27 at 14:26
@LeylaAlkan - Yes, it is also called Hilbert system. The first property of this system proved in Mendelson's book is exactly weakening (p. 35, point 1).
– Taroccoesbrocco
Nov 27 at 14:30
add a comment |
If you are allowed to use soundness and completeness theorems (which hold not only in propositional logic but also in first-order logic), the proof is quite easy.
$Leftarrow$: Suppose $Sigma cup {negvarphi}$ is inconsistent, then there exists a formula $psi$ such that $Sigma cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$.
By soundness theorem, $Sigma cup {negvarphi} models psi$ and $Sigma cup {negvarphi}models negpsi$, which means that every model of $Sigma cup {negvarphi}$ satisfies both $psi$ and $lnot psi$. Now, by definition, there is no structure in first-order logic that satisfies a formula and its negation.
Therefore, there is no model of $Sigma cup {negvarphi}$, which means that every model of $Sigma$ is a model of $varphi$ as well, i.e. $Sigma models varphi$.
According to completeness theorem, $Sigma vdash varphi$.
$Rightarrow:$ Suppose $Sigma vdash varphi$. Then, $Sigma cup {lnot varphi} vdash varphi$, according to the weakening property (which holds in any deduction system for "traditional logics").
But $Sigma cup {negvarphi} vdash lnot varphi$ as well, since $lnot varphi in Sigma cup {negvarphi}$. Hence, $Sigma cup {negvarphi}$ is inconsistent. $qquadsquare$
Note the your use of the soundness theorem in your original post is not correct, or at least not well-written: according to soundness theorem, $Sigma vdash varphi$ does not imply that $varphi$ is logically valid (a formula is logically valid iff every structure satisfies it), but it implies that every model of $Sigma$ satisfies $varphi$ (it is possible that $Sigma$ has no models and $varphi$ is unsatisfiable as well).
Roughly, weakening property says that if you can prove something starting from some hypothesis $Sigma$, you can prove it even when you add more hypotheses to $Sigma$.
If you are not allowed to use soundness and correctness theorems, the proof of ($Leftarrow$) is slightly more technical and it depends on the deduction system and the inference rules you are allowed to use. This means that soundness and completeness theorems are not necessary to prove ($Leftarrow$) but they simplify the proof and also they "universalize" the proof, in the sense that by appealing to these theorems the proof of ($Leftarrow$) does not depend explicitly on the deduction system and the inference rules you are allowed to use.
Anyway, if the deduction system you are using is Hilbert system with the axiom $(lnot varphi to lnot psi) to ((lnot varphi to psi) to varphi)$ (as the systems described in Mendelson's book, pp. 35 and 69 for propositional and first order logic, respectively), you can easily prove $(Leftarrow)$ as described in this post, without appealing to the semantic notions involved in soundess and completeness theorems.
I understood the first one, but I don't know if it's okay for us to use weakening property, since we didn't cover it in class
– Leyla Alkan
Nov 27 at 14:19
@LeylaAlkan - Which deduction system are you using? I guess you are using Hilbert system and if it is so, weakening is a trivial property which follows immediately from the definition of derivation in such a system.
– Taroccoesbrocco
Nov 27 at 14:20
What do you mean by deduction system? We are basically following Mendelson's book
– Leyla Alkan
Nov 27 at 14:26
@LeylaAlkan - Yes, it is also called Hilbert system. The first property of this system proved in Mendelson's book is exactly weakening (p. 35, point 1).
– Taroccoesbrocco
Nov 27 at 14:30
add a comment |
If you are allowed to use soundness and completeness theorems (which hold not only in propositional logic but also in first-order logic), the proof is quite easy.
$Leftarrow$: Suppose $Sigma cup {negvarphi}$ is inconsistent, then there exists a formula $psi$ such that $Sigma cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$.
By soundness theorem, $Sigma cup {negvarphi} models psi$ and $Sigma cup {negvarphi}models negpsi$, which means that every model of $Sigma cup {negvarphi}$ satisfies both $psi$ and $lnot psi$. Now, by definition, there is no structure in first-order logic that satisfies a formula and its negation.
Therefore, there is no model of $Sigma cup {negvarphi}$, which means that every model of $Sigma$ is a model of $varphi$ as well, i.e. $Sigma models varphi$.
According to completeness theorem, $Sigma vdash varphi$.
$Rightarrow:$ Suppose $Sigma vdash varphi$. Then, $Sigma cup {lnot varphi} vdash varphi$, according to the weakening property (which holds in any deduction system for "traditional logics").
But $Sigma cup {negvarphi} vdash lnot varphi$ as well, since $lnot varphi in Sigma cup {negvarphi}$. Hence, $Sigma cup {negvarphi}$ is inconsistent. $qquadsquare$
Note the your use of the soundness theorem in your original post is not correct, or at least not well-written: according to soundness theorem, $Sigma vdash varphi$ does not imply that $varphi$ is logically valid (a formula is logically valid iff every structure satisfies it), but it implies that every model of $Sigma$ satisfies $varphi$ (it is possible that $Sigma$ has no models and $varphi$ is unsatisfiable as well).
Roughly, weakening property says that if you can prove something starting from some hypothesis $Sigma$, you can prove it even when you add more hypotheses to $Sigma$.
If you are not allowed to use soundness and correctness theorems, the proof of ($Leftarrow$) is slightly more technical and it depends on the deduction system and the inference rules you are allowed to use. This means that soundness and completeness theorems are not necessary to prove ($Leftarrow$) but they simplify the proof and also they "universalize" the proof, in the sense that by appealing to these theorems the proof of ($Leftarrow$) does not depend explicitly on the deduction system and the inference rules you are allowed to use.
Anyway, if the deduction system you are using is Hilbert system with the axiom $(lnot varphi to lnot psi) to ((lnot varphi to psi) to varphi)$ (as the systems described in Mendelson's book, pp. 35 and 69 for propositional and first order logic, respectively), you can easily prove $(Leftarrow)$ as described in this post, without appealing to the semantic notions involved in soundess and completeness theorems.
If you are allowed to use soundness and completeness theorems (which hold not only in propositional logic but also in first-order logic), the proof is quite easy.
$Leftarrow$: Suppose $Sigma cup {negvarphi}$ is inconsistent, then there exists a formula $psi$ such that $Sigma cup {negvarphi}vdashpsi$ and $Sigma,cup {negvarphi}vdashnegpsi$.
By soundness theorem, $Sigma cup {negvarphi} models psi$ and $Sigma cup {negvarphi}models negpsi$, which means that every model of $Sigma cup {negvarphi}$ satisfies both $psi$ and $lnot psi$. Now, by definition, there is no structure in first-order logic that satisfies a formula and its negation.
Therefore, there is no model of $Sigma cup {negvarphi}$, which means that every model of $Sigma$ is a model of $varphi$ as well, i.e. $Sigma models varphi$.
According to completeness theorem, $Sigma vdash varphi$.
$Rightarrow:$ Suppose $Sigma vdash varphi$. Then, $Sigma cup {lnot varphi} vdash varphi$, according to the weakening property (which holds in any deduction system for "traditional logics").
But $Sigma cup {negvarphi} vdash lnot varphi$ as well, since $lnot varphi in Sigma cup {negvarphi}$. Hence, $Sigma cup {negvarphi}$ is inconsistent. $qquadsquare$
Note the your use of the soundness theorem in your original post is not correct, or at least not well-written: according to soundness theorem, $Sigma vdash varphi$ does not imply that $varphi$ is logically valid (a formula is logically valid iff every structure satisfies it), but it implies that every model of $Sigma$ satisfies $varphi$ (it is possible that $Sigma$ has no models and $varphi$ is unsatisfiable as well).
Roughly, weakening property says that if you can prove something starting from some hypothesis $Sigma$, you can prove it even when you add more hypotheses to $Sigma$.
If you are not allowed to use soundness and correctness theorems, the proof of ($Leftarrow$) is slightly more technical and it depends on the deduction system and the inference rules you are allowed to use. This means that soundness and completeness theorems are not necessary to prove ($Leftarrow$) but they simplify the proof and also they "universalize" the proof, in the sense that by appealing to these theorems the proof of ($Leftarrow$) does not depend explicitly on the deduction system and the inference rules you are allowed to use.
Anyway, if the deduction system you are using is Hilbert system with the axiom $(lnot varphi to lnot psi) to ((lnot varphi to psi) to varphi)$ (as the systems described in Mendelson's book, pp. 35 and 69 for propositional and first order logic, respectively), you can easily prove $(Leftarrow)$ as described in this post, without appealing to the semantic notions involved in soundess and completeness theorems.
edited Nov 27 at 15:55
answered Nov 27 at 14:13
Taroccoesbrocco
5,05761839
5,05761839
I understood the first one, but I don't know if it's okay for us to use weakening property, since we didn't cover it in class
– Leyla Alkan
Nov 27 at 14:19
@LeylaAlkan - Which deduction system are you using? I guess you are using Hilbert system and if it is so, weakening is a trivial property which follows immediately from the definition of derivation in such a system.
– Taroccoesbrocco
Nov 27 at 14:20
What do you mean by deduction system? We are basically following Mendelson's book
– Leyla Alkan
Nov 27 at 14:26
@LeylaAlkan - Yes, it is also called Hilbert system. The first property of this system proved in Mendelson's book is exactly weakening (p. 35, point 1).
– Taroccoesbrocco
Nov 27 at 14:30
add a comment |
I understood the first one, but I don't know if it's okay for us to use weakening property, since we didn't cover it in class
– Leyla Alkan
Nov 27 at 14:19
@LeylaAlkan - Which deduction system are you using? I guess you are using Hilbert system and if it is so, weakening is a trivial property which follows immediately from the definition of derivation in such a system.
– Taroccoesbrocco
Nov 27 at 14:20
What do you mean by deduction system? We are basically following Mendelson's book
– Leyla Alkan
Nov 27 at 14:26
@LeylaAlkan - Yes, it is also called Hilbert system. The first property of this system proved in Mendelson's book is exactly weakening (p. 35, point 1).
– Taroccoesbrocco
Nov 27 at 14:30
I understood the first one, but I don't know if it's okay for us to use weakening property, since we didn't cover it in class
– Leyla Alkan
Nov 27 at 14:19
I understood the first one, but I don't know if it's okay for us to use weakening property, since we didn't cover it in class
– Leyla Alkan
Nov 27 at 14:19
@LeylaAlkan - Which deduction system are you using? I guess you are using Hilbert system and if it is so, weakening is a trivial property which follows immediately from the definition of derivation in such a system.
– Taroccoesbrocco
Nov 27 at 14:20
@LeylaAlkan - Which deduction system are you using? I guess you are using Hilbert system and if it is so, weakening is a trivial property which follows immediately from the definition of derivation in such a system.
– Taroccoesbrocco
Nov 27 at 14:20
What do you mean by deduction system? We are basically following Mendelson's book
– Leyla Alkan
Nov 27 at 14:26
What do you mean by deduction system? We are basically following Mendelson's book
– Leyla Alkan
Nov 27 at 14:26
@LeylaAlkan - Yes, it is also called Hilbert system. The first property of this system proved in Mendelson's book is exactly weakening (p. 35, point 1).
– Taroccoesbrocco
Nov 27 at 14:30
@LeylaAlkan - Yes, it is also called Hilbert system. The first property of this system proved in Mendelson's book is exactly weakening (p. 35, point 1).
– Taroccoesbrocco
Nov 27 at 14:30
add a comment |
Suppose $Sigma vdash varphi$. Trivially $negvarphi vdash negvarphi$. So $Sigma, negvarphi vdash varphi land negvarphi$. Therefore $Sigma, negvarphi vdash bot$, so $Sigma, negvarphi$ is (syntactically) inconsistent.
Suppose $Sigma, negvarphi$ is (syntactically) inconsistent, i.e. $Sigma, negvarphi vdash bot$. Then $Sigma vdash negvarphi to bot$. Whence $Sigma vdash negnegvarphi$. Whence, classically, $Sigma vdash varphi$.
There are some details you'll need to fill in depending on the proof-system that you have available (the one that defines the relation symbolized by '$vdash$'). But you won't need to appeal to soundness and completeness if syntactic consistency is in question. All you need are some simple properties of the relevant proof system.
If semantic consistency is in question then, yes, you'll need the soundness and completeness results that link the syntactic and semantic notions. But is very important for questions like this to be clear which notion of consistency is in question. (Your single turnstile is conventionally the sign for the syntactic proof relation, so this naturally goes along with the notion of syntactic consistency -- classically, not proving $bot$, or not proving an explicit contradiction, or not proving every sentence.)
add a comment |
Suppose $Sigma vdash varphi$. Trivially $negvarphi vdash negvarphi$. So $Sigma, negvarphi vdash varphi land negvarphi$. Therefore $Sigma, negvarphi vdash bot$, so $Sigma, negvarphi$ is (syntactically) inconsistent.
Suppose $Sigma, negvarphi$ is (syntactically) inconsistent, i.e. $Sigma, negvarphi vdash bot$. Then $Sigma vdash negvarphi to bot$. Whence $Sigma vdash negnegvarphi$. Whence, classically, $Sigma vdash varphi$.
There are some details you'll need to fill in depending on the proof-system that you have available (the one that defines the relation symbolized by '$vdash$'). But you won't need to appeal to soundness and completeness if syntactic consistency is in question. All you need are some simple properties of the relevant proof system.
If semantic consistency is in question then, yes, you'll need the soundness and completeness results that link the syntactic and semantic notions. But is very important for questions like this to be clear which notion of consistency is in question. (Your single turnstile is conventionally the sign for the syntactic proof relation, so this naturally goes along with the notion of syntactic consistency -- classically, not proving $bot$, or not proving an explicit contradiction, or not proving every sentence.)
add a comment |
Suppose $Sigma vdash varphi$. Trivially $negvarphi vdash negvarphi$. So $Sigma, negvarphi vdash varphi land negvarphi$. Therefore $Sigma, negvarphi vdash bot$, so $Sigma, negvarphi$ is (syntactically) inconsistent.
Suppose $Sigma, negvarphi$ is (syntactically) inconsistent, i.e. $Sigma, negvarphi vdash bot$. Then $Sigma vdash negvarphi to bot$. Whence $Sigma vdash negnegvarphi$. Whence, classically, $Sigma vdash varphi$.
There are some details you'll need to fill in depending on the proof-system that you have available (the one that defines the relation symbolized by '$vdash$'). But you won't need to appeal to soundness and completeness if syntactic consistency is in question. All you need are some simple properties of the relevant proof system.
If semantic consistency is in question then, yes, you'll need the soundness and completeness results that link the syntactic and semantic notions. But is very important for questions like this to be clear which notion of consistency is in question. (Your single turnstile is conventionally the sign for the syntactic proof relation, so this naturally goes along with the notion of syntactic consistency -- classically, not proving $bot$, or not proving an explicit contradiction, or not proving every sentence.)
Suppose $Sigma vdash varphi$. Trivially $negvarphi vdash negvarphi$. So $Sigma, negvarphi vdash varphi land negvarphi$. Therefore $Sigma, negvarphi vdash bot$, so $Sigma, negvarphi$ is (syntactically) inconsistent.
Suppose $Sigma, negvarphi$ is (syntactically) inconsistent, i.e. $Sigma, negvarphi vdash bot$. Then $Sigma vdash negvarphi to bot$. Whence $Sigma vdash negnegvarphi$. Whence, classically, $Sigma vdash varphi$.
There are some details you'll need to fill in depending on the proof-system that you have available (the one that defines the relation symbolized by '$vdash$'). But you won't need to appeal to soundness and completeness if syntactic consistency is in question. All you need are some simple properties of the relevant proof system.
If semantic consistency is in question then, yes, you'll need the soundness and completeness results that link the syntactic and semantic notions. But is very important for questions like this to be clear which notion of consistency is in question. (Your single turnstile is conventionally the sign for the syntactic proof relation, so this naturally goes along with the notion of syntactic consistency -- classically, not proving $bot$, or not proving an explicit contradiction, or not proving every sentence.)
edited Nov 27 at 15:00
answered Nov 27 at 14:29
Peter Smith
40.5k340120
40.5k340120
add a comment |
add a comment |
Neither for $Leftarrow$ nor for $Rightarrow$ is it necessery to involve semantics. The exact derivations depend on the particular deduction system you are using, but the general structure will be as follows.
For $Leftarrow$, continue with deriving $Sigma cup { lnot phi } vdash psi land lnot psi$. Therefore $Sigma vdash lnot phi to (psi land lnot psi)$. So $Sigma vdash lnot lnot phi$ and therefore $Sigma vdash phi$.
For $Rightarrow$, you already have $Sigma vdash phi$ and therefore also $Sigma cap { lnot phi } vdash phi$. Of course, also $Sigma cup { lnot phi } vdash lnot phi$. Together you can use this to derive $Sigma cup { lnot phi } vdash psi$ for an arbitrary $psi$.
add a comment |
Neither for $Leftarrow$ nor for $Rightarrow$ is it necessery to involve semantics. The exact derivations depend on the particular deduction system you are using, but the general structure will be as follows.
For $Leftarrow$, continue with deriving $Sigma cup { lnot phi } vdash psi land lnot psi$. Therefore $Sigma vdash lnot phi to (psi land lnot psi)$. So $Sigma vdash lnot lnot phi$ and therefore $Sigma vdash phi$.
For $Rightarrow$, you already have $Sigma vdash phi$ and therefore also $Sigma cap { lnot phi } vdash phi$. Of course, also $Sigma cup { lnot phi } vdash lnot phi$. Together you can use this to derive $Sigma cup { lnot phi } vdash psi$ for an arbitrary $psi$.
add a comment |
Neither for $Leftarrow$ nor for $Rightarrow$ is it necessery to involve semantics. The exact derivations depend on the particular deduction system you are using, but the general structure will be as follows.
For $Leftarrow$, continue with deriving $Sigma cup { lnot phi } vdash psi land lnot psi$. Therefore $Sigma vdash lnot phi to (psi land lnot psi)$. So $Sigma vdash lnot lnot phi$ and therefore $Sigma vdash phi$.
For $Rightarrow$, you already have $Sigma vdash phi$ and therefore also $Sigma cap { lnot phi } vdash phi$. Of course, also $Sigma cup { lnot phi } vdash lnot phi$. Together you can use this to derive $Sigma cup { lnot phi } vdash psi$ for an arbitrary $psi$.
Neither for $Leftarrow$ nor for $Rightarrow$ is it necessery to involve semantics. The exact derivations depend on the particular deduction system you are using, but the general structure will be as follows.
For $Leftarrow$, continue with deriving $Sigma cup { lnot phi } vdash psi land lnot psi$. Therefore $Sigma vdash lnot phi to (psi land lnot psi)$. So $Sigma vdash lnot lnot phi$ and therefore $Sigma vdash phi$.
For $Rightarrow$, you already have $Sigma vdash phi$ and therefore also $Sigma cap { lnot phi } vdash phi$. Of course, also $Sigma cup { lnot phi } vdash lnot phi$. Together you can use this to derive $Sigma cup { lnot phi } vdash psi$ for an arbitrary $psi$.
answered Nov 27 at 14:22
Magdiragdag
10.8k31532
10.8k31532
add a comment |
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%2f3015764%2fshow-that-sigma-vdash-varphi-if-and-only-if-sigma-cup-neg-varphi-i%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
Can you use soundness and completeness theorems?
– Taroccoesbrocco
Nov 27 at 13:37
We used these in propositional logic, but we haven't seen them so far in first order logic
– Leyla Alkan
Nov 27 at 13:41
Actually "every theorem of predicate calculus is logically valid" is soundness..
– Leyla Alkan
Nov 27 at 13:45
See also the post Prove that if $Gamma cup { lnot varphi }$ is inconsistent, then ...
– Mauro ALLEGRANZA
Nov 27 at 15:06
2
@MauroALLEGRANZA - I don't agree that the question is a duplicate of that one. Here the question is about both directions of the equivalence, not only one direction.
– Taroccoesbrocco
Nov 27 at 15:40