Log. Univers.


c 2015 Springer Basel
DOI 10.1007/s11787-015-0126-8 Logica Universalis

First-Order Logic and First-Order Functions

Rodrigo A. Freire

Abstract. This paper begins the study of first-order functions, which are a
generalization of truth-functions. The concepts of truth-table and systems
(and clones) of truth-functions, both introduced in propositional logic by
Post, are also generalized and studied in the quantificational setting. The
general facts about these concepts are given in the first five sections, and
constitute a “general theory” of first-order functions. The central theme
of this paper is the relation of definition among notions expressed by for-
mulas of first-order logic. We emphasize that logic is not concerned only
with the consequence relation among notions expressed by formulas. It
also attends to the relation of definition among notions, where a notion
is defined from other notions. Sections 5 and 6 deal exclusively with the
relation of definition among notions expressed by formulas of first-order
logic. In these sections, we study the systems of first-order functions,
which are the sets of first-order functions closed under definitions. Sec-
tions 7 and 8 are concerned with the relativization of first-order functions
to a class of structures. The relativization to a class of structures is a
fundamental operation which is used in order to relate the theory of first-
order functions with set theory and first-order model theory, a subject
which we have barely scratched the surface. The apparatus developed in
this paper enables us to define what is a vehicle for the foundation of clas-
sical mathematics in set theory, and, in Sect. 8, we prove that first-order
logic with one binary predicate variable is not a minimal vehicle for the
foundation of classical mathematics in set theory. Sections 9 and 10 intro-
duce further operations and ideals of first-order functions. Besides some
results on the influence of the arguments of a first-order function, a result
about definability is proved in Sect. 10.1. It is this theorem that provides
necessary and sufficient conditions for a first-order function to be in a
finitely generated ideal. In Sect. 11, this result is applied to the problem
of predicate definability in classes of structures, the problem with which
Beth’s theorem dealt in the case of elementary classes.

This paper was awarded the first Newton da Costa prize. This is a prize created in honour
of the great Brazilian logician for promoting logic in Brazil - see the details at http://www.
uni-log.org/newton-da-costa-premio.html.
 R. A. Freire Log. Univers.

Mathematics Subject Classification Primary 03B10; Secondary 03A99.

Keywords. Boolean functions, foundations of first-order logic, definability.

1. Introduction
Generally speaking, this paper is concerned with the nature and structure of
(classical) first-order logic. Of course, first-order logic is a very important log-
ical system and the general aim of this paper is to increase our understanding
of its nature. In this sense, this is a work on the foundations of first-order logic:
The technical apparatus developed here is motivated by a conceptual analysis
of first-order logic. Although some would say first-order logic is the logical
system, its textbook presentations can be annoyingly different, both from the
technical and conceptual points of view. Maybe this indicates we cannot take
the foundations of first-order logic as an unproblematic, crystallized branch of
the foundations of logic. This is the perspective adopted here. A classical and
extensionalist mathematical analysis of the foundations of first-order logic will
be presented.
We will approach first-order logic continuously with respect to the stan-
dard account of propositional logic in terms of truth-functions. In particu-
lar, we will provide a generalization of truth-functions, the first-order func-
tions that can account for the whole first-order logic. The theory of first-order
functions given in this paper can be understood as a natural development of
Fraı̈ssé’s approach to first-order logic as it is presented in his Cours de Logique
Mathématique (mainly in [3] and [4]). Although first-order logic is the only log-
ical system analyzed in this paper, the theory developed here can be adapted
to infinitary and higher-order logical systems.

2. The Concept of First-Order Function

First-order functions are the quantificational correlate of truth functions. In
order to understand the concept of first-order function, let us examine carefully
how we arrive at the concept of truth-function in propositional logic. In this
section and in Sects. 3 and 4, in order to define the quantificational correlates
of finite sequences of truth-values and of truth functions we shall take a new
look at key, basic concepts and results of first-order logic.

2.1. Propositional Value and Truth-Function

We begin with a canonical propositional signature, denoted by σ, constituted
by the set {¬, ∧, ∨} of logical connectives,1 and by the infinite sequence
P1 , P2 , . . . of propositional variables. The ordering of propositional variables
in this sequence is called alphabetical ordering. The propositional language

1 Of course, we could choose a smaller set of connectives. However, this particular set
is convenient for working with disjunctive normal forms, and these normal forms will be
important for us.
 First-Order Logic and First-Order Functions

obtained from σ, denoted by L(σ), constituted by sentences which are formed

under the rules of syntax.
The usual semantics for a propositional language such as L(σ) is given
in terms of assignments of truth-values for the propositional variables.
According to the usual semantics, it is not the case that a sentence ex-
presses a truth value, because there is no privileged assignment of truth-value.
We can understand the usual semantics in the following way: A sentence ϕ
from L(σ) expresses its truth-conditions, that is, the combinations of truth-
values for the propositional variables occurring in ϕ which obtain precisely
when ϕ is true. We say of one such combination of truth-values that it is good
for ϕ. For example, the sentence P1 ∨ P2 expresses the combinations TT, TF
and FT: The sentence P1 ∨P2 is true iff one of its three truth-conditions obtain.
According to this understanding of the usual semantics, a sentence ϕ in
2
the propositional variables P1 and P2 expresses a subset of {T, F} constituted
by those combinations of two truth-values that are good for ϕ. The character-
istic function of this set is the 2-ary truth-function expressed by ϕ. In general,
m
an m-ary truth-function is a function from {T, F} to {T, F}. Therefore, a
sentence ϕ in m propositional variables expresses, through the usual seman-
m
tics, the m-ary truth function which assigns T to the elements of {T, F} that
are good for it and F to the others.
The combination of truth-values for the variables P1 , . . . , Pm is the min-
imum we must know from an assignment of truth-values to the propositional
variables in order to determine the truth-value of ϕ, for all sentences ϕ in
the propositional variables P1 , . . . , Pm , in the following sense: If s and t are
sequences of m truth-values, we say s ≈ t if for every sentence ϕ in the propo-
sitional variables P1 , . . . , Pm , the sequence s is good for ϕ iff the sequence
t is good for ϕ. In the propositional case the relation s ≈ t is the equality
relation between sequences of m truth-values, and an equivalence class un-
der this relation is identified with a unique sequence of m truth-values. This
minimal information, the combination of truth-values for m propositional vari-
ables, which is necessary and sufficient in order to determine the truth-value
of all sentences in the variables P1 , . . . , Pm is called a propositional value for
a subsequence of P1 , P2 , . . . constituted by m propositional variables.
An m-ary truth function is a function assigning a truth-value for each
propositional values for m propositional variables.

2.2. First-Order Value and First-Order Function

As we saw above, the concept of truth-function can be obtained from the
concept of propositional value. We now pass to the quantificational case. We
begin with a canonical first-order signature, denoted by Σ, constituted by the
set {¬, ∧, ∨} of connectives, by the existential quantifier ∃, by a sequence
x1 , x2 , . . . of individual variables, and by an infinite sequence
 0 0 
P1 , P2 , . . . , P11 , P21 , . . . , P12 , P22 , . . . ,
of predicate variables, in which P10 , P20 , . . . are 0-ary predicate variables,
P11 , P21 , . . . are 1-ary predicate variables, and so forth. The 0-ary predicate
 R. A. Freire Log. Univers.

variables are identified with propositional variables. The first-order language

associated with Σ, denoted by L(Σ), is constituted by the formulas. Finite,
non-empty subsequences of the sequence of predicate variables are denoted by
S, S  , etc. Those subsequences are called signatures. We use P, R, P  , R , and
Ri , for i ∈ ω, as syntactical variables for predicate variables.
The usual semantics for a first-order language such as L(Σ) is based on
first-order structures. A first-order structure D for Σ is constituted by a domain
of individuals D, and by a sequence of predicates
 0 0 
D1 , D2 , . . . , D11 , D21 , . . . , D12 , D22 , . . . ,
in this domain, such that D10 D20 , . . . are 0-ary predicates, or truth-values,
D11 , D21 , . . . are 1-ary predicates, and so forth. The predicates Dji interpret
the corresponding predicate variables Pji . One such structure D, and a se-
quence of individuals d1 , d2 , . . ., such that the individuals di interpret the
corresponding individual variables xi , determine, according to the satisfaction
relation, a unique assignment of truth values, T or F, to the  formulas in L(Σ).
We denote by Λ the class of all structures D for Σ, and by (Λ, ω) the class
of pairs (D, d1 , d2 , . . .), in which D is in Λ and d1 , d2 , . . . is a sequence of ω
individuals in D.
Each formula ϕ in L(Σ) contains a finite number of individual variables
and predicate variables. For each structure D for the canonical signature Σ,
and each sequence of individuals d1 , d2 , . . ., the truth-value of ϕ is determined
by the individuals corresponding to the individual variables occurring free in
ϕ and by the predicates D assigns to the predicate variablesoccurring in ϕ.
If S is the subsequence of P10 , P20 , . . . , P11 , P21 , . . . , P12 , P22 , . . . constituted by
the predicate variables which occur in ϕ, and x1 , . . . , xn are the individual
variables which occur free in ϕ, then the reduct D|S of D and the finite sequence
of individuals d = d1 , . . . , dn  are enough information in order to determine
the truth-value assigned to ϕ by D and d1 , d2 , . . .. However, the complete
information contained in the reduct D|S and in the finite sequence d is far
from being a necessary condition in order to determine the truth-value of ϕ.
For example, the information given by the isomorphism class of (D|S , d) would
already be enough in order to determine the truth-value of any formula with
the same variables as ϕ, and this information still is not a necessary condition
for this determination. We  denote by Λ|S the class of structures D|S for S,
and, for each n ∈ ω, by (Λ|S , n) the class of pairs (D|S , d), in which D|S is
in Λ|S and d is an n-tuple of individuals in D|S .
If ϕ is a formula free of individual variables, then ϕ can contain only 0-
ary predicate variables and connectives. Suppose S is the sequence of m 0-ary
predicate variables, in the alphabetical ordering, which occur in ϕ. This is the
propositional case, and we know it is necessary and sufficient to have only the
truth-values in D corresponding to the 0-ary predicate variables in S in order
to determine what truth value D assigns to any formula in the same predicate
variables and free of individual variables.
Now, consider the characterization below of the notion of propositional
value for a sequence of m 0-ary predicate variables. A propositional value for
 First-Order Logic and First-Order Functions

 
a subsequence S of P10 , P20 , . . . constituted by m 0-ary predicate variables is
an equivalence class of structures for S under the following equivalence rela-
tion: A ≈0 B iff for every quantifier-free sentence ϕ with predicate variables in
S, A |= ϕ iff B |= ϕ. An equivalence class under the relation ≈0 is determined
by a sequence of truth-values. The first-order generalization of this character-
ization of propositional-value for a sequence of m 0-ary predicate variables is
immediate, and it is given in Definition 2.1 below.
Let n and q be natural numbers. Let S be a signature, that is, a finite
and non-empty sequence of predicate variables. Let A and B be S-structures,
and a and b be n-tuples in A and B, respectively. We say that the pairs (A, a)
and (B, b) are q-equivalent iff for each formula ϕ in the signature S, such that
no variable other than x1 , . . . , xn is free, and with at most q nested quantifiers,

A |= ϕ[a] iff B |= ϕ[b].

For each signature S and natural number n, we denote the corresponding

relation of q-equivalence by ≈q . The equivalence class of the pair (A, a), under
≈q , is denoted by [(A, a)]q .
Take n1 , . . . , nk  to be a strictly increasing, non-empty sequence of nat-
ural numbers, and m1 , . . . , mk  a finite sequence of natural numbers. Let S be
a signature containing, for each i ∈{1, . . . , k} , mi ni -ary predicate variables.
m1 mk
   
We say that S is a signature of type n1 , . . . , n1 , . . . , nk , . . . , nk . We say of an
 m1 mk
   
S-structure that it is a structure of type n1 , . . . , n1 , . . . , nk , . . . , nk . Notice

the class Λ|S depends only on the type of S.

Definition 2.1. A first-order value, of rank q and type

 m1 mk
   
n1 , . . . , n1 , . . . , nk , . . . , nk → n,

is an equivalence class [(A, a)]q , in which A is a structure of type

 m1 mk
   
n1 , . . . , n1 , . . . , nk , . . . , nk ,

and a is an n-tuple in A. We say that [(A, a)]q is the first-order value of rank
q of the pair (A, a).

Remark 2.2. First-order values are the quantificational correlate of finite se-
quences of truth-values, that is, of propositional values. This is an important
point: Finding out the quantificational correlate of finite sequences of truth-
values is the first task that must be completed in order to develop first-order
logic continuously with respect to the standard account of propositional logic
in terms of truth-functions.
 R. A. Freire Log. Univers.

 m1 mk
   
Let A be a structure of type n1 , . . . , n1 , . . . , nk , . . . , nk , and a an

n-tuple in A. The first-order value [(A, a)]q is an element of the quotient


(Λ|S , n)/≈q , in which S is a signature of the appropriate type, and [(A, a)]q is
the minimum information about (A, a) needed in order to determine whether
A |= ϕ[a] or not, for all formulas ϕ with predicate variables in S, such that no
variable other than x1 , . . . , xn is free, and with at most q nested quantifiers.
A formula ϕ determines a signature S, which is the sequence of predicate
variables which occur in ϕ. If the free variables of ϕ are x1 , . . . , xn , we say
that the pair (A, a) satisfies ϕ if A |= ϕ[a]. If q is the quantificational rank of
ϕ, then the first-order values [(A, a)]q such that the pair (A, a) satisfies ϕ are
the satisfaction-conditions of ϕ.
A formula of first-order logic expresses its satisfaction-conditions. The
characteristic function of the collection of all satisfaction-conditions of ϕ is the
first-order function expressed by ϕ:

Definition 2.3. A function of first-order values, or first-order function, for

short, of rank q and type
 m1 mk
   
n1 , . . . , n1 , . . . , nk , . . . , nk → n

is the function which assigns a truth-value, T or F, to each first-order value

[(A, a)]q , in which A is a structure and a is an n-tuple in A.
 m1 mk
    
Let S be a signature of type n1 , . . . , n1 , . . . , nk , . . . , nk . Since (Λ|S , n)

depends only on the type of S, a first-order function of rank q and type

 m1 mk
   
n1 , . . . , n1 , . . . , nk , . . . , nk → n


is a function from (Λ|S , n)/≈q to {T, F}.

Definition 2.4. If Q : (Λ|S , n)/≈q → {T, F} is a first-order function, in which
 m1 mk
   
S is of type n1 , . . . , n1 , . . . , nk , . . . , nk , then we say that the type

 m1 mk
   
n1 , . . . , n1 , . . . , nk , . . . , nk →n

and the rank q of Q are the classifying parameters of this function.

The classifying parameters of a first-order function play a role similar to

the role played by the number and nature of the arguments and the degree in
the theory of polynomial functions.
 First-Order Logic and First-Order Functions

 m
 
A first-order value of rank 0 and type 0, . . . , 0 → 0 is naturally iden-

tified with an m-ary propositional value. In this sense, a first-order function

 m
 
of rank 0 and type 0, . . . , 0 → 0 is simply an m-ary truth-function.


Notation 2.5. The notation Q : (Λ| , n)/ → {T, F} means Q is a first-
 Sm1 ≈q mk
   
order function of rank q and type n1 , . . . , n1 , . . . , nk , . . . , nk → n, in which
 m1 mk
   
n1 , . . . , n1 , . . . , nk , . . . , nk is the type of S.


