Linear Arithmetic Desecsed

(with John K. Slaney and Robert K. Meyer) “Linear Arithmetic Desecsed,” Logique et Analyse, 39 (1996) 379-388 (published in 1998).

In classical and intuitionistic arithmetics, any formula implies a true equation, and a false equation implies anything. In weaker logics fewer implications hold. In this paper we rehearse known results about the relevant arithmetic R#, and we show that in linear arithmetic LL# by contrast false equations never imply true ones. As a result, linear arithmetic is desecsed. A formula A which entails 0=0 is a secondary equation; one entailed by 0≠0 is a secondary unequation. A system of formal arithmetic is secsed if every extensional formula is either a secondary equation or a secondary unequation. We are indebted to the program MaGIC for the simple countermodel SZ7, on which 0=1 is not a secondary formula. This is a small but significant success for automated reasoning.