% Part: first-order-logic
% Chapter: syntax-and-semantics
% Section: first-order-languages

\documentclass[../../../include/open-logic-section]{subfiles}

\begin{document}

\olfileid{fol}{syn}{fol}

\olsection{First-Order Languages}


Expressions of first-order logic are built up from a basic vocabulary
containing \emph{!!{variable}s}, \emph{!!{constant}s},
\emph{!!{predicate}s} and sometimes \emph{!!{function}s}.  From them,
together with logical connectives, quantifiers, and punctuation
symbols such as parentheses and commas, \emph{terms} and
\emph{!!{formula}s} are formed.

\begin{explain}
Informally, !!{predicate}s are names for properties and relations,
!!{constant}s are names for individual objects, and !!{function}s are
names for mappings.  These, except for the !!{identity}~$\eq$, are the
\emph{non-logical symbols} and together make up a language.  Any
first-order language~$\Lang L$ is determined by its non-logical
symbols.  In the most general case, $\Lang L$ contains infinitely many
symbols of each kind.
\end{explain}

In the general case, we make use of the following symbols in
first-order logic:

\begin{enumerate}
\item Logical symbols
\begin{enumerate}
\item Logical connectives:
  \startycommalist
  \iftag{prvNot}{\ycomma $\lnot$ (negation)}{}%
  \iftag{prvAnd}{\ycomma $\land$ (conjunction)}{}%
  \iftag{prvOr}{\ycomma $\lor$ (disjunction)}{}%
  \iftag{prvIf}{\ycomma $\lif$ (!!{conditional})}{}%
  \iftag{prvIff}{\ycomma $\liff$ (!!{biconditional})}{}%
  \iftag{prvAll}{\ycomma $\lforall$ (universal quantifier)}{}%
  \iftag{prvEx}{\ycomma $\lexists$ (existential quantifier)}{}.
\tagitem{prvFalse}{The propositional constant for !!{falsity}~$\lfalse$.}{}
\tagitem{prvTrue}{The propositional constant for !!{truth}~$\ltrue$.}{}
\item The two-place !!{identity}~$\eq$.
\item A !!{denumerable}s set of !!{variable}s: $\Obj v_0$, $\Obj v_1$, $\Obj
  v_2$, \dots
\end{enumerate}
\item Non-logical symbols, making up the \emph{standard
  language} of first-order logic
\begin{enumerate}
\item A !!{denumerable}s set of $n$-place !!{predicate}s for each $n>0$: $\Obj
  A^n_0$, $\Obj A^n_1$, $\Obj A^n_2$, \dots
\item A !!{denumerable}s set of !!{constant}s: $\Obj c_0$, $\Obj c_1$, $\Obj
  c_2$, \dots.
\item A !!{denumerable}s set of $n$-place !!{function}s for each $n>0$:
  $\Obj f^n_0$, $\Obj f^n_1$, $\Obj f^n_2$, \dots
\end{enumerate}
\item Punctuation marks: (, ), and the comma.
\end{enumerate}

Most of our definitions and results will be formulated for the full
standard language of first-order logic.  However, depending on the
application, we may also restrict the language to only a few
!!{predicate}s, !!{constant}s, and !!{function}s.

\begin{ex}
The language~$\Lang L_A$ of arithmetic contains a single two-place
!!{predicate}~$<$, a single !!{constant}~$\Obj 0$, one one-place
!!{function}~$\prime$, and two two-place !!{function}s~$+$ and~$\times$.
\end{ex}

\begin{ex}
The language of set theory~$\Lang L_Z$ contains only the single
two-place !!{predicate}~$\in$.
\end{ex}

\begin{ex}
The language of orders~$\Lang L_\le$ contains only the two-place
!!{predicate}~$\le$.
\end{ex}

Again, these are conventions: officially, these are just aliases,
e.g., $<$, $\in$, and $\le$ are aliases for $\Obj A^2_0$, $\Obj 0$ for
$\Obj c_0$, $\prime$ for $\Obj f^1_0$, $+$ for $\Obj f^2_0$, $\times$ for
$\Obj f^2_1$.