Remark 2.6. Fix a first-order function Q : (Λ|S , n)/≈q → {T, F}, in which
S = R1 , . . . , Rm . In this case, Q is a first-order function of m arguments, rep-
resented by R1 , . . . ,Rm , and we can write Q(R1 , . . . , Rm ) if we want to make
this explicit. However, and here is an important difference with respect to the
propositional case, the sequence of predicate variables R1 , . . . , Rm  assumes
a value as a whole. Values are not assigned to each one of the variables inde-
pendent of the others. On the contrary, the admissible values for the sequence
R1 , . . . , Rm  are the first-order values [(A, a)]q , in which A is an S-structure
and a is an n-tuple in A.
Definition 2.1 is based on a characterization of propositional value ac-
cording to which one such value for a sequence of m propositional variables
is an equivalence class of sequences of m truth-values under the following
equivalence relation: s ≈ t iff, given a sequence of m propositional variables
S = R1 , . . . , Rm , for every sentence ϕ in S, s is good for ϕ iff t is good for ϕ.
Another characterization of propositional value is obtained from the character-
istic formula: a propositional value for a sequence of m propositional variables
is a sequence of truth-values good for a characteristic formula ±R1 ∧. . .∧±Rm ,
in which each propositional variable Ri is affirmed or negated according to the
prefix + or −. A formula of this kind is a state description based on R1 , . . . ,
Rm .
In the next section, we will show the first-order values to also be obtain-
able from the appropriate generalization of the characteristic formulas, and the
equivalence relations ≈q to be characterizable in purely structural terms. After
that, we will show first-order logic to be functionally complete with respect to
the first-order functions, and first-order functions to be representable by finite
and computable tables generalizing truth-tables.

3. Theorems of Fraı̈ssé and Hintikka Revisited

Consider a signature S. Recall that the first-order value of rank q of a pair
(A, a), in which A is an S-structure and a is an n-tuple in A, is the minimum
information about (A, a) one must have in order to determine for every formula
 R. A. Freire Log. Univers.

ϕ, with quantificational rank at most q and such that no variable other than
x1 , . . . , xn is free, whetherA |= ϕ[a] or not. This means a first-order value is
an element of the quotient (Λ|S , n)/≈q , in which (A, a) ≈q (B, b) iff for every
formula φ, with quantificational rank at most q and such that no variable other
than x1 , . . . , xn is free,
A |= φ[a] iff B |= φ[b].
In the propositional case, in which the classifying parameters are 0 and
 m
 
0, . . . , 0 → 0, we know ≈0 admits a structural characterization:

(A, ∅) ≈0 (B, ∅) iff the S-structures A and B contain the same sequence

of truth-values for the 0-ary predicate variables in S. This also holds in the
first-order case.
3.1. Back-and-Forth
Definition 3.1. Let A and B be S-structures. We say that r is a q-partial
isomorphism relation between (A, a) and (B, b) iff q is a natural number, a and
b are finite sequences of individuals in A and B, respectively, of the same length,
r is a binary relation, dom(r) is a finite subset of the domain of A, range(r)
is a finite subset of the domain of B, the elements of a are in dom(r), the
elements of b are in range(r), for each ai in a and each bi in b, the pair (ai , bi )
is in r and either
1. q = 0 and if P is a k-ary predicate variable in S, and P A and P B are
the corresponding predicates in A and B, respectively, and a1 , . . . , ak ∈
dom(r), b1 , . . . , bk ∈ range(r), and the pair (ai , bi ) is in r, for each i ∈
{1, . . . , k}, then
P A (a1 , . . . , ak ) iff P B (b1 , . . . , bk ),
or
2. q > 0 and the back-and-forth condition holds:
(a) (Forth) For every a in the domain of A there is a b in the domain of
B and an extension r̂ of r such that r̂ is a q − 1-partial isomorphism
relation between (A, aˆa) and (B, bˆb).
(b) (Back) For every b in the domain of B there is an a in the domain of
A and an extension r̂ of r such that r̂ is a q − 1-partial isomorphism
relation between (A, aˆa) and (B, bˆb).
Notation 3.2. We denote by r : (A, a) ≈q (B, b) the relation among r, q, a and
b defined by induction on q, with A and B as parameters, in Definition 3.1.
Definition 3.3. We say that the pairs (A, a) and (B, b) are in a q-partial iso-
morphism relation if there is an r such that r : (A, a) ≈q (B, b).
3.2. Theorem of Fraı̈ssé
Notation 3.4. The quantificational rank of a formula ϕ, denoted by rk(ϕ), is
defined by induction: If ϕ is atomic then rk(ϕ) = 0; if ϕ is ¬φ then rk(ϕ) =
rk(φ); if ϕ is either φ ∧ ψ or φ ∨ ψ then rk(ϕ) = max(rk(φ), rk(ψ)); if ϕ is ∃yφ
then rk(ϕ) = rk(φ) + 1.
 First-Order Logic and First-Order Functions

Notation 3.5. The set of free variables of a formula ϕ, denoted by f v(ϕ), is

defined by induction in the obvious manner.

Theorem 3.6. (Theorem of Fraı̈ssé, first part) If (A, a) and (B, b) are in a
q-partial isomorphism relation, then for each formula ϕ such that rk(ϕ) ≤ q
and f v(ϕ) ⊆ {x1 , . . . , xn },
A |= ϕ[a] iff B |= ϕ[b].

Proof. This part is proved by induction on the complexity of ϕ. 

We will define by induction on q a family of sets (ΓS (n, q))n∈ω and an

auxiliary family (Cq,n )n∈ω .
If q = 0, consider the finite set
C0,n = {φ1 , . . . , φm }
of all atomic formulas of the form P xi1 . . . xik , such that no variable other than
x1 , . . . , xn is free. Let ΓS (n, 0) be the set of all state descriptions based on
C0,n , that is, ΓS (n, 0) is the finite set of all conjunctions of the form
φ∗1 ∧ . . . ∧ φ∗m ,
in which φ∗i is either φi or ¬φi , for each i ∈ {1, . . . , m}.
If q > 0, then ΓS (n, q) is obtained from the finite set ΓS (n + 1, q − 1) =
{ϕ1 , . . . , ϕl } in the following way: ΓS (n, q) is the set of all state descriptions
based on the set
Cq,n = {∃xn+1 ϕ1 , . . . , ∃xn+1 ϕl } ,
that is, ΓS (n, q) is the finite set of all conjunctions of the form
(∃xn+1 ϕ1 )∗ ∧ . . . ∧ (∃xn+1 ϕl )∗ ,
in which (∃xn+1 ϕi )∗ is either ∃xn+1 ϕi or ¬∃xn+1 ϕi , for each i ∈ {1, . . . , l}.
The state descriptions ψ in ΓS (n, q) generalize the characteristic formulas
of the lines in a truth-table. These state descriptions characterize the first-order
values.

Remark 3.7. The sets in the family (ΓS (n, q))n,q∈ω are finite, and their cardi-
nalities satisfy the following recursion:
S
|ΓS (n, q + 1)| = 2|Γ (n+1,q)|
.
S
The disjunction of the formulas in Γ (n, q) is a tautology, and any two of those
formulas are incompatible.

Theorem 3.8. (Theorem of Fraı̈ssé, second part) If for every formula ϕ such
that rk(ϕ) ≤ q and f v(ϕ) ⊆ {x1 , . . . , xn },
A |= ϕ[a] iff B |= ϕ[b],
then (A, a) and (B, b) are in a q-partial isomorphism relation.
 R. A. Freire Log. Univers.

Proof. If q+n = 0, then, from the hypothesis, it follows that the empty relation
is a 0-partial isomorphism relation between A and B. Otherwise, it is enough
to prove, by induction on q, that if there is a formula ψ in ΓS (n, q) such that
A |= ψ[a] and B |= ψ[b],
then r = {(a1 , b1 ), . . . , (an , bn )} is a q-partial isomorphism relation between
(A, a) and (B, b). 
3.3. A Partial Ordering on the Set of Values
The theorem of Fraı̈ssé shows the first-order values [(A, a)]q and [(B, b)]q to be
equal iff (A, a) and (B, b) are in a q-partial isomorphism relation. Furthermore,
the theorem of Fraı̈ssé suggests a natural partial ordering relation on the set
of first-order values.
Definition 3.9. Given two S-structures A and B, we say that r is a q-partial
homomorphism relation between (A, a) and (B, b) iff q is a natural number,
a and b are finite sequences of individuals in A and B, respectively, of the
same length, r is a binary relation, dom(r) is a finite subset of the domain
of A, range(r) is a finite subset of the domain of B, the elements of a are in
dom(r), the elements of b are in range(r), for each ai in a and each bi in b,
the pair (ai , bi ) is in r and either
1. q = 0 and if P is a k-ary predicate variable in S, and P A and P B are
the corresponding predicates in A and B, respectively, and a1 , . . . , ak ∈
dom(r), b1 , . . . , bk ∈ range(r), and the pair (ai , bi ) is in r, for each i ∈
{1, . . . , k}, then
P A (a1 , . . . , ak ) implies P B (b1 , . . . , bk ),
or
2. q > 0 and the forth condition holds:
(a) (Forth) For every a in the domain of A there is a b in the domain
of B and an extension r̂ of r such that r̂ : (A, aˆa) ≈q−1 (B, bˆb).
Now, we can stipulate [(A, a)]q ≤ [(B, b)]q iff there is a q-partial homo-
morphism relation between (A, a) and (B, b). Notice this relation is transitive
and antisymmetric:
[(A, a)]q ≤ [(B, b)]q and [(B, b)]q ≤ [(C, c)]q implies [(A, a)]q ≤ [(C, c)]q ;
[(A, a)]q ≤ [(B, b)]q and [(B, b)]q ≤ [(A, a)]q implies [(A, a)]q = [(B, b)]q .
Remark 3.10. If q > 0, then [(A, a)]q ≤ [(B, b)]q iff the set of first-order values
[(A, aˆa)]q−1 obtained from [(A, a)]q is contained in the set of first-order values
[(B, bˆb)]q−1 obtained from [(B, b)]q .
The partial ordering relation [(A, a)]q ≤ [(B, b)]q can be characterized
in terms of formulas. In order to do that, recall the definition of the sets
of formulas Cq,n : The set C0,n is the set of all atomic formulas of the form
P xi1 . . . xik such that no variable other than x1 , . . . , xn is free. The set Cq+1,n
is the set of formulas ∃xn+1 φ, in which φ ∈ ΓS (n + 1, q − 1).
 First-Order Logic and First-Order Functions

Theorem 3.11. There is a q-partial homomorphism relation between (A, a) and

(B, b) iff for each formula ϕ in Cq,n ,
A |= ϕ[a] implies B |= ϕ[b].
Proof. Let r be a q-partial homomorphism relation between (A, a) and (B, b).
It is important to notice r is always a 0-partial homomorphism relation between
(A, a) and (B, b). In fact, if q = 0, then r is a 0-partial homomorphism relation;
if q > 0, then there is an extension of r which is a q − 1-partial isomorphism
relation, and it follows that r is a 0-partial isomorphism relation.
It is easy to prove by induction on the ordinal function by which the
sets Cq,n are inductively defined that the existence of a q-partial homomor-
phism relation between (A, a) and (B, b) implies that for every formula ϕ in
p≤q Cp,n ,

if A |= ϕ[a] then B |= ϕ[b]

For the converse, it is enough to prove, by induction on q, that for every
n, if for each formula ϕ in Cq,n ,
A |= ϕ[a] implies B |= ϕ[b],
then the relation r = {(a1 , b1 ), . . . , (an , bn )} is a q-partial homomorphism re-
lation between (A, a) and (B, b). 

Remark 3.12. Let p≤q Cp,n be the least set of formulas containing the set
p≤q Cp,n and is closed under disjunction and conjunction. Notice the above
result can be restated in the following way:
There is a q-partial homomorphism relation between (A, a) and (B, b) iff
for each formula ϕ in p≤q Cp,n ,
A |= ϕ[a] implies B |= ϕ[b].
3.4. Hintikka’s Normal Form Theorem
For a non-empty signature
 S, there is a correspondence between first-order
values [(A, a)]q in (Λ|S , n)/≈q and satisfiable state descriptions in ΓS (n, q),
such that each first-order value corresponds to the state description defin-
ing it. This correspondence between first-order values and state descriptions
generalizes the correspondence between finite sequences of truth-values and
characteristic formulas. The result below, Hintikka’s Normal Form Theorem,
generalizes the disjunctive normal forms of propositional logic to the quantifi-
cational setting.
Theorem 3.13. (Hintikka’s Normal Form Theorem) If ϕ is a formula such
that rk(ϕ) ≤ q and f v(ϕ) ⊆ {x1 , . . . , xn }, then ϕ is equivalent to a disjunc-
tion2 of formulas in ΓS (n, q). There is an effective procedure to find one such
disjunction, and we say that it is a normal form for ϕ in ΓS (n, q).

2 We adopt the convention that the empty disjunction is allowed. If a formula ϕ is equiva-

lent to the empty disjunction then ϕ is unsatisfiable.

 R. A. Freire Log. Univers.

Proof. Under the conditions of the statement, if ψ ∈ Γ(n, q) then

|= ∀x1 . . . ∀xn (ψ → ϕ) or |= ∀x1 . . . ∀xn (ψ → ¬ϕ),
and both occur only in case ψ is unsatisfiable.
In order to find a normal form, we can apply the following algorithm: For
each ψ ∈ ΓS (n, q),
search for a proof of ∀x1 . . . ∀xn (ψ → ϕ) and for a proof of
∀x1 . . . ∀xn (ψ → ¬ϕ).
At least one of those proofs will be found, and at the moment when one
such proof is found stop the search. If the proof given by the search is a proof
of ∀x1 . . . ∀xn (ψ → ϕ), then keep this ψ; otherwise discard ψ. At the end, we
obtain a set of ψ’s (those which were not discarded). Make the disjunction of
this set, and denote this disjunction by φ.
Now, it is easy to prove that
|= ∀x1 . . . ∀xn (ϕ ↔ φ).

Remark 3.14. If the satisfiability of the formulas ψ ∈ ΓS (n, q) were decidable,
then the validity of the formulas with quantificational rank at most q, and
such that no variable other than x1 , . . . , xn is free, would also be decidable.
In the next section we will see Hintikka’s Normal Form Theorem pro-
viding a representation of first-order functions in finite and computable tables
generalizing the representation of truth-functions in truth-tables.

4. Functional Completeness of First-Order Logic

and First-Order Tables
4.1. The Expression Relation Between Formulas and First-Order Functions
The primary relation between formulas and first-order functions is the relation
of expression.
Definition 4.1. Let ϕ be a formula such that rk(ϕ)  = q and f v(ϕ) =
{x1 , . . . , xn }, and let S be the signature of ϕ. Let Q : (Λ|S , n)/≈q → {T, F}
be a first-order function. We say that ϕ expresses Q if for each pair (A, a),
where A is an S-structure and a is an n-tuple of individuals in A,
A |= ϕ[a] iff Q([(A, a)]q ) = T.
Remark 4.2. Each formula ϕ such that f v(ϕ) = {x1 , . . . , xn } expresses a
unique first-order function. This condition on the free variables of ϕ is, of
course, not relevant: suppose φ is a formula such that f v(φ) = {y1 , . . . , yn }, in
which y1 , . . . , yn are in the alphabetical ordering. Renaming the bound indi-
vidual variables of φ, if necessary, we can assume x1 , . . . , xn have no bound
occurrences in φ. Let ϕ be the formula φy1 ...yn [x1 . . . xn ], that is, the formula
obtained from φ by replacing the free occurrences of the variables y1 , . . . , yn
 First-Order Logic and First-Order Functions

by x1 , . . . , xn . The formulas φ and ϕ express the same notion. Therefore, we

can define the first-order function expressed by φ as the one expressed by ϕ.
The first-order function Q expressed by a formula ϕ is the minimal object
which comprises exactly the satisfaction-conditions of ϕ, and such that the
classifying parameters of Q match with rk(ϕ), f v(ϕ), and the signature of ϕ.
It is very important to consider a secondary relation of expression, the weak
expression, in which the condition of matching the parameters of the formula
is weakened. In fact, the relation of weak expression will be the most useful.

Definition 4.3. Let ϕ be a formula and Q : (Λ|S , n)/≈q → {T, F} a first-order
function. We say that ϕ weakly expresses Q if f v(ϕ) ⊆ {x1 , . . . , xn }, and the
signature of ϕ is contained in S, and
A |= ϕ[a] iff Q([(A, a)]q ) = T.
If
Q: (Λ|S , n)/≈q → {T, F}
is a first-order function expressed by ϕ then ϕ weakly expresses Q. Suppose ϕ
weakly expresses Q and, furthermore, ψ is a formula with predicate variables
in the signature S, and such that no variable other than x1 , . . . , xn is free.
Under these conditions, ψ weakly expresses Q iff
|= ϕ ↔ ψ.
Consider a non-empty signature S and two natural numbers n and q.
Assume if n = q = 0, then S contains 0-ary predicate variables, and if S is
constituted by 0-ary predicate variables
 only, then n = q = 0. Under these
