Sequent Calculus

• $$\Gamma \Longrightarrow \Delta$$ is called a sequent
• The left side $$\Gamma$$ are the assumptions called antecedent
• The right side $$\Delta$$ is the conclusion called succedent
• A proof of the sequent $$\Gamma \Longrightarrow \Delta$$ is a finite tree constructed using inference rules such that the root is labeled with $$\Gamma \Longrightarrow \Delta$$ and axioms as leafs

Dealing with quantifiers

$$\begin{prooftree} \AxiomC{$$\Gamma \Longrightarrow \Delta, \varphi[t/x]$$} \RightLabel{ $$(\exists_R)$$} \UnaryInfC{$$\Gamma \Longrightarrow \Delta, \exists x \, \varphi$$} \end{prooftree}$$

• You prove “$$\exists x \, \varphi$$” by specifying a concrete witness that would fullfil $$\varphi$$
• $$t$$ is a ground term

$$\begin{prooftree} \AxiomC{$$\Gamma, \varphi[t/x] \Longrightarrow \Delta$$} \RightLabel{ $$(\forall_L)$$} \UnaryInfC{$$\Gamma, \forall x \, \varphi \Longrightarrow \Delta$$} \end{prooftree}$$

• If you want to use the hypothesis “$$\forall x \, \varphi$$”, then we can use any witness and continue with $$\varphi[t/x]$$
• $$t$$ is a ground term

$$\begin{prooftree} \AxiomC{$$\Gamma \Longrightarrow \Delta, \varphi[c/t]$$} \RightLabel{ $$(\forall_R)$$} \UnaryInfC{$$\Gamma \Longrightarrow \Delta, \forall x \, \varphi$$} \end{prooftree}$$

• You prove “$$\forall x \, \varphi$$” by instantiating $$x$$ arbitrarily and then prove $$\varphi$$ without any additional assumptions on $$x$$
• $$c$$ is a new constant symbol that is not already used anywhere
• It has to be new because we do not want to make any assumptions on it

$$\begin{prooftree} \AxiomC{$$\Gamma, \varphi[x/c] \Longrightarrow \Delta$$} \RightLabel{ $$(\exists_L)$$} \UnaryInfC{$$\Gamma, \exists x \, \varphi \Longrightarrow \Delta$$} \end{prooftree}$$

• If you want to use “$$\exists x \, \varphi$$”, you can use $$\varphi[c/x]$$ for a fixed but arbitrary $$c$$
• $$c$$ represents the existing but unkown witness for the existensial statement
• Except that the witness has the listed property, no other assumptions may be made