(and (==> A B) (==> B A))

Definition: Logical equivalence or ‘if and only if’.

(forall [α :type] α)

Definition: Absurdity.

(==> A (not A) absurd)

Theorem: Introduction rule for absurdity.

(forall [C :type] (==> (==> A B C) C))

Definition: logical conjunction.

A notation defining an n-ary variant of and, which exploits the fact that conjunction is associative. By default we use the leaf-leaning expansion:

(and* p1 p2 ... pN-1 pN) ≡ (and (and ... (and p1 p2) pN-1) pN)))

We favor this variant because it is often the case that we use conjunction for a form of “subclassing”. Consider some mathematical <object> defined as having some properties (and p1 p2) (e.g. a preorder with reflexivity and transitivity). Then we might “subclass” such an object by considering a supplementary property, i.e. we want (and <object> p3) (e.g. a preorder with antisymetry hence a partial order). This is exactly (and (and p1 p2) p3), and if it is of course isomorphic to the right-leaning version (and p1 (and p2 p3)), only the left variant reflects the “subclassing” aspect.
A right-leaning nary conjunction is provided by r-and*.

This is a generic elimination rule for n-ary conjunction (e.g. as introduced by the and* notation). In (and-elim* n and-term) the index n corresponds to the n-th operand of the term.

For example (informally ):

• (and-elim* 1 (and* a b c)≡(and (and a b) c)) ==> a
• (and-elim* 2 (and* a b c)) ==> b
• (and-elim* 3 (and* a b c)) ==> c

Internally, the correct nesting of and-elim-left and and-elim-right is constructed. Errors are raised if the index is incorrect or if the specificied term is not a conjunction.

An implicit elimination rule that takes a proof p of type (and A B) and yields a proof of A.

This is an implicit version of and-elim-left-thm.

(==> (and A B) A)

Theorem: Elimination rule for logical conjunction. This one only keeps the left-side of the conjunction

An implicit elimination rule that takes a proof p of type (and A B) and yields a proof of B.

This is an implicit version of and-elim-right-thm.

(==> (and A B) B)

Theorem: Elimination rule for logical conjunction. This one only keeps the right-side of the conjunction

An introduction rule that takes a proof a of type A, a proof b of type B and yields a proof of type (and A B).

This is an implicit version of and-intro-thm.

A nary variant of and-intro, the introduction rule for conjunction. It builds a proof of (and* A1 A2 ... AN) from proofs of the Ai’s

(==> A B (and A B))

Theorem: Introduction rule for logical conjunction.

Symmetry of conjunction. Proves (and B A) from a proof p that (and A B).

This is an implicit version of and-sym-thm.

(==> (and A B) (and B A))

Theorem: Symmetry of conjunction.

(==> absurd A)

Theorem: Ex falso sequitur quodlibet (proof by contradiction, elimination for absurdity).

Left (if) elimination for <=>, an implicit version of iff-elim-if-thm.

(==> (<=> A B) (==> A B))

Theorem: Elimination rule for logical equivalence. This one only keeps the if part of the equivalence.

Right (only if) elimination for <=>, an implicit version of iff-elim-only-if-thm.

(==> (<=> A B) (==> B A))

Theorem: Elimination rule for logical equivalence. This one only keeps the only-if part of the equivalence.

Introduction rule for logical equivalence, an implicit version of iff-intro-thm.

(==> (==> A B) (==> B A) (<=> A B))

Theorem: Introduction rule for logical equivalence.

(<=> A A)

Theorem: Reflexivity of logical equivalence.

Symmetry of <=>, an implicit version of iff-sym-thm.

(==> (<=> A B) (<=> B A))

Theorem: Symmetry of logical equivalence.

Transitivity of <=>, an implicit version of iff-trans-thm.

(==> (<=> A B) (<=> B C) (<=> A C))

Theorem: Transitivity of logical equivalence.

(==> A B A)

Theorem: A variant of reflexivity.

(==> A (not (not A)))

Theorem: The if half of double negation.

This can be seen as an introduction rule for ¬¬ (not-not) propositions. Note that double-negation is a law of classical (non-intuitionistic) logic.