conditions, each first-order value in (Λ|S , n)/≈q is defined by a formula in
ΓS (n, q). Therefore, a first-order function
Q: (Λ|S , n)/≈q → {T, F} ,
which is not constant with range {F}, is expressed by the disjunction of for-
mulas in ΓS (n, q) which define the first-order values in Q−1 ({T}).
We have already remarked for each formula ϕ such that no variable other
than x1 , . . . , xn is free, for each signature S containing all predicate variables
occurring in ϕ and for each number q ≥ rk(ϕ), there is a first-order function
Q: (Λ|S , n)/≈q → {T, F} ,
such that Q is weakly expressed by ϕ. Now we give the converse:
Proposition 4.4. Functional Completeness of First-Order Logic. Every first-
order function is weakly expressed by a formula.
Proof. Let Q be a first-order function,
Q: (Λ|S , n)/≈q → {T, F} .
Assume if n = q = 0, then S contains 0-ary predicate variables, and if S
is constituted by 0-ary predicate variables only, then n = q = 0. Under these
conditions, ΓS (n, q) is non-empty and if Q is not constant with range {F},
 R. A. Freire Log. Univers.

then it is expressed by the disjunction of formulas in ΓS (n, q) which define the

first-order values in Q−1 ({T}). If Q is constant with range {F} and ψ is any
formula in ΓS (n, q), then Q is expressed by ψ ∧ ¬ψ.
If S is constituted by 0-ary
 predicate variables only, and n + q > 0,
then each first-order value in (Λ|S , n)/≈q is naturally identified with a finite
sequence of truth-values, and the first-order function Q can also be identified
with a truth-function. In this case, it is easy to see that the first-order function
Q is weakly expressed by any formula weakly expressing the associated truth-
function.
Assume S does not contain 0-ary predicate variables and n = q = 0.
Since there are no sentences with quantificational
 rank 0 in the signature S,
there is only one first-order value in (Λ|S , n)/≈q . In this case, Q is constant.
If Q is constant with range {F}, then Q is weakly expressed by a sentence
ψ ∧ ¬ψ, for some sentence ψ in the signature S. If Q is constant with range
{T}, then Q is weakly expressed by a sentence ψ ∨ ¬ψ, for some sentence ψ in
the signature S. 
4.2. First-Order Tables
Definition 4.5. Let S be a finite, non-empty signature. A first-order table of
rank q, for n individual variables and for the predicate variables in S, is a
matrix with l rows and 2 columns, in which l is the number of state descrip-
tions in ΓS (n, q).3 The first-column in the table is constituted by the state
descriptions in ΓS (n, q). The second column is constituted by the truth-values
T or F.
Definition 4.6. We say that a first-order function
Q: (Λ|S , n)/≈q → {T, F}
is represented by a first-order table of rank q, for n individual variables
 and for
predicate variables in S, if for each first-order value [(A, a)]q in (Λ|S , n)/≈q ,
Q([(A, a)]q ) = T iff the row corresponding to [(A, a)]q in the table gives T
in the second column.
4.3. Compositional Aspects of First-Order Tables
If Q is the first-order function expressed by ϕ, then the effective procedure
to find a normal form for ϕ provides a construction of a truth-table which
represents Q. In a truth-table, the truth-value for ϕ in a row can be obtained
from a composition of a series of simple computations. Now, we will sketch a
compositional construction of a first-order table representing a given first-order
function.

3 We discard the trivial case in which ΓS (n, q) is empty. Notice if m is the number of atomic
formulas of the form P xi1 . . . xik such that no variable other than x1 , . . . , xn+q is free, then
m
.2
..
l = 22
with q + 1 iterated powers. In the propositional case, q = 0 and the number of rows in a
truth-table is 2m , as is well-known.
 First-Order Logic and First-Order Functions

We say that a formula φ is elementary if φ is atomic or of the form

∃yγ. Every formula is a boolean combination of a finite number of elementary
formulas: if ϕ is a formula, then there is a variable-free sentence β, obtained
from 0-ary predicate variables by the application of connectives, such that ϕ is
obtained from β by replacing all 0-ary predicate variables by elementary for-
mulas. In this case, we say that ϕ is β(φ1 , . . . , φm ), for a variable-free sentence
β, and for some elementary formulas φ1 , . . . , φm .
It is sufficient, for our purposes, to construct, in a compositional way,
normal forms for formulas ϕ such that f v(ϕ) = {x1 , . . . , xn } and rk(ϕ) = q.
Let S be the signature of one such formula ϕ. The formula ϕ is
β(φ1 , . . . , φm ),
for a variable-free sentence β, and for some elementary formulas φ1 , . . . , φm .
Let us construct, inductively, a normal form for ϕ.
If q = 0, then the formulas φ1 , . . . , φm are atomic and such that no vari-
able other than x1 , . . . , xn is free. We can assume, without loss of generality,
every atomic formula in the signature S containing no occurrences of a variable
other than x1 , . . . , xn is one of the φ1 , . . . , φm . If we denote by d.n.f.(β) the
disjunctive normal form of β, we have
β(φ1 , . . . , φm ) ↔ d.n.f.(β)(φ1 , . . . , φm ).
It is easy to verify that d.n.f.(β)(φ1 , . . . , φm ) is a disjunction of state descrip-
tions in ΓS (n, 0).
If q > 0, then for an i ∈ {1, . . . , m}, the elementary formula φi is of the
form ∃yγi . We can assume, without loss of generality, the quantificational rank
of each one of the elementary formulas φ1 , . . . , φm is q. Therefore, for each
i ∈ {1, . . . , m}, the formula φi is of the form ∃yγi . We can assume y is xn+1 ,
and f v(γi ) = {x1 , . . . , xn , xn+1 }.
By induction hypothesis, for each i ∈ {1, . . . , m}, a normal form is avail-
able for γi , since rk(γi ) = q − 1. We denote by ψ1i ∨ . . . ∨ ψki i the normal form
for γi , in which ψji are state descriptions in ΓS (n + 1, q − 1). We have
β(∃xn+1 γ1 , . . . , ∃xn+1 γm )
is equivalent to
β(∃xn+1 (ψ11 ∨ . . . ∨ ψk11 ), . . . , ∃xn+1 (ψ1m ∨ . . . ∨ ψkmm )).
Distributing the quantifier, we conclude
β(∃xn+1 (ψ11 ∨ . . . ∨ ψk11 ), . . . , ∃xn+1 (ψ1m ∨ . . . ∨ ψkmm ))
is equivalent to
β(∃xn+1 ψ11 ∨ . . . ∨ ∃xn+1 ψk11 , . . . , ∃xn+1 ψ1m ∨ . . . ∨ ∃xn+1 ψkmm ).
The formula β(∃xn+1 ψ11 ∨. . .∨∃xn+1 ψk11 , . . . , ∃xn+1 ψ1m ∨. . .∨∃xn+1 ψkmm )
is a boolean combination of the formulas ∃xn+1 ψji :
β(∃xn+1 ψ11 ∨ . . . ∨ ∃xn+1 ψk11 , . . . , ∃xn+1 ψ1m ∨ . . . ∨ ∃xn+1 ψkmm )
 R. A. Freire Log. Univers.

is
α(∃xn+1 ψ11 , . . . , ∃xn+1 ψk11 , . . . , ∃xn+1 ψ1m , . . . , ∃xn+1 ψkmm ).
We can assume all state descriptions in the set ΓS (n + 1, q − 1) occur in
α(∃xn+1 ψ11 , . . . , ∃xn+1 ψk11 , . . . , ∃xn+1 ψ1m , . . . , ∃xn+1 ψkmm ).
If we denote the disjunctive normal form of α by d.n.f.(α), then:
β(φ1 , . . . , φm )
is equivalent to
d.n.f.(α)(∃xn+1 ψ11 , . . . , ∃xn+1 ψk11 , . . . , ∃xn+1 ψ1m , . . . , ∃xn+1 ψkmm ).
It is easy to verify that
d.n.f.(α)(∃xn+1 ψ11 , . . . , ∃xn+1 ψk11 , . . . , ∃xn+1 ψ1m , . . . , ∃xn+1 ψkmm )
is a disjunction of state descriptions in ΓS (n, q).
If ϕ expresses the first-order function Q, then the compositional con-
struction above provides a first-order table representing Q.

5. Basic Operations with First-Order Functions

Now we turn to the problem of defining first-order functions from other first-
order functions. We will introduce four basic operations with first-order func-
tions that will be relevant in the characterization the relation of definition
among first-order functions. This will give rise to the definition of the sets of
first-order functions closed under definitions. These sets are called systems of
first-order functions, and are, intuitively, the conceptual subsystems of first-
order logic.
5.1. Compositions of First-Order Functions

A first-order function Q : (Λ|S , n)/≈q → {T, F} defines an n-ary predicate4
O which assigns, for each structure A ∈ Λ|S , a set of n-tuples OA in A such
that for every n-tuple of individuals in A,
OA (a) iff Q([(A, a)]q ) = T.
We use the notation OA (a) instead of a ∈ OA .
Notation 5.1. Let S be a signature, n1 , . . . , nm a non-decreasing sequence of
natural numbers, and Q1 , . . . , Qm first-order functions,
Qi : (Λ|S , ni )/≈qi → {T, F} ,
for each i ∈ {1, . . . , m}. If A is an S-structure, then every Qi defines an ni -ary
predicate OA i in A. We can define a new structure with the same domain as
A, and such that its predicates are OA A
1 , . . . , Om . We denote this structure by
(Q1 , . . . , Qm )(A).

4 Fraı̈ssé calls these predicates Opérateurs Logiques ([3], page 118). See also [4], page 13.
 First-Order Logic and First-Order Functions

Proposition 5.2. Using Notation 5.1, if

(A, a) ≈q+max{q1 ,...,qm } (B, b),
then
((Q1 , . . . , Qm )(A), a) ≈q ((Q1 , . . . , Qm )(B), b),
for every natural number q.
Proof. It is enough to prove the following fact by induction in q: For every
q ∈ ω, for every n ∈ ω and for every n-tuples a in A and b in B, if r is the
relation {(a1 , b1 ), . . . , (an , bn )} and
r : (A, a) ≈q+max{q1 ,...,qm } (B, b),
then
r : ((Q1 , . . . , Qm )(A), a) ≈q ((Q1 , . . . , Qm )(B), b).

Remark 5.3. Using Notation 5.1, the Proposition 5.2 guarantees, given a first-
order value [(A, a)]q+max{q1 ,...,qm } , the first-order value
[((Q1 , . . . , Qm )(A), a)]q
to be well-defined.
Definition 5.4. Let S and S  be signatures, n be a natural number, n1 , . . . ,nm
a non-decreasing sequence of natural numbers,
Q: (Λ|S  , n)/≈q → {T, F}
and Q1 , . . . ,Qm first-order functions,
Qi : (Λ|S , ni )/≈qi → {T, F} ,
for each i ∈ {1, . . . , m}. Suppose S  is of the type n1 , . . . , nm . Under these
conditions, we define the composition of Q with Q1 , . . . ,Qm as the first-order
function
Q(Q1 , . . . , Qm ) : (Λ|S , n)/≈q+max{q1 ,...,qm } → {T, F}
such that
Q(Q1 , . . . , Qm )([(A, a)]q+max{q1 ,...,qm } ) = Q([((Q1 , . . . , Qm )(A), a)]q ).
Example 5.5. Let S be a signature with m predicate variables, R1 , . . . , Rm , in
alphabetical ordering, with arities n1 , . . . , nm , respectively, and i ∈ {1, . . . , m}.
We say that the first-order function
PSi : (Λ|S , ni )/≈0 → {T, F} ,
weakly expressed by Ri x1 . . . xni , is the projection in the i-th argument. More
explicitly, PSi is defined by:
PSi ([(A, (a1 , . . . , ani ))]0 ) = T iff A |= Ri x1 . . . xni [(a1 , . . . , ani )].
 R. A. Freire Log. Univers.

If Q is a first-order function,

Q: (Λ|S , n)/≈q → {T, F} ,

and PS1 , . . . , PSm are the projections, then

Q(PS1 , . . . , PSm ) = Q.

5.2. ν-Operations
Let ν : {1, . . . , n } → {1, . . . , n} be a function. For each n-tuple a of individuals
in A, we can define the n -tuple

ν ∗ (a) = (aν(1) , . . . , aν(n ) ).

Let ϕ be a formula such that f v(ϕ ) ⊆ {x1 , . . . , xn }, and such that x1 , . . . ,
xn do not occur as bound variables in ϕ . Under these conditions, we say
that ν(ϕ ) is defined and in the formula obtained from ϕ by replacing each
individual variable xi which occurs free in ϕ , for i ∈ {1, . . . , n }, by xν(i) .

Lemma 5.6. If A is an S-structure, a is an n-tuple in A,

ν : {1, . . . , n } → {1, . . . , n}

is a function, and ϕ is a formula in the signature S, such that ν(ϕ ) is defined,

then

A |= ϕ [ν ∗ (a)] iff A |= ν(ϕ )[a].

Proof. By induction on the complexity of ϕ . 

Remark 5.7. The construction of ν ∗ (a) from a and ν is such that if (A, a) ≈q
(B, b), then (A, ν ∗ (a)) ≈q (B, ν ∗ (b)). This follows from Lemma 5.6, because for
every formula ϕ , such that f v(ϕ ) ⊆ {x1 , . . . , xn } and rk(ϕ ) ≤ q, there is a
variant ϕ of ϕ , such that ν(ϕ ) is defined and

A |= ϕ [ν ∗ (a)] iff A |= ν(ϕ )[a] iff B |= ν(ϕ )[b] iff B |= ϕ [ν ∗ (b)].


Let [(A, a)]q be a first-order value in (Λ|S , n)/≈q and

ν : {1, . . . , n } → {1, . . . , n}

a function. By Remark 5.7, the first-order value [(A, ν ∗ (a))]q in (Λ|S , n )/≈q
is well-defined.

. . , n } → {1, . . . , n} be a function and Q be a first-

