1

To me it seems there's no difference and you can prove each from the other one.

Having proved $\vdash p\rightarrow q$ we can get $p\vdash q$:

  1. $\;p$ --- premise
  2. $\;p\rightarrow q$ --- theorem intro
  3. $\;q$ --- $\rightarrow$ elim 1,2

and having proved $p\vdash q$ we can get $\vdash p\rightarrow q$:

  1. $\;\bullet\; p$ --- assumption
  2. $\;\bullet\; q$ --- Sequent Intro 1 ($p\vdash q$)
  3. $p\rightarrow q$ --- $\rightarrow$ intro 1,2
Pooria
  • 477
  • 2
    Yes; the first means that in the "calculus" (Hilbert-style, Natural deduction, etc.) we have a derivation ending with the formula $p \to q$, where $\to$ is the "if..., then..." connective. – Mauro ALLEGRANZA Sep 20 '17 at 15:19
  • 2
    The second means that we have a derivation of $q$ from the assumption $p$. – Mauro ALLEGRANZA Sep 20 '17 at 15:20
  • 3
    The two are linked by the Deduction Theorem (or $\to$-introducuion) and the Modus Ponens (or $\to$-elimination): if we have both, the calculus has the "nice" property that $\varphi \vdash \psi$ iff $\vdash \varphi \to \psi$. – Mauro ALLEGRANZA Sep 20 '17 at 15:22
  • 2
    In a "formal" setting: $p \to q$ is a formula (expression) of the calculus, because the connective $\to$ is a symbol of the language, while $\vdash p \to q$ is a statement of the meta-theory, meaning that there is in the calculus a proof of $p \to q$. With this point of view, $\vdash$ is not part of the language but is part of the meta-language. – Mauro ALLEGRANZA Sep 20 '17 at 15:25
  • 1
    A difference between the two is that the first ($p\vdash q$) is expressible in more logics than the second. Indeed most logics have a $\vdash$ relation (for sole authors this is part of the definition of a logic), but many have no $\to$ symbol – Maxime Ramzi Sep 20 '17 at 15:28
  • 1
    p$\rightarrow$q actually abbreviate (p$\rightarrow$q) or (p)$\rightarrow$(q) depending on how a formula gets defined. Also, Mauro seems to have mixed up the first and the second, but otherwise his answer comments I find correct. – Doug Spoonwood Sep 21 '17 at 03:14

1 Answers1

1

From your post it seems you are perfectly aware of the difference: $p \vdash q$ means that there is a derivation that has $p$ as a premise and $q$ as the conclusion. $\vdash p \rightarrow q$ means there is a derivation that has no premises and that has $p \rightarrow q$ as the conclusion.

And yes, give a sound and complete proof system we have $p \vdash q$ if and only if $\vdash p \rightarrow q$, but that does not make them identical. It's similar to $p \land q$ and $q \land p$ being equivalent, but not identical.

Bram28
  • 100,612
  • 6
  • 70
  • 118
  • Well I asked this basically because I can use both of them in my proofs(natural deduction) and I don't know how to decide which one to use! For example is it more cool to show that $P\vdash Q$ is true or show that $\vdash P\rightarrow Q$ is true :D – Pooria Sep 20 '17 at 15:35
  • 1
    @Pooria Use them of prove them? Anyway, I don't think there is much of a 'coolness' difference between the two either way :p – Bram28 Sep 20 '17 at 15:57
  • Both, anyway I've been using assumptions instead of premises all the way and it's worked. – Pooria Sep 20 '17 at 16:07
  • Soundness and completeness stand independent of having " p⊢q if and only if ⊢(p→q)". For example, there exist sound and complete axiomizations of Lukasiewicz three-valued logic, but "" p⊢q if and only if ⊢(p→q)"" is not true for Lukasiewicz three-valued logic. Any proposed set of axioms and rules for classical or intuitionistic axiom which are sound and complete will have " p⊢q if and only if ⊢(p→q)" as a meta-theorem though. So, the above does hold for classical logic... at least once make sure that all abbreviations get transformed into their full forms. – Doug Spoonwood Sep 21 '17 at 03:18
  • 1
    @Pooria The more you use ⊢(P→Q) the more likely you are to use modus ponens instead of more complicated or more dubious rules of inference. If you ever look at a proof of the deduction meta-theorem, you'll also find that it's proof suggests that in an axiomatic context, using P⊢Q would tend to result in long proofs. Frege would probably NEVER use P⊢Q and only use ⊢(P→Q). – Doug Spoonwood Sep 21 '17 at 03:20