Please register but do not use any information you wish to keep private. (The board is not under https.) Use a fake email like (fakeemail@trash-mail.com) and do not use a password you use anywhere else.
The
Schroeder Bernstein Theorem with formal exercises in higher-order set theory.
An introduction to
higher-order set theory in Megalodon,
with a
partial proof of Schroeder Bernstein in
to be completed by the student.
You can either install
Megalodon yourself
or do the exercises online at the links below.
A few simple basic logic exercises in Megalodon:
Three parts of Megalodon exercises leading up to and including the proof of Schroeder Bernstein (after March 8 2022):
A partial formalization of Schroeder Bernstein Coq is available
here. You should be able to compare and contrast the partial Coq version with the partial Megalodon version to (1) get an idea of the difference between type theory and set theory and (2) get an initial idea of how to make definitions and prove theorems in Coq. We will say more about Coq later in the course and then ask you to complete the proof of Schroeder Bernstein in Coq. Questions about the Coq version are welcome on the discussion board.