Example Definitions, Rules, and Theorems

Cumulative Topics – each link opens a blank Lurch document whose context consists of the rules for that topic, and those from the topics above it. The Theorem numbers refer to exercises in the draft of the course lecture notes.

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)$, Fibonacci numbers $\left(F_n\right)$, factorial $\left(!\right)$, multinomial coefficients $\left(m,n\right)$, binomial coefficients $\binom{n}{k}$, 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)

Additional Rules. The following rules can be optionally added by the instructor to any context above in a particular document. Currently, only one of the three Arithmetic rules can be used in a single document.

Arithmetic in the Natural Numbers

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)

Arithmetic in the Integers

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)

Arithmetic in the Rationals

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)

Algebra

Allows the user to say 'by algebra' after an equation to try to justify it using a CAS. There are 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).

Useful Cumulative Contexts. These contexts combine some proper subsets of the cumulative Math 299 contexts listed above.

Equations Only

Only the Equations rule and nothing else. Defines $=$. (view rules)

Equations and Logic Only

Equations, Logic Theorems, Predicate Logic, Propositional Logic. (view rules)

Sets, Equations, and Logic

Set Theory, Equations, Logic Theorems, Predicate Logic, Propositional Logic. This does not include Set Theory Theorems. (view rules)

Functions, Sets, Equations, and Logic

Functions, Set Theory Theorems, Set Theory, Equations, Logic Theorems, Predicate Logic, Propositional Logic. (view rules)

Topology

Defines topological space, open, closed, and continuous (in a toplogical space). Includes the Functions library above. (view rules)

Linear Algebra

Defines linear, subspace, closed under addition, closed under multiplication, nonempty, vectors, vector addition, and scalar multiplication (in $\mathbb{R}^2$ and $\mathbb{R}^3$). Includes the Functions, Sets, Equations, and Logic library above. (view rules) (examples).