A PRACTicAl Logic
It seems we now have all the ingredients for a logic with the potential to feel truly natural to use:
  1. A powerful set theory with Grothendieck universes embedded in simply-typed higher-order logic, as described here.
  2. A way to deal with undefinedness. This can be done as part of the simply-typed higher-order logic as described here, and will then also be available for the embedded set theory.
  3. A way to have data abstraction within set theory. There is hope that this can be done by just adding an additional axiom.
  4. A way to represent formal proofs, theorems, axioms, and definitions in a more conversational style via a controlled natural language, as argued for here.
  5. Powerful automation as already demonstrated to be possible in projects like Isabelle/Sledgehammer.
Let’s make set theory great again!
Stay tuned.