Fact-checked by Grok 2 weeks ago

Sequent

In mathematical logic, particularly in proof theory, a sequent is a formal expression that represents a logical argument in the form of an implication between two multisets of formulas. It is typically denoted as \Gamma \vdash \Delta, where \Gamma (the antecedent) is a finite multiset of formulas considered as premises, and \Delta (the succedent) is a finite multiset of formulas considered as conclusions. The notation \Gamma \vdash \Delta means that whenever all formulas in \Gamma are true, at least one formula in \Delta is true.^[1] The concept of the sequent was introduced by German mathematician Gerhard Gentzen in his 1934 work Untersuchungen über das logische Schließen (Investigations into Logical Reasoning), as part of developing sequent calculus, a deductive system that emphasizes the structure of proofs and facilitates the study of logical consistency.^[2] Sequents provide an intuitive framework for understanding deduction, bridging natural language arguments and formal proofs, and have influenced modern applications in automated theorem proving, programming language theory, and linear logic.^[3]

Definition and Formalism

Form and Semantics

A sequent is defined as a conditional assertion of the form \Gamma \vdash \Delta, where \Gamma is the antecedent consisting of a finite sequence of formulas interpreted as their conjunction, and \Delta is the succedent consisting of a finite sequence of formulas interpreted as their disjunction.^[4] This form, introduced by Gerhard Gentzen in his foundational work on proof theory, expresses that the formulas in \Gamma logically imply those in \Delta.^[5] Semantically, a sequent \Gamma \vdash \Delta holds if, in any model where all formulas in \Gamma are true, at least one formula in \Delta is true.^[4] The disjunctive interpretation of the succedent provides key benefits in proof theory, including symmetry between the introduction rules for connectives on the left and right sides of the sequent, which facilitates cut elimination and ensures the completeness of the system relative to classical semantics.^[4] This structure supports the subformula property, where proofs involve only subformulas of the endpoint sequent, enhancing the analytical power of sequent calculi.^[4] Sequents generalize simpler forms of logical judgments: an unconditional judgment is a sequent with an empty antecedent and a single formula in the succedent (\vdash A), asserting the formula's validity as a tautology; a simple conditional has multiple formulas in the antecedent but a single formula in the succedent (\Gamma \vdash A), indicating that A follows from the assumptions in \Gamma; and the full sequent allows multiple formulas on both sides, capturing more complex implications.^[4] Unlike tautologies, which require no assumptions, sequents express provability under a set of assumptions in \Gamma, allowing for hypothetical reasoning in formal proofs.^[4]

Syntax

In sequent calculus, a sequent is formally denoted as \Gamma \vdash \Delta, where \Gamma represents the antecedent (a sequence of formulas to the left of the turnstile \vdash) and \Delta the succedent (a sequence to the right), with commas separating individual formulas within each sequence.^[6]^[1] This notation, introduced by Gerhard Gentzen, uses the turnstile symbol \vdash (or sometimes \Rightarrow) to divide the two sides, emphasizing the conditional relationship that the conjunction of formulas in \Gamma implies the disjunction of those in \Delta.^[7] Unlike sets, which disallow repetitions and disregard order, the antecedent and succedent are treated as sequences (or lists) of formulas, permitting multiple occurrences of the same formula and preserving a nominal order among them.^[6] In classical logic, however, the order is typically irrelevant due to the structural rule of permutation, which allows arbitrary reordering of formulas within \Gamma or \Delta without altering the sequent's validity; for instance, if \Gamma, A, B \vdash \Delta holds, then \Gamma, B, A \vdash \Delta follows equivalently.^[1]^[7] This sequence-based approach accommodates the repeated use of assumptions, mirroring natural deduction systems where hypotheses can be invoked multiple times.^[6] The rule of contraction further refines this syntax by enabling the elimination of duplicate formulas; specifically, from \Gamma, A, A \vdash \Delta, one may derive \Gamma, A \vdash \Delta, effectively merging redundant instances while preserving the sequent's inferential force.^[1] In modern formulations of sequent calculus, sequences are often formalized as multisets—structures that capture multiplicity without regard to order—to streamline proofs and align with the permutation and contraction rules, which render strict sequencing unnecessary for most purposes.^[6]^[7] These syntactic conventions, including the use of sequences and structural rules like permutation and contraction, underpin the flexibility of sequent calculus derivations while ensuring that manipulations remain semantically neutral, focusing solely on the arrangement and duplication of formulas rather than their interpretive meaning.^[1]^[7]