Definition 5.8. Let ν : {1, .
order function defined
 in (Λ|S , n )/≈q . We denote by ν∗ (Q) the first-order
function defined in (Λ|S , n)/≈q by:

ν∗ (Q)([(A, a)]q ) = Q([(A, ν ∗ (a))]q ).

 First-Order Logic and First-Order Functions

5.3. π-operations
Let S and S  be signatures and π : S  → S a function such that π(R ) is of
the same arity as R , for every R in S  . If A is an S-structure, then we can
define an S  -structure π ∗ (A) with the same domain as A and which assigns to
each predicate variable R in S  the same predicate A assigns to π(R ). If ϕ
is a formula in the signature S  , then π(ϕ ) is the formula in the signature S
obtained from ϕ by replacing each predicate variable R (from S  ) occurring
in ϕ by π(R ).
Lemma 5.9. If A is an S-structure, a is an n-tuple in A, π : S  → S is a
function such that π(R ) is of the same arity as R , and ϕ is a formula in the
signature S  and such that f v(ϕ ) ⊆ {x1 , . . . , xn }, then
π ∗ (A) |= ϕ [a] iff A |= π(ϕ )[a].
Proof. By induction on the complexity of ϕ . 

Remark 5.10. If A and B are S-structures, and a and b are n-tuples such
that (A, a) ≈q (B, b), then (π ∗ (A), a) ≈q (π ∗ (B), b). This follows from Lemma
5.9, because for every formula ϕ in the signature S  , and such that f v(ϕ ) ⊆
{x1 , . . . , xn } and rk(ϕ ) ≤ q,
π ∗ (A) |= ϕ [a] iff A |= π(ϕ )[a] iff B |= π(ϕ )[b] iff π ∗ (B) |= ϕ [b].

Therefore, if [(A, a)]q is a first-order value in (Λ|S , n)/≈q , and π : S  →
 
S is a function between signatures such that  π(R ) is of the same arity as R ,
∗
then the first-order value [(π (A), a)]q in (Λ|S  , n)/≈q is well-defined.
Definition 5.11. If S and S  are signatures, π : S  → S is a function such that
π(R ) is of the samearity as R , for every R in S  , and Q is a first-order
function defined in  (Λ|S  , n)/≈q , then we denote by π∗ (Q) the first-order
function defined in (Λ|S , n)/≈q by:
π∗ (Q)([(A, a)]q ) = Q([(π ∗ (A), a)]q ).
5.4. Raising Rank
If q and q  are natural numbers such that q ≥ q  , then any q-partial isomor-

phism relation is also a q -partial isomorphism relation. Therefore, if [(A, a)]q
is a first-order value in (Λ|S , n)/≈q , then the first-order value [(A, a)]q is
well-defined.
Definition 5.12. If q is a natural number
 greater than or equal to q  and Q
is a first-order function defined in (Λ|S , n)/≈q , then we denote by Qqq the

first-order function defined in (Λ|S , n)/≈q by:
Qqq ([(A, a)]q ) = Q([(A, a)]q ).

We say that the first-order function Qqq is obtained from Q by raising

rank.
From the partial ordering ≤ between first-order values, defined in Sect.
3.3, we can define an increasing first-order function:
 R. A. Freire Log. Univers.

Definition 5.13. A first-order function

Q: (Λ|S , n)/≈q → {T, F}
is increasing if the following condition holds for all first-order values [(A, a)]q
and [(B, b)]q , such that [(A, a)]q ≤ [(B, b)]q :
If Q([(A, a)]q ) = T then Q([(B, b)]q ) = T.

For example, the projection on the i-th argument of S, denoted by PSi ,

is, for every i less than or equal to the length of S, an increasing first-order
function. It is easy to prove that the property of being increasing is preserved
by compositions, raising rank, ν-operations and π-operations.

6. Generation of First-Order Functions

In order to determine what a conceptual subsystem of first-order logic is, it is
necessary to determine the first-order functions that, intuitively, can be defined
from a set of first-order functions. We begin by defining this, and then we will
justify our definition with Theorem 6.7 in the Sect. 6.2 below. Our definition
is based on the basic operations with first-order functions introduced in the
previous section.

6.1. Systems of First-Order Functions

Definition 6.1. Let U be a set of first-order functions.
1. We say that U is closed under compositions of first-order functions if given
first-order functions Q, Q1 , . . . , Qm such that (i) the first-order function
Q: (Λ|S  , n)/≈q → {T, F}
is in U, (ii) the first-order function Q(Q1 , . . . , Qm ) is defined in
(Λ|S , n)/≈q+max{q1 ,...,qm } ,

and (iii) the first-order function Qi is in U or is a projection PSj(i) , in the

sense defined in Example 5.5, for each i ∈ {1, . . . , m}, then the first-order
function Q(Q1 , . . . , Qm ) is in U.
2. We say that U is closed under ν-operations if given a first-order function
Q: (Λ|S , n )/≈q → {T, F} in U
and a function ν : {1, . . . , n } → {1, . . . , n}, the first-order function ν∗ (Q)
is in U.
3. We say that U is closed under π-operations if given a function π : S  → S,
such that π(R ) is of the same arity as R , for every R in S  , and a first-order
function
Q: (Λ|S  , n)/≈q → {T, F} in U,
then π∗ (Q) ∈ U.
 First-Order Logic and First-Order Functions

4. We say that U is closed under rank variations if given a first-order function

Q: (Λ|S , n)/≈q → {T, F} ,
and a natural number q, with q  ≤ q, then Qqq ∈ U iff Q ∈ U.
5. We say that U is closed under eliminations of individual arguments if the
following condition obtains: Given a first-order function
Q: (Λ|S , n)/≈q → {T, F} ,
in U, if there is a natural number p such that for all S-structures A and B,
and all n-tuples a and b in A and B, respectively, if
[(A)]p = [(B)]p ,
then
Q([(A, a)]q ) = Q([(B, b)]q ),
then the first-order function Q defined by
Q([(A)]p ) = Q([(A, a)]q ),
for each S-structure A and n-tuple a in A is in U.
The definition of system of first-order functions, that is, of closed set of
first-order functions, is pretty obvious: A set of first-order functions is closed
iff it is closed under compositions, ν-operations, π-operations, rank variations,
and by eliminations of individual arguments. If we look at first-order logic as a
mathematical structure, then the domain of this structure is the set of all first-
order functions. The systems of first-order functions are the domains of the
substructures of this structure, which means the primitive operations of this
structure are compositions, ν-operations, π-operations, rank variations, and
eliminations of individual arguments. There is also a relation on this structure,
which is the consequence relation: For instance, given first-order functions Q1 ,
. . . , Qk and Q, all defined in the same domain (Λ|S , n)/≈q , we define
{Q1 , . . . , Qk } |= Q

iff for every first-order value [(A, a)]q in (Λ|S , n)/≈q ,
if Qi ([(A, a)]q ) = T, for each i ∈ {1, . . . , k} , then Q([(A, a)]q ) = T.
We can generalize the definition of the consequence relation to account for
those situations in which Q1 , . . . , Qk and Q do not share the same domain.
In order to do that, we can make use of the basic operations and replace the
first-order functions Q1 , . . . , Qk and Q by “equivalent” first-order functions
defined in the same domain. It is important to notice if we view first-order
logic as a structure, then the consequence relation must be a relation indeed,
and not an operation: In a substructure, one can consider the consequence
relation only among first-order functions which are available in its domain.
In further developments of the theory of first-order functions and their
systems, it will be important to consider variations of the canonical signature
Σ, fixed in Sect. 2.2. The use made of the canonical structure is not, in any way,
essential. Until now, the canonical signature has played the role of the source of
 R. A. Freire Log. Univers.

predicate variables for the finite signatures S. It was convenient to have it fixed
until now, but first-order logic is not committed to a fixed source of predicate
variables. Therefore, the canonical signature Σ will not have a privileged status
in the definition of systems of first-order functions, and from now on we can
change the source of predicate variables whenever this is necessary. For our
purposes, it is sufficient to consider non-empty (finite or infinite) subsequences
of Σ as possible sources of predicate variables.
Definition 6.2. Let Σ0 be an arbitrary subsequence of the canonical signature
Σ. Let Z be a set of first-order functions
Q: (Λ|S , n)/≈q → {T, F} ,
in which S is a subsequence of Σ0 , and n and q are natural numbers. We say
that Z is a system of first-order functions in Σ0 if Z is closed under com-
positions, rank variations, eliminations of individual variables, ν-operations,
and by those π-operations induced by functions π : S  → S  which are arity-
preserving and are such that S  and S  are non-empty subsequences of Σ0 . If
there is no risk of ambiguity, we just say that Z is a system.
A set of first-order functions Z is a system iff Z = Z, with the proviso
that the closure represented by − is relative to a, possibly infinite, sequence of
predicate variables Σ0 . This means the allowed π-operations are those induced
by functions π : S  → S  which are arity-preserving and are such that S  and
S  are subsequences of Σ0 . For each Σ0 , the set of all systems of first-order
functions in Σ0 , partially ordered by set-theoretic inclusion, is, of course, a
complete lattice.
Example 6.3. First-Order Logic in an Arbitrary Signature
For each Σ0 we have the system of all first-order functions
Q: (Λ|S , n)/≈q → {T, F} ,
in which S is a subsequence of Σ0 , and n and q are natural numbers. This sys-
tem
 0 is0 the0 first-order
 logic in the signature Σ0 . If Σ0 is the sequence
P1 , P2 , P3 , . . . of all propositional variables, then the system of all first-
order functions in Σ0 is naturally identified with the set of all truth-functions.
The structure of the lattice of all systems of truth functions was described
completely by Post in [9].
Example 6.4. Positive First-Order
 Functions
A first-order function Q : (Λ|S , n)/≈q → {T, F}, is positive iff Q is preserved
by homomorphic image, that is, iff for every surjective homomorphism
h : A → B,
we have
Q([(A, a)]q ) = Q([(B, b)]q ),
in which the n-tuple b is (h(a1 ), . . . , h(an )). It is easy to check that for each
Σ0 , the set of all positive first-order functions
Q: (Λ|S , n)/≈q → {T, F} ,
 First-Order Logic and First-Order Functions

in which S is a subsequence of Σ0 , is a system.

Given a set of first-order functions C, the system generated by C is the
least set of first-order functions containing C and closed under compositions
of first-order functions, ν-operations, π-operations, rank variations and elimi-
nations of individual variables. We denote the system generated by C by C.
In order to characterize the generation of systems of first-order functions
in terms of the relation of weak expression, we need one more lemma. In
order to state this lemma, let us define the composition of formulas. Suppose
ψ, ψ1 , . . . , ψm are formulas such that (i) exactly m predicate variables occur
in ψ, and (ii) if R1 , . . . , Rm are the predicate variables occurring in ψ, in
the alphabetical ordering, then the arity of Ri is greater than or equal to the
number of free variables of ψi , and is denoted by ni , for each i ∈ {1, . . . , m}.
In this case, we say that the composition ψ(ψ1 , . . . , ψm ) is defined, in which
ψ(ψ1 , . . . , ψm ) is the formula obtained from ψ by replacing each occurrence of
Ri of the form Ri y1 . . . yni by ψi [y1 . . . yni ],5 for each i ∈ {1, . . . , m}. Notice the
formula ψ(ψ1 , . . . , ψm ), when defined, is such that f v(ψ(ψ1 , . . . , ψm )) ⊆ f v(ψ).
Lemma 6.5. Let ψ, ψ1 , . . . , ψm be formulas such that their composition
ψ(ψ1 , . . . , ψm )
is defined. Suppose f v(ψ) ⊆ {x1 , . . . , xn }, and the first-order functions Q1 ,..,
Qm are defined in
(Λ|S , n1 )/≈q1 , . . . , (Λ|S , nm )/≈qm,
respectively, in which S is a signature extending the signatures of the for-
mulas ψi , and ni is the arity of the i-th predicate variable of ψ, for each
i ∈ {1, . . . , m}. Suppose further Q1 ,.., Qm are weakly expressed by ψ1 , . . . ,
ψm , respectively. Under these conditions, if A is an S-structure and a is an
n-tuple, then
(Q1 , . . . , Qm )(A) |= ψ[a] iff A |= ψ(ψ1 , . . . , ψm )[a].
Proof. By induction on the complexity of ψ. 
6.2. Characterization of the Generation of Systems in Terms of Weak
Expression
A set C of first-order functions can be associated with a set of formulas Δ, such
that every first-order function in C is weakly expressed by an unique formula
in Δ, and, reciprocally, each formula in Δ weakly expresses a function in C. In
fact, from the proof of Proposition 4.4, a canonical Δ with this property can
be obtained.
Definition 6.6. If Δ is a set of formulas, denote by Δ the least set X of
formulas such that:
1. Δ ⊆ X;

5 We are assuming each y1 , . . . , yni is substitutable for the j-th free variable of ψi , in the
alphabetical ordering.
 R. A. Freire Log. Univers.

2. If ψ, ψ1 , . . . , ψm are formulas such that (i) ψ is in X, (ii) the formula

ψ(ψ1 , . . . , ψm ) is defined, and (iii) the formula ψi is in X or is of the form
Rx1 . . . xni , in which R is a predicate variable and ni is the arity of the
i-th predicate variable which occur in ψ, for each i ∈ {1, . . . , m}, then
ψ(ψ1 , . . . , ψm ) is in X;
3. If ψ is in X and ψ  is obtained from ψ by renaming free and bound indi-
vidual variables, then ψ  is in X;
4. If ψ is in X and ψ  is obtained from ψ by renaming predicate variables,
then ψ  is in X.
5. If ψ is in X, ψ  is logically equivalent to ψ and the signature of ψ  is the
signature of ψ, then ψ  is in X.

The set of all formulas (in Σ) is of the form Δ, in which Δ can be
defined to be the set containing (i) all atomic formulas of the form P1n x1 . . . xn ,
in which P1n is the first n-ary predicate variable and x1 , . . . , xn are the n first
individual variables, for each n ∈ ω (ii) all the conjunctions, disjunctions and
negations of these atomic formulas, and (iii) all instantiations of the form
∃xi P1n x1 . . . xn , for i ∈ ω. In this sense, the construction of Δ from Δ is
a generalization of the definition of formula in the signature Σ: In Δ the
primitive predicate symbols are those given by formulas in Δ, and correspond
to the clause (i) above, and the basic logical operations, similar to existential
quantification, conjunction, disjunction and negation, are also those given by
formulas in Δ, and correspond to clauses (ii) and (iii) above.
Therefore, we can understand the construction of Δ as the construc-
tion of the language whose primitive resources, from which the formulas will
be constructed, are all in Δ. With this reading, the clause (1) in the above
definition implies, under the condition of closure under replacements of vari-
ables, the corresponding “atomic” formulas are in Δ. Similarly, given that
in a composition ψ(ψ1 , . . . , ψm ) the formula ψ plays the role of a connective
or a quantifier, clause (2) implies, under the condition of closure under re-
placements of variables, the set Δ is closed under the application of logical
operations given by formulas in Δ.
With this understanding of Δ as the language obtained with the logical
resources of Δ, the characterization contained in Theorem 6.7 below shows
that the set C of first-order functions is the set of those functions which can
be defined from C.

Theorem
 6.7. Let C be a set of first-order functions. For a first-order function
Q : (Λ|S , n)/≈q → {T,F}, the following conditions are equivalent:
1. Q is in C.
2. Q is weakly expressed by a formula in ΔC .

Proof. First part: (1) ⇒ (2).

Consider the set U of all first-order functions Q ∈ C, such that there is
a formula ϕ in ΔC  weakly expressing Q. We will prove that U satisfies the
conditions given in Definition 6.1.
 First-Order Logic and First-Order Functions

By the choice of ΔC , we know every first-order function Q belonging to

C to be in U. It remains to prove that U verifies the clauses (1) to (5) from
Definition 6.1.
(1) Consider m+ 1 first-order functions  Q, Q1 , . . . , Qm defined in the
sets (Λ|S  , n)/≈q , (Λ|S , n1 )/≈q1 , . . . , (Λ|S , nm )/≈qm , such that (i) Q is
in U, (ii) the first-order function Q(Q1 , . . . , Qm ) is defined in the set
(Λ|S , n)/≈q+max{q1 ,...,qm } ,

and (iii) the first-order function Qi is in U or is a projection PSj(i) , for each

i ∈ {1, . . . , m}.
Under these conditions, there are formulas ψ, ψ1 , . . . , ψm weakly ex-
pressing Q, Q1 , . . . , Qm , respectively, and such that ψ is in ΔC , and, for
each i ∈ {1, . . . , m}, if Qi is in U then ψi is in ΔC , and if Qi is a projection
PSj(i) then ψi is the atomic formula Rj(i) x1 . . . xni , in which Rj(i) is the j(i)-th
predicate variable in S. If Ri 1 , . . . , Ri k are the predicate variables from S 
which occur in ψ, in alphabetical ordering, then the formula ψ(ψi1 , . . . , ψik )
is defined,6 and belongs to the set ΔC . We will prove that ψ(ψi1 , . . . , ψik )
weakly expresses Q(Q1 , . . . , Qm ).
From the definition of composition,
Q(Q1 , . . . , Qm )([(A, a)]q+max{q1 ,...,qm } ) = Q([((Q1 , . . . , Qm )(A), a)]q ).
Since ψ weakly expresses Q,
Q([((Q1 , . . . , Qm )(A), a)]q ) = T iff (Q1 , . . . , Qm )(A) |= ψ[a].
Since the predicate variables from S  which occur in ψ are Ri 1 , . . . ,
Ri k ,
and (Qi1 , . . . , Qik )(A) is the reduct of (Q1 , . . . , Qm )(A) to the signature
constituted by Ri 1 , . . . , Ri k ,
(Q1 , . . . , Qm )(A) |= ψ[a] iff (Qi1 , . . . , Qik )(A) |= ψ[a].
From Lemma 6.5,
(Qi1 , . . . , Qik )(A) |= ψ[a] iff A |= ψ(ψi1 , . . . , ψik )[a],
and the result is proved. 
(2) Let Q be a first-order function defined in (Λ|S , n )/≈q , such that
Q ∈ U, and let ν : {1, . . . , n } → {1, . . . , n} be a function. From the hypothesis,
there is a formula ϕ ∈ ΔC  weakly expressing Q. We will prove that there is
a formula obtained from ϕ by renaming of free and bound individual variables
weakly expressing ν∗ (Q).
We know that
ν∗ (Q)([(A, a)]q ) = Q([(A, ν ∗ (a))]q ).
Let ϕ be a variant of ϕ such that the variables x1 , . . . , xn do not have
bound occurrences in ϕ . The formula ϕ weakly expresses Q, and, furthermore,

6 Recall that we can rename the bound variables of ψ1 , . . . , ψm within ΔC .

 R. A. Freire Log. Univers.

the replacement of free variables ν(ϕ ) is defined and belongs to ΔC . From
Lemma 5.6, using the fact that ϕ weakly expresses Q,
Q([(A, ν ∗ (a))]q ) = T iff A |= ν(ϕ )[a].
Since f v(ϕ ) ⊆ {x1 , . . . , xn }, it follows that ν(ϕ
) weakly expresses ν∗ (Q).
(3) Let Q be a first-order function defined in (Λ|S  , n)/≈q , such that
Q ∈ U, and π : S  → S is an arity-preserving function. From the hypothesis,
there is a formula ϕ ∈ ΔC  which weakly expresses Q. We will show that
the formula π(ϕ ), obtained from ϕ by renaming predicate variables, weakly
expresses π∗ (Q).
We know that
π∗ (Q)([(A, a)]q ) = Q([(π ∗ (A), a)]q ).
The formula π(ϕ ) belongs to ΔC  and, from Lemma 5.9, using the fact
that ϕ weakly expresses Q,
Q([(π ∗ (A), a)]q ) = T iff A |= π(ϕ )[a].
Since π(ϕ ) is a formula in the signature S  , it follows that π(ϕ ) weakly
expresses π∗ (Q). 
(4) Let Q be a first-order function defined in (Λ|S , n)/≈q , and q a
natural number greater than or equal to q  . If ϕ is a formula, then ϕ weakly
expresses Q iff ϕ weakly expresses Qqq . We conclude Q is in U iff Qqq is in U.
(5) Consider a first-order function
Q: (Λ|S , n)/≈q → {T, F} ,
in U, and a number p such that for all S-structures A and B, and n-tuples a
and b in A and B, respectively, if
[(A)]p = [(B)]p ,
then
Q([(A, a)]q ) = Q([(B, b)]q ).
There is a formula ϕ in ΔC  weakly expressing Q. From the hypothesis on Q,
if ϕ weakly expresses Q, then for each S-structure A, and n-tuples a and a
in A, respectively:
A |= ϕ[a] iff A |= ϕ[a ].
From this it follows that ϕ is logically equivalent to its existential (universal)
closure. In this case, the existential (universal) closure of ϕ is in ΔC  and
weakly expresses the first-order function Q defined by
Q([(A)]p ) = Q([(A, a)]q ),
for each S-structure A and n-tuple a in A. It follows that Q is in U.
Therefore, every first-order function in C is weakly expressed by a for-
mula in ΔC .
Second part: (2) ⇒ (1).
Consider the set X of formulas ϕ ∈ ΔC  which verify the following
condition: If Q is a first-order function weakly expressed by ϕ, then Q ∈ C.
 First-Order Logic and First-Order Functions

We will prove that X verifies the clauses (1) to (5) from Definition 6.6, relative
to the set ΔC .
(1) We will prove that X contains ΔC . Let ϕ be a formula in ΔC . We
need to prove that every first-order function weakly expressed by ϕ is in C.
From the definition of ΔC , ϕ is a formula ψQ , for a first-order function
Q in C,
Q : (Λ|S  , n )/≈q → {T, F} .
It follows from the definition of ψQ that the signature of ϕ is S  , and
that f v(ϕ) = {x1 , . . . , xn } or f v(ϕ) = ∅. If Q is a first-order function weakly
expressed by ϕ, in which
Q: (Λ|S , n)/≈q → {T, F} ,
then we have two cases:
Case (i): f v(ϕ) = {x1 , . . . , xn }. In this case,
f v(ϕ) = {x1 , . . . , xn } ⊆ {x1 , . . . , xn } .
We know, furthermore, that S  ⊆ S. Since C is closed under rank variations,
we can assume q = q  .
Let ν : {1, . . . , n } → {1, . . . , n} be a function such that ν|{1,...,n } is the
identity function, and π : S  → S is the inclusion function from S  to S. We
have,
π∗ (ν∗ (Q ))([(A, a)]q ) = Q ([(π ∗ (A), ν ∗ (a))]q )
= Q ([(A|S  , (a1 , . . . , an ))]q ).
Since ϕ weakly expresses both Q and Q ,
Q ([(A|S  , (a1 , . . . , an ))]q ) = T iff
A|S  |= ϕ[a1 , . . . , an ],
and
Q([(A, a)]q ) = T iff A |= ϕ[a].
However, because f v(ϕ) = {x1 , . . . , xn } and the signature of ϕ is S  , it
follows that
A|S  |= ϕ[a1 , . . . , an ] iff A |= ϕ[a].
Therefore, Q = π∗ (ν∗ (Q )) and hence Q ∈ C.
Case (ii): f v(ϕ) = ∅. In this case, S  contains 0-ary predicate variables
only. We know that S  ⊆ S. Since C is closed under rank variations, we can
assume q = q  , as usual.
Let Q be the truth-function obtained from Q by elimination of individ-
ual arguments. Let ν : ∅ → {1, . . . , n} be the empty function and π : S  → S
the inclusion of S  in S. For all S-structure A and n-tuple a,
A|S  |= ϕ iff A |= ϕ[a].
From the above equivalence, Q = π∗ (ν∗ (Q )).
 R. A. Freire Log. Univers.

We conclude ϕ is in X, and X verifies condition (1) from Definition 6.6

relative to ΔC .
(2) Now, we have to prove that if ψ, ψ1 , . . . , ψm are formulas such that
(i) ψ is in X, (ii) ψ(ψ1 , . . . , ψm ) is defined, and (iii) the formula ψi is in X or
it is of the form Rx1 . . . xni , in which R is a predicate variable, and R is ni -ary,
for each i ∈ {1, . . . , m}, then ψ(ψ1 , . . . , ψm ) is in X. Assume the hypothesis.
Consider Q , Q1 , . . . , Qm first-order functions weakly expressed by ψ, ψ1 , . . . ,
ψm , and such that Q , Q1 , . . . , Qm are defined in

(Λ|S  , n )/≈q , (Λ|S  , n1 )/≈q1 , . . . , (Λ|S  , nm )/≈qm,

respectively, in which S  is the signature of ψ(ψ1 , . . . , ψm ), the number q  is

the rank of ψ, and qi is the rank of ψi , and, furthermore, if ψi is Rx1 . . . xni
and R is the j(i)-th predicate variable in S  , then Qi is the corresponding

projection PSj(i) , for each i ∈ {1, . . . , m}.
Take Q to be a first-order function weakly expressed by ψ(ψ1 , . . . , ψm ).
We want to show that Q ∈ C. Since C is closed under rank variations, we
can assume Q is defined in
(Λ|S , n)/≈q +max(q1 ,...,qm ) ,

for some number n. Furthermore, we know that S  ⊆ S.

If xi1 , . . . , xik are the free variables of ψ(ψ1 , . . . , ψm ), then max(i1 , . . . , ik )
≤ n and max(i1 , . . . , ik ) ≤ n . Now we have two cases:
Case (i): n > 0 or n = 0. Let ν : {1, . . . , n } → {1, . . . , n} be a function
such that ν(i1 ) = i1 , . . . , ν(ik ) = ik and let π : S  → S be the inclusion.
Under these conditions,
π∗ (ν∗ (Q (Q1 , . . . , Qm )))([(A, a)]q +max(q1 ,...,qm ) )
= Q (Q1 , . . . , Qm )([(π ∗ (A), ν ∗ (a))]q +max(q1 ,...,qm ) )
= Q (Q1 , . . . , Qm )([(A|S  , (aν(1) , . . . , aν(n ) ))]q +max(q1 ,...,qm ) ).
From the definition of composition,
Q (Q1 , . . . , Qm )([(A|S  , ν ∗ (a))]q +max(q1 ,...,qm ) )
= Q ([(Q1 , . . . , Qm )(A|S  ), ν ∗ (a))]q +max(q1 ,...,qm ) ).
Since ψ expresses Q , we have
Q ([(Q1 , . . . , Qm )(A|S  ), ν ∗ (a))]q +max(q1 ,...,qm ) ) = T iff
(Q1 , . . . , Qm )(A|S  ) |= ψ[ν ∗ (a)].
From Lemma 6.5,
(Q1 , . . . , Qm )(A|S  ) |= ψ[ν ∗ (a)] iff A|S  |= ψ(ψ1 , . . . , ψm )[ν ∗ (a)].
From the definition of ν, and the fact that xi1 , . . . , xik are the free
variables of ψ(ψ1 , . . . , ψm ),
A|S  |= ψ(ψ1 , . . . , ψm )[ν ∗ (a)] iff A |= ψ(ψ1 , . . . , ψm )[a].
 First-Order Logic and First-Order Functions

