Sequent calculus is a powerful tool for constructing formal proofs in logic. It uses sequents, which are statements with antecedents and succedents, to represent logical relationships. This system provides a structured way to build proofs from the bottom up.

The rules of sequent calculus, including introduction and structural rules, guide the construction of proof trees. By applying these rules strategically, we can break down complex formulas and work towards simpler axioms, ultimately proving our desired conclusion.

Sequents and Their Components

Sequent Structure

• Sequent consists of two parts separated by a turnstile symbol (⊢)
• Left side of the turnstile is called the antecedent contains a list of formulas separated by commas
• Right side of the turnstile is called the succedent also contains a list of formulas separated by commas
• Sequent represents a logical statement where the conjunction of the formulas in the antecedent implies the disjunction of the formulas in the succedent

Interpreting Sequents

• Empty antecedent is interpreted as true
• Empty succedent is interpreted as false
• Sequent with an empty antecedent and a non-empty succedent (⊢ A) means the formula A is provable
• Sequent with a non-empty antecedent and an empty succedent (A ⊢) means the formula A is contradictory

Sequent Calculus Rules

Introduction Rules

• Left rules introduce logical connectives on the left side of the turnstile (antecedent)
  • Examples: $\frac{A, B, \Gamma \vdash \Delta}{A \land B, \Gamma \vdash \Delta}$ ($\land L$), $\frac{\Gamma \vdash \Delta, A \quad \Gamma \vdash \Delta, B}{\Gamma \vdash \Delta, A \land B}$ ($\land R$)
• Right rules introduce logical connectives on the right side of the turnstile (succedent)
  • Examples: $\frac{\Gamma, A \vdash \Delta}{\Gamma \vdash \Delta, A \lor B}$ ($\lor R1$), $\frac{\Gamma, B \vdash \Delta}{\Gamma \vdash \Delta, A \lor B}$ ($\lor R2$)

Cut Rule

• Cut rule allows the use of an intermediate formula in the proof
  • Example: $\frac{\Gamma \vdash \Delta, A \quad A, \Pi \vdash \Lambda}{\Gamma, \Pi \vdash \Delta, \Lambda}$ (Cut)
• Eliminates the need for assumptions by proving the intermediate formula and then using it in the proof

Structural Rules

Weakening Rules

• Weakening rules allow the addition of formulas to the antecedent or succedent
  • Example: $\frac{\Gamma \vdash \Delta}{\Gamma, A \vdash \Delta}$ (Weakening Left), $\frac{\Gamma \vdash \Delta}{\Gamma \vdash \Delta, A}$ (Weakening Right)
• Weakening rules are used to add unused assumptions or conclusions to the sequent

Contraction Rules

• Contraction rules allow the removal of duplicate formulas from the antecedent or succedent
  • Example: $\frac{\Gamma, A, A \vdash \Delta}{\Gamma, A \vdash \Delta}$ (Contraction Left), $\frac{\Gamma \vdash \Delta, A, A}{\Gamma \vdash \Delta, A}$ (Contraction Right)
• Contraction rules are used to simplify the sequent by removing redundant formulas

Exchange Rules

• Exchange rules allow the reordering of formulas in the antecedent or succedent
  • Example: $\frac{\Gamma, B, A, \Pi \vdash \Delta}{\Gamma, A, B, \Pi \vdash \Delta}$ (Exchange Left), $\frac{\Gamma \vdash \Delta, B, A, \Lambda}{\Gamma \vdash \Delta, A, B, \Lambda}$ (Exchange Right)
• Exchange rules are used to rearrange the order of formulas in the sequent without affecting the validity of the proof

Proof Construction

Building Proof Trees

• Proof tree in sequent calculus starts with the sequent to be proved at the bottom (root)
• Apply sequent calculus rules to the sequent, working upwards to create new nodes
• Each node in the proof tree is a sequent derived from the sequent below it by applying a rule
• Branches in the proof tree represent case distinctions or the use of multiple rules

Proof Strategies

• Work backwards from the desired conclusion (bottom-up approach)
• Break down complex formulas using introduction rules
• Use structural rules (weakening, contraction, exchange) to manipulate the sequent as needed
• Apply the cut rule to introduce intermediate formulas that can help in proving the sequent
• Aim to reach axioms (sequents with the same formula on both sides) at the top of the proof tree