Properties

Sequent calculus exhibits several key structural properties that arise from the conjunctive interpretation of the antecedent and disjunctive interpretation of the succedent, where a sequent \Gamma \vdash \Delta expresses that the conjunction of formulas in \Gamma implies the disjunction of formulas in \Delta.^[1]^[8] One fundamental property is weakening, which allows the addition of formulas to either side of the sequent while preserving its validity. Specifically, adding a formula A to the antecedent \Gamma results in \Gamma, A \vdash \Delta, which strengthens the antecedent and makes the sequent harder to prove semantically, as the premise now requires an additional assumption to hold.^[1] Conversely, adding A to the succedent \Delta yields \Gamma \vdash \Delta, A, which weakens the succedent by broadening the possible conclusions, rendering the sequent easier to prove.^[8] These operations reflect the monotonicity of classical logic, ensuring that if the original sequent is valid, the modified versions remain valid.^[1] Related to weakening are properties concerning the insertion of specific formulas. Inserting a tautology T into the succedent preserves the sequent's validity, as \bigwedge \Gamma \to \bigvee \Delta implies \bigwedge \Gamma \to (\bigvee \Delta \vee T), since \bigvee \Delta entails \bigvee \Delta \vee T.^[8] Special cases involving empty multisets highlight boundary behaviors of sequents. An empty antecedent, denoted \vdash \Delta, is valid if and only if the disjunction \bigvee \Delta is a tautology; this is equivalent to including the true constant \top in the succedent, and it holds whenever \Delta contains a tautologous formula, though a non-empty \Delta does not guarantee validity without such content.^[1]^[8] In contrast, an empty succedent, \Gamma \vdash, is valid only if the conjunction \bigwedge \Gamma is a contradiction, equivalent to deriving \bot from \Gamma, marking it as an inconsistent premise.^[1]^[8] A notable implication between sequents is that if \Gamma, A \vdash \Delta holds, then \Gamma \vdash A, \Delta follows, as the semantic content \bigwedge \Gamma \wedge A \to \bigvee \Delta entails \bigwedge \Gamma \to (A \vee \bigvee \Delta).^[1] This property underscores the flexibility of sequent structure in capturing logical relationships without invoking explicit inference steps.^[8]

Examples and Inference

Basic Examples

One fundamental example of a sequent is A \vdash A, which expresses reflexivity and is valid by the assumption that if A holds, then A follows directly.^[9] This axiom forms the basis for identity rules in sequent calculus, where a formula on the left side of the turnstile immediately justifies itself on the right.^[10] Another basic valid sequent is \vdash A \lor \neg A, illustrating the law of excluded middle with an empty antecedent, indicating that the disjunction is a tautology true in all interpretations.^[6] The empty left side emphasizes that no assumptions are needed for this principle to hold classically. The sequent A, \neg A \vdash B demonstrates ex falso quodlibet, valid because the contradictory assumptions A and \neg A cannot both be true, allowing any conclusion B to follow.^[9] This holds even if the succedent is empty, as the antecedent's inconsistency renders the implication vacuously true. A non-tautologous valid sequent, such as \vdash (B \lor A), (C \lor \neg A), is valid because the disjunction of the succedents covers all cases: if A is true, then B \lor A holds; if \neg A is true, then C \lor \neg A holds, ensuring at least one succedent is satisfied in every model.^[10] Here, neither individual succedent is a tautology, but the overall semantics—where the empty antecedent implies the disjunction of the succedents—establishes validity through exhaustive case analysis on A.^[10] To contrast validity with invalidity, consider the sequent P \vdash P \land Q, which is invalid because assuming P alone does not entail the conjunction P \land Q without the additional assumption of Q.^[9] In contrast, P \land Q \vdash P, Q is valid, as the conjunction on the left implies each conjunct individually via elimination, allowing both to appear in the succedent.^[10] These examples highlight how structural properties like weakening can extend antecedents or succedents without affecting validity, but only when applied to already valid forms.^[10]

