## You are here

Homelogical language

## Primary tabs

# 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 $\neg$, $\wedge$, $\vee$, $\rightarrow$ 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 $\langle n_{1},\ldots,n_{n}\rangle$.

The underlying logic has a (possibly empty) set of types $T$. There is a function^{} $\operatorname{Type}:F\cup V\rightarrow T$ which assignes a type to each function and variable. For each arity $n$ is a function $\operatorname{Inputs}_{n}:F_{n}\cup R_{n}\rightarrow T^{n}$ which gives the types of each of the arguments to a function symbol or relation^{}. In addition^{}, for each quantifier type $\langle n_{1},\ldots,n_{n}\rangle$ there is a function $\operatorname{Inputs}_{{\langle n_{1},\ldots,n_{n}\rangle}}$ defined on $Q_{{\langle n_{1},\ldots,n_{n}\rangle}}$ (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 $\operatorname{Type}(v)=t$ then $v$ is a term of type $t$

- 2.
If $f$ is an $n$-ary function symbol such that $\operatorname{Type}(f)=t$ and $t_{1},\ldots,t_{n}$ are terms such that for each $i<n$ $\operatorname{Type}(t_{i})=(\operatorname{Inputs}_{n}(f))_{i}$ then $ft_{1},\ldots,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},\ldots,t_{n}$ are terms such that $\operatorname{Type}(t_{i})=(\operatorname{Inputs}_{n}(r))_{i}$ then $rt_{1},\ldots,t_{n}$ is a formula

- 2.
If $c$ is an $n$-ary connective and $f_{1},\ldots,f_{n}$ are formulas then $cf_{1},\ldots,f_{n}$ is a formula

- 3.
If $q$ is a quantifier of type $\langle n_{1},\ldots,n_{n}\rangle$, $v_{{1,1}},\ldots,v_{{1,n_{1}}},v_{{2,1}},\ldots,v_{{n,1}},\ldots,v_{{n,n_{n}}}$ are a sequence of variables such that $\operatorname{Type}(v_{{i,j}})=((\operatorname{Inputs}_{{\langle n_{1},\ldots,% n_{n}\rangle}}(q))_{j})_{i}$ and $f_{1},\ldots,f_{n}$ are formulas then $qv_{{1,1}},\ldots,v_{{1,n_{1}}},v_{{2,1}},\ldots,v_{{n,1}},\ldots,v_{{n,n_{n}}% }f_{1},\ldots,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.

## Mathematics Subject Classification

03B15*no label found*03B10

*no label found*

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff
- Corrections

## Corrections

"By" by gumau ✓

formula 3 needs connective by cppLarry ✘

typo by norm ✓

linking restriction by akrowne ✓