\iftag{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}{%
In addition to the primitive connectives and
\iftag{notprvEx,notprvAll}{quantifier}{quantifiers} introduced
above, we also use the following \emph{defined} symbols:
\startycommalist
  \iftag{defNot}{\ycomma $\lnot$ (negation)}{}%
  \iftag{defAnd}{\ycomma $\land$ (conjunction)}{}%
  \iftag{defOr}{\ycomma $\lor$ (disjunction)}{}%
  \iftag{defIf}{\ycomma $\lif$ (!!{conditional})}{}%
  \iftag{defIff}{\ycomma $\liff$ (!!{biconditional})}{}%
  \iftag{defAll}{\ycomma $\lforall$ (universal quantifier)}{}%
  \iftag{defEx}{\ycomma $\lexists$ (existential quantifier)}{}%
  \iftag{defFalse}{\ycomma !!{falsity}~$\lfalse$}{}%
  \iftag{defTrue}{\ycomma !!{truth}~$\ltrue$}}{}.

\begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll}
\begin{explain}
A defined symbol is not officially part of the language, but is
introduced as an informal abbreviation: it allows us to abbreviate
formulas which would, if we only used primitive symbols, get quite
long.  This is obviously an advantage.  The bigger advantage, however,
is that proofs become shorter.  If a symbol is primitive, it has to be
treated separately in proofs. The more primitive symbols, therefore,
the longer our proofs.
\end{explain}
\end{tagblock}

% Alternate symbols

\begin{intro}
You may be familiar with different terminology and symbols than the
ones we use above. Logic texts (and teachers) commonly use 
$\sim$, $\neg$, or~!\ for ``negation'', $\wedge$, $\cdot$, or $\&$
for ``conjunction''.  Commonly used symbols for the ``conditional'' or
``implication'' are $\rightarrow$, $\Rightarrow$, and $\supset$.
\iftag{prvIff,defIff}{Symbols for ``biconditional,'' ``bi-implication,''
  or ``(material) equivalence'' are $\leftrightarrow$,
  $\Leftrightarrow$, and $\equiv$.}{}
\iftag{prvFalse,defFalse}{The $\lfalse$ symbol is variously called
  ``falsity,'' ``falsum,'', ``absurdity,'' or ``bottom.''}{}
\iftag{prvTrue,defTrue}{The $\ltrue$ symbol is variously called
  ``truth,'' ``verum,'' or ``top.''}{}

It is conventional to use lower case letters (e.g., $a$, $b$, $c$) from
the beginning of the Latin alphabet for !!{constant}s (sometimes called
names), and lower case letters from the end (e.g., $x$, $y$, $z$) for
!!{variable}s. Quantifiers combine with !!{variable}s, e.g., $x$;
notational variations include $\forall x$, $(\forall x)$, $(x)$, $\Pi x$,
$\bigwedge_x$ for the universal quantifier and $\exists x$, $(\exists
x)$, $(Ex)$, $\Sigma x$, $\bigvee_x$ for the existential quantifier.
\end{intro}

\begin{explain}
We might treat all the propositional operators and both quantifiers as
primitive symbols of the language.  We might instead choose a smaller
stock of primitive symbols and treat the other !!{operator}s as
defined. ``Truth functionally complete'' sets of Boolean operators
include $\{ \lnot, \lor \}$, $\{ \lnot, \land \}$, and $\{ \lnot,
\lif\}$---these can be combined with either quantifier for an
expressively complete first-order language.

You may be familiar with two other !!{operator}s: the Sheffer
stroke~$|$ (named after Henry Sheffer), and Peirce's
arrow~$\downarrow$, also known as Quine's dagger.  When given their
usual readings of ``nand'' and ``nor'' (respectively), these operators
are truth functionally complete by themselves.
\end{explain}

\end{document}