Symmetric Logic of Proofs
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 prope
- PDF / 437,984 Bytes
- 14 Pages / 430 x 660 pts Page_size
- 2 Downloads / 190 Views
ction
In [15], G¨ odel used the modal logic S4 to axiomatize classical provability and provide the formal provability semantics to the intuitionistic propositional logic IPC by reducing IPC to S4. The question of the provability semantics of S4 itself was left open and found its resolution in [1,2] via the Logic of Proofs LP1 which provided a complete axiomatization of the proof predicate t is a proof of F in a propositional language with a sufficiently rich system of operations on proofs. On the other hand, LP can realize every S4 derivation by recovering corresponding proof terms at every occurrence of the modality (the Realization Theorem from [1,2], cf. Theorem 1). The combination of these two features renders LP a bridge between intuitionistic logic and the realm of formal mathematical proofs in the style of Brouwer-Heyting-Kolmogorov: IPC → S4 → LP → G¨ odelian proof predicates. 1
The first (incomplete) sketch of the logic of proofs was given by G¨ odel in one of his lectures of 1938 [16]. This lecture was published only in 1995; by that time, the complete system LP for the Logic of Proofs had already been discovered and shown to provide a desired provability semantics for intuitionistic logic (cf. [1,2]).
A. Avron et al. (Eds.): Trakhtenbrot/Festschrift, LNCS 4800, pp. 58–71, 2008. c Springer-Verlag Berlin Heidelberg 2008
Symmetric Logic of Proofs
59
In this diagram, IPC → S4 denotes G¨odel’s faithful embedding of IPC into S4 [15], S4 → LP signifies the Realization Theorem which faithfully embeds S4 into LP [1,2], and LP → G¨ odelian proof predicates refers to the arithmetical soundness (and completeness) theorem ([1,2]) for the Logic of Proofs. We refer the reader to [2] and surveys [6,7] for detailed discussion of these matters.
2
LP Basics
The Logic of Proofs has three basic operations on proofs: Application ‘·’ (binary), Choice ‘+’ (binary), and Proof Checker ‘!’(unary). Proof polynomials are terms built by these operations from proof variables x, y, z, . . . and proof constants a, b, c, . . .. The formulas of LP are defined by the grammar A = S | A → A | A ∧ A | A ∨ A | ¬A | t:A where t stands for any proof polynomial and S for any sentence letter. As usual, we shorten s · t to st when convenient. The binding priority from strong to weak is !, ·, +, :, ¬, ∧, ∨,→ . In particular, t(u + v):F → tu:F ∨tv:F denotes {[t·(u + v)]:F } → {[(t·u):F ]∨[(t·v):F ]}. The postulates of the Logic of Proofs LP are 1. a fixed set of axioms for classical propositional logic with Modus Ponens as its only rule of inference, e.g., the set from [18]; 2. s:(F → G) → (t:F → (s·t):G) (Application); 3. t:F → !t:(t:F ) (Proof Checker ); 4. s:F → (s+t):F , t:F → (s+t):F (Choice); 5. t:F → F (Reflection); 6. Constant Specification Rule: If c is a proof constant and A is an axiom from 1-5, then infer c:A. LP is closed under substitutions of proof polynomials for proof variables and formulas for propositional variables, and enjoys the deduction theorem. Constant Specification CS is a set of formulas {c1 :A1 , c2 :A2 , . . .} wh
Data Loading...
