logical language (original) (raw)
In its most general form, a logical language is a set of rules for constructing formulas for some logic, which can then be assigned truth values based on the rules of that logic.
A logical language ℒ consists of:
- •
- •
A set R of relation symbols (common examples include = and <) - •
- •
- •
Every function symbol, relation symbol, and connective is associated with an arity (the set of n-ary function symbols is denoted Fn, and similarly for relation symbols and connectives). Each quantifier is a generalized quantifier associated with a quantifier type ⟨n1,…,nn⟩.
The underlying logic has a (possibly empty) set of types T. There is a function Type:F∪V→T which assignes a type to each function and variable. For each arity n is a function Inputsn:Fn∪Rn→Tn which gives the types of each of the arguments to a function symbol or relation. In addition
, for each quantifier type ⟨n1,…,nn⟩ there is a function Inputs⟨n1,…,nn⟩ defined on Q⟨n1,…,nn⟩ (the set of quantifiers of that type) which gives an n-tuple of ni-tuples of types of the arguments taken by formulas the quantifier applies to.
The terms of ℒ of type t∈T are built as follows:
- If v is a variable such that Type(v)=t then v is a term of type t
- If f is an n-ary function symbol such that Type(f)=t and t1,…,tn are terms such that for each i<n Type(ti)=(Inputsn(f))i then ft1,…,tn is a term of type t
The formulas of ℒ are built as follows:
- If r is an n-ary relation symbol and t1,…,tn are terms such that Type(ti)=(Inputsn(r))i then rt1,…,tn is a formula
- If c is an n-ary connective and f1,…,fn are formulas then cf1,…,fn is a formula
- If q is a quantifier of type ⟨n1,…,nn⟩, v1,1,…,v1,n1,v2,1,…,vn,1,…,vn,nn are a sequence
of variables such that Type(vi,j)=((Inputs⟨n1,…,nn⟩(q))j)i and f1,…,fn are formulas then qv1,1,…,v1,n1,v2,1,…,vn,1,…,vn,nnf1,…,fn is a formula
- If q is a quantifier of type ⟨n1,…,nn⟩, v1,1,…,v1,n1,v2,1,…,vn,1,…,vn,nn are a sequence
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 0-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 2-ary function which represents function application; this views second order objects as functions rather than sets).