First Order Logic

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

1. Logical Symbols: These are symbols that have a standard meaning, like: AND, OR, NOT, ALL, EXISTS, IMPLIES, IFF, FALSE, =.
2. Non-Logical Symbols: divided in:

o Constants:

• Predicates: 1-ary, 2-ary, .., n-ary. These are usually just identifiers.
• Functions: 0-ary, 1-ary, 2-ary, .., n-ary. These are usually just identifiers. 0-ary functions are also called individual 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:

• (A IMPLIES B) is equivalent to ( (NOT A) OR B)
• (A AND B IMPLIES FALSE) is equivalent to ((NOT A) OR (NOT B)).

6 Formulae: A Formula is either:

• an atomic formula, or
• a Negation, i.e. the NOT of a formula, or
• a Conjunctive Formula, i.e. the AND of formulae, or
• a Disjunctive Formula, i.e. the OR of formulae, or
• an Implication, that is a formula of the form (formula1 IMPLIES formula2), or
• an Equivalence, that is a formula of the form (formula1 IFF formula2), or
• a Universally Quantified Formula, that is a formula of the form (ALL variable formula). We say that occurrences of variable are bound in formula [we should be more precise]. Or
• a Existentially Quantified Formula, that is a formula of the form (EXISTS variable formula). We say that occurrences of variable are bound in formula [we should be more precise].

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:

• t, if s is the variable x
• y, if s is the variable y different from x
• F(s1[t/x] s2[t/x] .. sn[t/x]), if s is F(s1 s2 .. sn).

Given a formula A, the result (substitution instance) of substituting a term t in A for a variable x, A[t/x], is:

• FALSE, if A is FALSE,
• P(t1[t/x] t2[t/x] .. tn[t/x]), if A is P(t1 t2 .. tn),
• (B[t/x] AND C[t/x]) if A is (B AND C), and similarly for the other connectives,
• (ALL x B) if A is (ALL x B), (similarly for EXISTS),
• (ALL y B[t/x]), if A is (ALL y B) and y is different from x (similarly for EXISTS).

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.