Truth values, substitutions and abbreviations.

We define some more operations on formulas: a map computing the truth value of a closed atomic formula, another map replacing a free variable in a formula by a closed expression, another abbreviating a closed formula by a fresh predicate symbol.

Created by Mathematica  (October 17, 2006)