The Definitional View of Atomic Systems in Proof-Theoretic Semantics

Abstract

Atomic systems, that is, sets of rules containing only atomic formulas, play an important role in proof-theoretic notions of logical validity. We consider a view of atomic systems as definitions that allows us to discuss a proposal made by Prawitz (2016, DOI: 10.1007/978-3-319-22686-6_2). The implementation of this view in the base case of an inductive definition of validity leads to the problem that derivability of atomic formulas in an atomic system does not coincide with the validity of these formulas. This is due to the fact that, on the definitional view of atomic systems, there are not just production rules, but both introduction and elimination rules for atoms, which may even generate non-normalizable atomic derivations. This shows that the way atomic systems are handled is a fundamental issue of proof-theoretic semantics.