Difference between turnstile and implication

Question

Does anyone know the difference between proving that

|- phi
------------------
|- ( psi -> phi )

and proving that

|- phi -> ( psi -> phi)  ?

Answer 1

@Joel's answer is concise and correct, and I am glad that @Henry mentioned the connection to modal logic. I'd like to add one more perspective: they seem similar because -- when you look at the right category -- turnstile is the external hom and implication is the internal hom.

Hilbert-style deductive systems form a category: let the objects be propositions and let a morphism from $A$ to $B$ be a proof starting from axiom $\vdash A$ and ending with conclusion $\vdash B$. Conjunction can be used to represent proofs with multiple axioms (or conclusions).

Clearly from axiom $\vdash A$ we may prove $\vdash A$, so we have identity morphisms $A\to A$. Moreover we can easily append proofs to each other if the (sole) conclusion of one is the (sole) axiom of the other:

$$ \begin{array}{c} \vdash A \\\\ \vdots \\\\ \vdash B \end{array} \ \ \ \ \ \&\ \ \ \ \ \begin{array}{c} \vdash B \\\\ \vdots \\\\ \vdash C \end{array} \ \ \ \ \ \Rightarrow\ \ \ \ \ \begin{array}{c} \vdash A \\\\ \vdots \\\\ \vdash B \\\\ \vdots \\\\ \vdash C \end{array} $$

So we can compose morphisms $A\to B$ and $B\to C$ to get a morphism $A\to C$. If we treat all proofs as equal (for simplicity) the identity/associativity laws hold trivially, and we have a category.

Moreover, if we have implication as a connective, the category will be cartesian closed with implication as the exponential or "internal hom", because proofs of the following two forms are in one-to-one correspondence:

$$ \begin{array}{c} \vdash A\wedge B\\\\ \vdots\\\\ \vdash C \end{array} \ \ \ \ \ \ \ \ \ \ \ \ \begin{array}{c} \vdash A \\\\ \vdots \\\\ \vdash B\supset C \end{array} $$

It turns out that this category of Hilbert-style proofs is enriched in the category of natural deduction proofs over the same propositions. The latter category has as its objects lists of zero or more sequents $A\vdash B$, and has as morphisms proofs of one list of sequents from another list of sequents. The identity and composition laws of the enrichment are given by the proofs of the initial sequent and cut rule, respectively:

$$ {\over A\vdash A} \ \ \ \ \ \ \ \ \ \ \ \ {A\vdash B\ \ \ \ \ \ B\vdash C\over A\vdash C} $$

The covariant hom-functor $Hom_X$ from the Hilbert-category to the NaturalDeduction-category sends a Hilbert-morphism $A\to B$ to a natural deduction proof

$$ Hom_X\left(\begin{array}{c} \vdash A \\\\ \vdots \\\\ \vdash B \end{array}\right) \ \ \ \ \ =\ \ \ \ \ {X\vdash A\over X\vdash B} $$

... hence the claim that turnstile is the "external hom".

Answer 2

In the second case, you are saying that a certain tautology is provable. In the first case, you are saying that if phi is provable, then a certain other implication is provable. And one way you could know that is by using that the fact that the tautology of the second case is provable and then applying modus ponens.

Answer 3

To add to Joel's answer, in the most common theories (for instance, ordinary first-order logic), these are equivalent (by the deduction theorem), but there are plenty of theories where they aren't.

One classic example is conventional modal logic, where

$\vdash\phi$

............

$\vdash\Box\phi$

is a rule, but $\phi\rightarrow\Box\phi$ is definitely not provable. It we interpret $\Box\phi$ as "$\phi$ is true in all situations", it's clear why: if $\phi$ is a logical tautology, it will always be a logical tautology, and therefore always true. But something true of a particular situation need not be true in all situations.

There are similar situations in certain subsystems of second order arithmetic (note that, despite the name, this is a first-order theory with two types); there are theories where the deduction theorem fails because "from $\phi$ infer $\phi'$" is added as a rule, but the axiom $\phi\rightarrow\phi'$ is not. (And why would we do this? Because we don't want $\phi'$ to contain free variables---probably set variables---which could appear in premises to $\phi$; that is, we don't want to allow the deduction from $\psi\rightarrow\phi$ to $\psi\rightarrow\phi'$ where $\psi$ and $\phi'$ might share free set variables.)

Answer 4

This is not an answer to the question intended by OP, but rather a philosophical meta-answer and might be interesting to some readers.

The use of sign $\vdash$ is completely different from $\rightarrow$. You can not prove "$\varphi \vdash \psi$", since it is not a proposition. It is a speech-act, it is invented by Frege and has been discussed extensively in philosophy of mathematics and philosophy of language. This speech-act is called assertion and is composed of two separate parts "|" and "-". It is an act of judgment. For more details see this SEP article. This distinction between a proposition and a judgment is very important and essential for Martin-Lof's type theory and philosophy.

In fact, from this viewpoint, $\varphi \vdash \psi$ is a common formal misuse because the assumptions cannot be before the speech-act. For this reason Martin-Lof prefers to write the assumptions of the assertion after the proposition in his type theories.

For difference between $\vdash$ and $\rightarrow$ see this article.

Answer 5

Even with all previous answers, I'm still not fully convinced that

$\vdash \phi\ \Rightarrow\ \vdash \psi$

is equivalent to $\vdash (\phi\rightarrow \psi)$ in first-order logic.

The rule of generalization (an axiom of the predicate calculus) tells us that

$ \vdash\phi\ \Rightarrow\ \vdash\forall x.\phi $

but we know from another axiom of the predicate calculus (quantifier introduction) that

$\vdash(\phi\rightarrow\forall x.\phi)$

requires the proviso that $x$ does not occur in $\phi$. So, it would appear they are not equivalent.

Am I missing something?

Answer 6

If you can prove $\phi$, then you can prove $\psi \rightarrow \phi$. Also, you can always prove $\phi \rightarrow (\psi \rightarrow \phi)$. Thus there's no difference between the two situations you mentioned since they're always possible (no matter what $\phi$ and $\psi$ are). Looking at your comments to Joel's answer, what you meant to ask was the relationship between items 2 and 3 in the list below:

1. $\phi \vdash \psi$
2. $\vdash \phi \rightarrow \psi$
3. If $\vdash \phi$ then $\vdash \psi$

Let's restrict ourselves to first-order predicate logic. The Deduction Theorem tells us that (1) implies (2). That (2) implies (1) is an easy consequence of modus ponens. (2) implies (3) easily because of modus ponens as well. But you and Joel have already pointed out (3) doesn't imply (2).