Lurch for Math 299

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)

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.

Math 299 Spring 2024 Assignments – each link one opens a Lurch document containing a homework assignment from the course. Note that Lurch was under development during this semester so that some assignments are not good examples of what can be done today if these were rewritten to take advantage of some of the new features. But we hope to update them soon.

Assignment #12

Peano arithmetic and induction.

Assignment #13

Peano arithmetic and induction.

Assignment #14

Sequences, Recursion, and Induction.

Assignment #15

Sequences, Recursion, and Induction.

Assignment #16

Real numbers and field axioms.

Assignment #17

Real numbers and field axioms.

Assignment #18

Elementary Set Theory.

Assignment #19

Elementary Set Theory.

Assignment #20

Functions and composition.

Assignment #21

Functions and composition.

Assignment #22

Equivalence relations and partial orders.

Assignment #23

Equivalence relations and congruence.

Assignment #24

Modular arithmetic.