Inference Rules

In sequent calculus, inference rules are divided into structural rules, which manipulate the context of formulas without altering their logical content, and logical rules, which introduce or eliminate logical connectives. These rules, originally formulated by Gerhard Gentzen, enable the construction of proofs by deriving sequents from axioms or initial sequents. Structural rules include weakening, which allows the addition of a formula to the antecedent or succedent without affecting provability; contraction, which removes duplicate occurrences of a formula in the antecedent or succedent; and exchange (or permutation), which permits reordering of formulas within the antecedent or succedent. For instance, the left weakening rule states that if \Gamma \vdash \Delta, then \Gamma, A \vdash \Delta, preserving the derivability of the sequent. These rules ensure flexibility in proof construction while maintaining logical equivalence.^[1] Logical rules correspond to the introduction of connectives and are specified separately for the left (antecedent) and right (succedent) sides of the sequent. For conjunction (\wedge), the left introduction rule (\wedge L) derives \Gamma, A \wedge B \vdash \Delta from \Gamma, A, B \vdash \Delta, allowing the conjunctive antecedent to be introduced from its components. On the right, the conjunction (\wedge R) introduction rule derives \Gamma \vdash A \wedge B, \Delta from both \Gamma \vdash A, \Delta and \Gamma \vdash B, \Delta, reflecting the need to establish both conjuncts in the succedent. Similar rules exist for other connectives like implication and negation, ensuring that proofs mirror the semantics of classical logic.^[1] The cut rule provides a mechanism for composing proofs by eliminating an intermediate formula A: if \Gamma \vdash A, \Delta and \Gamma', A \vdash \Delta', then \Gamma, \Gamma' \vdash \Delta, \Delta'. In classical sequent calculus, the cut rule is admissible, meaning it can be eliminated from proofs without loss of derivability, which underlies the cut-elimination theorem central to Gentzen's consistency proofs.^[11] Together, these rules establish the soundness and completeness of sequent calculus for classical propositional logic, such that a sequent is provable if and only if it is semantically valid as a tautology.^[12]^[13]

Historical and Interpretive Aspects

Etymology and Origins

The term "sequent" derives from the German word Sequenz, which Gerhard Gentzen introduced in 1934 to describe a structured expression in logic comprising a sequence of antecedent formulas on the left side and succedent formulas on the right, symbolizing a logical implication from premises to conclusions. The English term "sequent" was suggested by Stephen Kleene in 1952 to translate Gentzen's "Sequenz," distinguishing it from "sequence" (corresponding to German "Folge"). This coinage emphasized the relational progression in deductive reasoning rather than a mere enumeration, distinguishing it from the mathematical concept of a sequence as a successive ordering of elements.^[14] Gentzen first employed the term in his seminal paper Untersuchungen über das logische Schließen (Investigations into Logical Deduction), published in Mathematische Zeitschrift, where he developed the sequent calculus as part of his broader framework for formalizing proofs. In this work, a sequent takes the form \Gamma > \Delta (using the original notation; modern variants include \Gamma \vdash \Delta), where \Gamma and \Delta are multisets of formulas, intuitively representing that the conjunction of formulas in \Gamma implies the disjunction of those in \Delta.^[15] The introduction of sequents was influenced by David Hilbert's program for the foundations of mathematics, which sought to analyze the structure of proofs through finitary methods to establish consistency.^[2] Gentzen formalized sequents specifically to circumvent paradoxes arising in infinitary proof constructions, enabling the elimination of the cut rule and yielding cut-free proofs that align with Hilbert's emphasis on constructive rigor.^[16]

