TheLogic LP

We begin by recalling some of the machinery from Chapter 2, beginning with the Logic of Proofs, LP, itself. The language for the Logic of Proofs contains:

• the language of classical propositional logic, which includes propositional variables, propositional constant ?, and Boolean connectives

• proof variables x₀, xι,..., proof constants α₀, a_n,...

• function symbols: monadic !, binary ■ and +

• operator symbol of the type “term : formula.”

Terms are defined by the grammar

We call these terms proof polynomials and denote them by p, r, s.... Constants

100

It should be noticed that the Curry-Howard isomorphism covers only a sim­ple instance of the internalization property when all of G₁,..., G_n, F are purely propositional formulas without proof terms.

Corollary 6.3 (Necessitation rule for LP)for some

ground proof polynomial p.

6.2