Mixing
Semantic Consequence Definition
$begingroup$
"What is the difference between
⊨
(semantic consequence) and
⊢
(syntactic consequence)?" was a question that has been posted, but I am wanting a more specific answer. For example, this video explains what a syntactic consequence is. After watching this video, it is obvious that we say
p
⊢q
when p->q is a tautology where p and q are given propositions forming the tautology. What is an easy way to explain what a semantic consequence is? I have been obsessed looking at this question for awhile. Any help would be greatly appreciated.
logic propositional-calculus
edited Apr 13 '17 at 12:21
Community♦
1
asked Mar 27 '17 at 18:28
WillWill
163110
$endgroup$
add a comment |
$begingroup$
"What is the difference between
⊨
(semantic consequence) and
⊢
(syntactic consequence)?" was a question that has been posted, but I am wanting a more specific answer. For example, this video explains what a syntactic consequence is. After watching this video, it is obvious that we say
p
⊢q
when p->q is a tautology where p and q are given propositions forming the tautology. What is an easy way to explain what a semantic consequence is? I have been obsessed looking at this question for awhile. Any help would be greatly appreciated.
logic propositional-calculus
edited Apr 13 '17 at 12:21
Community♦
1
asked Mar 27 '17 at 18:28
WillWill
163110
$endgroup$
1
$begingroup$
See the post : difference-between-syntactic-consequence-and-semantic-consequence.
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:30
1
$begingroup$
See also the post : what-is-the-meaning-of-the-double-turnstile-symbol
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:32
1
$begingroup$
See also the post : why-are $vdash$ and $vDash$ symbols-from-metalanguage
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:34
1
$begingroup$
See also the post meaning-of-symbols $vdash$ and $models$
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:35
$begingroup$
I can not help but notice that you are the same person that wrote about the axiom for set theory. I am still confused with these symbols. I will read about them more. Can you explain them to me?
$endgroup$
– Will
Mar 27 '17 at 18:42
add a comment |
$begingroup$
"What is the difference between
⊨
(semantic consequence) and
⊢
(syntactic consequence)?" was a question that has been posted, but I am wanting a more specific answer. For example, this video explains what a syntactic consequence is. After watching this video, it is obvious that we say
p
⊢q
when p->q is a tautology where p and q are given propositions forming the tautology. What is an easy way to explain what a semantic consequence is? I have been obsessed looking at this question for awhile. Any help would be greatly appreciated.
logic propositional-calculus
edited Apr 13 '17 at 12:21
Community♦
1
asked Mar 27 '17 at 18:28
WillWill
163110
$endgroup$
"What is the difference between
⊨
(semantic consequence) and
⊢
(syntactic consequence)?" was a question that has been posted, but I am wanting a more specific answer. For example, this video explains what a syntactic consequence is. After watching this video, it is obvious that we say
p
⊢q
when p->q is a tautology where p and q are given propositions forming the tautology. What is an easy way to explain what a semantic consequence is? I have been obsessed looking at this question for awhile. Any help would be greatly appreciated.
logic propositional-calculus
logic propositional-calculus
edited Apr 13 '17 at 12:21
Community♦
1
asked Mar 27 '17 at 18:28
WillWill
163110
edited Apr 13 '17 at 12:21
Community♦
1
asked Mar 27 '17 at 18:28
WillWill
163110
edited Apr 13 '17 at 12:21
Community♦
1
edited Apr 13 '17 at 12:21
Community♦
1
edited Apr 13 '17 at 12:21
Community♦
1
1
asked Mar 27 '17 at 18:28
WillWill
163110
asked Mar 27 '17 at 18:28
WillWill
163110
asked Mar 27 '17 at 18:28
WillWill
163110
163110
1
$begingroup$
See the post : difference-between-syntactic-consequence-and-semantic-consequence.
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:30
1
$begingroup$
See also the post : what-is-the-meaning-of-the-double-turnstile-symbol
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:32
1
$begingroup$
See also the post : why-are $vdash$ and $vDash$ symbols-from-metalanguage
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:34
1
$begingroup$
See also the post meaning-of-symbols $vdash$ and $models$
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:35
$begingroup$
I can not help but notice that you are the same person that wrote about the axiom for set theory. I am still confused with these symbols. I will read about them more. Can you explain them to me?
$endgroup$
– Will
Mar 27 '17 at 18:42
add a comment |
1
$begingroup$
See the post : difference-between-syntactic-consequence-and-semantic-consequence.
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:30
1
$begingroup$
See also the post : what-is-the-meaning-of-the-double-turnstile-symbol
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:32
1
$begingroup$
See also the post : why-are $vdash$ and $vDash$ symbols-from-metalanguage
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:34
1
$begingroup$
See also the post meaning-of-symbols $vdash$ and $models$
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:35
$begingroup$
I can not help but notice that you are the same person that wrote about the axiom for set theory. I am still confused with these symbols. I will read about them more. Can you explain them to me?
$endgroup$
– Will
Mar 27 '17 at 18:42
1
1
$begingroup$
See the post : difference-between-syntactic-consequence-and-semantic-consequence.
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:30
$begingroup$
See the post : difference-between-syntactic-consequence-and-semantic-consequence.
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:30
1
1
$begingroup$
See also the post : what-is-the-meaning-of-the-double-turnstile-symbol
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:32
$begingroup$
See also the post : what-is-the-meaning-of-the-double-turnstile-symbol
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:32
1
1
$begingroup$
See also the post : why-are $vdash$ and $vDash$ symbols-from-metalanguage
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:34
$begingroup$
See also the post : why-are $vdash$ and $vDash$ symbols-from-metalanguage
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:34
1
1
$begingroup$
See also the post meaning-of-symbols $vdash$ and $models$
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:35
$begingroup$
See also the post meaning-of-symbols $vdash$ and $models$
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:35
$begingroup$
I can not help but notice that you are the same person that wrote about the axiom for set theory. I am still confused with these symbols. I will read about them more. Can you explain them to me?
$endgroup$
– Will
Mar 27 '17 at 18:42
$begingroup$
I can not help but notice that you are the same person that wrote about the axiom for set theory. I am still confused with these symbols. I will read about them more. Can you explain them to me?
$endgroup$
– Will
Mar 27 '17 at 18:42
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
$vDash$ means: logical consequence.
The general definition of it is:
A sentence $varphi$ is said to be a logical consequence of a set of sentences $Gamma$ (in symbols: $Gamma vDash varphi$) if and only if there is no model $mathcal {I}$ in which all members of $Gamma$ are true and $varphi$ is false.
In the context of propositional logic, this means that:
for every truth assignment (or valuation) $v$, i.e. for every function that assign a truth-value (T or F) to every sentential letter occurring in the formulas in $Gamma$ or $varphi$, if $v$ satisfy every formulas in $Gamma$, then it satisfy also $varphi$.
Trivial example (where $Gamma$ has only one formula):
${ p land q } vDash p$.
A truth assignment $v$ satisfy $p land q$ only if $v(p)=v(q)=$ T.
Thus, every truth assignment $v$ that satisfy every formulas in $Gamma$, i.e. that satisfy $p land q$, satisfy also $p$.
$Gamma vdash_{mathcal S} varphi$, instead, means that $varphi$ is derivable (in the proof system $mathcal S$) from the set of assumptions $Gamma$.
answered Mar 27 '17 at 18:41
Mauro ALLEGRANZAMauro ALLEGRANZA
66.4k449115
$endgroup$
$begingroup$
P= 1, 1, 0, 0 and Q=1, 0, 1, 0. Then, P^Q= 1, 0, 0, 0. Therefore, {P^Q} ⊨ P, since there is no combination where {P^Q}=1 and P would be a 0 correct? How would that be different from a syntactic consequence?
$endgroup$
– Will
Mar 27 '17 at 19:10
$begingroup$
Your answer did help me though. I appreciate it.
$endgroup$
– Will
Mar 27 '17 at 19:10
add a comment |
$begingroup$
$vdash$ is used to make statement about formal proof systems, which include rules of inference, that say:
"If you have a (or two) statement(s) that look like such-and-so, then you can write down a new statement that looks like this-and-that".
For example, many formal proof systems include the following rule of inference called Modus Ponens:
$$varphi$$
$$varphi rightarrow psi$$
$$therefore psi$$
So with this rule, I can, for example, infer $B land C$ from $A$ and $A rightarrow (B land C)$. The fact that I can do this within the proof system we write as: $A, A rightarrow (B land C) vdash B land C$.
Now, as it so happens, $B land C$ does in fact logically follow from $A$ and $A rightarrow (B land C)$. That is, the way we defined the formal semantics (think truth-tables) is such that whenever $A$ and $A rightarrow (B land C)$ are true, $B land C$ will have to be true as well. And that we write as $A, A rightarrow (B land C) vDash B land C$.
But maybe the best way to illustrate the difference between $vdash$ and $vDash$ is to consider a case where they don't both hold at the same time.
So, suppose I write a new logic textbook, and suppose that I develop a very simple system for making formal proofs, in that it has a single rule of inference:
Hokus Ponens
$$therefore varphi$$
Now, with Hokus Ponens, I can derive anything from nothing. Thus, for example, it will be true that $P vdash Q$. Here is the derivation/formal proof:
$P$ Premise
$Q$ Hokus Ponens!
But obviously, $Q$ does not logically follow from $P$. That is: $P not vDash Q$.
answered Mar 27 '17 at 19:48
Bram28Bram28
63.1k44793
$endgroup$
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%2f2205688%2fsemantic-consequence-definition%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$
$vDash$ means: logical consequence.
The general definition of it is:
A sentence $varphi$ is said to be a logical consequence of a set of sentences $Gamma$ (in symbols: $Gamma vDash varphi$) if and only if there is no model $mathcal {I}$ in which all members of $Gamma$ are true and $varphi$ is false.
In the context of propositional logic, this means that:
for every truth assignment (or valuation) $v$, i.e. for every function that assign a truth-value (T or F) to every sentential letter occurring in the formulas in $Gamma$ or $varphi$, if $v$ satisfy every formulas in $Gamma$, then it satisfy also $varphi$.
Trivial example (where $Gamma$ has only one formula):
${ p land q } vDash p$.
A truth assignment $v$ satisfy $p land q$ only if $v(p)=v(q)=$ T.
Thus, every truth assignment $v$ that satisfy every formulas in $Gamma$, i.e. that satisfy $p land q$, satisfy also $p$.
$Gamma vdash_{mathcal S} varphi$, instead, means that $varphi$ is derivable (in the proof system $mathcal S$) from the set of assumptions $Gamma$.
answered Mar 27 '17 at 18:41
Mauro ALLEGRANZAMauro ALLEGRANZA
66.4k449115
$endgroup$
$begingroup$
P= 1, 1, 0, 0 and Q=1, 0, 1, 0. Then, P^Q= 1, 0, 0, 0. Therefore, {P^Q} ⊨ P, since there is no combination where {P^Q}=1 and P would be a 0 correct? How would that be different from a syntactic consequence?
$endgroup$
– Will
Mar 27 '17 at 19:10
$begingroup$
Your answer did help me though. I appreciate it.
$endgroup$
– Will
Mar 27 '17 at 19:10
add a comment |
$begingroup$
$vDash$ means: logical consequence.
The general definition of it is:
A sentence $varphi$ is said to be a logical consequence of a set of sentences $Gamma$ (in symbols: $Gamma vDash varphi$) if and only if there is no model $mathcal {I}$ in which all members of $Gamma$ are true and $varphi$ is false.
In the context of propositional logic, this means that:
for every truth assignment (or valuation) $v$, i.e. for every function that assign a truth-value (T or F) to every sentential letter occurring in the formulas in $Gamma$ or $varphi$, if $v$ satisfy every formulas in $Gamma$, then it satisfy also $varphi$.
Trivial example (where $Gamma$ has only one formula):
${ p land q } vDash p$.
A truth assignment $v$ satisfy $p land q$ only if $v(p)=v(q)=$ T.
Thus, every truth assignment $v$ that satisfy every formulas in $Gamma$, i.e. that satisfy $p land q$, satisfy also $p$.
$Gamma vdash_{mathcal S} varphi$, instead, means that $varphi$ is derivable (in the proof system $mathcal S$) from the set of assumptions $Gamma$.
answered Mar 27 '17 at 18:41
Mauro ALLEGRANZAMauro ALLEGRANZA
66.4k449115
$endgroup$
$begingroup$
P= 1, 1, 0, 0 and Q=1, 0, 1, 0. Then, P^Q= 1, 0, 0, 0. Therefore, {P^Q} ⊨ P, since there is no combination where {P^Q}=1 and P would be a 0 correct? How would that be different from a syntactic consequence?
$endgroup$
– Will
Mar 27 '17 at 19:10
$begingroup$
Your answer did help me though. I appreciate it.
$endgroup$
– Will
Mar 27 '17 at 19:10
add a comment |
$begingroup$
$vDash$ means: logical consequence.
The general definition of it is:
A sentence $varphi$ is said to be a logical consequence of a set of sentences $Gamma$ (in symbols: $Gamma vDash varphi$) if and only if there is no model $mathcal {I}$ in which all members of $Gamma$ are true and $varphi$ is false.
In the context of propositional logic, this means that:
for every truth assignment (or valuation) $v$, i.e. for every function that assign a truth-value (T or F) to every sentential letter occurring in the formulas in $Gamma$ or $varphi$, if $v$ satisfy every formulas in $Gamma$, then it satisfy also $varphi$.
Trivial example (where $Gamma$ has only one formula):
${ p land q } vDash p$.
A truth assignment $v$ satisfy $p land q$ only if $v(p)=v(q)=$ T.
Thus, every truth assignment $v$ that satisfy every formulas in $Gamma$, i.e. that satisfy $p land q$, satisfy also $p$.
$Gamma vdash_{mathcal S} varphi$, instead, means that $varphi$ is derivable (in the proof system $mathcal S$) from the set of assumptions $Gamma$.
answered Mar 27 '17 at 18:41
Mauro ALLEGRANZAMauro ALLEGRANZA
66.4k449115
$endgroup$
$vDash$ means: logical consequence.
The general definition of it is:
A sentence $varphi$ is said to be a logical consequence of a set of sentences $Gamma$ (in symbols: $Gamma vDash varphi$) if and only if there is no model $mathcal {I}$ in which all members of $Gamma$ are true and $varphi$ is false.
In the context of propositional logic, this means that:
for every truth assignment (or valuation) $v$, i.e. for every function that assign a truth-value (T or F) to every sentential letter occurring in the formulas in $Gamma$ or $varphi$, if $v$ satisfy every formulas in $Gamma$, then it satisfy also $varphi$.
Trivial example (where $Gamma$ has only one formula):
${ p land q } vDash p$.
A truth assignment $v$ satisfy $p land q$ only if $v(p)=v(q)=$ T.
Thus, every truth assignment $v$ that satisfy every formulas in $Gamma$, i.e. that satisfy $p land q$, satisfy also $p$.
$Gamma vdash_{mathcal S} varphi$, instead, means that $varphi$ is derivable (in the proof system $mathcal S$) from the set of assumptions $Gamma$.
answered Mar 27 '17 at 18:41
Mauro ALLEGRANZAMauro ALLEGRANZA
66.4k449115
edited Mar 27 '17 at 19:23
answered Mar 27 '17 at 18:41
Mauro ALLEGRANZAMauro ALLEGRANZA
66.4k449115
answered Mar 27 '17 at 18:41
Mauro ALLEGRANZAMauro ALLEGRANZA
66.4k449115
answered Mar 27 '17 at 18:41
Mauro ALLEGRANZAMauro ALLEGRANZA
66.4k449115
66.4k449115
$begingroup$
P= 1, 1, 0, 0 and Q=1, 0, 1, 0. Then, P^Q= 1, 0, 0, 0. Therefore, {P^Q} ⊨ P, since there is no combination where {P^Q}=1 and P would be a 0 correct? How would that be different from a syntactic consequence?
$endgroup$
– Will
Mar 27 '17 at 19:10
$begingroup$
Your answer did help me though. I appreciate it.
$endgroup$
– Will
Mar 27 '17 at 19:10
add a comment |
$begingroup$
P= 1, 1, 0, 0 and Q=1, 0, 1, 0. Then, P^Q= 1, 0, 0, 0. Therefore, {P^Q} ⊨ P, since there is no combination where {P^Q}=1 and P would be a 0 correct? How would that be different from a syntactic consequence?
$endgroup$
– Will
Mar 27 '17 at 19:10
$begingroup$
Your answer did help me though. I appreciate it.
$endgroup$
– Will
Mar 27 '17 at 19:10
$begingroup$
P= 1, 1, 0, 0 and Q=1, 0, 1, 0. Then, P^Q= 1, 0, 0, 0. Therefore, {P^Q} ⊨ P, since there is no combination where {P^Q}=1 and P would be a 0 correct? How would that be different from a syntactic consequence?
$endgroup$
– Will
Mar 27 '17 at 19:10
$begingroup$
P= 1, 1, 0, 0 and Q=1, 0, 1, 0. Then, P^Q= 1, 0, 0, 0. Therefore, {P^Q} ⊨ P, since there is no combination where {P^Q}=1 and P would be a 0 correct? How would that be different from a syntactic consequence?
$endgroup$
– Will
Mar 27 '17 at 19:10
$begingroup$
Your answer did help me though. I appreciate it.
$endgroup$
– Will
Mar 27 '17 at 19:10
$begingroup$
Your answer did help me though. I appreciate it.
$endgroup$
– Will
Mar 27 '17 at 19:10
add a comment |
$begingroup$
$vdash$ is used to make statement about formal proof systems, which include rules of inference, that say:
"If you have a (or two) statement(s) that look like such-and-so, then you can write down a new statement that looks like this-and-that".
For example, many formal proof systems include the following rule of inference called Modus Ponens:
$$varphi$$
$$varphi rightarrow psi$$
$$therefore psi$$
So with this rule, I can, for example, infer $B land C$ from $A$ and $A rightarrow (B land C)$. The fact that I can do this within the proof system we write as: $A, A rightarrow (B land C) vdash B land C$.
Now, as it so happens, $B land C$ does in fact logically follow from $A$ and $A rightarrow (B land C)$. That is, the way we defined the formal semantics (think truth-tables) is such that whenever $A$ and $A rightarrow (B land C)$ are true, $B land C$ will have to be true as well. And that we write as $A, A rightarrow (B land C) vDash B land C$.
But maybe the best way to illustrate the difference between $vdash$ and $vDash$ is to consider a case where they don't both hold at the same time.
So, suppose I write a new logic textbook, and suppose that I develop a very simple system for making formal proofs, in that it has a single rule of inference:
Hokus Ponens
$$therefore varphi$$
Now, with Hokus Ponens, I can derive anything from nothing. Thus, for example, it will be true that $P vdash Q$. Here is the derivation/formal proof:
$P$ Premise
$Q$ Hokus Ponens!
But obviously, $Q$ does not logically follow from $P$. That is: $P not vDash Q$.
answered Mar 27 '17 at 19:48
Bram28Bram28
63.1k44793
$endgroup$
add a comment |
$begingroup$
$vdash$ is used to make statement about formal proof systems, which include rules of inference, that say:
"If you have a (or two) statement(s) that look like such-and-so, then you can write down a new statement that looks like this-and-that".
For example, many formal proof systems include the following rule of inference called Modus Ponens:
$$varphi$$
$$varphi rightarrow psi$$
$$therefore psi$$
So with this rule, I can, for example, infer $B land C$ from $A$ and $A rightarrow (B land C)$. The fact that I can do this within the proof system we write as: $A, A rightarrow (B land C) vdash B land C$.
Now, as it so happens, $B land C$ does in fact logically follow from $A$ and $A rightarrow (B land C)$. That is, the way we defined the formal semantics (think truth-tables) is such that whenever $A$ and $A rightarrow (B land C)$ are true, $B land C$ will have to be true as well. And that we write as $A, A rightarrow (B land C) vDash B land C$.
But maybe the best way to illustrate the difference between $vdash$ and $vDash$ is to consider a case where they don't both hold at the same time.
So, suppose I write a new logic textbook, and suppose that I develop a very simple system for making formal proofs, in that it has a single rule of inference:
Hokus Ponens
$$therefore varphi$$
Now, with Hokus Ponens, I can derive anything from nothing. Thus, for example, it will be true that $P vdash Q$. Here is the derivation/formal proof:
$P$ Premise
$Q$ Hokus Ponens!
But obviously, $Q$ does not logically follow from $P$. That is: $P not vDash Q$.
answered Mar 27 '17 at 19:48
Bram28Bram28
63.1k44793
$endgroup$
add a comment |
$begingroup$
$vdash$ is used to make statement about formal proof systems, which include rules of inference, that say:
"If you have a (or two) statement(s) that look like such-and-so, then you can write down a new statement that looks like this-and-that".
For example, many formal proof systems include the following rule of inference called Modus Ponens:
$$varphi$$
$$varphi rightarrow psi$$
$$therefore psi$$
So with this rule, I can, for example, infer $B land C$ from $A$ and $A rightarrow (B land C)$. The fact that I can do this within the proof system we write as: $A, A rightarrow (B land C) vdash B land C$.
Now, as it so happens, $B land C$ does in fact logically follow from $A$ and $A rightarrow (B land C)$. That is, the way we defined the formal semantics (think truth-tables) is such that whenever $A$ and $A rightarrow (B land C)$ are true, $B land C$ will have to be true as well. And that we write as $A, A rightarrow (B land C) vDash B land C$.
But maybe the best way to illustrate the difference between $vdash$ and $vDash$ is to consider a case where they don't both hold at the same time.
So, suppose I write a new logic textbook, and suppose that I develop a very simple system for making formal proofs, in that it has a single rule of inference:
Hokus Ponens
$$therefore varphi$$
Now, with Hokus Ponens, I can derive anything from nothing. Thus, for example, it will be true that $P vdash Q$. Here is the derivation/formal proof:
$P$ Premise
$Q$ Hokus Ponens!
But obviously, $Q$ does not logically follow from $P$. That is: $P not vDash Q$.
answered Mar 27 '17 at 19:48
Bram28Bram28
63.1k44793
$endgroup$
$vdash$ is used to make statement about formal proof systems, which include rules of inference, that say:
"If you have a (or two) statement(s) that look like such-and-so, then you can write down a new statement that looks like this-and-that".
For example, many formal proof systems include the following rule of inference called Modus Ponens:
$$varphi$$
$$varphi rightarrow psi$$
$$therefore psi$$
So with this rule, I can, for example, infer $B land C$ from $A$ and $A rightarrow (B land C)$. The fact that I can do this within the proof system we write as: $A, A rightarrow (B land C) vdash B land C$.
Now, as it so happens, $B land C$ does in fact logically follow from $A$ and $A rightarrow (B land C)$. That is, the way we defined the formal semantics (think truth-tables) is such that whenever $A$ and $A rightarrow (B land C)$ are true, $B land C$ will have to be true as well. And that we write as $A, A rightarrow (B land C) vDash B land C$.
But maybe the best way to illustrate the difference between $vdash$ and $vDash$ is to consider a case where they don't both hold at the same time.
So, suppose I write a new logic textbook, and suppose that I develop a very simple system for making formal proofs, in that it has a single rule of inference:
Hokus Ponens
$$therefore varphi$$
Now, with Hokus Ponens, I can derive anything from nothing. Thus, for example, it will be true that $P vdash Q$. Here is the derivation/formal proof:
$P$ Premise
$Q$ Hokus Ponens!
But obviously, $Q$ does not logically follow from $P$. That is: $P not vDash Q$.
answered Mar 27 '17 at 19:48
Bram28Bram28
63.1k44793
edited Jan 16 at 19:21
answered Mar 27 '17 at 19:48
Bram28Bram28
63.1k44793
answered Mar 27 '17 at 19:48
Bram28Bram28
63.1k44793
answered Mar 27 '17 at 19:48
Bram28Bram28
63.1k44793
63.1k44793
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.
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%2f2205688%2fsemantic-consequence-definition%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
1
$begingroup$
See the post : difference-between-syntactic-consequence-and-semantic-consequence.
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:30
1
$begingroup$
See also the post : what-is-the-meaning-of-the-double-turnstile-symbol
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:32
1
$begingroup$
See also the post : why-are $vdash$ and $vDash$ symbols-from-metalanguage
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:34
1
$begingroup$
See also the post meaning-of-symbols $vdash$ and $models$
$endgroup$
– Mauro ALLEGRANZA
Mar 27 '17 at 18:35
$begingroup$
I can not help but notice that you are the same person that wrote about the axiom for set theory. I am still confused with these symbols. I will read about them more. Can you explain them to me?
$endgroup$
– Will
Mar 27 '17 at 18:42