Evolution of Meaning

Gerhard Gentzen introduced the concept of sequents in his 1934 paper as expressions of the form \Gamma > \Delta (original notation; modern variants include \Gamma \to \Delta), interpreting them semantically as implications where the premises in \Gamma entail the conclusions in \Delta under classical truth conditions. To accommodate intuitionistic logic, which rejects the law of excluded middle, sequent calculus was adapted into the system LJ with modified rules, while maintaining the semantic intuition adjusted for intuitionistic semantics; sequents are understood as provability assertions in the proof-theoretic framework. This allowed sequent calculus to serve both classical (LK) and intuitionistic (LJ) logics. Following Gentzen's foundational work, sequent calculus saw increased adoption in metalogical studies during the 1950s, particularly for analyzing derivability relations. Evert W. Beth's 1955 paper "Semantic Entailment and Formal Derivability" highlighted the distinction between semantic validity and syntactic provability, emphasizing the latter in sequent-based systems to rigorously separate proof-theoretic from model-theoretic concerns. This development reinforced the syntactic focus, enabling precise investigations into consistency and completeness independent of underlying truth semantics. The emphasis on syntactic provability was crucial for Gentzen's 1935 cut-elimination theorem, which demonstrates that any derivation using the cut rule can be transformed into an equivalent cut-free derivation, thereby establishing key properties like subformula adherence in proofs. This theorem underscored the power of the provability interpretation in facilitating analytic proofs. Dag Prawitz's 1965 monograph Natural Deduction: A Proof-Theoretical Study further influenced sequent interpretations by developing normalization theorems for natural deduction systems, which translate directly to cut-elimination in sequent calculus via established equivalences between the two frameworks, thereby deepening the understanding of sequents as structured representations of normalized proofs.^[17]

Intuitive Interpretation

A sequent \Gamma \vdash \Delta captures the intuitive notion that if all the assumptions in the antecedent \Gamma hold true, then at least one conclusion in the succedent \Delta must follow.^[18] This formulation mirrors everyday conditional reasoning, where a set of premises jointly supports one or more outcomes, emphasizing the conjunctive nature of the assumptions on the left and the disjunctive possibilities on the right.^[19] From a proof-theoretic standpoint, the notation \Gamma \vdash \Delta signifies the existence of a formal proof tree in sequent calculus that derives the sequent from basic axioms, building upward through applications of inference rules until reaching the root sequent.^[20] In classical logic, this intuitive entailment aligns precisely with the semantic equivalence (\bigwedge \Gamma) \to (\bigvee \Delta), where the conjunction of antecedents implies the disjunction of succedents.^[21] In intuitionistic logic, however, the sequent is typically restricted to a single succedent formula, as in \Gamma \vdash A, requiring a constructive proof that explicitly builds the truth of A from \Gamma without indirect methods like proof by contradiction.^[18] This distinction underscores the emphasis on verifiable constructions over mere truth preservation, providing a more direct analogy to step-by-step deduction in natural reasoning.^[19]

Variations and Applications

Variations in Logics

