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?
Best Answer
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