Revision #2877 → #3330 · back to history
modifiedFree variable occurrencea494e43e1370
| Field | From #2877 | To #3330 |
|---|
| note | Mathlib's ModelTheory tracks free variables in first-order formulas (e.g. freeVarFinset), but not as part of a sequent-calculus inference system. | Mathlib's ModelTheory tracks free variables in first-order formulas (freeVarFinset, verified via decl_exists), but not as part of a sequent-calculus inference system. |
modifiedSubstitution notation27c55c818a61
| Field | From #2877 | To #3330 |
|---|
| note | Substitution of terms into first-order formulas exists in ModelTheory (e.g. BoundedFormula.subst), though not tied to LK notation. | Substitution of terms into first-order formulas exists in ModelTheory (BoundedFormula.subst, verified via decl_exists), though not tied to LK notation. |
addedGentzen-style advantages for quantifier reasoning0d511d81779d
addedSymmetry of conjunction and disjunction rulesc2f311837b6d
addedTurnstile symbol1daec4f983d7
addedEquivalence of natural-deduction judgments2da765f88810
addedEquivalence of sequents (extension of proofs)6346be720577
addedSemantic invariance of reduction-tree stepsc9846d51e449
addedSplit-context variant of two-premise rules3d70c71eafbc