Arithmetical Semantics for FOLP
Disclaimer Despite our best efforts, this section is not easy reading and may require a certain proficiency in reasoning “within” formal theories, in particular, PA, Peano arithmetic (PA has been widely used already, e.g., in Chapter 9).
Several variants of arithmetical provability semantics for FOLP were sketched in Artemov and Yavorskaya (Sidon) (2011), and a detailed exposition of all their aspects goes far beyond the scope of this book. The study of arithmetical provability semantics for FOLP, first-order S4, and first-order intuitionistic logic HPC is currently work in progress.According to the classical Gddel approach as realized for the propositional case in Chapter 9, the main idea is to interpret FOLP formulas as arithmetical formulas, proof terms as proofs in PA, and proof assertions t:XF as arithmetical proof predicates t is a proof of F in PA with parameters from X.
The big difference from the propositional case, however, is the intrinsic incompleteness of the first-order logic of proofs, Section 10.4.3, which makes explorations in the first-order case an open-ended endeavor.
10.4.1 Free Variables in First-Order Derivations
The role of X in t: xF is to provide substitutional access to derivation t and formula F for all variables from X, in a sense, to keep variables in X “global,” i.e., open for substitution in t:XF. Other free variables in t and F are treated as “local”: They are syntactic objects serving their purposes but not available for substitutions in t:XF. This idea is implemented in the corresponding definitions below.
We assume the following convention about free occurrences of variables in derivations. By a PA-proof d of arithmetic formulas F1, F2,..., Fn, we mean a finite collection of tree-like PA-derivations of formulas Fi,s for every i.
Free variables in these F1, F2,..., Fn are called free variables ofd. We assume that if x is free in a proof d of F and b is a term then d(b∕x) is a proof of F(b∕x) (with the natural renaming of bound variables if necessary).Let X be a finite set of individual variables, which we call “global variables,” and let d be a PA-proof. We write d(X) to reflect the fact that free variables in d that are from X are marked as global and other free variables in d as local.
10.4.2 Basic Semantics: Derivations from Hypotheses in PA
The intended interpretation of t:XF is:
t(X) is a proof of F(X).
There are different ways to interpret t:XF as a proof assertion in Peano arithmetic. The most straightforward approach would be to read t as a PA-derivation of F with variables from X accessible for substitution in both. The soundness
In this section, we will model t: xF by derivations from hypotheses. So, t will be interpreted as a derivation of F from hypotheses in PA; without loss of generality we assume that each t has only one hypothesis Ht, or just H where H is an arithmetical formula, possibly with free variables. For technical convenience, e.g., to keep proof assertions decidable, we will limit such hypotheses to primitive recursive formulas. Furthermore, we assume that all true instances of primitive recursive formulas are axioms of PA. Therefore, for some values 
As a notational example, consider arithmetical formulas F(x, y) and G(x). A natural arithmetical term for 
in the full notation will be 
and in our simplified notation
We assume that Peano arithmetic PA contains all primitive recursive terms and their defining equalities, cf.
Smorytiski (1985). A primitive recursive formula is a formula
for some primitive recursive term f. A formula is provably primitive recursive if it is provably in PA equivalent to some primitive recursive formula. The class of provably primitive recursive formulas is closed under Boolean connectives, bounded quantifiers, and bounded μ- operator. Primitive recursive formulas constitute a decidable class: there is an algorithm, which for any given arithmetical formula decides whether this formula is primitive recursive.
Definition 10.48 A filtered derivation d is a derivation (tree) with a primitive recursive hypothesis H in PA. In particular, d may be a PA-derivation without hypotheses. A filtered proof p is a finite set of filtered derivations, p is a filtered proof of a formula F if F is the root formula of some filtered derivation occurring in p.
Comment. Due to the so-called !-completeness of PA, any instance of a primitive recursive formula H(X) is provable if true. We make the convenient assumption that all true instances of primitive recursive formulas are axioms of PA.
Proofs are sets of filtered derivations and this reflects the multiconclusion character of FOLP proof objects. Technically, we need sets to interpret the operation Lemma 10.51.
PA proves some simple combinatorial facts about filtered derivations, e.g., a filtered derivation d with hypothesis H is a PA-proof iff H is true.
Let us fix a natural multiconclusion Gddel proof predicate Proof(x, y) stating that x is the Godel number of a PA-derivation of a formula with Godel number y. By construction, Proof(x, y) is primitive recursive.
Lemma 10.49 For each filtered proof d, arithmetical formula F, and set of variables X, PA proves
Proof A representative special case of this claim is: if
holds with y being a local variable, then making y global preserves the derivation:
with a free variable y.
The proof is essentially a straightforward formalization of the property that a substitution of any y for a free variable in a derivation d of a formula F is a legitimate derivation d(y) of F(y). ?Lemma 10.50 For each filtered proof d, arithmetical formula F, and set of variables X, PA proves
Proof By external induction on the construction of d from assumptions to conclusions. Without loss of generality, assume that d is itself a filtered derivation and reason in PA. Suppose Proof(d(X), F(X)) and F is the leaf node of d. If F is an instance of a PA-axiom, then F holds. Let F be a hypothesis H. Reason in PA. By the construction of a proof predicate, Proof(d(X), F(X)) holds only if X contains all free variables of H and H(X) is true, hence H given X. All steps down derivation tree in d are made according to the derivation rules in first-order logic, which are respected by proofs in PA, hence all F’s from d hold. ?
We define natural computable operations on filtered proofs that correspond to the functional symbols of FOLP.
id="Picutre 474" class="lazyload" data-src="/files/uch_group76/uch_pgroup316/uch_uch7360/image/image474.jpg">
Proof
?
Example 10.52 In this example we illustrate how local and global parameters work in filtered proofs, and we see how the operation genx behaves in part (3) of Lemma 10.51. Let d be a filtered proof (derivation) {x = 0), where this itself is a legitimate primitive recursive hypothesis. Then the filtered proof genx(d) will consist of two filtered derivations
The formula Proof(genx(d), F) without global variables is false for any F,
(1) maps proof variables and constants to filtered arithmetical proofs,
(2) maps predicate symbols of arity n to arithmetical formulas with n free variables, and
(3) commutes with the renaming of individual variables.
the specific proof predicate Proof(x, y) and hence to a specific (Gddel) numbering of PA-axioms. In particular, the usual Gddel numbering is monotonic and the number of a formula is always greater than the number of any term that is part of it. Because the number of a proof of a formula is not less than a number of the formula, this makes all nested constructions of the type u:A(u) vacuously false. This produces scores of “identities” :u:A(u) not justified by their intended provability reading, cf. Chapter 9 in which this phenomenon was discussed for the propositional logic of proofs. We again refer to Artemov and Yavorskaya (Sidon) (2011) for approaches to mitigate this defect.