Glossary

4.2 Sequent calculus: rules and proof construction

3 min read•august 7, 2024

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 , 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

Top images from around the web for Sequent Structure

  • tikz pgf - Sequent Calculus - TeX - LaTeX Stack Exchange View original

    Is this image relevant?

  • Logic & circuits View original

    Is this image relevant?

  • tikz pgf - Sequent Calculus - TeX - LaTeX Stack Exchange View original

    Is this image relevant?

1 of 3

Top images from around the web for Sequent Structure

  • tikz pgf - Sequent Calculus - TeX - LaTeX Stack Exchange View original

    Is this image relevant?

  • Logic & circuits View original

    Is this image relevant?

  • tikz pgf - Sequent Calculus - TeX - LaTeX Stack Exchange View original

    Is this image relevant?

1 of 3
  • Sequent consists of two parts separated by a (⊢)
  • Left side of the turnstile is called the contains a list of formulas separated by commas
  • Right side of the turnstile is called the 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 on the left side of the turnstile (antecedent)
    • Examples: A,B,Γ⊢ΔA∧B,Γ⊢Δ\frac{A, B, \Gamma \vdash \Delta}{A \land B, \Gamma \vdash \Delta} (∧L\land L), Γ⊢Δ,AΓ⊢Δ,BΓ⊢Δ,A∧B\frac{\Gamma \vdash \Delta, A \quad \Gamma \vdash \Delta, B}{\Gamma \vdash \Delta, A \land B} (∧R\land R)
  • Right rules introduce logical connectives on the right side of the turnstile (succedent)
    • Examples: Γ,A⊢ΔΓ⊢Δ,A∨B\frac{\Gamma, A \vdash \Delta}{\Gamma \vdash \Delta, A \lor B} (∨R1\lor R1), Γ,B⊢ΔΓ⊢Δ,A∨B\frac{\Gamma, B \vdash \Delta}{\Gamma \vdash \Delta, A \lor B} (∨R2\lor R2)

Cut Rule

  • allows the use of an intermediate formula in the proof
    • Example: Γ⊢Δ,AA,Π⊢ΛΓ,Π⊢Δ,Λ\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: Γ⊢ΔΓ,A⊢Δ\frac{\Gamma \vdash \Delta}{\Gamma, A \vdash \Delta} (Weakening Left), Γ⊢ΔΓ⊢Δ,A\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: Γ,A,A⊢ΔΓ,A⊢Δ\frac{\Gamma, A, A \vdash \Delta}{\Gamma, A \vdash \Delta} (Contraction Left), Γ⊢Δ,A,AΓ⊢Δ,A\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: Γ,B,A,Π⊢ΔΓ,A,B,Π⊢Δ\frac{\Gamma, B, A, \Pi \vdash \Delta}{\Gamma, A, B, \Pi \vdash \Delta} (Exchange Left), Γ⊢Δ,B,A,ΛΓ⊢Δ,A,B,Λ\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

  • 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
  • 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

Key Terms to Review (24)

