Home

Notes

• We need to come up with a start on a table of contents. It can change, but this will let us get started with the writing.

• We agree: lots of exercises.

• We need Gabriel and Bryan to provide this functionality in VS Code:

  • try it! button: creates a folder in a hierarchy with a snippet, or open if it is already there
  • show more! button: opens a read-only file We need to come up with a general mechanism to specify where the files go.

• The emphasis will be on mathematics rather than logic; we teach students the logic only insofar as they need to do mathematics. (But is still not clear to me whether it is bad to have some general schematic identities, or to say words like "conjunction" and "quantifier".)

• Some sections should focus on basic skills: equational reasoning, proof by induction, etc. Others should be substantial mathematical examples, showing students how to use basic concepts in mathematics and how to write serious proofs.

• The current site is here

• Patrick's tutorial is here

• Kevin's Lagrange gist is here, Jeremy's follow up is here.

• Kevin's propositional exercises are here

• There are also exercises in TPIL and Logic and Proof.

• A glossary or cheat sheet like this one will be helpful.

Ideas for a table of contents

Basic skills

Maybe follow Patrick's strategy?

• equational reasoning
• inequalities (basically using lemmas, forall, and implication)
• disjunctions
• negations
• existential quantifiers

Sets, relations, and functions

Any objection to just doing the usual things? Set identities, order and equivalence relations, injective functions.

We can do something on finite sets and cardinalities (though this may mean fighting with the current mathlib).

Numbers

What goes here? Proof by induction? Primes and gcd?

Algebra

Elementary group theory?

Lattices and Galois Connections

I am not sure why Patrick is keen on this.

Topology and analysis