Revision #1558 → #2185 · back to history
modifiedSequent calculus33c87c64147a
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no formalization of sequent calculus as a proof system; ModelTheory only covers first-order syntax and semantics, not deduction systems. |
| status | — | not_formalized |
modifiedHilbert stylebb294320cef0
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Hilbert-style deduction system is defined in Mathlib. |
| status | — | not_formalized |
modifiedGentzen stylea9721db0682f
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Gentzen-style sequent proofs are not formalized in Mathlib. |
| status | — | not_formalized |
modifiedNatural deduction3e9260334cd8
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib does not formalize natural deduction as an explicit proof system. |
| status | — | not_formalized |
modifiedSequent calculus line form87c7825df693
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The multi-conclusion sequent form is not defined in Mathlib. |
| status | — | not_formalized |
modifiedGentzen's Hauptsatz (cut-elimination)7f7385b069a8
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Cut-elimination / Hauptsatz is not in Mathlib (no hits for 'Hauptsatz' or 'cut elimination'). |
| status | — | not_formalized |
modifiedConsistency of Peano arithmetic11c3bc6e5214
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Gentzen's transfinite consistency proof of PA is not formalized in Mathlib. |
| status | — | not_formalized |
modifiedHilbert-style judgment463d96cefb79
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no Hilbert-style judgment form. |
| status | — | not_formalized |
modifiedNatural deduction judgment043d7a433533
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Natural-deduction judgments Γ ⊢ A are not formalized in Mathlib. |
| status | — | not_formalized |
modifiedSemantics of natural deduction judgmente422b9ae5fd2
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No formalized semantics of natural-deduction judgments in Mathlib. |
| status | — | not_formalized |
modifiedSequent880766f809f5
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | There is no 'sequent' object defined in Mathlib (the 89 hits for 'sequent' are all 'sequence'/'sequential'). |
| status | — | not_formalized |
modifiedAntecedent and succedentc46201d99a78
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Antecedent/succedent terminology and the underlying sequent object are absent from Mathlib. |
| status | — | not_formalized |
modifiedSemantics of a sequentf326ad643b9d
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Sequent semantics ⋀Γ ⊨ ⋁Δ is not in Mathlib. |
| status | — | not_formalized |
modifiedEmpty sequent is false182ffe24f234
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No sequents are defined, so no statement about the empty sequent. |
| status | — | not_formalized |
modifiedClassical reformulations of sequent semantics958fcb3f047c
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Classical equivalences of sequent semantics are not formalized in Mathlib. |
| status | — | not_formalized |
modifiedReduction tree example formulaebadc802a543
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Specific reduction-tree example is not in Mathlib. |
| status | — | not_formalized |
modifiedReduction treec15126b701ab
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Reduction trees for sequents are not defined in Mathlib. |
| status | — | not_formalized |
modifiedAxiom condition for atomic sequentsfb5dbb2a0ae1
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No formalization of the atomic-axiom criterion. |
| status | — | not_formalized |
modifiedSoundness and completeness of reduction-tree systemd394873b2142
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Soundness/completeness of a reduction-tree calculus is not formalized in Mathlib. |
| status | — | not_formalized |
modifiedProvability via reduction trees69e84f8425ac
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Mathlib statement linking Hilbert provability to reduction trees. |
| status | — | not_formalized |
modifiedFormal proof in LK619259b91d0e
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | LK proofs are not defined in Mathlib. |
| status | — | not_formalized |
modifiedFree variable occurrencea494e43e1370
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | FirstOrder.Language.BoundedFormula.freeVarFinset |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.ModelTheory.Syntax |
| note | — | Mathlib's ModelTheory tracks free variables in first-order formulas (e.g. freeVarFinset), but not as part of a sequent-calculus inference system. |
| status | — | partial |
modifiedSubstitution notation27c55c818a61
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | FirstOrder.Language.BoundedFormula.subst |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.ModelTheory.Syntax |
| note | — | Substitution of terms into first-order formulas exists in ModelTheory (e.g. BoundedFormula.subst), though not tied to LK notation. |
| status | — | partial |
modifiedStructural rule abbreviationsb056a39e4302
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Structural inference rules (W/C/P) are not defined in Mathlib. |
| status | — | not_formalized |
modifiedCut-elimination theorem3364bc35f434
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Cut-elimination is not formalized in Mathlib. |
| status | — | not_formalized |
modifiedCompleteness of atomic initial sequents6527c3d1878a
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No formalization of restricting LK's initial rule to atomic formulas. |
| status | — | not_formalized |
modifiedLaw of excluded middle derivation3c7ef824fda4
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The LEM derivation in LK is not formalized; Mathlib has Classical.em as a logical axiom, not a sequent-calculus derivation. |
| status | — | not_formalized |
modifiedQuantifier fact derivationc1c55ef887c7
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No LK example derivations are formalized in Mathlib. |
| status | — | not_formalized |
modifiedLK derivation showing automated proving03d491c3e8ae
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | LK and automated derivation in LK are not formalized in Mathlib. |
| status | — | not_formalized |
modifiedSequent proof ↔ closed analytic tableau2631950d9ab8
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has neither sequent proofs nor analytic tableaux to relate. |
| status | — | not_formalized |
modifiedWeakening rule95d791b659d1
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Weakening inference rule is defined in Mathlib. |
| status | — | not_formalized |
modifiedContraction and Permutation7784176e4039
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Contraction and Permutation structural rules are not formalized in Mathlib. |
| status | — | not_formalized |
modifiedSubstructural logicsb1f46a3eb93b
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Substructural logics are not defined in Mathlib. |
| status | — | not_formalized |
modifiedSoundness and completeness of LK99e69bcc3ab2
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | LK soundness and completeness are not formalized in Mathlib (Mathlib has model-theoretic semantics but no LK proof system). |
| status | — | not_formalized |
modifiedAdmissibility of cut (Hauptsatz)ebe23e05c0f5
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Admissibility of cut in sequent calculus is not formalized in Mathlib. |
| status | — | not_formalized |
modifiedAdmissibility of weakening via modified axiom5cf79469df2a
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Variants of LK's axiom rule and weakening admissibility are not in Mathlib. |
| status | — | not_formalized |
modifiedAbsurdity constant8e1c115e7564
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No object-level absurdity constant with a sequent-calculus axiom is defined in Mathlib (Lean's False is metalevel). |
| status | — | not_formalized |
modifiedNegation from implication3ac30411bf39
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Definition of ¬A := A → ⊥ inside a formal proof system is not given in Mathlib. |
| status | — | not_formalized |
modifiedSystem LJe04ee6ab443b
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The intuitionistic sequent calculus LJ is not defined in Mathlib. |
| status | — | not_formalized |
modifiedSoundness and completeness of LJadea44d23db0
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | LJ soundness/completeness and its cut-elimination are absent from Mathlib. |
| status | — | not_formalized |
modifiedDisjunction and existence properties9ad7e290763b
| Field | From #1558 | To #2185 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Intuitionistic disjunction/existence properties for LJ are not formalized in Mathlib. |
| status | — | not_formalized |
addedSequent (Gentzen's terminology)65773e5bb160
addedCedents (sequent formulas)4aab0313c9dc
addedLeft–right symmetry from De Morgan duality1922335d590d
addedConjunction/disjunction reading of cedentsc3f434bd42a5
addedEigenvariable restriction on quantifier rulesdca83fdf242a
addedContexts (Γ, Δ)b24afc2e5c61
addedRestriction to single-formula succedents for LJeb24bc8ab1e8
addedModus ponens implemented by cuta28d91aa6cd6