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.

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.

Share

COinS