Lurch for Instructors

Cumulative Topics – each link one opens a blank Lurch document whose context consists of the rules for that topic, and those from the topics above it.

Propositional Logic

defines and, or, not, implies, iff, and contradiction (view rules)

Predicate Logic with Equality

defines forall $\left(\forall\right)$, exists $\left(\exists\right)$, equality $\left(=\right)$, unique existence $\left(\exists!\right)$ (view rules)

Logic Theorems

provides some common theorems from Logic (view rules)

Natural Numbers

the Peano Axioms for the Natural Numbers (view rules)

Number Theory Definitions

defines, less than $\left(\lt\right)$, divides $\left(\mid\right)$, prime, even, odd (view rules)

Equations

defines a single ‘rule’ that enables Lurch to validate transitive chains of equalities without needing substitution, reflexivity, symmetry, or transitivity (view rules)

Number Theory Theorems

provides some useful theorems from Number Theory that are provable from the Peano Axioms (view rules)

Sequences and Recursion

defines summation $\left(\sum\right)$, Fibonnaci numbers $\left(F_n\right)$, factorial $\left(!\right)$, multinomial coefficients $\binom{n}{k}$, binomial coefficients, exponentiation $\left(z^n\right)$ (view rules)

Real Numbers

defines the field axioms for the Real Numbers (view rules)

Set Theory

defines in $\left(\in\right)$, subset $\left(\subseteq\right)$, intersection $\left(\cap\right)$, union $\left(\cup\right)$, complement $\left(‘\right)$, set difference $\left(\setminus\right)$, powerset $\left(\mathscr{P}\right)$, Cartesian product $\left(\times\right)$, finite set $\left(\{ \ldots \}\right)$, tuple $\langle\ldots\rangle$, Indexed Union $\left(\bigcup\right)$, Indexed Intersection $\left(\bigcap\right)$, Set Builder notation $\left(\{ z : \ldots\}\right)$ (view rules)

Functions

defines maps $\left(f\colon A \to B\right)$, function application $\left(f(x)\right)$, maps to $\left(\mapsto\right)$, image $\left(f(U)\right)$, identity map $\left(\text{id}_A\right)$ inverse image $\left(f^\text{inv}(U)\right)$, composition $\left(\circ\right)$, inverse function $\left(f^{-1}\right)$, injective, surjective, bijective (view rules)

Relations

defines reflexive, symmetric, transitive, irreflexive, antisymmetric, total, partial order, strict partial order, total order, equivalence relation, partition, equivalence class $[a]$ (view rules)

Some Other Useful Contexts

Equations and Logic Only

Equations, Logic Theorems, Predicate Logic, Propositional Logic.

Sets, Equations, and Logic

Set Theory, Equations, Logic Theorems, Predicate Logic, Propositional Logic.

Functions, Sets, Equations, and Logic

Functions, Set Theory, Equations, Logic Theorems, Predicate Logic, Propositional Logic.

Prove it! Topics – each link one opens a blank Lurch document whose context consists of the rules for that topic.

Proof by Contradiction and Cases

defines or, not, and contradiction (view rules)