The modal logic of Reverse Mathematics
Document Type
Article
Publication Date
1-2015
Abstract
The implication relationship between subsystems in Reverse Mathematics has an underlying logic, which can be used to deduce certain new Reverse Mathematics results from existing ones in a routine way. We use techniques of modal logic to formalize the logic of Reverse Mathematics into a system that we name s-logic. We argue that s-logic captures precisely the "logical" content of the implication and nonimplication relations between subsystems in Reverse Mathematics. We present a sound, complete, decidable, and compact tableau-style deductive system for s-logic, and explore in detail two fragments that are particularly relevant to Reverse Mathematics practice and automated theorem proving of Reverse Mathematics results.
Recommended Citation
Mummert, C., Saadaoui, A. & Sovine, S. The modal logic of Reverse Mathematics. Arch. Math. Logic 54, 425–437 (2015). https://doi.org/10.1007/s00153-015-0417-z
Comments
This is the author's manuscript. The published version of record is available from the publisher at https://doi.org/10.1007/s00153-015-0417-z. Copyright © 2015 Taylor & Francis. All rights reserved.