logical language
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 $\mathcal{L}$ consists of:

•
A set $F$ of function symbols (common examples include $+$ and $\cdot $)

•
A set $R$ of relation symbols (common examples include $=$ and $$)

•
A set $C$ of logical connectives (usually $\mathrm{\neg}$, $\wedge $, $\vee $, $\to $ and $\leftrightarrow $)

•
A set $Q$ of quantifiers^{} (usuallly $\forall $ and $\exists $)

•
A set $V$ of variables
Every function symbol, relation symbol, and connective is associated with an arity (the set of $n$ary function symbols is denoted ${F}_{n}$, and similarly for relation symbols and connectives). Each quantifier is a generalized quantifier associated with a quantifier type $\u27e8{n}_{1},\mathrm{\dots},{n}_{n}\u27e9$.
The underlying logic has a (possibly empty) set of types $T$. There is a function $\mathrm{Type}:F\cup V\to T$ which assignes a type to each function and variable. For each arity $n$ is a function ${\mathrm{Inputs}}_{n}:{F}_{n}\cup {R}_{n}\to {T}^{n}$ which gives the types of each of the arguments to a function symbol or relation^{}. In addition^{}, for each quantifier type $\u27e8{n}_{1},\mathrm{\dots},{n}_{n}\u27e9$ there is a function ${\mathrm{Inputs}}_{\u27e8{n}_{1},\mathrm{\dots},{n}_{n}\u27e9}$ defined on ${Q}_{\u27e8{n}_{1},\mathrm{\dots},{n}_{n}\u27e9}$ (the set of quantifiers of that type) which gives an $n$tuple of ${n}_{i}$tuples of types of the arguments taken by formulas the quantifier applies to.
The terms of $\mathcal{L}$ of type $t\in T$ are built as follows:

1.
If $v$ is a variable such that $\mathrm{Type}(v)=t$ then $v$ is a term of type $t$

2.
If $f$ is an $n$ary function symbol such that $\mathrm{Type}(f)=t$ and ${t}_{1},\mathrm{\dots},{t}_{n}$ are terms such that for each $$ $\mathrm{Type}({t}_{i})={({\mathrm{Inputs}}_{n}(f))}_{i}$ then $f{t}_{1},\mathrm{\dots},{t}_{n}$ is a term of type $t$
The formulas of $\mathcal{L}$ are built as follows:

1.
If $r$ is an $n$ary relation symbol and ${t}_{1},\mathrm{\dots},{t}_{n}$ are terms such that $\mathrm{Type}({t}_{i})={({\mathrm{Inputs}}_{n}(r))}_{i}$ then $r{t}_{1},\mathrm{\dots},{t}_{n}$ is a formula

2.
If $c$ is an $n$ary connective and ${f}_{1},\mathrm{\dots},{f}_{n}$ are formulas then $c{f}_{1},\mathrm{\dots},{f}_{n}$ is a formula

3.
If $q$ is a quantifier of type $\u27e8{n}_{1},\mathrm{\dots},{n}_{n}\u27e9$, ${v}_{1,1},\mathrm{\dots},{v}_{1,{n}_{1}},{v}_{2,1},\mathrm{\dots},{v}_{n,1},\mathrm{\dots},{v}_{n,{n}_{n}}$ are a sequence^{} of variables such that $\mathrm{Type}({v}_{i,j})={({({\mathrm{Inputs}}_{\u27e8{n}_{1},\mathrm{\dots},{n}_{n}\u27e9}(q))}_{j})}_{i}$ and ${f}_{1},\mathrm{\dots},{f}_{n}$ are formulas then $q{v}_{1,1},\mathrm{\dots},{v}_{1,{n}_{1}},{v}_{2,1},\mathrm{\dots},{v}_{n,1},\mathrm{\dots},{v}_{n,{n}_{n}}{f}_{1},\mathrm{\dots},{f}_{n}$ 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 $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 $\in $ with appropriate semantics, this is second order logic (a slightly different formulation replaces $\in $ with a $2$ary function which represents function application; this views second order objects as functions rather than sets).
Note that often connectives are written with infix notation with parentheses used to control order of operations.
Title  logical language 

Canonical name  LogicalLanguage 
Date of creation  20130322 12:59:55 
Last modified on  20130322 12:59:55 
Owner  Henry (455) 
Last modified by  Henry (455) 
Numerical id  14 
Author  Henry (455) 
Entry type  Definition 
Classification  msc 03B15 
Classification  msc 03B10 
Related topic  QuantifierFree 
Defines  term 
Defines  formula 
Defines  constant 