Logic for Computer Scientists/Predicate Logic/Syntax

Syntax edit

Definition 1 (Syntax of predicate logic - Terms) edit

Assume a

  • countable set of function symbols  
  • a countable set of  

The set of terms is defined by the following induction:

  • Variables   are terms.
  • If   are terms and   is a function symbol, then   is a term.

Terms of type   are special ones, they are called constants. In this case we omit the braces and denote them as  .

Terms are the syntactic counterpart of the above mentioned objects. Constants will denote the elements of the domain and function symbols will denote a way to refer to such objects.

The following definition introduces the formulae.

Definition 2 (Syntax of predicate logic - Formulae) edit

Assume a countable set of predicate symbols . The set of (well-formed) formulae is defined by the following induction:

  • If   are terms and   is a predicate symbol, then   is a formula.
  • If   and   are formulae, then   and   are formulae.
  • If   is a formula, then   is a formula.
  • If   is a variable and   a formula, then   and   are formulae.

Formulae of type   are called atoms or atomic formulae.

Note that the concept of subformulae applies exactly like in the propositional case (Syntax (Propositional Logic)).

We introduce the following abbreviations, which will be used with indices as well:

  for variables
  for constants
  for function symbols
  for predicate symbols


Note the arity of function and predicate symbols is ommited in these abbreviations; we assume that it will be obvious from the context.

Example: Assume we want to represent the following equation, which holds for arbitrary elements in a field:

 

The two operators   and   are represented in a predicate logic formula as binary function symbols   and  , the three variables are   and  , and the equality relation   is the binary predicate symbol  . Altogether we have the following formula in predicate logic:

 

In the following we will use the obvious and more liberal notation as in the propositional case.

Definition 3: Bound and Free Occurrences of Variables edit

An occurrence of a variable   in a formula   is called bound, if it occurs in a subformula of   which is of the form   or  . Otherwise we call the occurrence free.

A formula, which does not contain a free occurrence of a variable is called closed.

Example: The following formula contains both free and bound occurrences of   and  .