Revision #3049 → #3555 · back to history
modifiedBivalence, noncontradiction, excluded middlefa531303995d
| Field | From #3049 | To #3555 |
|---|
| mathlib.decl | — | Classical.em |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Logic.Basic |
| note | Excluded middle (`Classical.em`) and noncontradiction are Lean-core theorems, not a Mathlib characterization of classical logic's distinctive features. | Excluded middle is `Classical.em` (Lean core, re-exported through Mathlib) and noncontradiction is `not_and_self`; these are theorems but not a Mathlib characterization of classical logic's distinctive features. |
| provenance | ai | ai-moderated |
| status | not_formalized | partial |
modifiedNumber of distinct interpretationse7d5e6108cca
| Field | From #3049 | To #3555 |
|---|
| mathlib.decl | — | Fintype.card_fun |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Data.Fintype.BigOperators |
| note | The count 2^n of interpretations is a cardinality fact (`card (Fin n → Bool)`) but is not stated about propositional interpretations. | The count 2^n of interpretations follows from `Fintype.card_fun` (giving `card (Fin n → Bool) = 2^n`), but it is not stated about propositional interpretations. |
| provenance | ai | ai-moderated |
| status | not_formalized | partial |
modifiedUncountably many interpretationsb616373a0b2f
| Field | From #3049 | To #3555 |
|---|
| mathlib.decl | — | Cardinal.cantor |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.SetTheory.Cardinal.Order |
| note | Uncountability of `ℕ → Bool` follows from Cantor's theorem in Mathlib, but is not stated about propositional interpretations. | Uncountability of `ℕ → Bool` follows from Cantor's theorem (`Cardinal.cantor`) in Mathlib, but is not stated about propositional interpretations. |
| provenance | ai | ai-moderated |
| status | not_formalized | partial |
modifiedEquivalence/biconditional truth condition8bca82d368d8
| Field | From #3049 | To #3555 |
|---|
| mathlib.module | Mathlib.Logic.Basic | Init.Core |
addedPrinciple of bivalence and law of excluded middlea715ad04c114
addedInterdefinability of ∨ via ¬ and ∧a90ddb0bc0bf
addedTruth of negation (¬ semantics)660bb6beb891
addedDe Morgan's lawsed46955a3ce1
addedDouble negation985a50e62f11
addedTransposition (contrapositive)bff512f29491
addedMaterial implicationf7855a15422c
addedCommutativity of ∧ and ∨13b85341e6b8
addedAssociativity of ∧ and ∨6cc5634b52c8
addedDistributivity of ∧ over ∨be82f40ef17c
addedExportation14316a195d67
addedDisjunctive syllogism2dab1e6b0fea
addedModus tollens1fcf38af50c7