A logical language consists of:
Every function symbol, relation symbol, and connective is associated with an arity (the set of -ary function symbols is denoted , and similarly for relation symbols and connectives). Each quantifier is a generalized quantifier associated with a quantifier type .
The underlying logic has a (possibly empty) set of types . There is a function which assignes a type to each function and variable. For each arity is a function which gives the types of each of the arguments to a function symbol or relation. In addition, for each quantifier type there is a function defined on (the set of quantifiers of that type) which gives an -tuple of -tuples of types of the arguments taken by formulas the quantifier applies to.
The terms of of type are built as follows:
If is a variable such that then is a term of type
If is an -ary function symbol such that and are terms such that for each then is a term of type
The formulas of are built as follows:
If is an -ary relation symbol and are terms such that then is a formula
If is an -ary connective and are formulas then is a formula
If is a quantifier of type , are a sequence of variables such that and are formulas then is a formula
Generally the connectives, quantifiers, and variables are specified by the appropriate logic, while the function and relation symbols are specified for particular languages. Note that -ary functions are usually called constants.
If there is only one type which is equated directly with truth values then this is essentially a propositional logic. If the standard quantifiers and connectives are used, there is only one type, and one of the relations is (with its usual semantics), this produces first order logic. If the standard quantifiers and connectives are used, there are two types, and the relations include and with appropriate semantics, this is second order logic (a slightly different formulation replaces with a -ary function which represents function application; this views second order objects as functions rather than sets).
|Date of creation||2013-03-22 12:59:55|
|Last modified on||2013-03-22 12:59:55|
|Last modified by||Henry (455)|