Sequent calculus | EPFL Graph Search

Are you an EPFL student looking for a semester project?

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the natural style of deduction used by mathematicians than to David Hilbert's earlier style of formal logic, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms. In that case, sequents signify conditional theorems in a first-order language rather than conditional tautologies. Sequent calculus is one of several extant styles of proof calculus for expressing line-by-line logical arguments. Hilbert style. Every line is an unconditional tautology (or theorem). Gentzen style. Every line is a conditional tautology (or theorem) with zero or more conditions on the left. Natural deduction. Every (conditional) line has exactly one asserted proposition on the right. Sequent calculus. Every (conditional) line has zero or more asserted propositions on the right. In other words, natural deduction and sequent calculus systems are particular distinct kinds of Gentzen-style systems. Hilbert-style systems typically have a very small number of inference rules, relying more on sets of axioms. Gentzen-style systems typically have very few axioms, if any, relying more on sets of rules. Gentzen-style systems have significant practical and theoretical advantages compared to Hilbert-style systems. For example, both natural deduction and sequent calculus systems facilitate the elimination and introduction of universal and existential quantifiers so that unquantified logical expressions can be manipulated according to the much simpler rules of propositional calculus.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (66)

Related courses (4)

Related lectures (32)

MATH-381: Mathematical logic

Branche des mathématiques en lien avec le fondement des mathématiques et l'informatique théorique. Le cours est centré sur la logique du 1er ordre et l'articulation entre syntaxe et sémantique.

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

CS-452: Foundations of software

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a progr

Sequent Calculus: Basics and Applications CS-550: Formal verification

Covers the basics and applications of Sequent Calculus in Logic and Proof Theory, including Cut Elimination and practical proof analysis.

Proposition: Demonstration by Absurd Reasoning MOOC: Analyse I

Explores the proposition that X² is not equal to 2 using absurd reasoning.

Propositions Calculation

Covers the calculation of propositions in predicate logic with a focus on logical connectives.

Logic

Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or logical truths. It studies how conclusions follow from premises due to the structure of arguments alone, independent of their topic and content. Informal logic is associated with informal fallacies, critical thinking, and argumentation theory. It examines arguments expressed in natural language while formal logic uses formal language.

Sequent calculus

Proof theory

Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.