How sequent calculus are connected with the usual notion of satisfiability or validitiy of formula?

Question

I know the notions "satisfiablity", "validity" and "consequence" as applied to the logic, e.g. First Order logic https://en.wikipedia.org/wiki/First-order_logic#Validity,_satisfiability,_and_logical_consequence . But I am struggling to connect those notions with the use of sequent calculus (FOL also admit ones). The validity of FO formula can be established by herbrandization or skolemization (conversion to propositional formula) and the following solution of the satisfiability problem. But what is the role of sequent calculus - do they provide some kind of shortcut for this process?

Answer 1

Sequent calculus has some nice properties very useful in the context of proof theory.

The semantics for sequents is derived from "usual" semantics. For the classical version :

we say that a sequent $\Gamma \Rightarrow \Delta$ is refutable if there is a valuation $v$ such that

$\min(v(C)) > \min(v(D))$ for formulas $C \in \Gamma$ and for formulas $D \in \Delta$,

and we say that a sequent $\Gamma \Rightarrow \Delta$ is valid if it is not refutable.

A formula $A$ is provable in e.g. $\mathsf {LK}$ (classical) sequent calculus iff the sequent $\Rightarrow A$ is derivable in the calculus.

We have the completeness of the calculus $\mathsf {LK}$ :

A formula is provable in $\mathsf {LK}$ if and only if it is valid.

Having said that, I do not think that sequent calculus can add something specific in order to address the Satisfiability problem.

But it is worth noting that there is an historical link from Sequent calculus to Tableau and Resolution proof-procedures; see R.Smullyan, First-Order Logic (1961).