|
|
|
Viewing Version
1
of
'logical language'
|
[ view 'logical language'
|
back to history
]
| Title of object: |
logical language |
| Canonical Name: |
LogicalLanguage |
| Type: |
Topic |
| Created on: |
2002-08-28 18:52:02.952302-04 |
| Modified on: |
2002-08-28 18:52:02.952302-04 |
| Classification: |
msc:03B15, msc:03B10 |
| Defines: |
term, formula |
Revision comment (for changes between this and next version):
| Changes for correction # (''). |
Preamble:
% this is the default PlanetMath preamble. as your knowledge
% of TeX increases, you will probably want to edit this, but
% it should be fine as is for beginners.
% almost certainly you want these
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
% used for TeXing text within eps files
%\usepackage{psfrag}
% need this for including graphics (\includegraphics)
%\usepackage{graphicx}
% for neatly defining theorems and propositions
%\usepackage{amsthm}
% making logically defined graphics
%\usepackage{xypic}
% there are many more packages, add them here as you need them
% define commands here
%\PMlinkescapeword{theory} |
Content:
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:
\begin{itemize}
\item Function symbols (common examples include $+$ and $\cdot$)
\item Relation symbols (common examples include $=$ and $<$)
\item Logical connectives (usually $\neg$, $\wedge$, $\vee$, $\rightarrow$ and $\leftrightarrow$)
\item Quantifiers (usuallly $\forall$ and $\exists$)
\item Variables
\end{itemize}
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$ 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:
\begin{enumerate}
\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 $f(t_1,\ldots,t_n)$ is a term of type $t$
\end{enumerate}
The formulas of $\mathcal{L}$ are build as follows:
\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 $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 $c(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}
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. |
|
|
|
|
|
