On proof term representation for deterministic operations on proofs
by
Vladimir Krupski
Moscow State University

The FLP-language is a propositional language with additional sort of objects - proof terms - and additional binary constructor [t]F which denotes a functional proof predicate `` t proves F''. The proof terms are built from the proof variables using the following operations on proofs: × - binary operation induced by the application of modus ponens rule and ! - unary proof checker, given a proof t of F it constructs a proof of the statement `` t proves F''.

We consider the arithmetical (PA) interpretations of FLP-language where [·](·)-constructor ranges over functional proof predicates for PA represented by \Delta₁-formulas and proof terms correspond to the programs (recursive terms) which construct the codes of proofs in the form suitable for the proof predicate (the ``call-by-name'' approach is used). This semantics was axiomatized via functional proof logic FLP which is proved to be sound and complete with respect to all functional PA-interpretations:

1. All tautologies
2. [t]F --> F,
3. [t](F --> G) --> ([s]F --> [t×s]G),
4. [t]F --> [!t][t]F,
5. [t₁]F₁ /\ ... /\ [t_n]F_n --> (G --> H) if Gc=Hc for every substitution c satisfying the conditions: t_ic=t_jc ===> F_ic=F_jc , (i, j=1, ... , n).

Rule: Modus ponens.

The FLP-formulas can be used as specifications for inference rules in PA-language: a formula Spec=(F₁ /\ ... /\ F_n --> F) specifies the rule

R={F1*, ... , Fn*|- F* | * is an interpretation }.

We prove that R is PA-admissible iff FLP |- Spec. As a consequence we get an explicit {×, !}-term representation for computable operation on proofs induced by application of PA-admissible rule R specified by Spec:

FLP|-[x1]F1 /\ ... /\ [xn]Fn --> (B --> [t]F)

where t is the proof term representing the operation and B is a formula which binds all variables in t different from x₁, ... , x_n to some proofs of FLP-axioms. This representation can be constructed effectively from the proof of Spec.

Comment. FLP is a deterministic variant of the proof logic LP introduced by S.Artemov. The presented results correspond to the functional completeness theorem for LP which gives the term representation for invariant computable operations on nondeterministic proofs, i.e. on some codes of finite sets of PA-derivations. The functionality condition on proof predicate forced by FLP makes it possible to use a similar approach in the case of operations on more primitive data structures - on codes of particular derivations.

Date received: February 21, 1999