(Last modified Tue Jan 22 22:41 2008)
Figure 1
First-order logic extends propositional logic by considering things that are true and false of objects or entities in a partial view of the world, called a domain. This is done by adding to PL:
We use the phrase "first-order logic" so frequently that we will abbreviate it as FOL.
The various syntactic kinds of FOL formulae (things that can be true or false) are shown in Figure 1. Besides the constants, propositional variables, negations, conjunctions, disjunctions, and parentheses of Propositional logic (PL), there are also predicates and existential and universal quantifications. (The remaining elements of FOL are the various kinds of terms.)
We will use metavariables in discussing FOL syntax, as we did for PL. A FOL metavariable represents a syntactically-correct FOL formula. We will write FOL metavariables as α, β, γ, ... , α1, α2, ....
We assume each of the (possibly countably infinite number of) objects in the domain has a name. There is an unbounded supply of object names, which we will write in quotes "a", "b", "c", .... Each name is a syntactically correct FOL term.
A variable refers to an object in the domain, but we may not know which object. There is an unbounded supply of variables, which we write beginning with lowercase letters a, b, c, ... , a1, a2, ... , aa, ab, .... Each variable is a syntactically correct FOL term.
Variables are analogous to propositional variables, but while a propositional variable represents a (possibly) unknown truth value, a variable represent an unknown object. A propositional variable is a formula, while a variable is a term. Unlike a propositional variable, which is bound by an interpretation or not bound at all, a variable name is bound by a quantification or not bound at all. A variable that is not bound is said to be free.
A function takes one or more objects and produces an object. Each function has an arity, or number of terms, that is appropriate to it. There is an unbounded supply of function names, which we will write beginning with lowercase letters. Each function application is represented by a name followed by a list of terms in parentheses, and is a syntactically correct FOL term. For example, a("chrysophite"), b(t, "mambo"), and fatherOf("Homer Simpson"), are syntactically correct FOL terms.
Terms represent objects in the domain. A term can be either a name, a variable, or an application of a function to the appropriate number of terms.
The component parts of PL formulae are themselves formulae, but FOL formulae are composed of two kinds of parts: formulae and terms.
A predicate takes one or more objects and produces true or false. Each predicate has an arity, or number of terms, that is appropriate to it. Each predicate application is represented by a name, of which there is an unbounded supply all beginning with lowercase letters, followed by a list of terms in parentheses, and is a syntactically correct FOL formula: for example, A("chrysophite"), B(t, "mambo"). and AreSiblings("the Dalai Lama", "Arnold Schwarzenegger"), are syntactically correct FOL formulae.
A quantification is either an existential quantification, written as ∃ followed by a variable and a formula, or a universal quantification, written as ∀ followed by a variable and a formula. In addition, each variable in a formula must be the variable of at most one quantification. There are scoping rules to disambiguate the case in which two quantifiers bind variables with the same name; the innermost quantifier wins, so that ∀x (∃x x=x)∧x=x is equivalent to the more clearly-written ∀x (∃y y=y)∧x=x. A quantification is a syntactically-correct FOL formula.
For example, ∃x AreSiblings("Elvis Presley", x) and ∀y(¬NeedsPeople(y)∨IsAmongLuckiest(y)) are syntactically correct FOL formulae.
A quantification is said to bind its variable in the formula; every appearance of that variable in the formula is bound to the quantification. Any variable that is not bound in a formula is free in that formula.
The most common convention in first-order logic seems to be that a quantifier binds to the first complete formula following it, in other words more tightly than the binary operators ∧ and ∨ but less tightly than the unary operator ¬. For example, ∃x f(x)∧g(x) is considered to be the same as (∃x f(x)) ∧g(x), rather than ∃x (f(x)∧g(x)).
