Weak logic is a partial logic developed by Olaf Owe for program verification and specification. This paper extends Owe’s work on weak logic by presenting a sound and complete Gentzen-style proof system, a cut elimination theorem, interpolation theorems, a resolution-based proof method, and a procedure for translating weak logic into first-order logic. Holden uses one of the interpolation theorems to prove that if a formula’s validity on one level of abstraction implies its validity on a less abstract level, then the formula is of a certain type. (Owe has previously proved the converse.)

The paper does not give much intuition for weak logic, which is unfortunate since the primary source referenced is a technical report. Some properties of weak logic that emerge are that p ∨ ⌝ p is not valid, that p → q is true if q is undefined, and that a = a is false if a is undefined. None of these properties are forced on the logic simply by the presence of nondenoting terms, and one wonders why a formalism with these particular properties was chosen. The author also does not explain why, for example, the predicate in is introduced. It seems that the assertion in(e), which expresses the fact that e denotes some object, could be expressed as ( ∃ x ) x = e.