Logic of Proof and Storage Predicates

Tatiana Yavorskaya (Sidon)

Propositional logic of proofs was introduced and studed by S. Artemov in [1]. He incorporated the proof predicate “t is a proof of F” denoted by t:F in the propositional language and found the complete axiom system for the logic of proofs LP. Proofs are represented by proof terms constructed by three elementary operations on proofs that realize application, (positive) proof checking and nondeterministic choice. Artemov proved that LP is sufficient to realize the modality in the whole Gödel’s provability logic S4 (see [2]) and thus provided S4 with the intended provability reading.

We describe logic of proofs extended by the additional storage predicate [t]F with the informal reading “t knows about F”. In the intended semantics t is a reference for a text containing the information (knowledge) F. Some of the texts represent proofs. This fact is denoted by t: F. Proofs contain only valid information that is reflected via the reflexivity principle t : F ∧ [t]G → G. The presence of the storage predicate allows us to specify operations on proofs depending on the formula arguments. For example, negative proof checking that verifies whether t is a proof of F and if no then returnes the proof of ¬(t:F) depends on both t and F. In our language we can replace F by the reference for t:F

[a](t:F) ∧ ¬(t:F) → check(a):(¬t:F).

We present the complete axiom system for the logic of proof and storage predicates LPS. The obtained system is sufficient to realize S4 in such a way that the constructed realization makes sence for the arbitrary proof predicate.

1. S. Artemov, Operational modal logic. Tech. Rep. 95–29, MSI, Cornell University, 1995.

2. K. Gödel, Eine Interpretation des intuitionistischen Aussagenkalkuls, Ergebnisse Math. Kolloq., Bd. 4 (1933), S. 39-40.

Address: Department of Mathematical Logic, Faculty of Mechanics and Mathematics, Moscow State University, 119899, Moscow, RUSSIA

E-mail: tanya@lpcs.math.msu.ru