Change "model" to "representation" in many places, as in "model of propositional logic" to "representation thereof," provably satisfying all its essential axioms and and algebraic properties. One thing we haven't done yet is to formalize and verify the property of a propositional logic formula (a "proposition") as valid, satisfiable, unsat. It takes a bit of programming. I can help with one way to do it. But then you have both a (brute force) SAT solver as well as logically formal as well as computable satisfiability, validity, and unsatisfiability predicates. Your solution should provide fully abstract notation, unlimited variables, a full set of operators and their algebraic properties, axioms for formal reasoning, and theorems ultimately derived from them. [Kevin non-stationary foundations.]

[kevinsullivan]