# Difference between turnstile and implication

Hi,

Does anyone know the difference between proving that

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


and proving that

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


Thanks for any help!

All the best, Surikator.

-

@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".

-
Can you confirm that the horizontal line in between the 2 formal statements is just notation for a turnstile. Like what exactly does the horizontal line here en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Typing_rules mean? –  CMCDragonkai Dec 30 '14 at 9:02

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.

-
@Joel Thanks for that. I know how the two cases translate to English. But I wonder if the two cases are that different. Rephrasing my question: is it the case that "if p is provable then q is provable" is equivalent to "it is provable that p -> q"? In other words, if I happen to prove that "p -> q is provable" can I have for granted that "if p is provable then q is provable" and vice-versa? –  Surikator Oct 31 '10 at 13:53
That way of phrasing the question is exactly the Deduction theorem of first order logic. See en.wikipedia.org/wiki/Deduction_theorem. For further questions about it, I would suggest math.stackexchange.com as a more appropriate forum. –  Joel David Hamkins Oct 31 '10 at 14:00
@Joel Thanks for the reference. OK, I thought this was an appropriate forum, but just realised this forum was for research level questions. Sorry. Thanks for the help. –  Surikator Oct 31 '10 at 14:13
@Joel: In a Hilbert-style proof-calculus, these are identical, are they not? –  Harry Gindi Oct 31 '10 at 16:50
@Harry: No, they are not. The deduction theorem shows their equivalence in classical propositional logic, meaning that whenever you can get one, you can also get the other, and there is an algorithm that shows you how to transform a proof of one into a proof of the other. But the lengths of the associated proofs are different. besides this, as Henry points out in his answer, the underlying logic may change the answer; even if the proof-calculus we use is Hilbert-style. –  Andres Caicedo Oct 31 '10 at 17:56

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.)

-
The fact that the deduction theorem does not hold for arbitrary systems, although it does hold for conventional first-order logic, should be better emphasized (that is, at least pointed out) in more elementary logic books. It is very easy to come away with the opinion that the deduction theorem holds in general, when as Henry says that is far from the truth. –  Carl Mummert Oct 31 '10 at 19:53
I enthusiastically second Carl's comment! The "Hilbert Derivability Conditions" on the provability predicate also exhibit this peculiarity (although since Solovay we've known that the derivability conditions can be interpreted as a particular kind of modal logic). Assuming that the deduction theorem held for those systems was a major impediment to me when I was learning about them. –  Adam Oct 31 '10 at 21:18
Although the Deduction theorem fails in modal logic, the particular use of it in the OP's question (with those implications) does not fail for modal logic. His first case follows from the provability of the tautology of the second case and modus ponens, which is valid for virtually all logics commonly studied. –  Joel David Hamkins Oct 31 '10 at 21:29

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.

-
What does the horizontal line between 2 statements mean? I'm referring to the big long one here: en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Typing_rules –  CMCDragonkai Dec 30 '14 at 9:03

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?

-
No, you're not missing something. (I should have included that example in my post; I remembered the fancy and obscure cases, but forgot that very straightforward one.) –  Henry Towsner Nov 1 '10 at 17:55
Another example: let $\phi$ be any independent statement, and $\psi$ tautologically false. Then $\vdash\phi$ implies $\vdash\psi$, but not $\vdash(\phi\rightarrow\psi)$. (I take back my earlier comment about the Deduction theorem.) –  Joel David Hamkins Nov 1 '10 at 18:31
Note that the equivalence or non-equivalence of these two statements is not the same as the original question. –  Joel David Hamkins Nov 1 '10 at 19:50

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).

-
@Amit I don't understand the reason for your answer. No one mentioned the case (1) in the whole of the previous discussion. So, yes, I agree with you regarding the relation between (2) and (3). That's what had already been said before. No? –  Surikator Dec 8 '10 at 22:56