# What is the order of precedence to $\Gamma \vdash \phi \Rightarrow \psi$?

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.) 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$.
• 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? – Paul Nov 10 '15 at 20:16
• Yes, I misused precedence. To be clear, it is $\Gamma\vdash(\phi\implies \psi)$. – André Nicolas Nov 10 '15 at 20:19
• 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. – BrianO Nov 10 '15 at 20:22
• Yes that's right. So $\vdash$ also has lower precedence than comma :) – BrianO Nov 11 '15 at 20:05