Defines and, or, not, implies, iff, and contradiction. view rules

Defines forall $\left(\forall\right)$, exists $\left(\exists\right)$ and equality $\left(=\right)$. view rules

Provides some common theorems about logic. (Includes: Equations) view rules

The Peano Axioms for the Natural Numbers. view rules

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

Provides some useful theorems from Number Theory that are provable from the Peano Axioms. view rules

Defines summation $\left(\sum\right)$, Fibonacci numbers $\left(F_n\right)$, factorial $\left(!\right)$, multinomial coefficients $\left(m,n\right)$, binomial coefficients $\binom{n}{k}$ and exponentiation $\left(z^n\right)$. (Includes: Arithmetic in $\NN$) view rules

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)$, power set $\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)$ and Set Builder notation $\left\{ z :\ldots \right\}$. view rules

Defines the field axioms for the Real Numbers. view rules

Defines the sets $\NN$, $\ZZ$, and $\QQ$, and some basic theorems about them including induction, strong induction, and induction from $a$ in $\NN$. (Includes: Arithmetic in $\QQ$) view rules

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 and bijective.
(Includes: Algebra) view rules

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

Defines a single ‘rule’ that enables Lurch to validate transitive chains of equalities without needing substitution, reflexivity, symmetry, or transitivity. Declares is to be a constant and provides a substitution rule for is. view rules

Allows the user to say 'by arithmetic' after an expression to try to justify it using a CAS. The expression can only contain natural number constants (e.g. $0$, $1$, $2$, etc) the operators $+$, $\cdot$, and $\text{^}$, and the relations $=$, $\neq$, $\leq$, and $\lt$. view rules

Allows the user to say 'by arithmetic' after an expression to try to justify it using a CAS. The expression can only contain natural number constants (e.g. $0$, $1$, $2$, etc) the operators $+$, $\cdot$, $\text{^}$, and $-$ and the relations $=$, $\neq$, $\leq$, and $\lt$. Exponents cannot be negative. view rules

Allows the user to say 'by arithmetic' after an expression to try to justify it using a CAS. The expression can only contain natural number constants (e.g. $0$, $1$, $2$, etc) the operators $+$, $\cdot$, $\text{^}$, $-$, and $/$, and the relations $=$, $\neq$, $\leq$, and $\lt$. Exponents must be integers and you cannot divide by zero. view rules

Allows the user to say 'by algebra' after an equation to try to justify it using a CAS. There are little or no restrictions on what the equation can contain, so use at your own discretion. The identity is evaluated using Algebrite. This rule also validates inequalities that can be validated by the previous rule (Arithmetic in the Rationals). view rules examples.