Technical Report TR-ARP-2-96

Abstract

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 6= 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 signi cant success for automated reasoning.

Download options

PhilArchive



    Upload a copy of this work     Papers currently archived: 72,879

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

Analytics

Added to PP
2010-12-22

Downloads
38 (#303,486)

6 months
1 (#386,016)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Greg Restall
University of Melbourne

References found in this work

No references found.

Add more references

Citations of this work

No citations found.

Add more citations