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.

Stay tuned.