Mixing
$to$ vs. $vdash$ in logic
Clash Royale CLAN TAG#URR8PPP
up vote
3
down vote
favorite
I am really lost trying to understand the difference between the logical connective "implies", $to$, and the metalogical symbol (or maybe it's also a connective?) $vdash$. (This is all focusing on prepositional logic here).
In metalogical terms, for example with modus ponens, it is said that $P, P to Q vdash Q$, which means "If we have a proof of $P$, and we have a proof of $P to Q$, then we can infer / make a proof of $Q$". But I don't understand what the difference is between that and saying something like $P land (P to Q) to Q$ which is similar but uses $to$ instead of $vdash$.
For example the $P to Q$, at least in my experience, means "it is possible to go from $P$ to $Q$" but I don't see how "going to $Q$" is different from "inferring $Q$." Simply telling me that one is metalogical and one is not doesn't really help me understand what's going on.
I've also been given the example of what the tortoise said to Achilles but I don't understand this, either. It sounds like the tortoise is constantly rejecting implications because "who says I have to accept conclusions just because the premises are true?" but then somehow introducing a metalogical $vdash$ solves this? "We use the metalogical symbol $vdash$ to basically force that stubborn tortoise to accept the conclusions and we've now circumvented the issue."
Unless I've grossly misunderstood something I just don't see why that's even a thing. Who says then I have to accept $vdash$? Is $vdash$ just a stronger form of $to$, like a "sudo $to$" or something (to borrow a Linux term), a form of implies that forces the conclusion to be accepted from the premise(s)?
What's the difference? How are they working here? Why do we need them? Are there any concrete examples showing the difference of both?
logic definition propositional-calculus metalogic
edited Sep 3 at 18:02
David C. Ullrich
55.6k43787
asked Sep 3 at 13:52
user525966
1,535619
 |Â
show 6 more comments
up vote
3
down vote
favorite
I am really lost trying to understand the difference between the logical connective "implies", $to$, and the metalogical symbol (or maybe it's also a connective?) $vdash$. (This is all focusing on prepositional logic here).
In metalogical terms, for example with modus ponens, it is said that $P, P to Q vdash Q$, which means "If we have a proof of $P$, and we have a proof of $P to Q$, then we can infer / make a proof of $Q$". But I don't understand what the difference is between that and saying something like $P land (P to Q) to Q$ which is similar but uses $to$ instead of $vdash$.
For example the $P to Q$, at least in my experience, means "it is possible to go from $P$ to $Q$" but I don't see how "going to $Q$" is different from "inferring $Q$." Simply telling me that one is metalogical and one is not doesn't really help me understand what's going on.
I've also been given the example of what the tortoise said to Achilles but I don't understand this, either. It sounds like the tortoise is constantly rejecting implications because "who says I have to accept conclusions just because the premises are true?" but then somehow introducing a metalogical $vdash$ solves this? "We use the metalogical symbol $vdash$ to basically force that stubborn tortoise to accept the conclusions and we've now circumvented the issue."
Unless I've grossly misunderstood something I just don't see why that's even a thing. Who says then I have to accept $vdash$? Is $vdash$ just a stronger form of $to$, like a "sudo $to$" or something (to borrow a Linux term), a form of implies that forces the conclusion to be accepted from the premise(s)?
What's the difference? How are they working here? Why do we need them? Are there any concrete examples showing the difference of both?
logic definition propositional-calculus metalogic
edited Sep 3 at 18:02
David C. Ullrich
55.6k43787
asked Sep 3 at 13:52
user525966
1,535619
First basic difference: we may have a logical language without the connective $to$ (for classical logic $land$ and $lnot$ are enough) but the relationS of $vdash$ (derivability in the calculus) and $vDash$ (logical consequence) will not change.
– Mauro ALLEGRANZA
Sep 3 at 13:55
But then using your connectives $land, lnot$ what stops us from defining $p lor q = lnot(lnot p land lnot q)$, and $p to q = lnot p lor q$ and introducing the symbols all the same?
– user525966
Sep 3 at 13:57
I don't think this is a duplicate -- I've seen that answer already and all it says is basically "this one's metalogic, this one's within logic" which does not address my confusion
– user525966
Sep 3 at 13:59
$lnot p lor q$ means (in the "standard" classical (i.e. truth-functional) reading of the connectives) : "either $p$ is false or $q$ is true".
– Mauro ALLEGRANZA
Sep 3 at 14:00
2
See also the post Implies vs Entails vs Provable
– Mauro ALLEGRANZA
Sep 3 at 14:02
 |Â
show 6 more comments
up vote
3
down vote
favorite
up vote
3
down vote
favorite
I am really lost trying to understand the difference between the logical connective "implies", $to$, and the metalogical symbol (or maybe it's also a connective?) $vdash$. (This is all focusing on prepositional logic here).
In metalogical terms, for example with modus ponens, it is said that $P, P to Q vdash Q$, which means "If we have a proof of $P$, and we have a proof of $P to Q$, then we can infer / make a proof of $Q$". But I don't understand what the difference is between that and saying something like $P land (P to Q) to Q$ which is similar but uses $to$ instead of $vdash$.
For example the $P to Q$, at least in my experience, means "it is possible to go from $P$ to $Q$" but I don't see how "going to $Q$" is different from "inferring $Q$." Simply telling me that one is metalogical and one is not doesn't really help me understand what's going on.
I've also been given the example of what the tortoise said to Achilles but I don't understand this, either. It sounds like the tortoise is constantly rejecting implications because "who says I have to accept conclusions just because the premises are true?" but then somehow introducing a metalogical $vdash$ solves this? "We use the metalogical symbol $vdash$ to basically force that stubborn tortoise to accept the conclusions and we've now circumvented the issue."
Unless I've grossly misunderstood something I just don't see why that's even a thing. Who says then I have to accept $vdash$? Is $vdash$ just a stronger form of $to$, like a "sudo $to$" or something (to borrow a Linux term), a form of implies that forces the conclusion to be accepted from the premise(s)?
What's the difference? How are they working here? Why do we need them? Are there any concrete examples showing the difference of both?
logic definition propositional-calculus metalogic
edited Sep 3 at 18:02
David C. Ullrich
55.6k43787
asked Sep 3 at 13:52
user525966
1,535619
I am really lost trying to understand the difference between the logical connective "implies", $to$, and the metalogical symbol (or maybe it's also a connective?) $vdash$. (This is all focusing on prepositional logic here).
In metalogical terms, for example with modus ponens, it is said that $P, P to Q vdash Q$, which means "If we have a proof of $P$, and we have a proof of $P to Q$, then we can infer / make a proof of $Q$". But I don't understand what the difference is between that and saying something like $P land (P to Q) to Q$ which is similar but uses $to$ instead of $vdash$.
For example the $P to Q$, at least in my experience, means "it is possible to go from $P$ to $Q$" but I don't see how "going to $Q$" is different from "inferring $Q$." Simply telling me that one is metalogical and one is not doesn't really help me understand what's going on.
I've also been given the example of what the tortoise said to Achilles but I don't understand this, either. It sounds like the tortoise is constantly rejecting implications because "who says I have to accept conclusions just because the premises are true?" but then somehow introducing a metalogical $vdash$ solves this? "We use the metalogical symbol $vdash$ to basically force that stubborn tortoise to accept the conclusions and we've now circumvented the issue."
Unless I've grossly misunderstood something I just don't see why that's even a thing. Who says then I have to accept $vdash$? Is $vdash$ just a stronger form of $to$, like a "sudo $to$" or something (to borrow a Linux term), a form of implies that forces the conclusion to be accepted from the premise(s)?
What's the difference? How are they working here? Why do we need them? Are there any concrete examples showing the difference of both?
logic definition propositional-calculus metalogic
edited Sep 3 at 18:02
David C. Ullrich
55.6k43787
asked Sep 3 at 13:52
user525966
1,535619
edited Sep 3 at 18:02
David C. Ullrich
55.6k43787
edited Sep 3 at 18:02
David C. Ullrich
55.6k43787
edited Sep 3 at 18:02
David C. Ullrich
55.6k43787
55.6k43787
asked Sep 3 at 13:52
user525966
1,535619
asked Sep 3 at 13:52
user525966
1,535619
asked Sep 3 at 13:52
user525966
1,535619
1,535619
First basic difference: we may have a logical language without the connective $to$ (for classical logic $land$ and $lnot$ are enough) but the relationS of $vdash$ (derivability in the calculus) and $vDash$ (logical consequence) will not change.
– Mauro ALLEGRANZA
Sep 3 at 13:55
But then using your connectives $land, lnot$ what stops us from defining $p lor q = lnot(lnot p land lnot q)$, and $p to q = lnot p lor q$ and introducing the symbols all the same?
– user525966
Sep 3 at 13:57
I don't think this is a duplicate -- I've seen that answer already and all it says is basically "this one's metalogic, this one's within logic" which does not address my confusion
– user525966
Sep 3 at 13:59
$lnot p lor q$ means (in the "standard" classical (i.e. truth-functional) reading of the connectives) : "either $p$ is false or $q$ is true".
– Mauro ALLEGRANZA
Sep 3 at 14:00
2
See also the post Implies vs Entails vs Provable
– Mauro ALLEGRANZA
Sep 3 at 14:02
 |Â
show 6 more comments
First basic difference: we may have a logical language without the connective $to$ (for classical logic $land$ and $lnot$ are enough) but the relationS of $vdash$ (derivability in the calculus) and $vDash$ (logical consequence) will not change.
– Mauro ALLEGRANZA
Sep 3 at 13:55
But then using your connectives $land, lnot$ what stops us from defining $p lor q = lnot(lnot p land lnot q)$, and $p to q = lnot p lor q$ and introducing the symbols all the same?
– user525966
Sep 3 at 13:57
I don't think this is a duplicate -- I've seen that answer already and all it says is basically "this one's metalogic, this one's within logic" which does not address my confusion
– user525966
Sep 3 at 13:59
$lnot p lor q$ means (in the "standard" classical (i.e. truth-functional) reading of the connectives) : "either $p$ is false or $q$ is true".
– Mauro ALLEGRANZA
Sep 3 at 14:00
2
See also the post Implies vs Entails vs Provable
– Mauro ALLEGRANZA
Sep 3 at 14:02
First basic difference: we may have a logical language without the connective $to$ (for classical logic $land$ and $lnot$ are enough) but the relationS of $vdash$ (derivability in the calculus) and $vDash$ (logical consequence) will not change.
– Mauro ALLEGRANZA
Sep 3 at 13:55
First basic difference: we may have a logical language without the connective $to$ (for classical logic $land$ and $lnot$ are enough) but the relationS of $vdash$ (derivability in the calculus) and $vDash$ (logical consequence) will not change.
– Mauro ALLEGRANZA
Sep 3 at 13:55
But then using your connectives $land, lnot$ what stops us from defining $p lor q = lnot(lnot p land lnot q)$, and $p to q = lnot p lor q$ and introducing the symbols all the same?
– user525966
Sep 3 at 13:57
But then using your connectives $land, lnot$ what stops us from defining $p lor q = lnot(lnot p land lnot q)$, and $p to q = lnot p lor q$ and introducing the symbols all the same?
– user525966
Sep 3 at 13:57
I don't think this is a duplicate -- I've seen that answer already and all it says is basically "this one's metalogic, this one's within logic" which does not address my confusion
– user525966
Sep 3 at 13:59
I don't think this is a duplicate -- I've seen that answer already and all it says is basically "this one's metalogic, this one's within logic" which does not address my confusion
– user525966
Sep 3 at 13:59
$lnot p lor q$ means (in the "standard" classical (i.e. truth-functional) reading of the connectives) : "either $p$ is false or $q$ is true".
– Mauro ALLEGRANZA
Sep 3 at 14:00
$lnot p lor q$ means (in the "standard" classical (i.e. truth-functional) reading of the connectives) : "either $p$ is false or $q$ is true".
– Mauro ALLEGRANZA
Sep 3 at 14:00
2
2
See also the post Implies vs Entails vs Provable
– Mauro ALLEGRANZA
Sep 3 at 14:02
See also the post Implies vs Entails vs Provable
– Mauro ALLEGRANZA
Sep 3 at 14:02
 |Â
show 6 more comments
3 Answers
3
active
oldest
votes
up vote
6
down vote
accepted
First, I'm surprised that nobody has pointed out that reading $vdash$ as "infers" is simply wrong: implies versus infers.
You might read $vdash$ as "proves" or "entails". On the other hand, "infers" is roughly the same as "deduces". Saying $Avdash B$ means that one can deduce $B$ from $A$; if you read $vdash$ as "infers" you're reading $Avdash B$ as "$A$ deduces $B$", which, regardless of whether it makes any sense, certainly does not mean the same thing.
On the difference between $to$ and $vdash$: $Ato B$ is just a formula in ur formal system; it does not say anything (it's not an assertion). On the other hand, $Avdash B$ is a statement about the formulas $A$ and $B$; it says that given $A$ there is a proof of $B$ in whatever formal proof system we're taking about.
If the proof system is sound and complete then $Avdash B$ is equivalent to "$Ato B$ is a tautology". But jumping from there to the conclusion that $Avdash B$ is equivalent to $Ato B$ is wrong; "$Ato B$ is a tautology" is a statement about $A$ and $B$, while $Ato B$ is simply not a statement at all.
An analogy from algebra: if $x$ and $y$ are numbers then $x>y$ is a statement about $x$ and $y$, while $x-y$ is not a statement at all, it's just a number. It is true that "$x>y$ is equivalent to $x-y>0$", but if you concluded that "$x>y$ is equivalent to $x-y$" that would be clearly nonsense. Going from the true fact "$Avdash B$ is equivalent to the statement that $Ato B$ is a tautology" to "$Avdash B$ is equivalent to $Ato B$" is making exactly the same error
answered Sep 3 at 15:47
David C. Ullrich
55.6k43787
1
Yes, precisely! (In fact what I mean is that the $to$ means even less than "an arbitrary symbol relating $A$ and $B$ in some way". In a careful development of mathematical logic a wff is just a sting of symbols. There's a definition that specifies what strings are or are not wffs - part of the definition is "if $A$ and $B$ are wffs then $Ato B$ is a wff". Nothing about "relating $A$ to $B$"; wffs have no "meaning" until we assign truth values.)
– David C. Ullrich
Sep 3 at 17:16
1
When I say that the $to$ does not "relate $A$ and $B$": Analogously, the $+$ sign in $2+3$ does not "relate $2$ and $3$'. The $+$ sign is not a relation, it is an operator that takes two numbers and produces another number. If you want to understand the difference between $to$ and $vdash$ you need to understand that in exactly the same way $to$ is not a relation, it is an operator tat takes two wffs and produces another wff, and that's all it is. Otoh $vdash$ is a relation.
– David C. Ullrich
Sep 3 at 17:32
1
Yes. Again, a formal proof system is just a set of rules that says that we may "derive" a wff from other wffs; it doesn't necesarily have anything to do with the "meaning" of anything. For the specific proof system you have in mind it turns out that $Avdash B$ is equivalent to $Amodels B$, in other words $v(B)=T$ for every truth assignment $v$ such that $v(A)=T$. But that's a theorem, not something that has to be true for any proof system.
– David C. Ullrich
Sep 3 at 17:35
1
How an operator differs from a relation: They're not the same thing at all. For example, if I say "2+3" I haven't asserted anything; + is an operator, not a relation, so when I say "2+3" I've just pronounced a name for the number 5. On the other hand, $<$ is a relation: If I say "$2<3$" I have asserted something.
– David C. Ullrich
Sep 3 at 18:20
1
Yes, an operator is exactly a function! Except of course for the notation; since $+$ is a binary "infix" operator we write $2+3$ instead of $+(2,3)$. (Yes, it seems there's always some circularity. The formal definitions in logic talk about sets of this and sets of that - then formal set theory is defined using formal logic...)
– David C. Ullrich
Sep 3 at 18:48
 |Â
show 13 more comments
up vote
4
down vote
We have in place a very sharp distinction between the object language connective $to$ and the metalinguistic sign $vdash$ for the derivability relation (and the metalinguistic sign $vDash$ for the logical consequence (or entailment) relation).
$(P land Q) vdash Q$ expresses the existence in the propositional claculus
of an argument.
The metalinguistic formula asserts that we have a derivation of $Q$ from hypothesis $P land Q$.
A derivation in the calculus is the formal counterpart of the concept of inference: every step in the derivation is the application of a rule of inference (like e.g. modus ponens) and a rule of inference is the formalization of an "elementary step" in the inferential process.
The formula $(P land Q) to Q$ is a single formula in the language of propositional calculus.
If we assert it, we are assering that "either $(P land Q)$ is false or $Q$ is true".
In ordwer to appreciate the difference, we have to consider that we can formalize the propositional calculus with only teo conenctives :
$land$ and $lnot$ (or $lor$ and $lnot$)
but the derivability relation does not change its definition.
Of course, there is a link between the two notions, and the link is formalized by the meta-logic property of the calculus expressed by the Deduction Theorem stating that :
if a formula $B$ is derivable from a set of assumptions $Delta cup A$, then the formula $A to B$ is derivable from $Delta$.
The deduction theorem is a formalization of the common proof technique in which an implication $A to B$ is proved by assuming $A$ and then deriving $B$ from this assumption conjoined with known results.
answered Sep 3 at 14:43
Mauro ALLEGRANZA
61.1k446105
But say we only formalize the calculus with $lnot, land$. How do we then define and show how some new symbol like $to$ works?
– user525966
Sep 3 at 14:55
1
@user525966 - we introduce $p to q$ as an abbreviation of the formula $lnot p lor q$ (in classical logic) or as an abbreviation for $lnot (p land lnot q)$.
– Mauro ALLEGRANZA
Sep 3 at 15:04
But even after we introduce that symbol with that definition, how do we then know it is the appropriate connective to describe movement in things like mathematical proofs? How do we define how $land$ and $lnot$ work without truth tables? Do we have to define true and false?
– user525966
Sep 3 at 15:39
@user525966 - two steps. Syntactically, connectives are "defined" in thecalculus through the axioms and rules. Then, semantically, we have the truth tables for the connectives. We want that the two approaches match: this is the role of soundness and completeness properties: we want that the axioms and theorems of the calculus are sound (i.e. TRUE according to the semantical interpretation) and complete (i.e. that all TRUE formuklas will be derivable).
– Mauro ALLEGRANZA
Sep 4 at 6:19
Are truth tables the only way to give semantic quality? I thought they were more of a convenience rather than a necessity. The semantics can't be extracted from the way the axioms/inference rules are set up? Are truth tables metalogical?
– user525966
Sep 4 at 12:07
add a comment |Â
up vote
0
down vote
In our world, it is true that if it rains, things will get wet. We can express this truth as:
$R rightarrow W$
But it is certainly not true that:
$R vdash W$
That is, given $R$, we can't logically infer $W$. Why? Because we can imagine worlds where nothing gets wet, even if it rains.
answered Sep 3 at 17:24
Bram28
55.5k33982
So $A vdash B$ means $B$ is provable from $A$ regardless of the system we use, regardless of the "world" we're in?
– user525966
Sep 3 at 17:26
Saying we can express this truth as $Ato B$ is really totally missing the point.
– David C. Ullrich
Sep 3 at 17:40
@user525966 What $Avdash B$ means depends on what proof system we're talking about. A proof system has axioms and inference rules - given a proof system, saying $Avdash B$ means there is a finite sequence of wffs $A_1,dots, A_n$ such that $A_n=B$ and each $A_j$ is either $A$, an axiom, or a consequence of previous $A_i$ by one of the rules. That's all it means.
– David C. Ullrich
Sep 3 at 17:46
3
Why I say it's missing the point: What you're actually explaining here is more the difference between $Ato B$ and $models(Ato B)$. Of course it's a theorem that (for standard proof systems) $models(Ato B)$ if and only if $Avdash B$, but the two don't mean the same thing! If they meant the same thing the Soundness and Completeness theorems would have no content.
– David C. Ullrich
Sep 3 at 17:59
@DavidC.Ullrich The $vdash$ symbol then I imagine is mostly used in those inference rules in set $Z$ (I'm reading en.wikipedia.org/wiki/… when I reference this), giving you the rules that dictate how to jump from one wff (or collection thereof) to another wff. And then axioms are basically inference rules that don't have any premises, i.e. the conclusions come out of nothing by default?
– user525966
Sep 3 at 18:08
 |Â
show 5 more comments
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
6
down vote
accepted
First, I'm surprised that nobody has pointed out that reading $vdash$ as "infers" is simply wrong: implies versus infers.
You might read $vdash$ as "proves" or "entails". On the other hand, "infers" is roughly the same as "deduces". Saying $Avdash B$ means that one can deduce $B$ from $A$; if you read $vdash$ as "infers" you're reading $Avdash B$ as "$A$ deduces $B$", which, regardless of whether it makes any sense, certainly does not mean the same thing.
On the difference between $to$ and $vdash$: $Ato B$ is just a formula in ur formal system; it does not say anything (it's not an assertion). On the other hand, $Avdash B$ is a statement about the formulas $A$ and $B$; it says that given $A$ there is a proof of $B$ in whatever formal proof system we're taking about.
If the proof system is sound and complete then $Avdash B$ is equivalent to "$Ato B$ is a tautology". But jumping from there to the conclusion that $Avdash B$ is equivalent to $Ato B$ is wrong; "$Ato B$ is a tautology" is a statement about $A$ and $B$, while $Ato B$ is simply not a statement at all.
An analogy from algebra: if $x$ and $y$ are numbers then $x>y$ is a statement about $x$ and $y$, while $x-y$ is not a statement at all, it's just a number. It is true that "$x>y$ is equivalent to $x-y>0$", but if you concluded that "$x>y$ is equivalent to $x-y$" that would be clearly nonsense. Going from the true fact "$Avdash B$ is equivalent to the statement that $Ato B$ is a tautology" to "$Avdash B$ is equivalent to $Ato B$" is making exactly the same error
answered Sep 3 at 15:47
David C. Ullrich
55.6k43787
1
Yes, precisely! (In fact what I mean is that the $to$ means even less than "an arbitrary symbol relating $A$ and $B$ in some way". In a careful development of mathematical logic a wff is just a sting of symbols. There's a definition that specifies what strings are or are not wffs - part of the definition is "if $A$ and $B$ are wffs then $Ato B$ is a wff". Nothing about "relating $A$ to $B$"; wffs have no "meaning" until we assign truth values.)
– David C. Ullrich
Sep 3 at 17:16
1
When I say that the $to$ does not "relate $A$ and $B$": Analogously, the $+$ sign in $2+3$ does not "relate $2$ and $3$'. The $+$ sign is not a relation, it is an operator that takes two numbers and produces another number. If you want to understand the difference between $to$ and $vdash$ you need to understand that in exactly the same way $to$ is not a relation, it is an operator tat takes two wffs and produces another wff, and that's all it is. Otoh $vdash$ is a relation.
– David C. Ullrich
Sep 3 at 17:32
1
Yes. Again, a formal proof system is just a set of rules that says that we may "derive" a wff from other wffs; it doesn't necesarily have anything to do with the "meaning" of anything. For the specific proof system you have in mind it turns out that $Avdash B$ is equivalent to $Amodels B$, in other words $v(B)=T$ for every truth assignment $v$ such that $v(A)=T$. But that's a theorem, not something that has to be true for any proof system.
– David C. Ullrich
Sep 3 at 17:35
1
How an operator differs from a relation: They're not the same thing at all. For example, if I say "2+3" I haven't asserted anything; + is an operator, not a relation, so when I say "2+3" I've just pronounced a name for the number 5. On the other hand, $<$ is a relation: If I say "$2<3$" I have asserted something.
– David C. Ullrich
Sep 3 at 18:20
1
Yes, an operator is exactly a function! Except of course for the notation; since $+$ is a binary "infix" operator we write $2+3$ instead of $+(2,3)$. (Yes, it seems there's always some circularity. The formal definitions in logic talk about sets of this and sets of that - then formal set theory is defined using formal logic...)
– David C. Ullrich
Sep 3 at 18:48
 |Â
show 13 more comments
up vote
6
down vote
accepted
First, I'm surprised that nobody has pointed out that reading $vdash$ as "infers" is simply wrong: implies versus infers.
You might read $vdash$ as "proves" or "entails". On the other hand, "infers" is roughly the same as "deduces". Saying $Avdash B$ means that one can deduce $B$ from $A$; if you read $vdash$ as "infers" you're reading $Avdash B$ as "$A$ deduces $B$", which, regardless of whether it makes any sense, certainly does not mean the same thing.
On the difference between $to$ and $vdash$: $Ato B$ is just a formula in ur formal system; it does not say anything (it's not an assertion). On the other hand, $Avdash B$ is a statement about the formulas $A$ and $B$; it says that given $A$ there is a proof of $B$ in whatever formal proof system we're taking about.
If the proof system is sound and complete then $Avdash B$ is equivalent to "$Ato B$ is a tautology". But jumping from there to the conclusion that $Avdash B$ is equivalent to $Ato B$ is wrong; "$Ato B$ is a tautology" is a statement about $A$ and $B$, while $Ato B$ is simply not a statement at all.
An analogy from algebra: if $x$ and $y$ are numbers then $x>y$ is a statement about $x$ and $y$, while $x-y$ is not a statement at all, it's just a number. It is true that "$x>y$ is equivalent to $x-y>0$", but if you concluded that "$x>y$ is equivalent to $x-y$" that would be clearly nonsense. Going from the true fact "$Avdash B$ is equivalent to the statement that $Ato B$ is a tautology" to "$Avdash B$ is equivalent to $Ato B$" is making exactly the same error
answered Sep 3 at 15:47
David C. Ullrich
55.6k43787
1
Yes, precisely! (In fact what I mean is that the $to$ means even less than "an arbitrary symbol relating $A$ and $B$ in some way". In a careful development of mathematical logic a wff is just a sting of symbols. There's a definition that specifies what strings are or are not wffs - part of the definition is "if $A$ and $B$ are wffs then $Ato B$ is a wff". Nothing about "relating $A$ to $B$"; wffs have no "meaning" until we assign truth values.)
– David C. Ullrich
Sep 3 at 17:16
1
When I say that the $to$ does not "relate $A$ and $B$": Analogously, the $+$ sign in $2+3$ does not "relate $2$ and $3$'. The $+$ sign is not a relation, it is an operator that takes two numbers and produces another number. If you want to understand the difference between $to$ and $vdash$ you need to understand that in exactly the same way $to$ is not a relation, it is an operator tat takes two wffs and produces another wff, and that's all it is. Otoh $vdash$ is a relation.
– David C. Ullrich
Sep 3 at 17:32
1
Yes. Again, a formal proof system is just a set of rules that says that we may "derive" a wff from other wffs; it doesn't necesarily have anything to do with the "meaning" of anything. For the specific proof system you have in mind it turns out that $Avdash B$ is equivalent to $Amodels B$, in other words $v(B)=T$ for every truth assignment $v$ such that $v(A)=T$. But that's a theorem, not something that has to be true for any proof system.
– David C. Ullrich
Sep 3 at 17:35
1
How an operator differs from a relation: They're not the same thing at all. For example, if I say "2+3" I haven't asserted anything; + is an operator, not a relation, so when I say "2+3" I've just pronounced a name for the number 5. On the other hand, $<$ is a relation: If I say "$2<3$" I have asserted something.
– David C. Ullrich
Sep 3 at 18:20
1
Yes, an operator is exactly a function! Except of course for the notation; since $+$ is a binary "infix" operator we write $2+3$ instead of $+(2,3)$. (Yes, it seems there's always some circularity. The formal definitions in logic talk about sets of this and sets of that - then formal set theory is defined using formal logic...)
– David C. Ullrich
Sep 3 at 18:48
 |Â
show 13 more comments
up vote
6
down vote
accepted
up vote
6
down vote
accepted
First, I'm surprised that nobody has pointed out that reading $vdash$ as "infers" is simply wrong: implies versus infers.
You might read $vdash$ as "proves" or "entails". On the other hand, "infers" is roughly the same as "deduces". Saying $Avdash B$ means that one can deduce $B$ from $A$; if you read $vdash$ as "infers" you're reading $Avdash B$ as "$A$ deduces $B$", which, regardless of whether it makes any sense, certainly does not mean the same thing.
On the difference between $to$ and $vdash$: $Ato B$ is just a formula in ur formal system; it does not say anything (it's not an assertion). On the other hand, $Avdash B$ is a statement about the formulas $A$ and $B$; it says that given $A$ there is a proof of $B$ in whatever formal proof system we're taking about.
If the proof system is sound and complete then $Avdash B$ is equivalent to "$Ato B$ is a tautology". But jumping from there to the conclusion that $Avdash B$ is equivalent to $Ato B$ is wrong; "$Ato B$ is a tautology" is a statement about $A$ and $B$, while $Ato B$ is simply not a statement at all.
An analogy from algebra: if $x$ and $y$ are numbers then $x>y$ is a statement about $x$ and $y$, while $x-y$ is not a statement at all, it's just a number. It is true that "$x>y$ is equivalent to $x-y>0$", but if you concluded that "$x>y$ is equivalent to $x-y$" that would be clearly nonsense. Going from the true fact "$Avdash B$ is equivalent to the statement that $Ato B$ is a tautology" to "$Avdash B$ is equivalent to $Ato B$" is making exactly the same error
answered Sep 3 at 15:47
David C. Ullrich
55.6k43787
First, I'm surprised that nobody has pointed out that reading $vdash$ as "infers" is simply wrong: implies versus infers.
You might read $vdash$ as "proves" or "entails". On the other hand, "infers" is roughly the same as "deduces". Saying $Avdash B$ means that one can deduce $B$ from $A$; if you read $vdash$ as "infers" you're reading $Avdash B$ as "$A$ deduces $B$", which, regardless of whether it makes any sense, certainly does not mean the same thing.
On the difference between $to$ and $vdash$: $Ato B$ is just a formula in ur formal system; it does not say anything (it's not an assertion). On the other hand, $Avdash B$ is a statement about the formulas $A$ and $B$; it says that given $A$ there is a proof of $B$ in whatever formal proof system we're taking about.
If the proof system is sound and complete then $Avdash B$ is equivalent to "$Ato B$ is a tautology". But jumping from there to the conclusion that $Avdash B$ is equivalent to $Ato B$ is wrong; "$Ato B$ is a tautology" is a statement about $A$ and $B$, while $Ato B$ is simply not a statement at all.
An analogy from algebra: if $x$ and $y$ are numbers then $x>y$ is a statement about $x$ and $y$, while $x-y$ is not a statement at all, it's just a number. It is true that "$x>y$ is equivalent to $x-y>0$", but if you concluded that "$x>y$ is equivalent to $x-y$" that would be clearly nonsense. Going from the true fact "$Avdash B$ is equivalent to the statement that $Ato B$ is a tautology" to "$Avdash B$ is equivalent to $Ato B$" is making exactly the same error
answered Sep 3 at 15:47
David C. Ullrich
55.6k43787
answered Sep 3 at 15:47
David C. Ullrich
55.6k43787
answered Sep 3 at 15:47
David C. Ullrich
55.6k43787
answered Sep 3 at 15:47
David C. Ullrich
55.6k43787
55.6k43787
1
Yes, precisely! (In fact what I mean is that the $to$ means even less than "an arbitrary symbol relating $A$ and $B$ in some way". In a careful development of mathematical logic a wff is just a sting of symbols. There's a definition that specifies what strings are or are not wffs - part of the definition is "if $A$ and $B$ are wffs then $Ato B$ is a wff". Nothing about "relating $A$ to $B$"; wffs have no "meaning" until we assign truth values.)
– David C. Ullrich
Sep 3 at 17:16
1
When I say that the $to$ does not "relate $A$ and $B$": Analogously, the $+$ sign in $2+3$ does not "relate $2$ and $3$'. The $+$ sign is not a relation, it is an operator that takes two numbers and produces another number. If you want to understand the difference between $to$ and $vdash$ you need to understand that in exactly the same way $to$ is not a relation, it is an operator tat takes two wffs and produces another wff, and that's all it is. Otoh $vdash$ is a relation.
– David C. Ullrich
Sep 3 at 17:32
1
Yes. Again, a formal proof system is just a set of rules that says that we may "derive" a wff from other wffs; it doesn't necesarily have anything to do with the "meaning" of anything. For the specific proof system you have in mind it turns out that $Avdash B$ is equivalent to $Amodels B$, in other words $v(B)=T$ for every truth assignment $v$ such that $v(A)=T$. But that's a theorem, not something that has to be true for any proof system.
– David C. Ullrich
Sep 3 at 17:35
1
How an operator differs from a relation: They're not the same thing at all. For example, if I say "2+3" I haven't asserted anything; + is an operator, not a relation, so when I say "2+3" I've just pronounced a name for the number 5. On the other hand, $<$ is a relation: If I say "$2<3$" I have asserted something.
– David C. Ullrich
Sep 3 at 18:20
1
Yes, an operator is exactly a function! Except of course for the notation; since $+$ is a binary "infix" operator we write $2+3$ instead of $+(2,3)$. (Yes, it seems there's always some circularity. The formal definitions in logic talk about sets of this and sets of that - then formal set theory is defined using formal logic...)
– David C. Ullrich
Sep 3 at 18:48
 |Â
show 13 more comments
1
Yes, precisely! (In fact what I mean is that the $to$ means even less than "an arbitrary symbol relating $A$ and $B$ in some way". In a careful development of mathematical logic a wff is just a sting of symbols. There's a definition that specifies what strings are or are not wffs - part of the definition is "if $A$ and $B$ are wffs then $Ato B$ is a wff". Nothing about "relating $A$ to $B$"; wffs have no "meaning" until we assign truth values.)
– David C. Ullrich
Sep 3 at 17:16
1
When I say that the $to$ does not "relate $A$ and $B$": Analogously, the $+$ sign in $2+3$ does not "relate $2$ and $3$'. The $+$ sign is not a relation, it is an operator that takes two numbers and produces another number. If you want to understand the difference between $to$ and $vdash$ you need to understand that in exactly the same way $to$ is not a relation, it is an operator tat takes two wffs and produces another wff, and that's all it is. Otoh $vdash$ is a relation.
– David C. Ullrich
Sep 3 at 17:32
1
Yes. Again, a formal proof system is just a set of rules that says that we may "derive" a wff from other wffs; it doesn't necesarily have anything to do with the "meaning" of anything. For the specific proof system you have in mind it turns out that $Avdash B$ is equivalent to $Amodels B$, in other words $v(B)=T$ for every truth assignment $v$ such that $v(A)=T$. But that's a theorem, not something that has to be true for any proof system.
– David C. Ullrich
Sep 3 at 17:35
1
How an operator differs from a relation: They're not the same thing at all. For example, if I say "2+3" I haven't asserted anything; + is an operator, not a relation, so when I say "2+3" I've just pronounced a name for the number 5. On the other hand, $<$ is a relation: If I say "$2<3$" I have asserted something.
– David C. Ullrich
Sep 3 at 18:20
1
Yes, an operator is exactly a function! Except of course for the notation; since $+$ is a binary "infix" operator we write $2+3$ instead of $+(2,3)$. (Yes, it seems there's always some circularity. The formal definitions in logic talk about sets of this and sets of that - then formal set theory is defined using formal logic...)
– David C. Ullrich
Sep 3 at 18:48
1
1
Yes, precisely! (In fact what I mean is that the $to$ means even less than "an arbitrary symbol relating $A$ and $B$ in some way". In a careful development of mathematical logic a wff is just a sting of symbols. There's a definition that specifies what strings are or are not wffs - part of the definition is "if $A$ and $B$ are wffs then $Ato B$ is a wff". Nothing about "relating $A$ to $B$"; wffs have no "meaning" until we assign truth values.)
– David C. Ullrich
Sep 3 at 17:16
Yes, precisely! (In fact what I mean is that the $to$ means even less than "an arbitrary symbol relating $A$ and $B$ in some way". In a careful development of mathematical logic a wff is just a sting of symbols. There's a definition that specifies what strings are or are not wffs - part of the definition is "if $A$ and $B$ are wffs then $Ato B$ is a wff". Nothing about "relating $A$ to $B$"; wffs have no "meaning" until we assign truth values.)
– David C. Ullrich
Sep 3 at 17:16
1
1
When I say that the $to$ does not "relate $A$ and $B$": Analogously, the $+$ sign in $2+3$ does not "relate $2$ and $3$'. The $+$ sign is not a relation, it is an operator that takes two numbers and produces another number. If you want to understand the difference between $to$ and $vdash$ you need to understand that in exactly the same way $to$ is not a relation, it is an operator tat takes two wffs and produces another wff, and that's all it is. Otoh $vdash$ is a relation.
– David C. Ullrich
Sep 3 at 17:32
When I say that the $to$ does not "relate $A$ and $B$": Analogously, the $+$ sign in $2+3$ does not "relate $2$ and $3$'. The $+$ sign is not a relation, it is an operator that takes two numbers and produces another number. If you want to understand the difference between $to$ and $vdash$ you need to understand that in exactly the same way $to$ is not a relation, it is an operator tat takes two wffs and produces another wff, and that's all it is. Otoh $vdash$ is a relation.
– David C. Ullrich
Sep 3 at 17:32
1
1
Yes. Again, a formal proof system is just a set of rules that says that we may "derive" a wff from other wffs; it doesn't necesarily have anything to do with the "meaning" of anything. For the specific proof system you have in mind it turns out that $Avdash B$ is equivalent to $Amodels B$, in other words $v(B)=T$ for every truth assignment $v$ such that $v(A)=T$. But that's a theorem, not something that has to be true for any proof system.
– David C. Ullrich
Sep 3 at 17:35
Yes. Again, a formal proof system is just a set of rules that says that we may "derive" a wff from other wffs; it doesn't necesarily have anything to do with the "meaning" of anything. For the specific proof system you have in mind it turns out that $Avdash B$ is equivalent to $Amodels B$, in other words $v(B)=T$ for every truth assignment $v$ such that $v(A)=T$. But that's a theorem, not something that has to be true for any proof system.
– David C. Ullrich
Sep 3 at 17:35
1
1
How an operator differs from a relation: They're not the same thing at all. For example, if I say "2+3" I haven't asserted anything; + is an operator, not a relation, so when I say "2+3" I've just pronounced a name for the number 5. On the other hand, $<$ is a relation: If I say "$2<3$" I have asserted something.
– David C. Ullrich
Sep 3 at 18:20
How an operator differs from a relation: They're not the same thing at all. For example, if I say "2+3" I haven't asserted anything; + is an operator, not a relation, so when I say "2+3" I've just pronounced a name for the number 5. On the other hand, $<$ is a relation: If I say "$2<3$" I have asserted something.
– David C. Ullrich
Sep 3 at 18:20
1
1
Yes, an operator is exactly a function! Except of course for the notation; since $+$ is a binary "infix" operator we write $2+3$ instead of $+(2,3)$. (Yes, it seems there's always some circularity. The formal definitions in logic talk about sets of this and sets of that - then formal set theory is defined using formal logic...)
– David C. Ullrich
Sep 3 at 18:48
Yes, an operator is exactly a function! Except of course for the notation; since $+$ is a binary "infix" operator we write $2+3$ instead of $+(2,3)$. (Yes, it seems there's always some circularity. The formal definitions in logic talk about sets of this and sets of that - then formal set theory is defined using formal logic...)
– David C. Ullrich
Sep 3 at 18:48
 |Â
show 13 more comments
up vote
4
down vote
We have in place a very sharp distinction between the object language connective $to$ and the metalinguistic sign $vdash$ for the derivability relation (and the metalinguistic sign $vDash$ for the logical consequence (or entailment) relation).
$(P land Q) vdash Q$ expresses the existence in the propositional claculus
of an argument.
The metalinguistic formula asserts that we have a derivation of $Q$ from hypothesis $P land Q$.
A derivation in the calculus is the formal counterpart of the concept of inference: every step in the derivation is the application of a rule of inference (like e.g. modus ponens) and a rule of inference is the formalization of an "elementary step" in the inferential process.
The formula $(P land Q) to Q$ is a single formula in the language of propositional calculus.
If we assert it, we are assering that "either $(P land Q)$ is false or $Q$ is true".
In ordwer to appreciate the difference, we have to consider that we can formalize the propositional calculus with only teo conenctives :
$land$ and $lnot$ (or $lor$ and $lnot$)
but the derivability relation does not change its definition.
Of course, there is a link between the two notions, and the link is formalized by the meta-logic property of the calculus expressed by the Deduction Theorem stating that :
if a formula $B$ is derivable from a set of assumptions $Delta cup A$, then the formula $A to B$ is derivable from $Delta$.
The deduction theorem is a formalization of the common proof technique in which an implication $A to B$ is proved by assuming $A$ and then deriving $B$ from this assumption conjoined with known results.
answered Sep 3 at 14:43
Mauro ALLEGRANZA
61.1k446105
But say we only formalize the calculus with $lnot, land$. How do we then define and show how some new symbol like $to$ works?
– user525966
Sep 3 at 14:55
1
@user525966 - we introduce $p to q$ as an abbreviation of the formula $lnot p lor q$ (in classical logic) or as an abbreviation for $lnot (p land lnot q)$.
– Mauro ALLEGRANZA
Sep 3 at 15:04
But even after we introduce that symbol with that definition, how do we then know it is the appropriate connective to describe movement in things like mathematical proofs? How do we define how $land$ and $lnot$ work without truth tables? Do we have to define true and false?
– user525966
Sep 3 at 15:39
@user525966 - two steps. Syntactically, connectives are "defined" in thecalculus through the axioms and rules. Then, semantically, we have the truth tables for the connectives. We want that the two approaches match: this is the role of soundness and completeness properties: we want that the axioms and theorems of the calculus are sound (i.e. TRUE according to the semantical interpretation) and complete (i.e. that all TRUE formuklas will be derivable).
– Mauro ALLEGRANZA
Sep 4 at 6:19
Are truth tables the only way to give semantic quality? I thought they were more of a convenience rather than a necessity. The semantics can't be extracted from the way the axioms/inference rules are set up? Are truth tables metalogical?
– user525966
Sep 4 at 12:07
add a comment |Â
up vote
4
down vote
We have in place a very sharp distinction between the object language connective $to$ and the metalinguistic sign $vdash$ for the derivability relation (and the metalinguistic sign $vDash$ for the logical consequence (or entailment) relation).
$(P land Q) vdash Q$ expresses the existence in the propositional claculus
of an argument.
The metalinguistic formula asserts that we have a derivation of $Q$ from hypothesis $P land Q$.
A derivation in the calculus is the formal counterpart of the concept of inference: every step in the derivation is the application of a rule of inference (like e.g. modus ponens) and a rule of inference is the formalization of an "elementary step" in the inferential process.
The formula $(P land Q) to Q$ is a single formula in the language of propositional calculus.
If we assert it, we are assering that "either $(P land Q)$ is false or $Q$ is true".
In ordwer to appreciate the difference, we have to consider that we can formalize the propositional calculus with only teo conenctives :
$land$ and $lnot$ (or $lor$ and $lnot$)
but the derivability relation does not change its definition.
Of course, there is a link between the two notions, and the link is formalized by the meta-logic property of the calculus expressed by the Deduction Theorem stating that :
if a formula $B$ is derivable from a set of assumptions $Delta cup A$, then the formula $A to B$ is derivable from $Delta$.
The deduction theorem is a formalization of the common proof technique in which an implication $A to B$ is proved by assuming $A$ and then deriving $B$ from this assumption conjoined with known results.
answered Sep 3 at 14:43
Mauro ALLEGRANZA
61.1k446105
But say we only formalize the calculus with $lnot, land$. How do we then define and show how some new symbol like $to$ works?
– user525966
Sep 3 at 14:55
1
@user525966 - we introduce $p to q$ as an abbreviation of the formula $lnot p lor q$ (in classical logic) or as an abbreviation for $lnot (p land lnot q)$.
– Mauro ALLEGRANZA
Sep 3 at 15:04
But even after we introduce that symbol with that definition, how do we then know it is the appropriate connective to describe movement in things like mathematical proofs? How do we define how $land$ and $lnot$ work without truth tables? Do we have to define true and false?
– user525966
Sep 3 at 15:39
@user525966 - two steps. Syntactically, connectives are "defined" in thecalculus through the axioms and rules. Then, semantically, we have the truth tables for the connectives. We want that the two approaches match: this is the role of soundness and completeness properties: we want that the axioms and theorems of the calculus are sound (i.e. TRUE according to the semantical interpretation) and complete (i.e. that all TRUE formuklas will be derivable).
– Mauro ALLEGRANZA
Sep 4 at 6:19
Are truth tables the only way to give semantic quality? I thought they were more of a convenience rather than a necessity. The semantics can't be extracted from the way the axioms/inference rules are set up? Are truth tables metalogical?
– user525966
Sep 4 at 12:07
add a comment |Â
up vote
4
down vote
up vote
4
down vote
We have in place a very sharp distinction between the object language connective $to$ and the metalinguistic sign $vdash$ for the derivability relation (and the metalinguistic sign $vDash$ for the logical consequence (or entailment) relation).
$(P land Q) vdash Q$ expresses the existence in the propositional claculus
of an argument.
The metalinguistic formula asserts that we have a derivation of $Q$ from hypothesis $P land Q$.
A derivation in the calculus is the formal counterpart of the concept of inference: every step in the derivation is the application of a rule of inference (like e.g. modus ponens) and a rule of inference is the formalization of an "elementary step" in the inferential process.
The formula $(P land Q) to Q$ is a single formula in the language of propositional calculus.
If we assert it, we are assering that "either $(P land Q)$ is false or $Q$ is true".
In ordwer to appreciate the difference, we have to consider that we can formalize the propositional calculus with only teo conenctives :
$land$ and $lnot$ (or $lor$ and $lnot$)
but the derivability relation does not change its definition.
Of course, there is a link between the two notions, and the link is formalized by the meta-logic property of the calculus expressed by the Deduction Theorem stating that :
if a formula $B$ is derivable from a set of assumptions $Delta cup A$, then the formula $A to B$ is derivable from $Delta$.
The deduction theorem is a formalization of the common proof technique in which an implication $A to B$ is proved by assuming $A$ and then deriving $B$ from this assumption conjoined with known results.
answered Sep 3 at 14:43
Mauro ALLEGRANZA
61.1k446105
We have in place a very sharp distinction between the object language connective $to$ and the metalinguistic sign $vdash$ for the derivability relation (and the metalinguistic sign $vDash$ for the logical consequence (or entailment) relation).
$(P land Q) vdash Q$ expresses the existence in the propositional claculus
of an argument.
The metalinguistic formula asserts that we have a derivation of $Q$ from hypothesis $P land Q$.
A derivation in the calculus is the formal counterpart of the concept of inference: every step in the derivation is the application of a rule of inference (like e.g. modus ponens) and a rule of inference is the formalization of an "elementary step" in the inferential process.
The formula $(P land Q) to Q$ is a single formula in the language of propositional calculus.
If we assert it, we are assering that "either $(P land Q)$ is false or $Q$ is true".
In ordwer to appreciate the difference, we have to consider that we can formalize the propositional calculus with only teo conenctives :
$land$ and $lnot$ (or $lor$ and $lnot$)
but the derivability relation does not change its definition.
Of course, there is a link between the two notions, and the link is formalized by the meta-logic property of the calculus expressed by the Deduction Theorem stating that :
if a formula $B$ is derivable from a set of assumptions $Delta cup A$, then the formula $A to B$ is derivable from $Delta$.
The deduction theorem is a formalization of the common proof technique in which an implication $A to B$ is proved by assuming $A$ and then deriving $B$ from this assumption conjoined with known results.
answered Sep 3 at 14:43
Mauro ALLEGRANZA
61.1k446105
edited Sep 3 at 14:54
answered Sep 3 at 14:43
Mauro ALLEGRANZA
61.1k446105
answered Sep 3 at 14:43
Mauro ALLEGRANZA
61.1k446105
answered Sep 3 at 14:43
Mauro ALLEGRANZA
61.1k446105
61.1k446105
But say we only formalize the calculus with $lnot, land$. How do we then define and show how some new symbol like $to$ works?
– user525966
Sep 3 at 14:55
1
@user525966 - we introduce $p to q$ as an abbreviation of the formula $lnot p lor q$ (in classical logic) or as an abbreviation for $lnot (p land lnot q)$.
– Mauro ALLEGRANZA
Sep 3 at 15:04
But even after we introduce that symbol with that definition, how do we then know it is the appropriate connective to describe movement in things like mathematical proofs? How do we define how $land$ and $lnot$ work without truth tables? Do we have to define true and false?
– user525966
Sep 3 at 15:39
@user525966 - two steps. Syntactically, connectives are "defined" in thecalculus through the axioms and rules. Then, semantically, we have the truth tables for the connectives. We want that the two approaches match: this is the role of soundness and completeness properties: we want that the axioms and theorems of the calculus are sound (i.e. TRUE according to the semantical interpretation) and complete (i.e. that all TRUE formuklas will be derivable).
– Mauro ALLEGRANZA
Sep 4 at 6:19
Are truth tables the only way to give semantic quality? I thought they were more of a convenience rather than a necessity. The semantics can't be extracted from the way the axioms/inference rules are set up? Are truth tables metalogical?
– user525966
Sep 4 at 12:07
add a comment |Â
But say we only formalize the calculus with $lnot, land$. How do we then define and show how some new symbol like $to$ works?
– user525966
Sep 3 at 14:55
1
@user525966 - we introduce $p to q$ as an abbreviation of the formula $lnot p lor q$ (in classical logic) or as an abbreviation for $lnot (p land lnot q)$.
– Mauro ALLEGRANZA
Sep 3 at 15:04
But even after we introduce that symbol with that definition, how do we then know it is the appropriate connective to describe movement in things like mathematical proofs? How do we define how $land$ and $lnot$ work without truth tables? Do we have to define true and false?
– user525966
Sep 3 at 15:39
@user525966 - two steps. Syntactically, connectives are "defined" in thecalculus through the axioms and rules. Then, semantically, we have the truth tables for the connectives. We want that the two approaches match: this is the role of soundness and completeness properties: we want that the axioms and theorems of the calculus are sound (i.e. TRUE according to the semantical interpretation) and complete (i.e. that all TRUE formuklas will be derivable).
– Mauro ALLEGRANZA
Sep 4 at 6:19
Are truth tables the only way to give semantic quality? I thought they were more of a convenience rather than a necessity. The semantics can't be extracted from the way the axioms/inference rules are set up? Are truth tables metalogical?
– user525966
Sep 4 at 12:07
But say we only formalize the calculus with $lnot, land$. How do we then define and show how some new symbol like $to$ works?
– user525966
Sep 3 at 14:55
But say we only formalize the calculus with $lnot, land$. How do we then define and show how some new symbol like $to$ works?
– user525966
Sep 3 at 14:55
1
1
@user525966 - we introduce $p to q$ as an abbreviation of the formula $lnot p lor q$ (in classical logic) or as an abbreviation for $lnot (p land lnot q)$.
– Mauro ALLEGRANZA
Sep 3 at 15:04
@user525966 - we introduce $p to q$ as an abbreviation of the formula $lnot p lor q$ (in classical logic) or as an abbreviation for $lnot (p land lnot q)$.
– Mauro ALLEGRANZA
Sep 3 at 15:04
But even after we introduce that symbol with that definition, how do we then know it is the appropriate connective to describe movement in things like mathematical proofs? How do we define how $land$ and $lnot$ work without truth tables? Do we have to define true and false?
– user525966
Sep 3 at 15:39
But even after we introduce that symbol with that definition, how do we then know it is the appropriate connective to describe movement in things like mathematical proofs? How do we define how $land$ and $lnot$ work without truth tables? Do we have to define true and false?
– user525966
Sep 3 at 15:39
@user525966 - two steps. Syntactically, connectives are "defined" in thecalculus through the axioms and rules. Then, semantically, we have the truth tables for the connectives. We want that the two approaches match: this is the role of soundness and completeness properties: we want that the axioms and theorems of the calculus are sound (i.e. TRUE according to the semantical interpretation) and complete (i.e. that all TRUE formuklas will be derivable).
– Mauro ALLEGRANZA
Sep 4 at 6:19
@user525966 - two steps. Syntactically, connectives are "defined" in thecalculus through the axioms and rules. Then, semantically, we have the truth tables for the connectives. We want that the two approaches match: this is the role of soundness and completeness properties: we want that the axioms and theorems of the calculus are sound (i.e. TRUE according to the semantical interpretation) and complete (i.e. that all TRUE formuklas will be derivable).
– Mauro ALLEGRANZA
Sep 4 at 6:19
Are truth tables the only way to give semantic quality? I thought they were more of a convenience rather than a necessity. The semantics can't be extracted from the way the axioms/inference rules are set up? Are truth tables metalogical?
– user525966
Sep 4 at 12:07
Are truth tables the only way to give semantic quality? I thought they were more of a convenience rather than a necessity. The semantics can't be extracted from the way the axioms/inference rules are set up? Are truth tables metalogical?
– user525966
Sep 4 at 12:07
add a comment |Â
up vote
0
down vote
In our world, it is true that if it rains, things will get wet. We can express this truth as:
$R rightarrow W$
But it is certainly not true that:
$R vdash W$
That is, given $R$, we can't logically infer $W$. Why? Because we can imagine worlds where nothing gets wet, even if it rains.
answered Sep 3 at 17:24
Bram28
55.5k33982
So $A vdash B$ means $B$ is provable from $A$ regardless of the system we use, regardless of the "world" we're in?
– user525966
Sep 3 at 17:26
Saying we can express this truth as $Ato B$ is really totally missing the point.
– David C. Ullrich
Sep 3 at 17:40
@user525966 What $Avdash B$ means depends on what proof system we're talking about. A proof system has axioms and inference rules - given a proof system, saying $Avdash B$ means there is a finite sequence of wffs $A_1,dots, A_n$ such that $A_n=B$ and each $A_j$ is either $A$, an axiom, or a consequence of previous $A_i$ by one of the rules. That's all it means.
– David C. Ullrich
Sep 3 at 17:46
3
Why I say it's missing the point: What you're actually explaining here is more the difference between $Ato B$ and $models(Ato B)$. Of course it's a theorem that (for standard proof systems) $models(Ato B)$ if and only if $Avdash B$, but the two don't mean the same thing! If they meant the same thing the Soundness and Completeness theorems would have no content.
– David C. Ullrich
Sep 3 at 17:59
@DavidC.Ullrich The $vdash$ symbol then I imagine is mostly used in those inference rules in set $Z$ (I'm reading en.wikipedia.org/wiki/… when I reference this), giving you the rules that dictate how to jump from one wff (or collection thereof) to another wff. And then axioms are basically inference rules that don't have any premises, i.e. the conclusions come out of nothing by default?
– user525966
Sep 3 at 18:08
 |Â
show 5 more comments
up vote
0
down vote
In our world, it is true that if it rains, things will get wet. We can express this truth as:
$R rightarrow W$
But it is certainly not true that:
$R vdash W$
That is, given $R$, we can't logically infer $W$. Why? Because we can imagine worlds where nothing gets wet, even if it rains.
answered Sep 3 at 17:24
Bram28
55.5k33982
So $A vdash B$ means $B$ is provable from $A$ regardless of the system we use, regardless of the "world" we're in?
– user525966
Sep 3 at 17:26
Saying we can express this truth as $Ato B$ is really totally missing the point.
– David C. Ullrich
Sep 3 at 17:40
@user525966 What $Avdash B$ means depends on what proof system we're talking about. A proof system has axioms and inference rules - given a proof system, saying $Avdash B$ means there is a finite sequence of wffs $A_1,dots, A_n$ such that $A_n=B$ and each $A_j$ is either $A$, an axiom, or a consequence of previous $A_i$ by one of the rules. That's all it means.
– David C. Ullrich
Sep 3 at 17:46
3
Why I say it's missing the point: What you're actually explaining here is more the difference between $Ato B$ and $models(Ato B)$. Of course it's a theorem that (for standard proof systems) $models(Ato B)$ if and only if $Avdash B$, but the two don't mean the same thing! If they meant the same thing the Soundness and Completeness theorems would have no content.
– David C. Ullrich
Sep 3 at 17:59
@DavidC.Ullrich The $vdash$ symbol then I imagine is mostly used in those inference rules in set $Z$ (I'm reading en.wikipedia.org/wiki/… when I reference this), giving you the rules that dictate how to jump from one wff (or collection thereof) to another wff. And then axioms are basically inference rules that don't have any premises, i.e. the conclusions come out of nothing by default?
– user525966
Sep 3 at 18:08
 |Â
show 5 more comments
up vote
0
down vote
up vote
0
down vote
In our world, it is true that if it rains, things will get wet. We can express this truth as:
$R rightarrow W$
But it is certainly not true that:
$R vdash W$
That is, given $R$, we can't logically infer $W$. Why? Because we can imagine worlds where nothing gets wet, even if it rains.
answered Sep 3 at 17:24
Bram28
55.5k33982
In our world, it is true that if it rains, things will get wet. We can express this truth as:
$R rightarrow W$
But it is certainly not true that:
$R vdash W$
That is, given $R$, we can't logically infer $W$. Why? Because we can imagine worlds where nothing gets wet, even if it rains.
answered Sep 3 at 17:24
Bram28
55.5k33982
answered Sep 3 at 17:24
Bram28
55.5k33982
answered Sep 3 at 17:24
Bram28
55.5k33982
answered Sep 3 at 17:24
Bram28
55.5k33982
55.5k33982
So $A vdash B$ means $B$ is provable from $A$ regardless of the system we use, regardless of the "world" we're in?
– user525966
Sep 3 at 17:26
Saying we can express this truth as $Ato B$ is really totally missing the point.
– David C. Ullrich
Sep 3 at 17:40
@user525966 What $Avdash B$ means depends on what proof system we're talking about. A proof system has axioms and inference rules - given a proof system, saying $Avdash B$ means there is a finite sequence of wffs $A_1,dots, A_n$ such that $A_n=B$ and each $A_j$ is either $A$, an axiom, or a consequence of previous $A_i$ by one of the rules. That's all it means.
– David C. Ullrich
Sep 3 at 17:46
3
Why I say it's missing the point: What you're actually explaining here is more the difference between $Ato B$ and $models(Ato B)$. Of course it's a theorem that (for standard proof systems) $models(Ato B)$ if and only if $Avdash B$, but the two don't mean the same thing! If they meant the same thing the Soundness and Completeness theorems would have no content.
– David C. Ullrich
Sep 3 at 17:59
@DavidC.Ullrich The $vdash$ symbol then I imagine is mostly used in those inference rules in set $Z$ (I'm reading en.wikipedia.org/wiki/… when I reference this), giving you the rules that dictate how to jump from one wff (or collection thereof) to another wff. And then axioms are basically inference rules that don't have any premises, i.e. the conclusions come out of nothing by default?
– user525966
Sep 3 at 18:08
 |Â
show 5 more comments
So $A vdash B$ means $B$ is provable from $A$ regardless of the system we use, regardless of the "world" we're in?
– user525966
Sep 3 at 17:26
Saying we can express this truth as $Ato B$ is really totally missing the point.
– David C. Ullrich
Sep 3 at 17:40
@user525966 What $Avdash B$ means depends on what proof system we're talking about. A proof system has axioms and inference rules - given a proof system, saying $Avdash B$ means there is a finite sequence of wffs $A_1,dots, A_n$ such that $A_n=B$ and each $A_j$ is either $A$, an axiom, or a consequence of previous $A_i$ by one of the rules. That's all it means.
– David C. Ullrich
Sep 3 at 17:46
3
Why I say it's missing the point: What you're actually explaining here is more the difference between $Ato B$ and $models(Ato B)$. Of course it's a theorem that (for standard proof systems) $models(Ato B)$ if and only if $Avdash B$, but the two don't mean the same thing! If they meant the same thing the Soundness and Completeness theorems would have no content.
– David C. Ullrich
Sep 3 at 17:59
@DavidC.Ullrich The $vdash$ symbol then I imagine is mostly used in those inference rules in set $Z$ (I'm reading en.wikipedia.org/wiki/… when I reference this), giving you the rules that dictate how to jump from one wff (or collection thereof) to another wff. And then axioms are basically inference rules that don't have any premises, i.e. the conclusions come out of nothing by default?
– user525966
Sep 3 at 18:08
So $A vdash B$ means $B$ is provable from $A$ regardless of the system we use, regardless of the "world" we're in?
– user525966
Sep 3 at 17:26
So $A vdash B$ means $B$ is provable from $A$ regardless of the system we use, regardless of the "world" we're in?
– user525966
Sep 3 at 17:26
Saying we can express this truth as $Ato B$ is really totally missing the point.
– David C. Ullrich
Sep 3 at 17:40
Saying we can express this truth as $Ato B$ is really totally missing the point.
– David C. Ullrich
Sep 3 at 17:40
@user525966 What $Avdash B$ means depends on what proof system we're talking about. A proof system has axioms and inference rules - given a proof system, saying $Avdash B$ means there is a finite sequence of wffs $A_1,dots, A_n$ such that $A_n=B$ and each $A_j$ is either $A$, an axiom, or a consequence of previous $A_i$ by one of the rules. That's all it means.
– David C. Ullrich
Sep 3 at 17:46
@user525966 What $Avdash B$ means depends on what proof system we're talking about. A proof system has axioms and inference rules - given a proof system, saying $Avdash B$ means there is a finite sequence of wffs $A_1,dots, A_n$ such that $A_n=B$ and each $A_j$ is either $A$, an axiom, or a consequence of previous $A_i$ by one of the rules. That's all it means.
– David C. Ullrich
Sep 3 at 17:46
3
3
Why I say it's missing the point: What you're actually explaining here is more the difference between $Ato B$ and $models(Ato B)$. Of course it's a theorem that (for standard proof systems) $models(Ato B)$ if and only if $Avdash B$, but the two don't mean the same thing! If they meant the same thing the Soundness and Completeness theorems would have no content.
– David C. Ullrich
Sep 3 at 17:59
Why I say it's missing the point: What you're actually explaining here is more the difference between $Ato B$ and $models(Ato B)$. Of course it's a theorem that (for standard proof systems) $models(Ato B)$ if and only if $Avdash B$, but the two don't mean the same thing! If they meant the same thing the Soundness and Completeness theorems would have no content.
– David C. Ullrich
Sep 3 at 17:59
@DavidC.Ullrich The $vdash$ symbol then I imagine is mostly used in those inference rules in set $Z$ (I'm reading en.wikipedia.org/wiki/… when I reference this), giving you the rules that dictate how to jump from one wff (or collection thereof) to another wff. And then axioms are basically inference rules that don't have any premises, i.e. the conclusions come out of nothing by default?
– user525966
Sep 3 at 18:08
@DavidC.Ullrich The $vdash$ symbol then I imagine is mostly used in those inference rules in set $Z$ (I'm reading en.wikipedia.org/wiki/… when I reference this), giving you the rules that dictate how to jump from one wff (or collection thereof) to another wff. And then axioms are basically inference rules that don't have any premises, i.e. the conclusions come out of nothing by default?
– user525966
Sep 3 at 18:08
 |Â
show 5 more comments
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
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2903877%2fto-vs-vdash-in-logic%23new-answer', 'question_page');
);
Post as a guest
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
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
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
First basic difference: we may have a logical language without the connective $to$ (for classical logic $land$ and $lnot$ are enough) but the relationS of $vdash$ (derivability in the calculus) and $vDash$ (logical consequence) will not change.
– Mauro ALLEGRANZA
Sep 3 at 13:55
But then using your connectives $land, lnot$ what stops us from defining $p lor q = lnot(lnot p land lnot q)$, and $p to q = lnot p lor q$ and introducing the symbols all the same?
– user525966
Sep 3 at 13:57
I don't think this is a duplicate -- I've seen that answer already and all it says is basically "this one's metalogic, this one's within logic" which does not address my confusion
– user525966
Sep 3 at 13:59
$lnot p lor q$ means (in the "standard" classical (i.e. truth-functional) reading of the connectives) : "either $p$ is false or $q$ is true".
– Mauro ALLEGRANZA
Sep 3 at 14:00
2
See also the post Implies vs Entails vs Provable
– Mauro ALLEGRANZA
Sep 3 at 14:02