Logic for Computer Scientists/Predicate Logic/Syntax

Syntax Definition 1 (Syntax of predicate logic - Terms) 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) 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 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 .