Antecedent: An antecedent is a statement or proposition that precedes another in a logical argument or conditional statement. In the context of sequent calculus, the antecedent often refers to the premises or hypotheses from which conclusions can be drawn, forming the basis for proof construction and rule application.
Contraction Rule: The contraction rule is a principle in sequent calculus that allows for the simplification of expressions by eliminating duplicate formulas. This rule asserts that if a formula appears multiple times in the antecedent or succedent of a sequent, it can be reduced to a single occurrence without changing the logical meaning of the expression. This concept is essential for maintaining conciseness in proofs and contributes to the structure and efficiency of proof construction.
Cut Elimination: Cut elimination is a fundamental process in proof theory that aims to simplify proofs by removing 'cut' rules, which allow for the introduction of intermediate assertions not originally present in the premises. This concept is crucial for understanding the efficiency and structure of proofs, as it transforms proofs into a more direct form, aligning them closer to intuitionistic principles and providing a clearer representation of derivations.
Cut Rule: The cut rule is a principle in proof theory that allows for the introduction of intermediate formulas in the derivation process, enabling more complex proofs by breaking them down into simpler components. This rule highlights the difference between natural deduction and sequent calculus, as it can be seen as a mechanism for managing how assumptions are applied and discharged within a proof. Understanding the cut rule is essential for grasping the structure of proofs in both propositional and first-order logic.
Exchange Rule: The exchange rule is a principle in sequent calculus that allows for the reordering of the propositions in a sequent. This rule asserts that the order of the formulas does not affect the validity of the inference, making it possible to rearrange premises and conclusions freely within a sequent. This property is crucial for simplifying proofs and making logical reasoning more flexible, as it helps to clarify how different propositions interact within a proof structure.
Formal proof: A formal proof is a rigorous sequence of statements and logical deductions that demonstrate the truth of a mathematical or logical assertion using a specific set of rules and axioms. It serves as the foundation for establishing the validity of arguments within a formal system, emphasizing clarity, precision, and deductive reasoning.
Gentzen's Consistency Theorem: Gentzen's Consistency Theorem states that if a formal system is consistent, then it has a proof of its consistency within a stronger system. This theorem highlights the relationship between syntactic proof systems, such as sequent calculus, and semantic notions of consistency. It emphasizes the importance of rules and proof construction in ensuring that a formal system does not derive contradictions.
Gerhard Gentzen: Gerhard Gentzen was a German mathematician and logician known for his groundbreaking contributions to proof theory, particularly in developing natural deduction and sequent calculus. His work laid the foundation for many modern concepts in logic, impacting various aspects of mathematical logic, including soundness, completeness, and proof systems.
Gödel's Completeness Theorem: Gödel's Completeness Theorem states that in first-order logic, every logically valid formula can be proven using a formal proof system. This theorem establishes a connection between semantic truth (truth in every model) and syntactic provability (provable from axioms), showing that if a statement is true in every model, then there is a formal proof of that statement within the system. It plays a significant role in understanding the foundational aspects of mathematical logic and formal systems.
Haskell Curry: Haskell Curry was a mathematician and logician known for his contributions to combinatory logic and proof theory. He developed the concept of 'currying,' which is the process of transforming a function that takes multiple arguments into a sequence of functions, each taking a single argument. This transformation plays a significant role in simplifying function application and has implications in areas such as lambda calculus, sequent calculus, and higher-order logics.
Introduction Rules: Introduction rules are specific guidelines in proof systems that dictate how to introduce logical connectives or quantifiers in a formal proof. These rules are crucial because they define how certain propositions can be derived based on the logical structure of the proof, whether in natural deduction or sequent calculus. They establish the conditions under which new formulas can be added to the proof, serving as a foundation for constructing valid arguments.
Intuitionistic sequent: An intuitionistic sequent is a formal structure used in intuitionistic logic, which expresses the relationship between premises and conclusions in a way that emphasizes constructive proofs. It typically has the form $$ rac{ ext{Antecedents}}{ ext{Consequents}}$$, indicating that if all the antecedents are provable, then at least one of the consequents can be constructed or proved. This approach differs from classical logic by rejecting the law of excluded middle, leading to a different interpretation of implication and proof.
Linear sequent: A linear sequent is a formal expression in proof theory that represents a relationship between premises and a conclusion, structured in a way that each premise appears exactly once and is presented in a linear format. This format emphasizes the sequential nature of reasoning, where each step leads directly to the next, making it easier to follow the logical progression from premises to conclusion without any repetition of premises.
Logical Connectives: Logical connectives are symbols or words used to connect propositions in logic, allowing the formation of more complex statements and expressions. They play a crucial role in determining the truth values of compound statements, influencing how we analyze and construct arguments. By combining simpler propositions using logical connectives, we can express relationships such as conjunction, disjunction, negation, implication, and equivalence, which are essential in both formal proofs and reasoning.
Modal logic: Modal logic is a type of formal logic that extends classical logic to include operators expressing modality, such as necessity and possibility. This allows for reasoning about statements that are not strictly true or false, enabling discussions about what could be, must be, or might have been. Modal logic connects to various areas, enhancing our understanding of semantics, proof structures, and computational applications.
Natural Deduction: Natural deduction is a proof system used in logic that allows one to derive conclusions from premises using a set of inference rules in a structured and intuitive way. It emphasizes the natural reasoning process, enabling proofs to be constructed through the application of these rules without the need for additional axioms or complex structures, making it particularly useful in various fields of mathematics and philosophy.
Proof normalization: Proof normalization is the process of transforming a proof into a simpler or more canonical form without changing its meaning or validity. This concept is crucial in understanding how proofs can be made more efficient and easier to analyze, particularly in formal systems where clarity and brevity are valued. It connects deeply with the goals of proof theory, the rules of sequent calculus, and the functioning of automated theorem proving and proof assistants.
Proof Tree: A proof tree is a graphical representation of the structure of a formal proof, illustrating how the conclusion follows from a set of premises through various inference rules. This visual format helps to clarify the relationships between different propositions and the rules applied at each step, making it easier to analyze and understand the flow of reasoning within logical arguments.
Provability: Provability refers to the property of a statement being demonstrable within a formal system based on its axioms and inference rules. It connects deeply with various foundational aspects of mathematical logic, emphasizing the importance of formal proofs in establishing the truth of mathematical propositions.
Sequent: A sequent is a formal representation used in proof theory, particularly in sequent calculus, to express logical entailment. It consists of a list of formulas on the left side, called the antecedent, and a single formula on the right side, known as the succedent, indicating that the formulas on the left entail the one on the right. Sequents are essential for constructing proofs and understanding the structure of logical arguments.
Structural Rules: Structural rules are foundational components in proof systems that govern the manipulation and arrangement of formulas within proofs. They play a crucial role in defining how propositions can be combined, separated, or preserved during logical reasoning, and are essential in both natural deduction and sequent calculus frameworks, impacting how proofs are constructed and understood.
Succedent: A succedent is a component of a sequent in sequent calculus that appears on the right-hand side, representing the conclusions that one aims to prove from the premises on the left. Understanding the role of succedents is crucial for constructing proofs and applying rules effectively, as they reflect the desired outcomes of logical arguments.
Turnstile Symbol: The turnstile symbol, denoted as `⊢`, is a fundamental notation in formal logic used to represent syntactic entailment or provability. It indicates that a particular statement or formula can be derived from a set of premises using formal proof techniques, signifying the relationship between syntactic expressions and their semantic interpretations in logic. This symbol plays a critical role in sequent calculus, where it helps structure proofs and rules of inference.
Weakening rule: The weakening rule is a principle in proof theory that allows one to derive a conclusion by adding extra assumptions to a given set of premises. This rule emphasizes the flexibility of logical systems, showing that if a conclusion can be reached from certain premises, it can still be valid even if additional, possibly irrelevant, premises are introduced. The weakening rule supports proof construction by illustrating that more assumptions do not invalidate the original argument.
© 2024 Fiveable Inc. All rights reserved.
AP® and SAT® are trademarks registered by the College Board, which is not affiliated with, and does not endorse this website.
Back
Practice QuizGlossary
Practice QuizGlossary
Next guide