latte-prelude.classic
The axioms of classical logic, and basic derived proof rules.
By convention, all the imports from this namespace must be done in a qualified way, i.e. favor classic/not-not-impl instead of the unqualifed not-not-impl.
excluded-middle-ax
(excluded-middle-ax [A :type])(or A (not A))
Axiom: The law of excluded middle for classical logic.
This axiom can be assumed for classical (sometimes called “non-constructive”) reasoning.
not-impl-or-intro
(not-impl-or-intro [A :type] [B :type])(==> (==> (not A) B) (or A B))
Theorem: An alternative elimination rule for disjunction.
Remark: this introduction is only provable in classical logic.
not-not
(not-not [A :type])(<=> A (not (not A)))
Theorem: The double-negation law of classical logic.
not-not-impl
(not-not-impl [A :type])(==> (not (not A)) A)
Theorem: The double-negation law of classical logic, obtained from the axiom of the excluded middle (the only-if part of double negation).
This can be seen as an elimination rule for ¬¬ (not-not) propositions.