From the hypothesis, ψ(ψ1 , . . . , ψm ) weakly expresses Q, and it follows

that
A |= ψ(ψ1 , . . . , ψm )[a] iff Q([(A, a)]q +max(q1 ,...,qm ) ) = T.
From the above equivalences, we conclude π∗ (ν∗ (Q (Q1 , . . . , Qm ))) = Q,
and Q ∈ C, because C is closed under compositions, ν-operations and
π-operations.
Case (ii): n = 0 and n > 0. In this case, ψ(ψ1 , . . . , ψm ) is a sen-
tence weakly expressing Q (Q1 , . . . , Qm ). Let p be the quantificational rank of
ψ(ψ1 , . . . , ψm ). It follows Q (Q1 , . . . , Qm ) is such that for all S  -structures B
and C, and n -tuples b and c in B and C, respectively, if
[(B)]p = [(C)]p ,
then

Q (Q1 , . . . , Qm )([(B, b)]q +max(q1 ,...,qm ) ) = Q (Q1 , . . . , Qm )([(C, c)]q +max(q1 ,...,qm ) ).

Therefore, the first-order function Q (Q1 , . . . , Qm ) defined by

Q (Q1 , . . . , Qm )([(B)]q +max(q1 ,...,qm ) ) = Q (Q1 , . . . , Qm )([(B, b)]q +max(q1 ,...,qm ) ),
for each S  -structure B and n -tuple b in B, is in C.
Let π : S  → S be the inclusion. The equality below is easy to check:
Q([(A)]q +max(q1 ,...,qm ) ) = π∗ (Q (Q1 , . . . , Qm ))([(A)]q +max(q1 ,...,qm ) ),
for each S-structure A. Therefore, Q ∈ C.
(3) Let ϕ be a formula obtained from a formula φ in X by renaming
free and bound individual variables. There are two basic renaming operations
for individual variables: The operation of taking variants and the operation
of replacing free individual variables. Every renaming of individual variables
can be obtained from a composition of those basic operations. It is enough,
therefore, to prove that (i) if ϕ is a variant of φ, then ϕ ∈ X, and (ii) if ϕ is
φxi1 ...xik [xj1 . . . xjk ] then ϕ ∈ X.
If ϕ is a variant of φ and Q is a first-order function weakly expressed by
ϕ, then Q is weakly expressed by φ. Since φ ∈ X, it follows that Q ∈ C.
From the definition of X, we have ϕ ∈ X.
If ϕ is obtained from φ by a replacement of free individual variables, then
ϕ is of the form φxi1 ...xik [xj1 . . . xjk ]. We can add innocuous replacements (of
the kind xi replacing xi ), if necessary, and, therefore, we can assume f v(φ) =
{xi1 , . . . , xik }. Let
Q: (Λ|S , n)/≈q → {T, F}
be a first-order function weakly expressed by ϕ. Since the signature of ϕ is
equal to the signature of φ, the signature of φ is contained in S and so we can
fix a first-order function
Q : (Λ|S , n )/≈q → {T, F}
weakly expressed by φ and such that q  is the quantificational rank of φ. We
know that Q is in C.
 R. A. Freire Log. Univers.

Since Q is weakly expressed by φ, the set {i1 , . . . , ik } is contained in

{1, . . . , n }. Similarly, the set {j1 , . . . , jk } is contained in {1, . . . , n}. Let
ν : {1, . . . , n } → {1, . . . , n}
be such that ν(i1 ) = j1 , . . . , ν(ik ) = jk .
Since C is closed under rank variations, we can assume q = q  . Un-
der these conditions, we have ν∗ (Q ) = Q. In fact, from the definition of
ν-operation,
ν∗ (Q )([(A, a)]q ) = Q ([(A, ν ∗ (a))]q ) = Q ([(A, (aν(1) , . . . , aν(n ) ))]q ).
Furthermore, from the fact that φ weakly expresses Q ,
Q([(A, (aν(1) , . . . , aν(n ) ))]q ) = T iff A |= φ[aν(1) , . . . , aν(n ) ],
and from Lemma 5.6, and the fact that ϕ is ν(φ),
A |= φ[aν(1) , . . . , aν(n ) ] iff A |= ϕ[a1 , . . . , an ].
Since Q is weakly expressed by ϕ, it follows that
ν∗ (Q )([(A, a)]q ) = T iff A |= ϕ[a1 , . . . , an ] iff Q([(A, a)]q ) = T.
Therefore, Q ∈ C, since Q is obtained from a first-order function in
C by a ν-operation. We conclude ϕ ∈ X, and X is closed under renaming of
individual variables.
(4) Suppose φ is in X and ϕ is obtained from φ by renaming predicate
variables π : S  → S̃, in which S̃ and S  are the signatures of ϕ and φ, respec-
tively. This means ϕ is π(φ). Fix Q a first-order function weakly expressed by
φ, and defined in (Λ|S  , n )/≈q . If

Q: (Λ|S , n)/≈q → {T, F}

is weakly expressed by ϕ, then S̃ ⊆ S and we can assume the codomain of π

is S. Furthermore, f v(φ) = f v(ϕ) ⊆ {x1 , . . . , xn }. Since C is closed under
rank variations, we can also assume q = q  .
Let ν : {1, . . . , n } → {1, . . . , n} be such that if xi ∈ f v(φ) then ν(i) = i.
From the definitions of the basic operations,
π∗ (ν∗ (Q ))([(A, a)]q ) = Q ([(π ∗ (A), ν ∗ (a))]q ).
Since φ weakly expresses Q ,
Q ([(π ∗ (A), ν ∗ (a))]q ) = T iff π ∗ (A) |= φ[ν ∗ (a)].
From Lemma 5.9, using the fact that ν is the identity function in the
indices of the free variables of φ,
π∗ (ν∗ (Q ))([(A, a)]q ) = T iff A |= ϕ[a],
and
π∗ (ν∗ (Q )) = Q.
Therefore, Q is in C and ϕ is in X.
 First-Order Logic and First-Order Functions

(5) Assume ψ is a formula equivalent to ψ  in X such that the signature

of ψ is the signature S  of ψ  . Let Q be a first-order function weakly expressed
by ψ such that
Q: (Λ|S , n)/≈q → {T, F} .
Let k and k  be the greatest indices of individual variables occurring in
ψ and ψ  , respectively. We know that k ≤ n and S  ⊆ S. If k  ≤ n, then ψ 
weakly expresses Q. In this case, the first-order function Q is in C.
Assume k  > n, and let Q be a first-order function weakly expressed by

ψ such that
Q : (Λ|S  , k  )/≈q → {T, F} .
As usual, we can assume q  = q. We have two cases:
Case (i): k = n = 0. The first-order function Q is weakly expressed by
the sentence ψ, and hence there is a number p ≥ q (for example, the maximum
between q and the quantificational rank of ψ) such that for all S  -structures
A and B, and k  -tuples a and b in A and B, respectively, if
[(A)]p = [(B)]p ,
then
Q ([(A, a)]q ) = Q ([(B, b)]q ).
From this it follows that the first-order function Q is defined and is in C. Let
π : S  → S be the inclusion. It is easy to check that π∗ (Q ) = Qpq . Therefore,
Q is in C.
Case (ii): n > 0. Let π : S  → S the inclusion and ν : {1, . . . , k  } →
{1, . . . , n} a function such that ν(1) = 1, . . . , ν(n) = n. Using the fact that ψ
and ψ  are equivalent, it is easy to check that π∗ (ν∗ Q ) = Q. Therefore, Q is
in C. 
Remark 6.8. The proof of the Theorem 6.7 shows that the set ΔC can be
replaced by any other set of formulas Δ satisfying the following property:
For every first-order function Q in C, and defined in (Λ|S , n)/≈q , there is a
formula ϕ in Δ with signature S weakly expressing Q, and such that f v(ϕ) =
{x1 , . . . , xn } or f v(ϕ) = ∅.