In intuitionistic logic, sequents are adapted to have a single succedent formula, expressed as Γ ⊢ A, where Γ is a multiset of formulas in the antecedent and A is the sole formula in the succedent.^[11] This restriction ensures that proofs constructively establish the succedent without relying on the law of excluded middle, which is rejected in intuitionistic systems as it cannot be proven without assuming non-constructive principles.^[22] Dual-intuitionistic logic, also known as co-intuitionistic logic, mirrors this adaptation by restricting sequents to a single antecedent formula, written as A ⊢ Γ, where A is the unique formula in the antecedent and Γ is the multiset in the succedent.^[11] This structure emphasizes co-implications, the dual of implications, allowing for a logic that focuses on refutations and co-Heyting algebras rather than constructive proofs.^[23] In modal logics, sequents are often indexed by worlds or accessibility relations to handle operators like necessity (□) and possibility (◇), resulting in forms such as Γ ⊢_i Δ, where i denotes a world or label.^[24] These labeled sequents enable rules that propagate modalities across worlds, distinguishing between local and global assumptions in Kripke-style semantics. Linear logic modifies classical sequents by incorporating exponential modalities ! (of course) and ? (why not) to regulate resource consumption, permitting contraction and weakening only on modalized formulas within the sequent.^[25] For instance, !A in the antecedent allows multiple uses of A as a reusable resource, while unmodalized formulas must be consumed exactly once, thus controlling the structural rules to model resource-sensitive reasoning.^[26] Relevance logic adapts sequents by restricting or eliminating the contraction rule in certain formulations to prevent derivations from irrelevant assumptions, ensuring that antecedents share content with consequents through variable-sharing constraints.^[27] In contraction-free variants, such as those developed by Brady, this avoids paradoxes like Curry's paradox while maintaining relevance in implications.^[27]

Connections to Proof Systems

Sequent calculus exhibits a close equivalence to natural deduction, another foundational proof system developed concurrently by Gerhard Gentzen. In sequent calculus, the left and right rules for logical connectives directly simulate the introduction and elimination rules of natural deduction, respectively, allowing proofs in one system to be systematically translated into the other without loss of expressive power. This correspondence enables the interchange of techniques between the two frameworks, such as cut-elimination in sequent calculus mirroring normalization in natural deduction. Gentzen established this interderivability formally in his seminal 1935 work, demonstrating that any natural deduction proof can be transformed into a sequent calculus derivation and vice versa, thereby proving the logical equivalence of the systems for classical and intuitionistic logics. This result underpins much of modern proof theory, facilitating the study of proof normalization and consistency across different formalisms. Sequent calculus also connects to resolution, a key method in automated theorem proving, particularly for first-order logic. The antecedents of a sequent can be converted to clausal normal form, where the multiple premises are represented as disjunctive clauses, enabling the application of resolution steps to derive contradictions or proofs from refutation. This translation preserves completeness, as resolution's refutational soundness derives from the underlying sequent calculus structure, making sequents a bridge between manual proof construction and computational verification.^[28] Through the Curry-Howard isomorphism, sequents in intuitionistic logic model type inhabitation in the lambda calculus, where a provable sequent \Gamma \vdash A corresponds to the existence of a lambda term of type A under assumptions \Gamma. This encoding extends the proofs-as-programs paradigm to sequent-based systems, with focused sequent calculi providing refined correspondences that align proof search with term normalization, as explored in extensions of the isomorphism to handle classical features.^[29]

Modern Uses

In automated theorem proving, sequent calculi form the foundational structure for interactive proof assistants such as Lean, Coq, and Isabelle, enabling users to construct and verify formal proofs through step-by-step manipulation of sequents.^[30]^[31] These systems represent proof states as sequents, where antecedents and succedents guide the application of inference rules, facilitating the development of large-scale mathematical libraries and software verifications. For instance, Lean's tactic language operates over sequent-like goals, allowing for modular proof construction in dependent type theory. Since the 2000s, sequents have been integral to formal verification tools like Isabelle/HOL, where they underpin the checking of software and hardware correctness by encoding system properties as provable sequents. This approach has supported high-profile applications, including the verification of operating system kernels and cryptographic protocols, by providing a rigorous framework for discharging proof obligations. In artificial intelligence, sequent calculi extend to reasoning tasks in description logics, the basis for OWL ontologies used in semantic web technologies. These calculi enable automated inference over complex knowledge bases, such as classifying concepts and checking consistency in biomedical ontologies, through cut-free sequent derivations that mirror tableau-based methods but offer finer control over subformula properties.^[32] A notable application appears in quantum computing, where categorical semantics inspired by linear logic model the no-cloning theorem, demonstrating that arbitrary quantum states cannot be perfectly duplicated. In this framework, introduced by Abramsky in 2009, the resource-sensitive nature of linear logic—where hypotheses are used exactly once—captures quantum non-duplicability by showing that cloning operations lead to unprovable sequents under multiplicative rules.^[33] In the 2020s, sequent-based proof search has integrated with machine learning through neural theorem provers, enhancing automation in systems like Lean and Coq. These models, such as DeepSeek-Prover and HyperTree Proof Search, train on proof corpora to predict sequent transformations via tactics, achieving significant success rates on benchmark theorems by guiding search trees over sequent derivations. This hybrid approach addresses the combinatorial explosion in proof search, leveraging neural networks to prioritize promising sequent branches.

