A BASIC FORMAL EQUATIONAL PREDICATE LOGIC { PART II
George Tourlakis · 2000
We continue our exploration of the \Basic Formal Equational Predicate Logic of Part I. Section numbering is consecutive to that of Part I. We show that a strong o-capture Leibniz, and a weak \full-capture version are derived rules (both access the interior of quantifler scopes). We derive general rules MON (monotonicity) and AMON (antimonotonicity) that are \as strong as possible for our logic. Finally, we show that our logic is sound and complete. The bibliography at the end applies to Part II only.