ProofTalk

ProofTalk extends MathTalk with the moves used to communicate proofs.

Proof moves (good):
- Direct proof (Def 3.7) — assume $P$, deduce $Q$, conclude $P \Rightarrow Q$.
- Proof by contradiction (Def 3.4) — assume $\neg P$, derive a contradiction.
- Proof by cases (Def 3.11) — split into exhaustive cases, prove each.
- Proof by exhaustion (Def 3.19) — enumerate all instances; usually only
works for very small sets.
- Contrapositive (Def 3.9) — to prove $P \Rightarrow Q$, prove $\neg Q \Rightarrow \neg P$.

Fallacies (bad):
- Proof by intimidation (Def 3.14) — "this is trivial".
- Proof by examples (Def 3.20) — verify on a few cases, claim done.
- Circular reasoning (Def 3.17) — assumes what you're trying to prove.

Proof communication (Def 3.22) — the proponent-skeptic game: the proponent
makes moves, the opponent tries to refute. A valid proof leaves the opponent
without a valid move.