How to establish the modus ponens inference rule in the LK sequent calculus for first-order logic?

Question

How can the modus ponens inference rule $$ \frac{\Gamma \vdash \varphi\hspace{1cm}\Delta\vdash \varphi\rightarrow\psi}{\Gamma,\Delta \vdash \psi} $$ be established in the LK sequent calculus for first-order logic without resorting to the fact that this calculus is semantically complete?

Answer 1

You can show that modus ponens is derivable in the sequent calculus LK.

In general, an inference rule

$$\dfrac{\Gamma_1 \vdash \Delta_1 \qquad \cdots \qquad \Gamma_n \vdash \Delta_n}{\Gamma \vdash \Delta}(*)$$

is derivable in LK if there is a LK derivation of the sequent $\Gamma \vdash \Delta$ starting from the premises $\Gamma_1 \vdash \Delta_1$, $\,\dots\,$, $\Gamma_n \vdash \Delta_n$. Intuitively this means that the rule $(*)$ can be simulated by the inference rules of LK.

The following shows that modus ponens is derivable in LK.

$$\frac{\dfrac{\Gamma \vdash \varphi \qquad \dfrac{}{\psi \vdash \psi}\text{ax}}{\Gamma, \varphi \to \psi \vdash \psi}\to_L \qquad \Delta \vdash \varphi \to \psi}{\Gamma, \Delta \vdash \psi}\text{cut}$$

The idea is that modus ponens is an elimination rule for the connective $\to$, and LK can simulate it via the rules $\to_L$ and cut.

Answer 2

For future reference, I will generalize the result a little, and show that $$ \dfrac{\Delta \vdash \Sigma, \varphi\rightarrow\psi\qquad\Gamma\vdash\Xi,\varphi}{\Delta,\Gamma\vdash\Sigma,\Xi,\psi} $$ using a proof that is essentially the one given by Taroccoesbrocco, but a little more detailed:

$$ \dfrac{\Delta \vdash \Sigma,\varphi \to \psi\qquad\dfrac{\dfrac{\dfrac{}{\psi \vdash \psi}{\text{ax}}}{\dfrac{\Gamma,\psi\vdash\psi}{\dfrac{\psi, \Gamma \vdash \psi}{\dfrac{\psi, \Gamma \vdash \psi,\Xi}{\psi, \Gamma \vdash \Xi,\psi}{\text{x R}}}{\text{wk R}}}{\text{x L}}}{\text{wk L}}\qquad\dfrac{\Gamma \vdash \Xi,\varphi}{\dfrac{\Gamma \vdash \Xi,\varphi, \psi}{\Gamma \vdash \Xi, \psi, \varphi}{\text{x R}}}{\text{wk R}}}{\varphi \to \psi,\Gamma \vdash \Xi,\psi}{\to L}}{\Delta, \Gamma \vdash \Sigma, \Xi,\psi}{\text{cut}} $$