A PRACTicAl Logic
It seems we now have all the ingredients for a logic with the potential to feel truly natural to use:
- A powerful set theory with Grothendieck universes embedded in simply-typed higher-order logic, as described here.
- 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.
- A way to have data abstraction within set theory. There is hope that this can be done by just adding an additional axiom.
- A way to represent formal proofs, theorems, axioms, and definitions in a more conversational style via a controlled natural language, as argued for here.
- Powerful automation as already demonstrated to be possible in projects like Isabelle/Sledgehammer.