The cut rule in LK allows deriving Γ,Γ' ⊢ Δ,Δ' by first proving Γ ⊢ Δ,A and then using A as an assumption in A,Γ' ⊢ Δ'. Cut-elimination (the Hauptsatz) proves that this rule can always be eliminated. What is the key consequence?
ACut-free proofs are shorter and therefore more efficient to verify
BCut-free proofs have the subformula property — every formula in the proof is a subformula of the conclusion — giving a syntactic consistency proof and making proof search deterministic
CEliminating cut shows that LK can derive more theorems than it could with cut
DCut-elimination proves that sequent calculus is more expressive than natural deduction
Cut-free proofs have the subformula property: no formula appears in the proof that isn't already present in the conclusion. This has two major consequences: (1) a syntactic consistency proof — ⊢ ∅ (provable contradiction) has no cut-free proof, so the system is consistent; and (2) proof search becomes analytic and terminating, since you only need to work with subformulas of the goal. Cut-free proofs are typically longer, not shorter. And cut-elimination shows the cut rule is redundant, not that it adds new theorems — LK with and without cut prove the same things.
Question 2 Multiple Choice
How does LK's treatment of logical connectives differ from natural deduction's treatment of the same connectives?
ALK has no elimination rules; it uses only introduction rules, unlike natural deduction which has both
BNatural deduction uses sequents while LK uses individual judgment forms
CLK provides both a left rule (for using a connective as an assumption) and a right rule (for proving a connective as a conclusion), making the system two-sided in a way natural deduction is not
DLK can only handle classical logic; natural deduction handles both classical and intuitionistic logic
In natural deduction, rules are either introduction rules (proving a connective) or elimination rules (using a connective). In LK, for each connective there is a right rule (decomposing it on the right of ⊢, i.e., in the conclusion) and a left rule (decomposing it on the left of ⊢, i.e., as an assumption). This two-sided structure makes the symmetry between hypothesis-use and conclusion-proof explicit. Natural deduction does have both introduction and elimination rules, but they are not organized symmetrically around a turnstile — that reorganization is what gives LK its structural clarity.
Question 3 True / False
The cut rule in LK is unsound — it can produce invalid derivations, which is why Gentzen proved it should be eliminated from any valid proof.
TTrue
FFalse
Answer: False
This is the central misconception about cut-elimination. The cut rule is perfectly sound — any derivation using cut derives only valid sequents. Cut-elimination shows that cut is *eliminable* (redundant) — every proof using cut can be transformed into a cut-free proof of the same sequent. The reason to care about cut-free proofs is not soundness but the subformula property they carry, which enables consistency proofs and analytic proof search. Soundness is never in question.
Question 4 True / False
A cut-free proof in LK contains only formulas that are subformulas of the sequent being proved.
TTrue
FFalse
Answer: True
This is the subformula property, and it is the key structural fact about cut-free proofs. It means that to prove Γ ⊢ Δ without cut, you never need to invent a formula from outside — you only decompose the formulas already present. This makes proof search analytic: you work top-down from the goal, breaking formulas into subformulas, and the process terminates because formulas can only get smaller. With cut, you can introduce an arbitrary intermediate formula A, which is what makes cut proofs shorter but proof search harder.
Question 5 Short Answer
What does cut-elimination imply about the consistency of LK, and why is this a syntactic rather than semantic argument?
Think about your answer, then reveal below.
Model answer: Cut-elimination implies consistency because the empty sequent ⊢ ∅ — which would represent a derivable contradiction — cannot have a cut-free proof. No right-side rule produces an empty succedent from valid inputs, and the subformula property ensures no formula can be conjured from nothing. Therefore the system cannot prove a contradiction, and is consistent. This is syntactic because the argument works entirely within the proof system itself — it does not appeal to a model or an interpretation of the formulas. Consistency is derived from the structure of the rules, not from semantic truth.
Semantic consistency proofs show 'no model satisfies a contradiction, and LK is sound, so it cannot derive one.' Syntactic consistency proofs (like Gentzen's) show 'no proof exists' by analyzing the shapes of derivations directly. Syntactic proofs are valued because they don't presuppose a semantic framework — they work even in settings where the semantics is unclear or disputed, which is important for foundational work in proof theory.