X l l NOTATION of constant symbols. The sets /, J, K may be empty. The arity of r is denoted by T0(i), the arity of ft by n(j). Here are some prominent examples of first-order languages: The language LQ of group theory has no relational symbols, one functional symbol * of arity 2, and one constant symbol e. The language Ls of set theory has no functional or constant symbols, and only one relational symbol G of arity 2. Similarly, the only nonlogical symbol of the language L is the relational symbol of arity 2. In principle, set theory could be developed in L and the theory of partial orders could be expressed in Ls the difference is purely a matter of convention. Given a language L, one defines the set TerrriL of all terms of L as the smallest set T of finite strings of symbols of L that satisfies the following conditions: (i) Vi eT for all i G u (ii) ckeT for all k G K (hi) If to,...,tn-i eT, j G J, and n(j) = n, then ft(t0,....,tn-i) G T. The set ForrriL of all formulas of L is the smallest set of finite strings of symbols of L that satisfies the following conditions: (i) If s, t G Term then s = t G F (ii) If t0, ...,tn_i G Term, i G /, and ro(i) = n, then n(t 0 , ...,tn_i) G F (hi) If ^ and ^ are in F , then so are (/? A -0), (-•£), and ( 3 ^ (/?). The above definition of TerrriL and FornriL allows us to use induction and recursion over the wellfounded relations of being a subterm or a subformula. These techniques are commonly referred to as induction or recursion over the length of a term or formula. The occurrence of a variable Vi in a formula p is bound if it happens within the range of a quantifier 3vi. Otherwise it is called free. A formula without free variables is called a sentence. Let L be a first-order language with nonlogical symbols {r^ : i G 1} U {ft : j G J } U {cfc : k G K}. A model of L or an L-structure is a structure of the form 51 = (A, (Ri)iei, (Fj)jej, (Ck)keK) The set A is called the universe or underlying set of the model 21. For each i G /, Ri is a relation on A of arity ro(i) (i.e., Ri ^ A ro( ^) for each j £ J, Fj is a function from ATl^ into ^4 and for each k G K, Ck is an element of A. For example, if M is a set and G denotes the membership relation restricted to elements of M, then (M, G) is a model of Ls- Now let us recall what it means for a model of L to satisfy a sentence of L. A valuation (of the variables) is a function s that assigns an element of A to each natural number. Given s, we assign to each t G Term some t5 G A as follows: = *(i) £ = ?* / / ( * 0 , . . . , * r i ( j ) - l ) = ^ j ( * 0 » - J * r i ( j ) - l ) - By recursion over the length of formulas we define a relation (read as: "21 satisfies p under the valuation s." The relation |=s is called the satisfaction relation.) a(= f l t 0 = *i iff tg = tf a K n ( t o , . . . , ^ ( 0 - i ) iff ( ^ . . . ^ . ^ G f ^ 21 |=s -/? iff it is not the case that 21 \=s ip\
Previous Page Next Page