Term and formula in Predicate logic

A Formal Language Predicate Logic provides a way to formalize natural language so that ambiguity is removed. A predicate logic formula involved two sorts of things. The first sort denotes the objects such as individuals a and p (referring to Andy and Paul) are examples, as are variables such as x and v. Function symbols allow us to refer to objects: thus, m(a) and g(x, y) are also objects. In predicate logic, an expression which denotes object is called term. The other sorts in predicate logic denote truth values; expressions in predicate logic, of this kind, are formulas: Y (x, m(x)) is a formula, though x and m(x) are terms.

The discussion of Predicate logic as a formal language is to give an impression of how we code up sentences as formulas of predicate logic. By giving syntactic rules for the formation of predicate logic formulas, we will be more precise about it. The predicate logic is much more complex than that of propositional logic, because of the power of this language.

There are three sets in predicate vocabulary. First is a set of predicate symbols ‘P’, the second is a set of function symbols ‘F’ and third is a set of constant symbols ‘C’. Each predicate symbol and each function symbol in predicate logic must come with an arity (the number of arguments it expects). Constants can be thought of as functions with 0-arity or which don’t take any arguments (even we drop the argument brackets). Therefore, constant symbols live in the set F (function symbols) together with the ‘true’ functions which do take arguments. So we may drop the set C since it is convenient to do so, and stipulate that constants are nullary functions (with 0-arity).

Term

The terms of predicated language are made up of variables, constant symbols, and functions applied to those. Functions may be nested, as in g(m(a), x): the grade obtained by Andy’s mother in the course x.

Terms are defined as follows.

• Any variable in predicate logic is a term.
• If c ∈ F (set of function symbols) is a nullary function, then c is a term.
• If t₁, t₂,…,t_n are the terms and f ∈ F has arity n > 0, then f(t₁, t₂,…,t_n) is a term.
• Nothing else is a term.

In Backus Naur form we may write as:

t ::= x | c | f(t,…,t)

Where x ranges over a set of variables var, c ranges over nullary function symbols in F, and f ranges over those elements of F with arity n > 0.

The first building block of terms is constants (nullary functions) and variables. The more complex terms are built from function symbols using as many previously built terms as required by such function symbols. And the notion of terms is dependent on the set F (function symbols). If we change it, we change the set of terms.

Examples:

Suppose ‘n’, ‘u’ and ‘b’ are function symbols, respectively nullary, unary and binary. Then b(u(n), n) and u(b(n, u(n))) are terms, but b(n) and u(u(n), n) are not ( as they violate the arities).

Suppose 0, 1,… are nullary, s is unary, and +, −, and ∗ are binary. Then ∗(−(2, +(s(x), y)), x) is a term. Usually, the binary symbols are written infix rather than a prefix; thus, the term is usually written as (2 − (s(x) + y)) ∗ x.

Formula

The choice of sets P and F for predicate and function symbols, respectively, is to relate that what we intend to describe.

We define the set of formulas over (F, P) inductively, using the already defined set of terms over F:

• If P ∈ P is a predicate symbol of arity n ≥ 1, and if t1, t2,…,tn are terms over F, then P(t1, t2,…,tn) is a formula.
• If φ is a formula, then so is (¬φ)
• If φ and ψ are formulas, then so are (φ ∧ ψ), (φ ∨ ψ) and (φ → ψ)
• If φ is a formula and x is a variable, then (∀x φ) and (∃x φ) are formulas.
• Nothing else is a formula.

In Backus Naur form we may write as:

φ ::= P(t1, t2,…,tn) | (¬φ) | (φ ∧ φ) | (φ ∨ φ) | (φ → φ) | (∀x φ) | (∃x φ)

Where P ∈ P is a predicate symbol of arity n ≥ 1, ti is termed over F (function symbol) and x is a variable. Recall that each occurrence of φ on the right-hand side of the::= stands for any formula already constructed by these rules.

Convention:

• ¬, ∀y and ∃y bind most tightly;
• then ∨ and ∧;
• then →, which is right-associative.

Often we also omit brackets around quantifiers, provided that doing so introduces no ambiguities. Predicate logic formula can be represented by a parse tree. For example, the formula ∀x ((P(x) → Q(x)) ∧ S(x, y)) represented by parse tree:

Example: Consider translating the sentence “Every son of my father is my brother” into predicate logic.

As a predicate, we choose a constant m for ‘me’ or ‘I,’ so m is a term, and further, we choose {S, F, B} as the set of predicates with meanings:

S(x, y): x is a son of y

F(x, y): x is the father of y

B(x, y): x is a brother of y

Then the symbolic encoding of the sentence is:

∀x ∀y (F(x, m) ∧ S(y, x) → B(y,m))

Saying as: ‘For all x and all y, if x is a father of m and if y is a son of x, then y is a brother of m.’

As a function, we keep m, S, and B as above and we write ’f’ for the function which, given an argument, returns the corresponding father. Note that, this works only because of the logic that fathers are unique and always defined, so ‘f’ really is a function as opposed to a mere relation.

The symbolic encoding of the sentence is now:

∀x (S(x, f(m)) → B(x, m))

Saying as: ‘For all x, if x is a son of the father of m, then x is a brother of m;’ it is less complex as it involves only one quantifier.

Predicate Logic