First-Order Logic (2)

< 1 2 3 >

The binding strength of the quantifiers x and x, is that same as that of . The rest of the connectives follow with the following decreasing binding strength . In Prolog, constant symbols conventionally begin with lower case letters, and variable symbols begin with upper case letters or an underscore.

In some texts, different symbols are used for the connectives:

Name	Connective	Alternative	Example
Negation		~	¬a
Conjunction		&	ab
Disjunction		or	ab
Conditional		if	ab
Biconditional		iff	ab

The first order language given by an alphabet consists of the set of all formulas constructable from the symbols of the alphabet. Here are some definitions of various pieces of informal grammar used in conjunction with an alphabet, when constructing first order predicate logic language:

• A term is either a constant symbol, a variable symbol or an n-ary function symbol applied to a tuple of n terms.
  • e.g. a, X, f(b, f(b,Y,Z),Y)
• An atomic formula is a predicate symbol applied to a tuple of terms.
  • e.g. likes(X,sim), borrows(book, sim)
• A well-formed formula is either an atomic formula or else takes one of the following forms:
  • W, ¬W, W1 W2, W1 W2, W1 W2, W1 W2, xW, xW.
• In a well formed formula, the scope of a quantifier is defined as W. We say that the quantifier (ie x or x) quantifies every occurrence of x in W.
• An occurrence of a variable symbol x in a well formed formula W is said to be bound if and only if it lies within the scope of or in some quantifier (x or x) which occurs in W.
• An occurrence of a variable symbol that is not bound is said to be unbound (or free).
• A sentence (or closed formula) is a well-formed formula in which every occurrence of every variable symbol is bound.
  • e.g. x (y child(x) father(y,x)) every child has a father.
• A literal is either an atomic formula or a negated atomic formula.
  • e.g. likes(sim, books), ¬likes(sim, pain)
• A ground term is a term containing no variable symbols.
• A ground formula is a formula containing no variable symbols.
• Atomic formulas are commonly called predicates.

< 1 2 3 >