|
|
|
Revision difference : logical language |
| Version 2 |
Version 1 |
| In its most general form, a \emph{logical language} is a set of rules for constructing \emph{formulas} which allows truth values to be assigned to each formula. |
In its most general form, a \emph{logical language} is a set of rules for constructing \emph{formulas} which allows truth values to be assigned to each formula. |
| A logical languages $\mathcal{L}$ consists of: |
A logical languages $\mathcal{L}$ consists of: |
| \begin{itemize} |
\begin{itemize} |
| \item Function symbols (common examples include $+$ and $\cdot$) |
\item Function symbols (common examples include $+$ and $\cdot$) |
| \item Relation symbols (common examples include $=$ and $<$) |
\item Relation symbols (common examples include $=$ and $<$) |
| \item Logical connectives (usually $\neg$, $\wedge$, $\vee$, $\rightarrow$ and $\leftrightarrow$) |
\item Logical connectives (usually $\neg$, $\wedge$, $\vee$, $\rightarrow$ and $\leftrightarrow$) |
| \item Quantifiers (usuallly $\forall$ and $\exists$) |
\item Quantifiers (usuallly $\forall$ and $\exists$) |
| \item Variables |
\item Variables |
| \end{itemize} |
\end{itemize} |
|
Every function symbol, relation symbol, and connective is associated with an arity. Each quantifier is a generalized quantifier associated with a quantifier type $\langle n_1,\ldots,n_n\rangle$.
|
Every function symbol, relation symbol, and connective is associated with an arity. Each quantifier is associated with two arities.
|
|
Each language has some number of types (possibly infinite). The set of types of $\mathcal{L}$ is denoted $T$. There is a function $A$ defined on every function symbol and variable which gives the type of that function symbol or variable. There is also a function $I_n$ defined on each $n$-ary function $f$ and relation $R$ which gives an $n$-tuple of types and a function $Q_{\langle n_1,\ldots,n_n\rangle}$ defined on each quantifier of quantifier type $\langle n_1,\ldots,n_n\rangle$ which gives an $n$-tuple of $n_i$-tuples of types.
|
Each language has some number of types (possibly infinite). The set of types of $\mathcal{L}$ is denoted $T$. There is a function $A$ defined on every function symbol and variable which gives the type of that function symbol or variable. There is also a function $I_n$ defined on each $n$-ary function $f$ and relation $R$ and each $n,m$-ary quantifier $Q$ which gives an $n$-tuple of types.
|
| The terms of $\mathcal{L}$ of type $t\in T$ are built as follows: |
The terms of $\mathcal{L}$ of type $t\in T$ are built as follows: |
| \begin{enumerate} |
\begin{enumerate} |
| \item If $v$ is a variable such that $A(v)=t$ then $v$ is a term of type $t$ |
\item If $v$ is a variable such that $A(v)=t$ then $v$ is a term of type $t$ |
|
\item If $f$ is an $n$-ary function symbol such that $A(f)=t$ and $t_1,\ldots,t_n$ are terms such that $t_i$ is of type $(I_n(f))_n$ (the type of the $n$-th parameter of $f$) then $ft_1,\ldots,t_n$ is a term of type $t$
|
\item If $f$ is an $n$-ary function symbol such that $A(f)=t$ and $t_1,\ldots,t_n$ are terms such that $t_i$ is of type $(I_n(f))_n$ (the type of the $n$-th parameter of $f$) then $f(t_1,\ldots,t_n)$ is a term of type $t$
|
| \end{enumerate} |
\end{enumerate} |
|
The formulas of $\mathcal{L}$ are built as follows:
|
The formulas of $\mathcal{L}$ are build as follows:
|
| \begin{enumerate} |
\begin{enumerate} |
|
\item If $R$ is an $n$-ary relation symbol and $t_1,\ldots,t_n$ are terms such that $t_i$ is of type $(I_n(f))_n$ (the type of the $n$-th parameter of $f$) then $Rt_1,\ldots,t_n$ is a formula
|
\item If $R$ is an $n$-ary relation symbol and $t_1,\ldots,t_n$ are terms such that $t_i$ is of type $(I_n(f))_n$ (the type of the $n$-th parameter of $f$) then $R(t_1,\ldots,t_n)$ is a formula
|
|
\item If $c$ is an $n$-ary connective and $f_1,\ldots,f_n$ are formulas then $cf_1,\ldots,f_n$ is a formula
|
\item If $c$ is an $n$-ary connective and $f_1,\ldots,f_n$ are formulas then $c(f_1,\ldots,f_n)$ is a formula
|
|
\item 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 $A(v_{i,j})=((Q_{\langle n_1,\ldots,n_n\rangle})_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
|
\item If $Q$ is an $m,n$-ary quantifier, $v_1,\ldots, v_m$ are variables such that $A(v_i)=(I_m(Q))_i$, and $f_1,\ldots,f_n$ are formulas then $Q(v_1,\ldots,v_m,f_1,\ldots,f_n)$ is a formula
|
| \end{enumerate} |
\end{enumerate} |
| If there are no types, this is essentially propositional logic. If the standard quantifiers and connectives are used and 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). |
If there are no types, this is essentially propositional logic. If the standard quantifiers and connectives are used and 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. |
Note that often connectives are written with infix notation with parentheses used to control order of operations. |
|
|
|
|
