In this context, $\phi$ and $\psi$ are formulas and $\Gamma$ is a set of formulas.

I'm not quite sure what it means. Does it mean $\Gamma \vdash (\phi \Rightarrow \psi)$ or does it mean $(\Gamma \vdash \phi )\Rightarrow \psi$ ?

The following is the exact context of my question. It is from the Handbook of Proof Theory by Samuel R. Buss on page 6 (page 16 if including the preface, table of contents etc.)

Excerpt from the Handbook of Proof Theory

Also, if you could explain section (b) in more detail to me, that would be much appreciated as well. I don't think I really grasp it fully.


It means $\Gamma\vdash (\phi \Rightarrow \psi)$. The alternative reading, $$(\Gamma\vdash \phi) \Rightarrow \psi \tag{*}$$ is a conceptual mess: $\Gamma\vdash \phi$ is a statement of the metatheory, $\psi$ a formula of the theory, and (*) seems to be a formula of the theory — or wants to be one, or something — but it isn't.

Re the reverse implication part of (b): if $\Gamma\vdash (\phi \Rightarrow \psi)$, then $\Gamma,\phi\vdash (\phi \Rightarrow \psi)$ too, so by modus ponens, $\Gamma,\phi\vdash \psi$.

Re the forward implication: This is by induction on lengths of proofs $C_1,C_2,\dotsc,C_{k-1},\psi$ of $\psi$ from $\Gamma,\phi$.

  • $\begingroup$ @BrianO, could you explain that last part again? $\endgroup$ – Paul Nov 10 '15 at 20:14
  • $\begingroup$ And @AndréNicolas, I don't understand how $(\Gamma \vdash \phi )\Rightarrow \psi$ has no meaning. To me it means, "If phi is provable by Gamma, then psi is true". Isn't this correct? $\endgroup$ – Paul Nov 10 '15 at 20:16
  • $\begingroup$ Yes, I misused precedence. To be clear, it is $\Gamma\vdash(\phi\implies \psi)$. $\endgroup$ – André Nicolas Nov 10 '15 at 20:19
  • $\begingroup$ OK, not it doesn't have a meaning but you have to clearly distinguish between if-then in the metatheory and the implication symbol $\Rightarrow$ of the formal language. And you should definitely not use the same symbol for both!, at least not until you've become clear about the distinction. $\endgroup$ – BrianO Nov 10 '15 at 20:22
  • 1
    $\begingroup$ Yes that's right. So $\vdash$ also has lower precedence than comma :) $\endgroup$ – BrianO Nov 11 '15 at 20:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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