References

[1]
Sequent Computer Systems
Sequent was founded in 1983 by former Intel employees. Their intention was to build computers based on SMP = Symmetric Multiprocessing.
[2]
Sequent Computer Systems To Be Acquired by I.B.M.
Jul 13, 1999 · Sequent Computer Systems to be acquired by IBM for $810 million; Sequent will be folded into IBM's server computers, including RS 6000 and ...<|control11|><|separator|>
[3]
Sequent was overmatched, CEO says - CNET
Sequent, a company that designs high-end servers at the center of corporate operations, this week lost its battle to remain independent.
[4]
Sequent Computer Systems Inc - Crunchbase Company Profile ...
Sequent Computer Systems designs and manufactures multiprocessing computer systems based on Cache Coherent Non-Uniform Memory Access architecture.
[5]
Proof Theory (Stanford Encyclopedia of Philosophy)
Summary of each segment:
[6]
Systems of Deduction - SpringerLink
Gentzen, G.: 1934, 'Untersuchungen über das logische Schliessen', Math. Zeitschrift 39, 176–210, 405–431. Complete English translation in Szabo [1969].
[7]
[PDF] Sequent Calculus
In this chapter we develop the sequent calculus as a formal system for proof search in natural deduction. The sequent calculus was originally introduced.
[8]
[PDF] The Sequent Calculus - Open Logic Project Builds
⊥ ⇒ for any sentence φ in the language. Derivations in the sequent calculus are certain trees of sequents, where the topmost sequents are initial sequents, and ...
[9]
[PDF] Lecture Notes on Sequent Calculus - André Platzer
May 13, 2024 · In this lecture we shift to a different presentation style for proof calculi. We develop the sequent calculus as a formal system for proof ...
[10]
https://www.cs.cmu.edu/~15414/s23/s22/lectures/12-sequents.pdf
[11]
Interactive Tutorial of the Sequent Calculus - Logitext
Sequents and axioms. The turnstile is always included in a sequent, an example of which is displayed below. You can interact with it by clicking on the A, ...
[12]
[PDF] Lecture Notes on Sequent Calculus
Feb 24, 2022 · If, for example, A is again a disjunction we'd like to be able to apply this rule again. This means the succedent should allow multiple formulas ...
[13]
sequent calculus in nLab
Sep 15, 2023 · A central property of sequent calculi, which distinguishes them from systems of natural deduction, is that it allows an easier analysis of ...
[14]
[PDF] Classical sequent calculus - Homepages of UvA/FNWI staff
(Soundness of the sequent calculus) If Γ ⇒ ∆ is derivable in the classical sequent calculus, then it is a tautology. The converse (completeness) holds as well ...
[15]
[PDF] Classical Sequent Calculus
The calculus LK0 is sound and complete for propositional classical logic: Γ `LK ∆ iff Γ |= ∆. Proof. Soundness amounts to check that each rule of LK0 ...
[16]
[PDF] Negri, S and von Plato, J Structural Proof Theory - - Logic Matters
441) explains the origin of the term as follows: "Gentzen says 'Sequenz', which we translate as 'sequent', because we have already used 'sequence' for any ...
[17]
None
### Summary of "Sequent" Definition and Introduction in Gentzen's 1934 Paper
[18]
The Development of Proof Theory
Apr 16, 2008 · He therefore invented another logical calculus that he called sequent calculus (Sequenzenkalkul, literally “calculus of sequences”) and made it ...
[19]
[PDF] Hilbert's Program Then and Now - arXiv
Aug 29, 2005 · Gentzen's development of natural deduction and the sequent calculus was carried out in the tradition of. Hilbert's program and with the aim ...
[20]
[PDF] Focusing Gentzen's sequent calculus - LIX
Feb 1, 2024 · A key observation about an inference rule is whether or not it is invertible: i.e., if the conclusion has a proof then all of its premises must ...
[21]
Propositional BI as a Sequent Calculus - SpringerLink
We reformulate BI's proof theory as a sequent calculus [Gentzen, 1934] in which the elimination rule for each connective, #, in a natural deduction system ...
[22]
Natural Deduction Systems in Logic
Oct 29, 2021 · We've called this way of presenting proofs “sequent natural deduction” to honour the way it is developed from sequent calculus. However ...
[23]
[PDF] A Tutorial on Computational Classical Logic and the Sequent Calculus
Rather, the structural properties of sequents (weakening, contraction, and exchange) define the meaning of static variables and co-variables. Similar to LK, the ...
[24]
[PDF] Sequent Calculus
Sequents: Notation. I We use set notation for multisets, eg {A,B → C,A}. I Drop {}: F1,...,Fm ⇒ G1,...Gn. I F,Γ abbreviates {F} ∪ Γ (similarly for ∆). I Γ1 ...
[25]
[PDF] Classical sequent calculus
One of the most important proof systems is the sequent calculus, which, like natural de- duction, was invented by the German proof-theorist Gerhard Gentzen.
[26]
Intuitionistic Logic - Stanford Encyclopedia of Philosophy
Sep 1, 1999 · Intuitionistic logic encompasses the general principles of logical reasoning which have been abstracted by logicians from intuitionistic mathematics.
[27]
Natural deduction for bi-intuitionistic logic - ScienceDirect.com
As implication is the distinctive connective of intuitionistic logic, the natural habitat of co-implication is dual-intuitionistic logic. A sequent calculus ...
[28]
[PDF] Modal Sequent Calculus - Open Logic Project Builds
Not every modal logic has such a sequent calculus. Even S5, which is se- mantically simple (it can be defined without using accessibility relations at all).Missing: analogy balance scale
[29]
https://drops.dagstuhl.de/storage/00lipics/lipics-vol038-tlca2015/LIPIcs.TLCA.2015.165/LIPIcs.TLCA.2015.165.pdf
[30]
https://www.youtube.com/watch?v=I483PWxwNy8
[31]
Relevance Logic - Stanford Encyclopedia of Philosophy
Jun 17, 1998 · Relevance logics are non-classical logics developed to avoid paradoxes of material and strict implication.
[32]
[PDF] Resolution Theorem Proving - Machine Logic
1 In fact, the refutational completeness of resolution can be derived from the completeness of the (proposi- tional) sequent calculus; and Herbrand's theorem, ...
[33]
[PDF] Curry-Howard for Sequent Calculus at Last! - DROPS
This paper tries to remove what seems to be the remaining stumbling blocks in the way to a full understanding of the Curry-Howard isomorphism for sequent ...Missing: inhabitation | Show results with:inhabitation
[34]
Sequents, semantics, and inductive types in Lean. - YouTube
May 14, 2022 · This is a talk I gave at a seminar on the automated proof assistant Lean. I introduce sequent calculus ... Infinitude of primes --- a Lean theorem ...
[35]
[2204.03884] SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
Apr 8, 2022 · SeCaV is a sequent calculus verifier for first-order logic in Isabelle/HOL, with an online tool to expand derivations.
[36]
[PDF] Uniform and Modular Sequent Systems for Description Logics
This paper introduces a framework for constructing sequent systems for description logics, providing a general recipe for generating proof systems.