Initial code commit

Formalizes 1.1.-1.1.4 and the axioms and definitions in sections 1.2
and 1.3.