9
$\begingroup$

Does anyone know the difference between proving that

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

and proving that

|- phi -> ( psi -> phi)  ?
$\endgroup$

6 Answers 6

13
$\begingroup$

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

$\endgroup$
1
7
$\begingroup$

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.

$\endgroup$
6
  • $\begingroup$ @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? $\endgroup$
    – Surikator
    Oct 31, 2010 at 13:53
  • 4
    $\begingroup$ 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. $\endgroup$ Oct 31, 2010 at 14:00
  • $\begingroup$ @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. $\endgroup$
    – Surikator
    Oct 31, 2010 at 14:13
  • $\begingroup$ @Joel: In a Hilbert-style proof-calculus, these are identical, are they not? $\endgroup$ Oct 31, 2010 at 16:50
  • 3
    $\begingroup$ @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. $\endgroup$ Oct 31, 2010 at 17:56
5
$\begingroup$

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

$\endgroup$
3
  • 1
    $\begingroup$ 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. $\endgroup$ Oct 31, 2010 at 19:53
  • 1
    $\begingroup$ 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. $\endgroup$
    – Adam
    Oct 31, 2010 at 21:18
  • 2
    $\begingroup$ 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. $\endgroup$ Oct 31, 2010 at 21:29
3
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ 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 $\endgroup$ Dec 30, 2014 at 9:03
  • $\begingroup$ For more details about "This distinction between a proposition and a judgment is very important and essential for Martin-Lof's type theory and philosophy" there is this conference by Martin-Löf discussing the history of "judgment" vs "proposition": Per Martin Löf: How did 'judgement' come to be a term of logic ? youtube.com/watch?v=FGUzgcLXNuk $\endgroup$ Jan 26, 2021 at 12:03
  • $\begingroup$ In the conference cited above, about the word "judgement", Martin-Löf says: "In Type Theory, I had a need for a term, a good term, that contrasts well with proposition, namely for the things that we demonstrate, and that we reason from and to in a demonstration" $\endgroup$ Jan 26, 2021 at 13:51
2
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ 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.) $\endgroup$ Nov 1, 2010 at 17:55
  • 1
    $\begingroup$ 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.) $\endgroup$ Nov 1, 2010 at 18:31
  • 2
    $\begingroup$ Note that the equivalence or non-equivalence of these two statements is not the same as the original question. $\endgroup$ Nov 1, 2010 at 19:50
0
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ @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? $\endgroup$
    – Surikator
    Dec 8, 2010 at 22:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.