7. First-Order Values and Functions Relative to a Class

of Structures
We introduced the first-order functions as a minimal object expressed by a
formula in first-order logic. A formula ϕ, with signature S, and such that
rk(ϕ) = q and f v(ϕ) = {x1 , . . . , xn }, expresses its satisfaction-conditions, that
 values [(A, a)]q such that A |= ϕ[a]. In this sense,
is, it expresses the first-order
each first-order value in (Λ|S , n)/≈q is a possible satisfaction-condition. In
other words, all S-structures provide legitimate satisfaction-conditions. Now,
we will study the situation in which not all S-structures provide legitimate
 R. A. Freire Log. Univers.

satisfaction-conditions. This happens, for example, if we consider as legitimate

only those satisfaction-conditions of the form [(A, a)]q in which A is a model
of a given theory.
The motivation for this investigation is very clear. A formula expresses
different things depending on a background theory. For example, the sentence

∀x∀y∃z(x ∈ z ∧ y ∈ z)

expresses the pairing axiom relative to a set theory which contains the axioms
of extensionality and comprehension. However, relative to first-order logic with
equality, this sentence does not express the pairing axiom, because, in this case,
it is not equivalent to

∀x∀y∃!z∀w(w ∈ z ↔ w = x ∨ w = y).

Therefore, it makes sense to consider what a formula expresses relative

to a context. The choice of a context, or of a background theory, is nothing
more than the choice of a class K of Σ-structures contained in the class Λ of
all Σ-structures. If we assume one such context, we consider as legitimate only
those satisfaction-conditions of the form [(A, a)]q in which A is an S-structure
in K|S .
Once again, it is important to notice that the role played by the canonical
signature Σ is not, in any way, essential. The canonical signature Σ is only a
convenient source of predicate variables, and everything can be done for an
arbitrary signature. In particular, any subsequence Σ0 of Σ can replace Σ in
the role of source of predicate variables. We will use this fact in Sect. 8 below,
in which the source of predicate variables will consist in a signature with only
one 2-ary predicate variable.
Until now, we have used first-order logic without equality as the back-
ground theory. Now we will consider variations of the background theory. From
the point of view of the theory of first-order functions, a background theory
corresponds to a choice of a class K of Σ-structures, and K need not be an
elementary class. For example, first-order logic with equality can be seen as
the background theory corresponding to the class K of Σ-structures such that
the predicate variable P12 is interpreted as equality.
In order to develop a theory of first-order functions relative to a class of
structures, we need to define, first, the notion of a first-order value relative to
a class of structures:

Definition 7.1. Let K be a class contained in Λ. Consider a non-empty, strictly

increasing sequence of natural numbers n1 , . . . , nk , and a finite sequence
of natural numbers m1 , . . . , mk . Let S be a signature, containing, for each
i ∈ {1, . . . , k} , mi ni -ary predicate variables. A first-order value, of rank q and
type
 m1 mk
   
n1 , . . . , n1 , . . . , nk , . . . , nk → n
 First-Order Logic and First-Order Functions

relative to K is an equivalence class of pairs (A, a), in which A is a structure

in K|S , and a is an n-tuple in A, by the equivalence relation ≈q . We say that
[(A, a)]K
q is the first-order value of rank q relative to K of the pair (A, a).

If we denote by (K|S , n) the class of all pairs (A, a), in which A is
a structure in K|S , then a first-ordervalue of rank q and appropriate type
relative to K is simply an element of (K|S , n)/≈q .
Remark 7.2. Each first-order value contains, at most, one first-order value
relative to K. In other words, if [(A, a)]q is a first-order value then there is at
most one first-order value [(B, b)]Kq , relative to K, such that

q ⊆ [(A, a)]q .
[(B, b)]K
In this case, the first-order value [(B, b)]Kq is constituted by the pairs (C, c)
in
 [(A, a)]q such that
 C ∈ K|S . Therefore, we can naturally embed the set
(K|S , n)/≈q in (Λ|S , n)/≈q .
Let us fix K as a class contained in Λ. We know that a first-order value
[(A, a)]q is defined by a formula ψ in ΓS (n, q), in the sense that for each pair

(B, b) in (Λ|S , n),
(B, b) ∈ [(A, a)]q iff B |= ψ[b].
If A ∈ K|S , then the first-order value [(A, a)]K
q , contained in [(A, a)]q , is defined

by the same formula ψ, in the sense that for every pair (B, b) in (K|S , n),
(B, b) ∈ [(A, a)]K
q iff B |= ψ[b].


Now the definition of first-order function
m1
relative to a class of structures
mk
   
is obvious. If S is a signature of type n1 , . . . , n1 , . . . , nk , . . . , nk , then a

first-order function of rank q and type

 m1 mk
   
n1 , . . . , n1 , . . . , nk , . . . , nk →n

relative to K is a function from (K|S , n)/≈q to {T, F}.
The relativization of first-order functions to a class K can be seen as an
operation
 with first-order
 functions: from Remark 7.2, we can naturally embed
(K|S , n)/≈q in (Λ|S , n)/≈q . Therefore, a functionfrom (K|S , n)/≈q to
 from (Λ|S , n)/≈q to {T, F}.
{T, F} can be seen as the restriction of a function
If Q is a first-order function defined in the set (Λ|S , n)/≈q , we denote by Q|K
the first-order function relative
 to K which is the composition of Q with the
