$\to$ vs. $\vdash$ in logic

Question

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?

Answer 1

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 $A\vdash B$ means that one can deduce $B$ from $A$; if you read $\vdash$ as "infers" you're reading $A\vdash 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$: $A\to B$ is just a formula in ur formal system; it does not say anything (it's not an assertion). On the other hand, $A\vdash 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 $A\vdash B$ is equivalent to "$A\to B$ is a tautology". But jumping from there to the conclusion that $A\vdash B$ is equivalent to $A\to B$ is wrong; "$A\to B$ is a tautology" is a statement about $A$ and $B$, while $A\to 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 "$A\vdash B$ is equivalent to the statement that $A\to B$ is a tautology" to "$A\vdash B$ is equivalent to $A\to B$" is making exactly the same error

Answer 2

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.

Answer 3

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.