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 $ℒ$ 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 $⟨n_1,\mathrm{\dots },n_n⟩$.

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 $⟨n_1,\mathrm{\dots },n_n⟩$ there is a function ${\mathrm{Inputs}}_{⟨n_1,\mathrm{\dots },n_n⟩}$ defined on $Q_{⟨n_1,\mathrm{\dots },n_n⟩}$ (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 $ℒ$ 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 $ℒ$ 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 $⟨n_1,\mathrm{\dots },n_n⟩$, $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}}_{⟨n_1,\mathrm{\dots },n_n⟩}(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.