A Note on the Use of Sum in the Logic of Proofs
Roman Kuznets · BORIS (University Library Bern) · 2009
The Logic of Proofs LP, introduced by Artemov, encodes the same reasoning as the modal logic S4 using proofs explicitly present in the language. In particular, Artemov showed that three operations on proofs (application ·, positive introspection!, and sum +) are sufficient to mimic provability concealed in S4 modality. While the first two operations go back to Gödel, the exact role of + remained somewhat unclear. In particular, it was not known whether the other two operations are sufficient by themselves. We provide a positive answer to this question under a very weak restriction on the axiomatization of LP.