Free Variables in Proofs
given a natural parameter x = n, formula A(n) is provable.
On the other hand, FOS4 cannot directly express the notion
formula A(x) with a free variable x is provable.
In FOLP, there are tools for representing both of the aforementioned readings of individual variables: as global parameters or local variables not accessible from outside the proof/provability operator. Suppose p is interpreted as a specific proof (in PA) and A as a specific formula (of PA) with a free variable x. We can read p:A in two ways:
In the language FOLP, the proof predicate is represented by formulas of the form
where X is a finite set of individual variables that are interpreted as global parameters, free in t:XA. All free variables of A, which are not in X are considered local and are not free in t:XA. For example, if A(x, y) is an atomic formula, then in
variable x is global/free, and variable y is local/not free. Likewise, in p⅛yjA(x,y) both variables are free, and in p:;A(x,y), neither x nor y is free.
Proofs are represented by proof terms that do not contain individual variables.
Definition 10.1 (FOLP Language) Let L denote the first-order language with individual variables that contains a countable set of predicate symbols of any arity, without functional symbols or equality. The language of FOLP is the extension of L with special means to represent proofs and proof assertions.
Definition 10.2 (FOLP Proof Term) Proof terms are constructed as follows: 
(4) If t is a proof term, A is a formula, and X is a finite set of individual variables, then t:XA is a formula.
The free individual variable occurrences in t:XA are the free individual variable occurrences in A, provided the variables also occur in X, together with all variable occurrences in X itself.The set of free variables of a formula G is denoted by FVar(G). According to Definition 10.4,
We use the abbreviation
Definition 10.5 (Substitution) There are two types of substitutions in the language of FOLP: individual variables and proof variables.
Definition 10.6 (FOLP Axiom System) The first-order logic of proofs FOLP0 is axiomatized as follows, where A, B are formulas, s, t are terms, X is a set of individual variables, and y is an individual variable.
Axiom Schemes:
Inference Rules: 
10.2