add definition of disjunction to bool_ctxt
split off context extension as a separate relation

the inference system is now dependent only on the theory (not a specific
list of updates, just the signature and the axioms) and does not update
the context. it is proved sound for an unchanging theory. a separate
relation defines the updates to a context that will be syntactically
allowed. have not proved soundness for these updates yet.