First Order Logic: Syntax: Let us first introduce the symbols, or alphabet, being used. Beware that there are all sorts of slightly different ways to define FOL.
1 Alphabet
o Constants:
Where predicates return true or false, functions can return any value.
o Variables: Usually an identifier.
One needs to be able to distinguish the identifiers used for predicates, functions, and variables by using some appropriate convention, for example, capitals for function and predicate symbols and lower cases for variables.
2 Terms: A Term is either an individual constant (a 0-ary function), or a variable, or an n-ary function applied to n terms: F(t1 t2 ..tn)
[We will use both the notation F(t1 t2 ..tn) and the notation (F t1 t2 .. tn)]
3 Atomic Formulae: An Atomic Formula is either FALSE or an n-ary predicate applied to n terms: P(t1 t2 .. tn). In the case that "=" is a logical symbol in the language, (t1 = t2), where t1 and t2 are terms, is an atomic formula.
4 Literals: A Literal is either an atomic formula (a Positive Literal), or the negation of an atomic formula (a Negative Literal). A Ground Literal is a variable-free literal
5 Clauses: A Clause is a disjunction of literals. A Ground Clause is a variable-free clause. A Horn Clause is a clause with at most one positive literal. A Definite Clause is a Horn Clause with exactly one positive Literal.
Notice that implications are equivalent to Horn or Definite clauses:
6 Formulae: A Formula is either:
An occurrence of a variable in a formula that is not bound, is said to be free. A formula where all occurrences of variables are bound is called a closed formula, one where all variables are free is called an open formula. A formula that is the disjunction of clauses is said to be in Clausal Form. We shall see that there is a sense in which every formula is equivalent to a clausal form. Often it is convenient to refer to terms and formulae with a single name. Form or Expression is used to this end.
Substitutions: Given a term s, the result [substitution instance] of substituting a term t in s for a variable x, s[t/x], is:
Given a formula A, the result (substitution instance) of substituting a term t in A for a variable x, A[t/x], is:
The substitution [t/x] can be seen as a map from terms to terms and from formulae to formulae. We can define similarly [t1/x1 t2/x2 .. tn/xn], where t1 t2 .. tn are terms and x1 x2 .. xn are variables, as a map, the [simultaneous] substitution of x1 by t1, x2 by t2, .., of xn by tn. [If all the terms t1 .. tn are variables, the substitution is called an alphabetic variant, and if they are ground terms, it is called a ground substitution.] Note that a simultaneous substitution is not the same as a sequential substitution.