(==> A A)

Theorem: Implication is reflexive.

Implication is transitive.

(impl-trans pAB pBC) yields (==> A C) from the proof pAB that (==> A B) and the proof pBC that (==> B C)

cf. impl-trans-thm

(==> (==> A B) (==> B C) (==> A C))

Theorem: Implication is transitive.

A simple utility for creating “left-leaning” n-ary operator calls. Remark: the args are reverted in input.

A simple utility for creating “right-leaning” n-ary operator calls.

(==> A absurd)

Definition: Logical negation.

(forall [C :type] (==> (==> A C) (==> B C) C))

Definition: logical disjunction.

A notation defining an n-ary variant of or, which exploits the fact that disjunction is associative. By convention we have:

(or* p1 p2 ... pN-1 pN) ≡ (or p1 (or p2 (or ... (or pN-1 pN))))

Remark: unlike for conjunction, there is no real motivation to use a left-leaning variant by default, so the simpler right-leaning encoding is prefered.

Associativity of disjunction, an implicit that subsumes both or-assoc-thm and or-assoc-conv-thm.

(==> (or A (or B C)) (or (or A B) C))

Theorem:

(==> (or (or A B) C) (or A (or B C)))

Theorem:

An elimination rule that takes a proof or-term of type (or A B), a proof left-proof of type (==> A prop), a proof right-proof of type (==> B prop), and thus concludes that prop holds by [[or-elim-thm]].

This is (for now) the easiest rule to use for proof-by-cases.

Elimination rule for n-ary disjunction (or* T1 T2 ... TN).

(or-elim* or-term case1 case2 ... caseN)

is the same thing as the repeated and nested uses of [[or-elim]] for binary disjunction.

(==> (or A B) (forall [C :type] (==> (==> A C) (==> B C) C)))

Theorem: Elimination rule for logical disjunction. This corresponds to a important scheme of reasoning by cases. To prove a proposition C under the assumption (or A B): - first case: assume A and prove C - second case: assume B and prove C

A generic introduction rule for or*. Suppose we have a proof p of a proposition Ai, and suppose also the sequence of types A1,…,Ai,…,An.

Then (or-intro* A1 ... p ... An) is a proof of (or* A1 ... Ai ... An).

Left introduction for a disjunction (or A B), with proofA a proof of A. This is an implicit version of or-intro-left-thm.

(==> A (or A B))

Theorem: Introduction rule for logical disjunction. This is the introduction by the left operand.

Right introduction for a disjunction (or A B), with proofB a proof of B. This is an implicit version of or-intro-left-thm.

(==> B (or A B))

Theorem: Introduction rule for logical disjunction. This is the introduction by the right operand.

(==> (or A B) (not B) A)

Theorem: An elimination rule for disjunction, simpler than or-elim. This eliminates to the left operand.

(==> (or A B) (not A) B)

Theorem: An elimination rule for disjunction, simpler than or-elim. This eliminates to the right operand.

(==> (or A B) (==> (not A) B))

Theorem: An alternative elimination rule for disjunction.

Symmetry of disjunction, an implicit version of or-sym-thm.

(==> (or A B) (or B A))

Theorem: Symmetry of disjunction.

A notation defining an n-ary variant of and, which exploits the fact that conjunction is associative. This version is the right-leaning variant of and*, which means the following:

(and* p1 p2 ... pN-1 pN) ≡ (and p1 (and p2 (and ... (and pN-1 pN))))

This is a generic elimination rule for (right-leaning) n-ary conjunction (e.g. as introduced by the r-and* notation). In (r-and-elim* n r-and-term) the index n corresponds to the n-th operand of the term.

This is the right-leaning version of the default and-elim*.

A nary “right-leaning” variant of and-intro, the introduction rule for conjunction. It builds a proof of (r-and* A1 A2 ... AN) from proofs of the Ai’s

Remark: the default “left-leaning” varient is and-intro*.

(not absurd)

Definition: Logical truth.

truth

Theorem: The truth is true (really ?).