(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.
I’m Greg Restall, and this is my personal website. I teach philosophy and logic as Professor of Philosophy at the University of Melbourne. ¶ Start at the home page of this site—a compendium of recent additions around here—and go from there to learn more about who I am and what I do. ¶ This is my personal site on the web. Nothing here is in any way endorsed by the University of Melbourne.