Thank you for the explanation. I think I understand what you're trying to say,
but what you're trying to say doesn't work in FOL. Perhaps it works in the
context of programming languages, but I can't really say.
The reason it doesn't work is that in FOL, variables, predicates and functions
are not "all substitute-able". Predicates don't "evaluate to booleans". They do
in some programming languages, but not in FOL. Perhaps more counter-intuitively,
not even functions are "substitute-able": there are no rules for replacing a
function with its value in FOL.
Let me back up a bit and point out the terminology again. I appreciate that you
think what I said above is "strictly syntactical" but the idea that there is a
difference between syntax and semantics is, itself, a programming language idea
that does not work in FOL. In FOL, syntax and semantics are one, that's part of
its power: FOL is unambiguous; what you see is what you get. For example, P ∧ Q
is a conjunction: syntactically and semantically. There is no way to take P ∧ Q
as anything but a conjunction, there is no compiler or interpreter translating P
∧ Q into something else. It's how you write a conjunction and it is a
conjunction. FOL is WYSIWIG, yes?
So if I tell you that ƒ(x) is a function, coming from a programming language
background you'd expect me to tell you how ƒ(x) is defined (as sdbrady says).
In FOL, if ƒ(x) is a function, then that's the function, right there. There's
nothing else to it: it's a function symbol followed by n comma-separated terms
in parentheses. There's no definition of ƒ(x) "somewhere else". There is no
"somewhere else". More to the point, ƒ(x) does not evaluate to anything and you
can't replace ƒ(x) with its value.
In the same way predicates don't "get evaluated to booleans" - they do in some
programming languages, but not in FOL. I think also you're using "predicate"
itself in a programming language sense. In FOL, a predicate is the name of a
relation between n entities in the domain of discourse, where n is the arity of
the predicate. So P(x,y) is not a predicate, it's an atom of the predicate P
of arity 2. And note that in P(x,y), x and y are variables.
Here's how this really works. In FOL, an atom is ground when it has no
variables. P(x,y) is not ground, P(a,b) is ground if a and b are constants.
Ground atoms are assigned truth values by an interpretation. An interpretation
can be written as the set of true atoms. So for example, I = {P(a,b), P(c,d)} is
an interpretation under which the atoms P(a,b) and P(c,d) are true and all other
atoms are false. Note that interpretations are in a sense completely arbitrary,
in that the same set of atoms can be assigned different truth values by
different interpretations and there can be as many interpretations as subsets of
a set of atoms. So it's literally "an interpretation".
Interpretations assign truth values to atoms so given an interpretation we can
derive the truth values of more complex formulae. Remember that atoms are
"atomic formulae", i.e. the simplest FOL formulae. We can make more complex
formulae by using the four logical operators. So for instance, we can write the
formula P(a,b) ∧ P(c,d). Under the interpretation I in my example above, the
preceding formula is true, because both of the operands of the conjunction are
true under I. The formula P(a,b) ∧ P(d,e) is not true under I because P(d,e) is
not true under I.
How about variables and quantifiers? Remember that an atom is a predicate symbol
followed by n comma-separated terms in parentheses and that terms are variables
or functions (including constants, i.e. functions of arity 0). So P(x,y) is an
atom with variables as terms. But, interpretations assign truth values to
ground atoms, so what is the truth value of P(x,y)? It depends on the
quantification of its variables. Essentially, quantifiers are a convenience that
allow us to avoid having to write every formula as a -possibly infinite- set of
ground atoms in order to determine the truth of the formula.
So for example, if we write ∃x,y: P(x,y) (I read that as: "there exist x and y
such that P(x,y) is true") that ... does what it says on the tin. P(x,y) is true
under the current interpretation for any values of x and y. If we write instead
∃x∀y: P(x,y) then we're saying that P(x,y) is true under the current
interpretation for at least one value of x and all values of y.
In our example, ∃x,y: P(x,y) is true under I because there exist at least two
values of x and y that make P(x,y) true, under I. ∃x∀y: P(x,y) is false because
there exists no value of x that makes P(x,y) true for all y under I.
Now let's go back to functions and how they're not actually replaced by their
values. The canonical example of a function in FOL is probably the Peano axiom
that describes the natural numbers. Here it is, in all its quantified glory:
∀x: n(0) ∧ n(x) → n(s(x)) (1)
In plain English "0 is a natural nuber and if x is a natural number the
successor of x, s(x), is a natural number". So s(x) is a function. But where is
it that s(x) is replaced with, substituted for, its value? Where is it even that
s(x) is evaluted? It's not!
Insted, FOL enables us to define rules of inference such as the method of
analytical Tableaus or the Resolution principle. Inference rules in turn allow
us to determine logical equivalences between FOL formulae. That's how it all
comes together. So, under Tableau or Resolution, we can prove that (1) is
equivalent to the following atomic formulae:
n(0), n(s(0)), n(s(s(0))), n(s(s(s(0)))), ... (2)
And so on - all the natural numbers in Peano's notation. Again, note there's no
substitution of "predicates" (actually, their atoms) or functions, there's no
evaluation of "predicates" (actually, their atoms) to booleans and there is no
evaluation of functions to their values. The manipulation is
purely algebraic.
We're just shifting symbols around.
Oh, but you'll notice that a substitution has happened: all instances of the
variable x in (1) have been substituted for ground terms in (2). Variable
sustbistitutions (but not "predicate" or function substitutions!) are a
mechanism introduced by Tableau and Resolution (full disclosure: I have only a
hazy idea of Tableau, but I think variable subsitutions are defined slightly
differently than in Resolution). They are not part of FOL, as such, but more
like plug-ins. In FOL, variables are quantified over terms, and that's all.
Inference rules allow us to derive new atoms (or entire new theorems) from FOL
formulae with quantified variables by substituting those variables with other
terms, but that's inference rules, built on top of FOL and not FOL itself.
Inference rules perform reasoning over FOL expressions. In a sense, FOL is the
language and the inference rules are the speakers of the language.
Well, that's my interpretation. You'll be hard pressed, unfortunately, to find
all that in one place all together, and you may find bits and pieces of it lying
around scattered in papers or books about logic programming and in particular
Prolog. I assume that's where you get your definitions from, perhaps from
functional programming books that also discuss logic programming? This is a
rather large comment already but suffice it to say that logic programming is
_yet another_ extension of FOL (usually based on the Resoultion inference rule)
and that the most popular logic programming language, Prolog, takes many
liberties with both logic programming principles and FOL principles. Prolog
definitely has "syntax" and "semantics" that are two different things. In
particular, Prolog syntax has a declarative semantics and a procedural
semantics, and neither of the two is quite exactly FOL. To make matters worse,
Prolog runs roughshod over FOL terminology, so for example what are called
"atoms" in Prolog are actually constants in FOL, and that can cause much
confusion (true story). But like I say, that's a different story, for another
Saturday, perhaps.