Symmetric logic of proofs

Abstract

The Logic of Proofs LP captures the invariant propositional properties of proof predicates t is a proof of F with a set of operations on proofs sufficient for realizing the whole modal logic S4 and hence the intuitionistic logic IPC. Some intuitive properties of proofs, however, are not invariant and hence not present in LP. For example, the choice function '+' in LP, which is specified by the condition s:Fvt:F→(s∈+∈t):F, is not necessarily symmetric. In this paper, we introduce an extension of the Logic of Proofs, SLP, which incorporates natural properties of the standard proof predicate in Peano Arithmetic: t is a code of a derivation containing F, including the symmetry of Choice. We show that SLP produces Brouwer-Heyting-Kolmogorov proofs with a rich structure, which can be useful for applications in epistemic logic and other areas. © 2008 Springer-Verlag Berlin Heidelberg.