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.

There is a lot to do, and only so much (unpaid for) time. For now, follow me on obua.com! Practal related stuff will show up there eventually 😎.