Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

EntailmentOne

Abstract

Licensed Foundation.Logic.Entailment source for the concrete first-order pair extension.

Source-command excerpt selected from Foundation.Logic.Entailment, lines 1-320, at Foundation revision 30a16ffa93d79d73ab4d02427fa00f50e039bf29. Only commands with live proof or source-elaboration consumers for the Kuratowski pair extension are retained.

The Lean file retains selected upstream commands and their compiler companions. The immutable source map, modification notices, full Apache-2.0 license and retirement condition are in Library/ConceptDynamics/foundation2026firstorder.md.

The retained commands supply the formulas, rewriting operations, set operations or proof and elaboration machinery used by the concrete pair interpretation. This excerpt does not represent the full upstream module.

References