Algebraic logic

There is little that is surprising to be said about the algebraic aspect of Watson. All theorems in a Watson theory are equations, implicitly universally quantified over their free variables.

We exhibit a set of formal axioms for equational logic which are supported by Watson:

reflexivity:

A = A is an axiom for any term A.

symmetry:

if A = B is a theorem, then B = A is a theorem.

transitivity:

if A = B is a theorem and B = C is a theorem, then A = C is a theorem.

We introduce notation A[T/x] for the result of substituting the term T for the free variable x in the term A. A formal analysis of substitution will be needed later when abstraction is considered.

substitution:

if A = B is a theorem, then C[A/x] = C[B/x] is a theorem.

generality:

if A = B is a theorem, then A[C/x] = B[C/x] is a theorem.

This logic of equations is familiar to all of us from high school algebra, though its formal study is not entirely trivial.

The path not taken here leads to the more usual approach to logic in which propositions rather than terms are taken as basic and propositional connectives and quantifiers are logical primitives. In Watson, the propositional connectives and quantifiers are not logical primitives: they can be defined in terms of the logical primitives of Watson (definition by cases and abstraction) or they can be introduced as user-defined primitives in a Watson theory.