Hostname: page-component-78c5997874-ndw9j Total loading time: 0 Render date: 2024-11-19T06:56:20.529Z Has data issue: false hasContentIssue false

Whither relevant arithmetic?

Published online by Cambridge University Press:  12 March 2014

Harvey Friedman
Affiliation:
Department of Mathematics, Ohio State University, Columbus, Ohio 43210
Robert K. Meyer
Affiliation:
Department of Mathematics, Ohio State University, Columbus, Ohio 43210

Abstract

Based on the relevant logic R, the system R# was proposed as a relevant Peano arithmetic. R# has many nice properties: the most conspicuous theorems of classical Peano arithmetic PA are readily provable therein; it is readily and effectively shown to be nontrivial; it incorporates both intuitionist and classical proof methods. But it is shown here that R# is properly weaker than PA, in the sense that there is a strictly positive theorem QRF of PA which is unprovable in R#. The reason is interesting: if PA is slightly weakened to a subtheory P+, it admits the complex ring C as a model; thus QRF is chosen to be a theorem of PA but false in C. Inasmuch as all strictly positive theorems of R# are already theorems of P+, this nonconservativity result shows that QRF is also a nontheorem of R#. As a consequence, Ackermann's rule γ is inadmissible in R#. Accordingly, an extension of R# which retains its good features is desired. The system R##, got by adding an omega-rule, is such an extension. Central question: is there an effectively axiomatizable system intermediate between R# and R#, which does formalize arithmetic on relevant principles, but also admits γ in a natural way?

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1992

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Thistlewaite, P. B., McRobbie, M. A. and Meyer, R. K., Automated theorem-proving in non-classical logics, Pitman, London, 1988.Google Scholar
[2]Kripke, S. A., The problem of entailment, this Journal, vol. 24 (1959), p. 324. (Abstract)Google Scholar
[3]McRobbie, M. A., Meyer, R. K. and Thistlewaite, P. B., Towards efficient “knowledge-based” automated theorem proving for non-standard logics, Proceedings of the ninth international conference on automated deduction, Lecture Notes in Computer Science, vol. 310, Springer-Verlag, Berlin, 1988, pp. 197217.CrossRefGoogle Scholar
[4]Meyer, R. K., Relevant arithmetic, Polish Academy of Sciences, Institute of Philosophy and Bulletin of the Section of Logic, vol. 5 (1976), pp. 133137.Google Scholar
[5]Kleene, S. C., Introduction to metamathematics, Van Nostrand, Princeton, New Jersey, 1952.Google Scholar
[6]Meyer, R. K., The consistency of arithmetic, typescript, 1975.Google Scholar
[7]Meyer, R. K. and Urbas, I., Conservative extension in relevant arithmetic, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 32 (1986), pp. 4550.CrossRefGoogle Scholar
[8]Friedman, H., typescript, 1988.Google Scholar
[9]Tarski, A., A decision method for elementary algebra and geometry, 2nd ed., University of California Press, Berkeley, California, 1951.CrossRefGoogle Scholar