Proof Verification with Lurch

Building the bridge to higher mathematics

Assignment #06Propositional logic

1. Theorem (Iff is stronger):$(P\Leftrightarrow Q)\Rightarrow(Q\Rightarrow P)$
2. Theorem (the other way around):$\neg(\neg A)\Rightarrow A$
3. Theorem (Modus Tollens):$(S \Rightarrow T)\text{ and } \neg T \Rightarrow \neg S$
4. Theorem (atomic statements don't have to be variables):$0 \lt x\text{ or }x\lt 10 \Rightarrow x\lt 10\text{ or } 0\lt x$
5. Theorem (excluded middle):$K\text{ or } \neg K$

Assignment #07Propositional logic

1. Theorem (implies is transitive):$((P\Rightarrow Q)\text{ and }(Q \Rightarrow R)) \Rightarrow (P \Rightarrow R)$
2. Theorem (alternate or-):$(S\text{ or } T)\text{ and } \neg S \Rightarrow T$

Assignment #08Predicate logic with Equality

1. Theorem (alpha equivalence warm up):$(\forall x.P(x)) \Rightarrow (\forall y.P(y))$
2. Theorem (same thing but for exists):$(\exists x.P(x)) \Rightarrow (\exists y.P(y))$
3. Theorem (commuting quantifiers):$(\forall x.\forall y.x\text{ loves }y) \Rightarrow (\forall y.\forall x.x\text{ loves }y)$
4. Theorem (same thing for exists):$(\exists x.\exists y.x\text{ loves }y) \Rightarrow (\exists y.\exists x.x\text{ loves }y)$
5. Theorem (DeMorgan):$\neg (S\text{ and }T) \Rightarrow \neg S\text{ or } \neg T$
6. Theorem (DeMorgan):$\neg (\forall x.R(x)) \Rightarrow (\exists x.\neg R(x))$
7. Theorem ($=$ is transitive):$x=y\text{ and }y=z \Rightarrow x=z$

Assignment #09Logic theorems

1. Theorem 5.10 (some are the same):$(\forall x.\forall y.P(x,y)) \Rightarrow (\forall z.P(z,z))$
2. Theorem 5.16 (excluded middle):$(\forall x.Q(x))\text{ or } (\exists x.\neg Q(x))$
3. Theorem 4.22 (alternate $\Rightarrow$):$(R \Rightarrow S) \Rightarrow \neg R\text{ or }S$

Assignment #10Logic review

1. Theorem (ex falso quodlibet):If Dracula fears Alice and Dracula does not fear Alice then Bob loves Alice.
2. Theorem 4.29 (the most beautiful?):$S \Rightarrow (S \Leftrightarrow S\text{ or }(\neg S \text{ and } S))$
3. Theorem 4.25 (shunting):$((P \text{ and } Q) \Rightarrow R) \Leftrightarrow (P \Rightarrow (Q \Rightarrow R))$
4. Theorem 5.21 (avoiding vacuous domains):$(\exists x. x = x)\text{ and }(\forall y. T(y)) \Rightarrow (\exists z. T(z))$
5. Theorem 5.5 (distributivity):$(\exists x. A(x) \Rightarrow B(x)) \Leftrightarrow (\forall y. A(y)) \Rightarrow (\exists z. B(z))$

Assignment #11Logic review

1. Theorem (Pierce's Law)$((S \Rightarrow T) \Rightarrow S) \Rightarrow S$
2. Theorem (quantifier fun):$(\forall x.\exists y.\forall z.A(x,y,z)) \Rightarrow (\forall z.\forall x.\exists y.A(x,y,z))$

Assignment #12Peano arithmetic and Induction

1. Theorem 7.3 (no number is it's own successor): $n\neq\sigma(n)$
2. Theorem 7.4 (alternate definition of $\sigma$): $\sigma(n)=n+1$
3. Theorem 7.5 (associativity of addition): $(m+n)+p=m+(n+p)$
4. Theorem 7.6 (additive identity, part 2): $0+n=n$
5. Theorem 7.7 (commutativity of adding $1$): $1+n=n+1$
6. Theorem 7.8 (commutativity of addition):$m+n=n+m$

Assignment #13Peano arithmetic and Induction

1. Theorem 7.11 (left multiplication by zero): $0\cdot m=0$
2. Theorem 7.19 (nonzero naturals are positive):
   • (a) $0\leq n$
   • (b) $0\lt n \Leftrightarrow n\neq 0$

Assignment #14Sequences, Recursion, and Induction

1. Theorem 8.3(a) (a useful identity): $n^2=n\cdot n$
2. Theorem 8.3(b) (useful identity): $2\cdot n=n+n$
3. Theorem 8.2(b) (power law): $z^m\cdot z^n=z^{m+n}$
4. Theorem 8.2(c) (power law): $(z^m)^n=z^{m\cdot n}$
5. Theorem 8.4 (quadratic beats linear):If $a+b\leq n$ then $a\cdot n+b\leq n^2$

Assignment #15Sequences, Recursion, and Induction

1. Theorem 8.7 (Fib fun): $F_{n+3}+F_n=2\cdot F_{n+2}$
2. Theorem 8.5(b) (basic sum property): $\displaystyle \sum_{i=0}^n s\cdot a_i = s\cdot \sum_{i=0}^n a_i$
3. Theorem 8.11 (closed formula for binomial coefficients): $\displaystyle(m!\cdot n!)\cdot \binom{n+m}{m}=(n+m)!$

Assignment #16Real numbers and Field axioms

1. Theorem 9.3 (cancellation for addition): If $x+z=y+z$ then $x=y$
2. Theorem 9.2(b) (signed product): $(-1)\cdot(-1)=1$
3. Theorem 9.2(c) (harder than it looks): $0\lt 1$
4. Theorem 9.2(d) (not mod 2): $-1\neq 1$

Assignment #17Real numbers and Field axioms

1. Theorem 9.4 (cancellation for multiplication): If $\neq 0$ and $z\cdot x=z\cdot y$ then $x=y$.
2. Theorem 9.6 (multiplicative inverses are unique): If $z\cdot x=1$ and $z\cdot y=1$ then $x=y$.
3. Theorem 9.10 (alternate additive inverse): $-x=-1\cdot x$
4. Theorem 9.18 (adding inequalities):If $w\lt y$ and $x\lt z$ then $w+x\lt y+z$.
5. Theorem 9.23 (scaling by a negative): If $z\lt 0$ and $x\lt y$ then $z\cdot y\lt z\cdot x$.
6. Theorem (between): There exists a real number strictly between 0 and 1, i.e., $\exists r.0\lt r \text{ and }r\lt 1$.

Assignment #18Elementary Set Theory

1. Theorem 10.5 (double negative): $\left(A'\right)'=A$
2. Theorem 10.32 (always in the power set): $\{~~\}\in \mathscr{P}(A)$
3. Theorem 10.34. (power sets of subsets): If $A\subseteq B$ then $\mathscr{P}(A)\subset\mathscr{P}(B)$.
4. Theorem 10.38 (relative complement is not associative): If $x\in A$, $x\in B$, and $x\in C$ then $(A\setminus B)\setminus C\neq A\setminus (B\setminus C)$.
5. Theorem 10.7 (a set of sets): $\{\,1,2\,\}\in\left\{\,Y:\{\,1\,\}\subseteq Y\right\}$

Assignment #19Elementary Set Theory

1. Theorem 10.23(b) (∩ distributes over ∪):$ A \cap (B \cup C) \subseteq (A \cap B) \cup (A \cap C)$
2. Theorem 10.37 (subsets are contagious):If $A \subseteq C$ and $B\subseteq D$ then $A\times B\subset C\times D$.
3. Theorem 10.31 (not a subset):$A \nsubseteq B$ if and only if $\exists x.x \in A \cap B'$
4. Theorem 10.27 (Baby DeMorgan):$A \setminus (B \cap C) = (A \setminus B) \cup (A \setminus C)$
5. Theorem 10.29 (Papa DeMorgan): $\displaystyle\left(\bigcap_{i \in I} A_i\right)' = \bigcup_{j\in I} A_j'$

Assignment #20Functions and Composition

1. Theorem 10.41 (composition is associative): If $h\colon A \to B$, $g\colon B \to C$, $f\colon C \to D$ then $$f\circ(g\circ h)=(f\circ g)\circ h.$$
2. Theorem 10.53 (a) (identity maps are injective):The map $\mathrm{id}_A$ is injective.
3. Theorem 10.53 (b) (identity maps are surjective):The map $\mathrm{id}_A$ is surjective.
4. Theorem 10.46 (image of subsets):If $f\colon A \to B$, $S \subseteq T$, and $T \subseteq A$ then $f(S)\subseteq f(T)$.

Assignment #21Functions and Composition

1. Theorem 10.43 (a linear bijection):If If $f\colon \mathbb{R} \to \mathbb{R}$ and $\forall x.f(x)=3\cdot x+1$ then $f$ is bijective.
2. Theorem (inverse images respect intersection):If $f\colon A \to B$, $S \subseteq B$, $T \subseteq B$ then $$f^\mathrm{inv}(S \cap T)=f^\mathrm{inv}(S) \cap f^\mathrm{inv}(T)$$
3. Theorem (inverse functions are bijective):If $f\colon A \to B$ and $f$ is bijective then $f^{-1}$ is bijective.
4. Theorem 10.52 (inverse of a composition):If $f\colon A \to B$, $g\colon B \to C$, $f$ is bijective, and $g$ is bijective then $$(g \circ f)^{-1} = f^{-1} \circ g^{-1}$$

Assignment #22Equivalence relations and Partial orders

1. Theorem (integer associates)Define $\sim$ to be the relation on $\mathbb{Z}$ such that for all $x,y\in \mathbb{Z}$, $$x\sim y\text{ if and only if }y=x\text{ or }y=−x$$ Then $\sim$ is an equivalence relation.
2. Theorem ($\subseteq$ is a partial order)Let $A$ be a set and suppose $\sim$ is a relation on $\mathscr{P}(A)$ such that for all $S,T\in\mathscr{P}(A)$ $$S\sim T\text{ if and only if }S\subseteq T$$ Then $\sim$ is a partial order.

Assignment #23Equivalence relations and Partial orders

1. Theorem 10.65Congruence mod $m$ is an equivalence relation on the set of integers.
2. Theorem 10.66 (class representatives): Every integer $a$ is congruent mod $m$ to a unique natural number that is less than $m$, i.e., $\exists r.a \underset{m}{\equiv}r\text{ and }0\leq r\text{ and }r\lt m$ and if $a \underset{m}{\equiv} s$, $0\leq s$, and $s\lt m$ and $a \underset{m}{\equiv} t$, $0\leq t$, and $t\lt m$ then $s=t$.

Assignment #24Modular arithmetic

1. Theorem 10.68 (modular addition):For any integers $a,b,c,d$, if $a \underset{m}{\equiv} b$ and $c \underset{m}{\equiv} d$ then $a+c \underset{m}{\equiv} b+d$
2. Theorem 10.69 (modular multiplication):For any integers $a,b,c,d$, if $a \underset{m}{\equiv} b$ and $c \underset{m}{\equiv} d$ then $a\cdot c \underset{m}{\equiv} b\cdot d$