canonical embedding of (K|S , n)/≈q in (Λ|S , n)/≈q .
If a first-order function Q is (weakly) expressed by a formula ϕ, then Q|K
is (weakly) expressed by the same formula ϕ, in the following sense:
q ) = T iff A |= ϕ[a].
Q|K ([(A, a)]K
This follows from the fact that
Q|K ([(A, a)]K
q ) = Q([(A, a)]q ).
 R. A. Freire Log. Univers.

We also remark two formulas ϕ and ϕ can (weakly) express different first-order
functions Q and Q , such that Q|K = Q |K for some class K.
We can define basic operations with first-order functions relative to a
class of structures. In particular, we can define the operation of raising rank:

Definition 7.3. Let Q be a first-order function defined in (K|S , n)/≈q . If p is
a natural number greater than or equal to q, then we define Qpq in the following
way.
Qpq ([(A, a)]K
p ) = Q([(A, a)]q ).
K


Remark 7.4. If Q is a first-order function defined in (Λ|S , n)/≈q , and Q|K is
the relativization of Q to a class K, then
(Q|K )pq = Qpq |K ,
for every p ≥ q. In fact,
p
(Q|K )pq ([(A, a)]K
p ) = (Q|K )([(A, a)]q ) = Q([(A, a)]q ) = Qq ([(A, a)]p ),
K

for every S-structure A in K|S , and every n-tuple a in A.

In the next section we use the first-order functions relative to a class of
structures to give an important result about the relation between first-order
logic and the foundation of classical mathematics in the theory of sets.

8. First-Order Functions and the Foundation of Classical

Mathematics in the Theory of Sets
We would like do define, intuitively, the minimum of resources required of a
logical system in order for it to support the foundation of classical mathematics
in the theory of sets. We know that first-order logic with one binary predicate
variable (and without equality) is expressive enough for the task, and first-
order logic with predicate variables of arity at most one is not expressive
enough. We have to answer the following question: What are the first-order
functions that a system of first-order functions for a signature constituted by
one binary predicate variable must contain in order to support the foundation
of classical mathematics in the theory of sets?
Formal systems for the theory of sets are usually presented as interpreted
axiomatic systems: Behind one such presentation the primitive binary relation
of set theory, usually denoted by ∈, is intended to be the membership relation
between sets, and should not be considered just as an arbitrary relation satis-
fying a given list of first-order axioms. The foundational role of the theory of
sets is related to the fact that it can be presented as an interpreted axiomatic
theory, based on the membership relation.
From the claim in the previous paragraph, we conclude, for the foun-
dational purposes, that membership is not to be understood as an arbitrary
relation satisfying a list of first-order axioms, just like equality is not an ar-
bitrary relation satisfying the first-order axioms of equality. If R is a binary
predicate variable, the structures for the signature R in which R is inter-
preted as the membership relation are called ∈-structures. It is enough for a
 First-Order Logic and First-Order Functions

logical system to express all the first-order functions relative to the class of
∈-structures, that is, it is enough to contain all the first-order functions of
membership.7 This preliminary discussion motivates the following definition:
Definition 8.1. Let R be a binary predicate variable and let R be the signa-
ture constituted by R. Let Z be a system of first-order functions in R. We
say that Z is a vehicle for the foundation of mathematics if (i) it contains all
valid first-order functions, that is, all first-order functions constantly true, and
(ii) the restriction of Z to the classK of all ∈-structures contains all first-order
functions relative to K defined in (K, n)/≈q , for n + q > 0. In other words, Z
is a vehicle for the foundation of mathematics if it contains all logically valid
first-order functions and the restriction of Z to the class K of all ∈-structures
contains all first-order functions relative to K.
The first-order logic with a binary predicate variable R is not a minimal
vehicle for the foundation of mathematics. We state this as a theorem:
Theorem 8.2. There are proper subsystems of the system of all first-order func-
tions in the signature R which are vehicles for the foundation of mathematics
in the theory of sets.
Proof. Let A be a structure such that
A |= ∀x1 ∀x2 Rx1 x2 .
Let Z(A) be the set which, for all natural numbers n and q, contains all, and
only those, first-order functions
Q: (Λ|R , n)/≈q → {T, F} ,
such that Q([(A, a)]q ) = T, for all n-tuples a. We will show that Z(A) is closed
under compositions: In fact, if Q and Q1 are such that the composition Q(Q1 )
is defined, then
Q(Q1 )([(A, a)]q+q1 ) = Q([(Q1 (A), a)]q ).
Since Q1 is in Z(A), and
A |= ∀x1 ∀x2 Rx1 x2 ,
the structure Q1 (A) is A. From this it follows that
Q(Q1 )([(A, a)]q+q1 ) = Q([(A, a)]q ) = T,
for Q is in Z(A). Therefore, Z(A) is closed under compositions. It is easy to
see that Z(A) contains all valid first-order functions and is closed under ν-
operations, π-operations, rank variations and eliminations of individual argu-
ments. Furthermore, the restriction of Z(A) to the class K of all ∈-structures
contains all relevant first-order functions relative to K: In fact, A is not 1-
equivalent to any ∈-structure, and, for every a1 in A, the pair (A, a1 ) is not

7 For a related discussion and an analysis of existential import based on ∈-structures see

[5].
 R. A. Freire Log. Univers.

0-equivalent to any pair (B, b1 ), in which B is an ∈-structure. It follows that

all first-order functions
Q: (K, n)/≈q → {T, F} ,
relative to K and such that n + q > 0, can be extended to a first-order function
Q̂ : (Λ|R , n)/≈q → {T, F} ,

such that Q̂([(A, a)]q ) = T. Therefore, Z(A) is a vehicle for the foundation of
mathematics in the theory of sets. 

Remark 8.3. It is interesting to notice that the system Z(A) is closed under
conjunction and disjunction, and is not closed under negation. Furthermore,
Z(A) contains the negation of every first-order function which is outside Z(A).
Using formulas, we can understand the system above as the system of all first-
order functions weakly expressed by a formula of the form (∀x1 ∀x2 Rx1 x2 )∨(ϕ).
Of course, each valid formula ψ is equivalent to the formula (∀x1 ∀x2 Rx1 x2 ) ∨
(ψ). Furthermore, the valid formulas of the form (∀x1 ∀x2 Rx1 x2 ) ∨ (ϕ) can be
recursively generated.

9. Further Operations with First-Order Functions

9.1. Elimination of Inessential Arguments

Definition 9.1. Let Q be a first-order function defined in (Λ|S , n)/≈q , and
let R be a predicate variable in S. We say that R represents an inessential
argument in Q if, for all S-structures A and B, if A and B differ only with
respect to the interpretation of R, that is, if A|S  = B|S  , in which S  is either
the empty set or the signature obtained from S by the elimination of R, then
Q([(A, a)]q ) = Q([(B, a)]q ).
We say that R represents an essential argument in Q iff R does not represent
an inessential argument in Q.
Remark 9.2. If all predicate variables in S represent inessential arguments in
Q, then Q is constant.
Remark 9.3. A simple induction proves that for all S-structures A and B, if A
and B differ only with respect to the interpretation of the predicate variables
which represent inessential arguments in Q, that is, if A|S  = B|S  , in which
S  is either empty or the signature obtained from S by the elimination of all
predicate variables representing inessential arguments in Q, then
Q([(A, a)]q ) = Q([(B, a)]q ).
Suppose S is a signature
 and R is a predicate variable in S. If a first-
order function Q defined in (Λ|S , n)/≈q is weakly expressed by a formula
containing no occurrence of the predicate variable R, then R represents an
inessential argument in Q. Proposition 9.4 shows the converse:
 First-Order Logic and First-Order Functions

Proposition 9.4. Let Q be a non-constant first-order function defined in

(Λ|S , n)/≈q .
Under these conditions, there is a formula ϕ weakly expressing Q, and such
that only predicate variables representing essential arguments in Q occur in ϕ.
Proof. Since Q is non-constant, there is at least one predicate variable in S
representing an essential argument in Q. Let S  be the signature obtained
from S by the elimination of the predicate variables representing inessential
arguments. Let π : S  → S be the inclusion of those signatures.
There is a unique first-order function
Q : (Λ|S  , n)/≈q → {T, F} ,
such that
Q ([(π ∗ (A), a)]q ) = Q([(A, a)]q ).
Let ϕ be a formula weakly expressing Q . Since π ∗ (A) is the reduct of A

to S ,
π ∗ (A) |= ϕ[a] iff A |= ϕ[a],
and ϕ weakly expresses Q. 
It follows from the  proof of Proposition 9.4 that there is a first-order
function Q defined in (Λ|S  , n)/≈q , such that the predicate variables in S 
are those of S which represent essential arguments8 in Q, and such that Q
π∗ (Q ). In this case, we have the following definition:
Definition 9.5. Using the notation established in the proof of Proposition 9.4,
we say that a first-order function Q is obtained from Q by elimination of
inessential arguments. We denote Q by π ∗ (Q).
Theorem 9.6 below gives a characterization of the predicate variables
representing inessential arguments in a first-order function in terms of polarity:
We say that a predicate variable P occurs negatively in a formula ϕ if there is
an occurrence of P within the scope of an odd number of negations. Similarly,
we say that P occurs positively in ϕ if there is an occurrence of P within the
scope of an even number of negations. The inductive definition of “P occurs
negatively/positively in a formula ϕ” is obvious.
Theorem 9.6. Suppose Q is a non-constant first-order function,
Q: (Λ|S , n)/≈q → {T, F} ,
and P is a k-ary predicate variable in S. If there are formulas ϕ and ϕ , weakly
expressing Q, and such that P occurs only negatively in ϕ and only positively
in ϕ , then the predicate variable P represents an inessential argument in Q.
Conversely, if P is a predicate variable in S and P represents an inessential
argument in Q, then there are formulas ϕ and ϕ , weakly expressing Q, and
such that P occurs only negatively in ϕ and only positively in ϕ .

8 Recall that there is at least one predicate variable in S  .

 R. A. Freire Log. Univers.

Proof. Suppose there are formulas ϕ e ϕ , weakly expressing Q, and such that
P occurs only negatively in ϕ and only positively in ϕ . Since Q is non-constant,
there is at least one predicate variable in S occurring in both ϕ and ϕ . Since
ϕ and ϕ weakly express the same first-order function, |= ϕ ↔ ϕ , and, in
particular, |= ϕ → ϕ . From Lyndon’s interpolation Lemma ([10], pages 130
and 131), there is a formula φ without occurrences of P , and such that
|= ϕ → φ and |= φ → ϕ
Therefore, |= ϕ ↔ φ, and φ weakly expresses Q. We conclude P represents an
inessential argument in Q.
Conversely, suppose P represents an inessential argument in Q. From
Proposition 9.4, there is a formula φ, weakly expressing Q, and such that φ
contains no occurrences of P . Since φ is tautologically equivalent to
φ ∨ ((∃y1 . . . ∃yk P y1 . . . yk ) ∧ φ)and to φ ∨ ((∃y1 . . . ∃yk ¬P y1 . . . yk ) ∧ φ),
it follows that both formulas weakly express Q, and P occurs only positively
in the former and only negatively in the latter. 
9.2. Conjunction, Disjunction and Negation
We now define operations with first-order functions which correspond to the
Let Q and Q
propositional connectives conjunction, disjunction and negation. 

be first-order functions, and assume both Q and Q are defined in (Λ|S , n)/≈q .
If Q and Q are not defined in the same domain, we can use the basic oper-
ations defined in Sect. 5 to transform Q and Q into “equivalent” first-order
functions with the same domain.
• The negation operator, denoted by ¬, maps Q to the first-order function
¬Q, defined by:
¬Q([(A, a)]q ) = T iff Q([(A, a)]q ) = F.
• The conjunction operator, denoted by ∧, maps the pair Q and Q to the
first-order function Q ∧ Q , defined by:
Q ∧ Q ([(A, a)]q ) = T iff Q([(A, a)]q ) = T and Q ([(A, a)]q ) = T.
• The disjunction operator, denoted by ∨, maps the pair Q and Q to the
first-order function Q ∨ Q , defined by:
Q ∨ Q ([(A, a)]q ) = T iff Q([(A, a)]q ) = T or Q ([(A, a)]q ) = T.
Remark 9.7. If Q and Q are first-order functions defined in the same domain,
and if ϕ and ϕ are formulas weakly expressing Q and Q , respectively, then
ϕ ∧ ϕ weakly expresses Q ∧ Q , and similarly for negation and disjunction.

Definition 9.8. Let Q be a first-order function defined in (Λ|S , n)/≈q , such
that P and R are the only predicate variables in S representing essential
arguments in Q. We say that Q is ∧-decomposable if there
 is a natural number
p ≥ q and first-order functions Q1 and Q2 , defined in (Λ|S , n)/≈p , such that
P is the only predicate variable representing an essential argument in Q1 , R
is the only predicate variables representing an essential argument in Q2 , and
Qpq = Q1 ∧ Q2 . In this case, we say that Q1 ∧ Q2 is a ∧-decomposition of Q.
 First-Order Logic and First-Order Functions

Similarly, we say that Q is ∨-decomposable if there

 is a natural number
p ≥ q and first-order functions Q1 and Q2 , defined in (Λ|S , n)/≈p , such that
P is the only predicate variable representing an essential argument in Q1 , R
is the only predicate variable representing an essential argument in Q2 , and
Qpq = Q1 ∨ Q2 . In this case, we say that Q1 ∨ Q2 is a ∨-decomposition of Q.
Let Q1 ∧Q2 be a ∧-decomposition of Q. Let ϕ1 and ϕ2 be formulas weakly
expressing Q1 and Q2 , respectively, such that P is the only predicate variable
occurring in ϕ1 and R is the only predicate variable occurring in ϕ2 . Under
these conditions, the conjunction ϕ1 ∧ ϕ2 , denoted by ϕ, weakly expresses Q
and is such that:
|= (ϕ(P, R ) ∧ ϕ(P  , R)) → ϕ(P, R),
in which ϕ(P, R ) is obtained from ϕ(P, R) by renaming the predicate variable
R, and similarly for ϕ(P  , R), and P  and R are predicate variables different
from P and R, but with the same arities as P and R, respectively. An analogous
result holds for ∨-decompositions. The theorem below gives the converse, and
it is closely related to a result by Humberstone ([7], page 369):

Theorem 9.9. Let Q be a first-order function defined in (Λ|S , n)/≈q , and P
and R be the only predicate variables representing essential arguments in Q.
Let P  and R be predicate variables different from P and R, but with the same
arities as P and R, respectively. Let ϕ be a formula weakly expressing Q, and
such that P and R are the only predicate variables occurring in ϕ; in this case,
we will use the notation ϕ(P, R). Suppose ϕ(P, R ) is obtained from ϕ(P, R)
by renaming the predicate variable R, and similarly for ϕ(P  , R).
1. If |= (ϕ(P, R ) ∧ ϕ(P  , R)) → ϕ(P, R), then Q is ∧-decomposable.
2. If |= ϕ(P, R) → (ϕ(P, R ) ∨ ϕ(P  , R)), then Q is ∨-decomposable.
Proof. (1): Assume ϕ(P, R) is a formula weakly expressing Q such that
|= (ϕ(P, R ) ∧ ϕ(P  , R)) → ϕ(P, R).
We can rewrite the hypothesis:
|= ϕ(P, R ) → (ϕ(P  , R) → ϕ(P, R)).
From Craig’s interpolation Lemma ([10], pages 128 and 129), there is a formula
ϕ1 (P ) such that f v(ϕ1 ) ⊆ f v(ϕ) and
|= ϕ(P, R ) → ϕ1 (P ) and |= ϕ1 (P ) → (ϕ(P  , R) → ϕ(P, R)).
We can rewrite the last implication:
|= ϕ(P  , R) → (ϕ1 (P ) → ϕ(P, R)).
Once again, from Craig’s interpolation lemma, there is a formula ϕ2 (R) such
that f v(ϕ2 ) ⊆ f v(ϕ) and
|= ϕ(P  , R) → ϕ2 (R) and |= ϕ2 (R) → (ϕ1 (P ) → ϕ(P, R)).
From |= ϕ(P, R ) → ϕ1 (P ) and |= ϕ(P  , R) → ϕ2 (R), it follows that
|= ϕ(P, R) → ϕ1 (P ) and |= ϕ(P, R) → ϕ2 (R),
 R. A. Freire Log. Univers.

and, therefore,
|= ϕ(P, R) → (ϕ1 (P ) ∧ ϕ2 (R)).
From |= ϕ2 (R) → (ϕ1 (P ) → ϕ(P, R)), it follows that
|= (ϕ1 (P ) ∧ ϕ2 (R)) → ϕ(P, R).
Therefore, |= ϕ(P, R) ↔ (ϕ1 (P ) ∧ ϕ2 (R)), and the formula ϕ1 (P ) ∧
 weakly expresses Q. Let Q1 and Q2 be first-order functions defined
ϕ2 (R)
in (Λ|S , n)/≈p , for some p ≥ q, and weakly expressed by ϕ1 and ϕ2 , respec-
tively.9 We have
Qpq = Q1 ∧ Q2 ,
and the first part is proved.
(2): Assume ϕ(P, R) is a formula weakly expressing Q and such that
|= ϕ(P, R) → (ϕ(P, R ) ∨ ϕ(P  , R)).
The above implication is equivalent to:
|= (¬ϕ(P, R ) ∧ ¬ϕ(P  , R)) → ¬ϕ(P, R).
Now, it follows from (1) that there are formulas ϕ1 (P ) and ϕ2 (R), such that
|= ¬ϕ(P, R) ↔ (ϕ1 (P ) ∧ ϕ2 (R)).
Therefore, |= ϕ(P, R) ↔ (¬ϕ1 (P ) ∨ ¬ϕ2 (R)), and, to finish the proof, it is
enough to consider two first-order functions, Q1 and Q2 , defined in
(Λ|S , n)/≈p ,
for some p ≥ q, and weakly expressed by ϕ1 and ϕ2 , respectively. 

9.3. Duality
Let S be a signature and A an S-structure. We can define another S-structure
A∗ , as follows: The interpretation of each predicate variable R in A∗ is the
set-theoretic complement of the interpretation of R in A.
Definition 9.10. Let Q be a first-order function. The dual first-order function
Q∗ , of Q, is the first-order function defined by
Q∗ ([(A, a)]q ) = ¬Q([(A∗ , a)]q ).
Definition 9.11. A first-order function Q is said to be self-dual if it is equal to
its dual first-order function Q∗ .
Remark 9.12. Notice that Q = Q∗∗ . Furthermore,
(Q1 ∧ Q2 )∗ = Q∗1 ∨ Q∗2 and (Q1 ∨ Q2 )∗ = Q∗1 ∧ Q∗2 .

9 One can always find first-order functions Q1 and Q2 with these properties. In order to see
this, consider the first-order functions expressed by ϕ1 and ϕ2 , and use the basic operations

to obtain first-order functions defined in a common domain (Λ|S , n)/≈p . For this, we can
assume f v(ϕ1 ) ⊆ f v(ϕ) ⊆ {x1 , . . . , xn } and f v(ϕ2 ) ⊆ f v(ϕ) ⊆ {x1 , . . . , xn }.
 First-Order Logic and First-Order Functions

10. Ideals of First-Order Functions

One of the most important tasks of the theory of first-order functions is to
formulate and study conditions under which a first-order function is defined
in terms of other first-order functions. A primary relation of definition among
first-order functions was established in Sect. 5: A first-order function Q is
defined in terms of the first-order functions in the set C iff Q is in the sys-
tem generated by C. In this section we will study another natural relation of
definition among first-order functions.
Throughout this section, we adopt
 the convention that  Q1 , . . . , Qm de-
note first-order functions defined in (Λ|S , n1 )/≈q1 , . . . , (Λ|S , nm )/≈qm , for
a common signature S and a non-decreasing sequence of numbers n1 , . . . , nm .
Definition 10.1. A set J of first-order functions closed under rank variations
is an ideal if the following condition holds: If the first-order functions Q1 ,
. . . , Qm are in J, and Q is a first-order function such that the composition
Q (Q1 , . . . , Qm ) is defined, then Q (Q1 , . . . , Qm ) is in J.
Example 10.2. Let S be a signature and J be the set of first-order functions
Q such that Q([(A, a)]q ) = Q([(A∗ , a)]q ), in which A is an S-structure and
A∗ is the S-structure defined in Sect. 9.3. The set J is an ideal of first-order
functions. Other ideals of first-order functions can be obtained similarly from
an operation on S-structures that consists in taking complements of some
interpretations of predicate variables (and preserving the others).
The closure under rank variations in Definition 10.1 is important be-
cause the compositional structure of first-order functions is strongly related to
rank variations: Even in the case in which Q , Q1 , . . . , Qm cannot have their
ranks “lowered”, the first-order function Q (Q1 , . . . , Qm ) can, eventually, be
obtained from another first-order function by raising rank. Let us illustrate this
relation between composition and rank variation with a preliminary result:
Lemma 10.3. Consider
  Q, Q1 , . . . , Qm first-order functions defined in the set
(Λ|S , n)/≈q , (Λ|S , n1 )/≈q1 , . . . , (Λ|S , nm )/≈qm , respectively, in which q
is greater than or equal to max {q1 , . . . , qm }. If there is a first-order function
Q and a function f : {1, . . . , k} → {1, . . . , m} such that
Q = Q (Qf (1) , . . . , Qf (k) ),
then there is a first-order function Q such that
q+max{q1 ,...,qm }−max{qf (1) ,...,qf (k) }
Qq = Q (Q1 , . . . , Qm ).
Proof. Assume the hypothesis. Let Q be a first-order function defined in

(Λ|S  , n)/≈ such that
q−max{qf (1) ,...,qf (k) }

Q = Q (Qf (1) , . . . , Qf (k) ).

 
Since Q (Qf (1) , . . . , Qf (k) ) is defined, nf (1) , . . . , nf (k) is a non-decreasing
 
sequence and the signature S  = R1 , . . . , Rk  is of type nf (1) , . . . , nf (k) .
 R. A. Freire Log. Univers.

Let S  = R1 , . . . , Rm

 be a signature of type n1 , . . . , nm , and π : S  → S 
defined by π(Ri ) = Rf (i) , for each i ∈ {1, . . . , k}.


Fix q  = q − max qf (1) , . . . , qf (k) and q̃ = q  + max {q1 , . . . , qm }. We
have:
π∗ (Q )(Q1 , . . . , Qm )([(A, a)]q̃ ) = π∗ (Q )([((Q1 , . . . , Qm )(A), a)]q ).
The result follows from the equations
π∗ (Q )([((Q1 , . . . , Qm )(A), a)]q ) = Q ([(π ∗ ((Q1 , . . . , Qm )(A)), a)]q )
and π ∗ ((Q1 , . . . , Qm )(A)) = (Qf (1) , . . . , Qf (k) )(A). 

We cannot eliminate the rank variation in Lemma 10.3. That is, it is

not possible, in general, to obtain a first-order function Q such that Q is
Q (Q1 , . . . , Qm ): For example, consider Q = Q1 = P1 (Q1 ), in which P1 is the
appropriate projection. If q1 < max {q1 , . . . , qm } it is not possible to write Q1
as a composition of the form Q (Q1 , . . . , Qm ). In this case, Q1 can only be
obtained from a composition with Q1 , . . . ,Qm by a lowering of rank after the
composition.

10.1. Finitely Generated Ideals

The next three lemmas are basic results about finitely generated ideals of
first-order functions. The first one gives the associativity of composition:
Q (Q1 (Q1 , . . . , Qm ), . . . , Qk (Q1 , . . . , Qm )) = Q (Q1 , . . . , Qk )(Q1 , . . . , Qm ).
Lemma 10.4. Let Q, Q1 , . . . , Qm , Q1 , . . . , Qk be first-order functions. Sup-
pose there are first-order functions Q , Q1 , . . . ,Qk such that
Q = Q (Q1 , . . . , Qk ) and Qi = Qi (Q1 , . . . , Qm ),
for each i ∈ {1, . . . , k}. Under these conditions, if Q = Q (Q1 , . . . , Qk ), then
Q = Q (Q1 , . . . , Qm ).
Proof. Let q, q1 , . . . , qm , q1 , . . . , qk , q  , q1 , . . . , qk be the ranks of
Q, Q1 , . . . , Qm , Q1 , . . . , Qk , Q , Q1 , . . . , Qk ,
respectively. We know that qi = qi + max {q1 , . . . , qm }, for each i ∈ {1, . . . , k}.
From this, it follows that
q  = q − max {q1 , . . . , qk } = q − max {q1 , . . . , qk } − max {q1 , . . . , qm } .
Let us evaluate Q (Q1 , . . . , Qm ) in a first-order value [(A, a)]q :
Q (Q1 , . . . , Qm )([(A, a)]q )
= Q (Q1 , . . . , Qk )([((Q1 , . . . , Qm )(A), a)]q−max{q1 ,...,qm } )
= Q ([((Q1 , . . . , Qk )((Q1 , . . . , Qm )(A)), a)]q ).
In order to finish the proof, it is enough to see that the structure
(Q1 , . . . , Qk )((Q1 , . . . , Qm )(A))
 First-Order Logic and First-Order Functions

is equal to
(Q1 (Q1 , . . . , Qm ), . . . , Qk (Q1 , . . . , Qm ))(A) = (Q1 , . . . , Qk )(A).

We know, from the paragraph below Lemma 10.3, that compositions and
rank variations do not, in general, commute. The next lemma shows that there
is a situation in which we can commute compositions and rank variations.
Lemma 10.5. Let Q, Q1 , . . . ,Qk be first-order functions, with ranks q, q1 ,
. . . ,qk , respectively, and p1 , . . . ,pk be natural numbers such that qi ≤ pi ,
for each i ∈ {1, . . . , k}. If the composition Q(Q1 , . . . , Qk ) is defined, then
the composition Q((Q1 )pq1 , . . . , (Qk )pqk ) is also defined and it is obtained from
1 k
Q(Q1 , . . . , Qk ) by raising rank.
Proof. Suppose the composition Q(Q1 , . . . , Qk ) is defined. Clearly, the com-
position Q((Q1 )pq1 , . . . , (Qk )pqk ) is also defined. We will calculate
1 k

Q((Q1 )pq1 , . . . , (Qk )pqk )([(A, a)]q+max{p1 ,...,pk } ).

1 k

For each i ∈ {1, . . . , k}, the first-order functions Qi and (Qi )pqi define the
i
same predicates in A. From this, it follows that
(Q1 , . . . , Qk )(A) = ((Q1 )pq1 , . . . , (Qk )pqk )(A).
1 k

Therefore,
Q((Q1 )pq1 , . . . , (Qk )pqk )([(A, a)]q+max{p1 ,...,pk } )
1 k

= Q([(((Q1 )pq1 , . . . , (Qk )pqk )(A), a)]q ) = Q([((Q1 , . . . , Qk )(A), a)]q ).
1 k

The result follows from the equality above. 

Lemma 10.6. Let Q, Q1 , . . . , Qm be first-order functions defined in the sets
(Λ|S , n)/≈q , (Λ|S , n1 )/≈q1 , . . . , (Λ|S , nm )/≈qm ,
respectively, in which q ≥ max {q1 , . . . , qm } and the sequence n1 , . . . , nm  is
non-decreasing. There is a first-order function, Q , with rank
q  = q − max {q1 , . . . , qm }
and type n1 , . . . , nm  → n such that Q = Q (Q1 , . . . , Qm ) iff for all first-order
values [(A, a)]q and [(B, b)]q , in which A and B are S-structures, and a and b
are n-tuples, if
[((Q1 , . . . , Qm )(A), a)]q−max{q1 ,...,qm } = [((Q1 , . . . , Qm )(B), b)]q−max{q1 ,...,qm } ,
then
Q([(A, a)]q ) = Q([(B, b)]q ).10

10 This lemma is basically a reformulation of the result on interpretability proved in [4],

page 25.
 R. A. Freire Log. Univers.

Proof. The condition is clearly necessary. We will show that it is also sufficient.
Suppose
[((Q1 , . . . , Qm )(A), a)]q−max{q1 ,...,qm } = [((Q1 , . . . , Qm )(B), b)]q−max{q1 ,...,qm }
implies
Q([(A, a)]q ) = Q([(B, b)]q ).
We define the first-order function Q of rank q  = q − max {q1 , . . . , qm } and
type n1 , . . . , nm  → n in the following way:
1. Given a first-order value[(A , a)]q of type n1 , . . . , nm , if there is a first-
order value [(A, a)]q in (Λ|S , n)/≈q such that
[(A , a)]q = [((Q1 , . . . , Qm )(A), a)]q ,
then we define
Q ([(A , a)]q ) = Q([(A, a)]q ).
2. Otherwise, we define
Q ([(A , a)]q ) = T.
The condition of the lemma guarantees that the first clause in this de-
finition
 does not depend on the choice of the first-order value [(A, a)]q in
(Λ|S , n)/≈q . Now, it is enough to verify that
Q([(A, a)]q ) = Q (Q1 , . . . , Qm )([(A, a)]q ),

for every [(A, a)]q in (Λ|S , n)/≈q . This equality follows from the definition

of Q , and the result is proved. 
Theorem 10.7. Let J be the ideal finitely generated by thefirst-order func-
tions Q1 , . . . , Qm . For a first-order function Q, defined in (Λ|S , n)/≈q , the
following conditions are equivalent:
1. Q ∈ J;
2. There is a natural number p ≥ q such that p ≥ max {q1 , . . . , qm } and
for all first-order values [(A, a)]p and [(B, b)]p , in which A and B are
S-structures, and a and b are n-tuples, if
[((Q1 , . . . , Qm )(A), a)]p−max{q1 ,...,qm } = [((Q1 , . . . , Qm )(B), b)]p−max{q1 ,...,qm } ,
then
Qpq ([(A, a)]p ) = Qpq ([(B, b)]p ).
Proof. Suppose condition (2) holds and let p be the least number satisfying
(2). From Lemma 10.6, the first-order function Qpq belongs to J. Since J is
closed under rank variations, Q ∈ J.
Now, for the converse implication, let us prove that the subset I of J con-
stituted by those first-order functions Q satisfying (2) contains Q1 , . . . , Qm ,
is closed under rank variations, and if the first-order functions Q1 , . . . , Qk are
in I and Q is a first-order function such that the composition Q (Q1 , . . . , Qk )
is defined, then Q (Q1 , . . . , Qk ) is in I.
 First-Order Logic and First-Order Functions

Clearly, I contains Q1 , . . . , Qm .
In order to prove that I is closed under rank variations, notice that if
p is a number given by condition (2) and p ≥ p, then p satisfies the same
property. In fact, let [(A, a)]p and [(B, b)]p be first-order values. Since p ≤ p ,
if
[((Q1 , . . . , Qm )(A), a)]p −max{q1 ,...,qm } = [((Q1 , . . . , Qm )(B), b)]p −max{q1 ,...,qm } ,
then
[((Q1 , . . . , Qm )(A), a)]p−max{q1 ,...,qm } = [((Q1 , . . . , Qm )(B), b)]p−max{q1 ,...,qm } .
From the hypothesis,
Qpq ([(A, a)]p ) = Qpq ([(B, b)]p ).
Since

Qpq ([(A, a)]p ) = Q([(A, a)]q ) = Qpq ([(A, a)]p ),

and similarly for (B, b), we have

 
Qpq ([(A, a)]p ) = Qpq ([(B, b)]p ).

Now, suppose Q ∈ I and Q is obtained from Q by rank variation. If p

is a number given by condition (2), we can assume p is also greater than or
equal to the rank q  of Q . Under these conditions, if
[((Q1 , . . . , Qm )(A), a)]p−max{q1 ,...,qm } = [((Q1 , . . . , Qm )(B), b)]p−max{q1 ,...,qm } ,
then
Qpq ([(A, a)]p ) = Qpq ([(B, b)]p ).
Since
Qpq ([(A, a)]p ) = Q([(A, a)]q ) = Q ([(A, a)]q ) = Qp
q  ([(A, a)]p ),

and similarly for (B, b), we have

Qp p
q  ([(A, a)]p ) = Qq  ([(B, b)]p ).

It remains to prove that I is closed under compositions, in the sense

of Definition 10.1. Let Q , Q1 , . . . , Qk be first-order functions with ranks
q  , q1 , . . . , qk , respectively. Suppose Q1 , . . . , Qk are in I and the composi-
tion Q (Q1 , . . . , Qk ) is defined. Let p1 , . . . , pk be natural numbers given by
condition (2) for Q1 , . . . , Qk , respectively.
From Lemma 10.5, the composition Q ((Q1 )pq1 , . . . , (Qk )pqk ) is defined and
1 k
is obtained from Q (Q1 , . . . , Qk ) by raising rank. Furthermore, from Lemma
10.6, the first-order function (Qi )pqi is of the form Qi (Q1 , . . . , Qm ), for each
i
i ∈ {1, . . . , k}. From Lemma 10.4 it follows that
Q ((Q1 )pq1 , . . . , (Qk )pqk ) = Q (Q1 , . . . , Qk )(Q1 , . . . , Qm ).
1 k
 R. A. Freire Log. Univers.

Therefore, once again by Lemma 10.6, it follows that the first-order function
Q (Q1 , . . . , Qk ) satisfies condition (2), in which the appropriate p is the rank
of
Q ((Q1 )pq1 , . . . , (Qk )pqk ).
1 k

11. Predicate Definability

As it is now clear, the relation of definition among first-order functions is
a central theme of the theory of these objects. In this section, we study the
relation of definition among first-order functions in a particular case of interest:
Predicate definability in classes of structures. This section is only a first step
in the direction of an understanding of this model-theoretic topic from the
perspective of the theory of first-order functions.
Definition 11.1. Let S be a signature and K a class of Σ-structures. Suppose
S is constituted by the predicate variables R1 , . . . , Rm , with arities n1 , . . . ,
nm , in the alphabetical ordering, and let P1S |K , . . . , Pm S
|K be the corresponding
projections, relative to the class K. Fix j ∈ {1, . . . , m}. We say that PjS |K is
definable in terms of P1S |K , . . . , Pj−1
S S
|K , Pj+1 |K , . . . , Pm S
|K if there is a first-
order function Qj , defined in

(Λ|R1 ,...,Rj−1 ,Rj+1 ,...,Rm  , nj )/≈q ,

such that
(PjS |K )q0 = Qj (P1S |K , . . . , Pj−1
S S
|K , Pj+1 S
|K , . . . , Pm |K ),
in which
Qj (P1S |K , . . . , Pj−1
S S
|K , Pj+1 S
|K , . . . , Pm |K ) = Qj (P1S , . . . , Pj−1
S S
, Pj+1 S
, . . . , Pm )|K .
Remark 11.2. If A is a structure in K|S , then it is important to notice that
(P1S , . . . , Pj−1
S S
, Pj+1 S
, . . . , Pm )(A)
is the reduct of A to the signature R1 , . . . , Rj−1 , Rj+1 , . . . , Rm .
Proposition 11.3. Using the notation given in Definition 11.1, the first-order
function PjS |K , relative to K, is definable in terms of
P1S |K , . . . , Pj−1
S S
|K , Pj+1 S
|K , . . . , Pm |K
iff there is a first-order function Q in the ideal finitely generated by
P1S , . . . , Pj−1
S S
, Pj+1 S
, . . . , Pm such that
(PjS |K )q0 = Q|K .

Proof. Suppose the first-order function PjS |K , relative to K, is definable in

terms of
P1S |K , . . . , Pj−1
S S
|K , Pj+1 S
|K , . . . , Pm |K .
 First-Order Logic and First-Order Functions

In this case, since

Qj (P1S |K , . . . , Pj−1
S S
|K , Pj+1 S
|K , . . . , Pm |K ) = Qj (P1S , . . . , Pj−1
S S
, Pj+1 S
, . . . , Pm )|K ,
it follows that Q = Qj (P1S , . . . , Pj−1
S S
, Pj+1 S
, . . . , Pm ) satisfies the condition.
On the other hand, suppose there is a first-order function Q in the ideal
finitely generated by P1S , . . . , Pj−1
S S
, Pj+1 , . . . , Pm S
such that
(PjS |K )q0 = Q|K .
From Lemma 10.6 and Theorem 10.7, there is a natural number p greater or
equal to the rank q of Q and a first-order function Q of rank p such that
Qpq = Q ((P1S , . . . , Pj−1
S S
, Pj+1 S
, . . . , Pm ).
Since (Qpq )|K = (Q|K )pq , we have
(PjS |K )p0 = Q |K .

The theorem below asserts the projection corresponding to the predicate
variable Rj , relative to K, is a first-order function, of rank q, relative to K, of
the projections corresponding to the other predicate variables in S, relative to
K, iff the value which it assigns to [(A, a)]K 0 is determined by the first-order
value, of rank q, of the pair constituted by the reduct of A to the signature
R1 , . . . , Rj−1 , Rj+1 , . . . , Rm  and by the n-tuple a.
Theorem 11.4. Still using the notation given in Definition 11.1, the first-order
function PjS |K , relative to K, is definable in terms of
P1S |K , . . . , Pj−1
S S
|K , Pj+1 S
|K , . . . , Pm |K
iff there is a natural number q such that for all S-structures A and B in K|S ,
and all n-tuples a in A and b in B
[((P1S , . . . , Pj−1
S S
, Pj+1 S
, . . . , Pm )(A), a)]q
= [((P1S , . . . , Pj−1
S S
, Pj+1 S
, . . . , Pm )(B), b)]q
implies
(PjS |K )q0 ([(A, a)]K S q
q ) = (Pj |K )0 ([(B, b)]q ).
K

Proof. If the first-order function PjS |K , relative to K, is definable in terms of

P1S |K , . . . , Pj−1
S S
|K , Pj+1 S
|K , . . . , Pm |K ,
then there is a first-order function Qj , defined in

(Λ|R1 ,...,Rj−1 ,Rj+1 ,...,Rm  , nj )/≈q ,

such that
(PjS |K )q0 = Qj (P1S |K , . . . , Pj−1
S S
|K , Pj+1 S
|K , . . . , Pm |K ).
Since
Qj (P1S |K , . . . , Pj−1
S S
|K , Pj+1 S
|K , . . . , Pm |K ) = Qj (P1S , . . . , Pj−1
S S
, Pj+1 S
, . . . , Pm )|K ,
 R. A. Freire Log. Univers.

the validity of the condition of the theorem follows from the definition of
composition of a first-order function with first-order functions relative to K.
Now, assume the condition of the theorem. Let Q be the unique first-order
function satisfying the following conditions:
1. Q|K = (PjS |K )q0 and
2. for every first-order value [(C, c)]q which does not contain a pair such that
the structure is in K|S ,
Q([(C, c)]q ) = T.
The first-order function Q thus defined satisfies the condition of Lemma
10.6. Therefore, Q is in the ideal finitely generated by P1S , . . . , Pj−1
S S
, Pj+1 ,
S S
. . . , Pm . From Proposition 11.3, the first-order function Pj |K , relative to K,
is definable in terms of
P1S |K , . . . , Pj−1
S S
|K , Pj+1 S
|K , . . . , Pm |K .


12. Final Remarks

The most important concept introduced in this paper is that of first-order
value. It is the first-order correlate of finite sequences of truth-values. Quite
surprisingly, such a basic concept was not clearly highlighted so far. It is sur-
prising because some closely related methods of first-order logic like the back-
and-forth and Hintikka’s normal forms are well-known. As far as we know, the
definition of first-order values was never presented as a separate definition of
independent interest and with the aim of developing a streamlined general-
ization of the theory of truth-functions. Once this concept is made explicit, a
generalization of the theory of truth-functions accounting for first-order logic
naturally emerges.
It is important to recall how first-order values appear after all: A propo-
sitional formula expresses its truth-conditions for its signature. More exactly,
a propositional formula expresses that one of its truth-conditions obtains. In
propositional logic, a truth-condition for propositional variables P1 , . . . , Pm
is a minimal information required in order to determine the truth-value of all
propositional formulas in this finite signature. Therefore, the truth-conditions
of a formula are identified with the finite sequences of truth-values, assigned to
the relevant propositional variables, making the formula true. We tacitly use
this remarks when we construct the full disjunctive normal form for a formula.
Transferring this picture to first-order logic, we grasp a formula ϕ, with
signature S, free variables x1 , . . . , xn and quantificational rank q, as expressing
its satisfaction-conditions, which are the first-order values [(A, a)]q such that
the pair (A, a) satisfies ϕ, that is, A |= ϕ[a]. This parallels the propositional
case, for the first-order value [(A, a)]q is the minimal information required in
order to determine whether or not the pair (A, a) satisfies a generic first-order
formula with signature S, free variables x1 , . . . , xn and quantificational rank
q.
 First-Order Logic and First-Order Functions

The theory of first-order functions can be developed in directions that we

have not explored in this paper. The paper is meant as an introduction to the
subject. Hopefully, there are enough results here showing this new perspective
on first-order logic to be fruitful.

Acknowledgements
The problem of constructing a theory of functions for first-order logic was
suggested to me by Roderick Batchelor, who has been working independently
on a different approach to this problem ([1,2]). I am also very much indebted
to Daniel Tausk, David Gilbert and Hilan Bensusan for many suggestions and
improvements. This research was financially supported by Conselho Nacional
de Desenvolvimento Cientı́fico e Tecnológico (CNPq), process 150046/2014-6.

References
[1] Batchelor, R.: Metaphysical Modal Logic, Volume I: Logical Functions. Sao Paulo,
Unpublished manuscript (2014)
[2] Batchelor, R.: Metaphysical Modal Logic, Volume II: Logical Systems. Sao Paulo,
Unpublished manuscript (2014)
[3] Fraı̈ssé, R.: Cours de Logique Mathématique, Tome 1. Gauthier-Villars, Paris
(1971)
[4] Fraı̈ssé, R.: Cours de Logique Mathématique, Tome 2. Gauthier-Villars, Paris
(1972)
[5] Freire, R.: On existence in set theory, part III: Applications to new axioms. South
Am. J. Log. 1(1), 249–265 (2015)
[6] Hintikka, J.: Distributive normal forms in the calculus of predicates. Acta Philos.
Fennica. 6, 71 (1953)
[7] Humberstone, L.: Monadic representability of certain binary relations. Bull. Aust.
Math. Soc. 29, 365–375 (1983)
[8] Poizat, B.: Cours de Théorie des Modèles. Nur Al-Mantiq Wal-Ma’rifah. Villeur-
banne (1985)
[9] Post, E.: The Two-Valued Iterative Systems of Mathematical Logic. Princeton,
New Jersey (1941)
[10] Smullyan, R.: First-Order Logic. New York (1995)

Rodrigo A. Freire
Department of Philosophy
University of Brası́lia
Brası́lia
Brazil
e-mail: [email protected]

Received: June 4, 2014.

Accepted: July 4, 2015.