split the axioms into conservative and axiomatic extensions

the tentative plan is to prove another theorem about the inference
system that says there is always a model for the conservative extensions
if there is a model for the axiomatic extensions. this should probably
enable the overall consistency proof.
define bool_ctxt: all the definitions and extensions up to INFINITY_AX