\chapter{Propositional model-theory}

This chapter is inspired in part by \cite[\S~1.2]{MR0409165}.
Generally, the term \tech{model-theory} refers to first-order
model-theory, because the logic it uses is first-order logic.  The
notion of \tech{structure} defined in ch.~\ref{ch:intro} is the notion
as used in first-order model-theory.
However, some model-theoretic ideas can be worked out in the simpler
context of propositional logic.  This is what is done here.  In
particular, a simpler notion of \tech{structure} will be introduced,
albeit one that retains the fundamental idea of providing an
interpretation for symbols.

  Our official signature for propositional logic will be
  \begin{equation*}
    \{\to,\lnot{}\}.
  \end{equation*}
Let $V$ be our set $\{P_k:k\in\varN\}$ of propositional variables.
For the sake of a precise definition of \tech{formula}, let $S$ be the set
of all finite strings (or sequences) of symbols 
from the set
\begin{equation*}
V\cup\{\mathord{\to},\mathord{\lnot}\}\cup\{\mathord (,\mathord )\}.
%  V\cup\{{}\to{},\lnot{}\}\cup\{{}\mathrel({},{}\mathrel){}\}.
\end{equation*}
Now let $\family U$ be the subset of $\pow S$ comprising the subsets $N$
of $S$ such that:
\begin{mylist}
  \item
$V\included N$, that is, $N$ contains all elements of $V$ (when these
    are considered as sequences of \tech{length} $1$);
\item
for all $F$ in $S$, if $F\in N$, then $\lnot F\in N$;
\item
for all $F$ and $G$ in $S$,
if $F$ and $G$ are in $N$, then $(F\to G)\in N$.
\end{mylist}
Let $\Fm{}{}=\bigcap\family U$.  This is just the set of propositional
\defn{formulas} in the signature $\{\to,\lnot\}$.  Throughout
this chapter, all formulas are elements of $\Fm{}{}$.

In particular, by construction, $\Fm{}{}$ is the \emph{smallest}
subset $N$ of $S$ with the properties above.
We may say that the definition of $\Fm{}{}$ is \defn{inductive},
because it makes proof by
\defn{induction} on formulas possible:  If $N\included\Fm{}{}$, then,
to prove $N=\Fm{}{}$, it is enough to show that
$N$ has the properties
($*$, $\dagger$, $\ddag$) above.

As a first example of proof by induction on formulas, we have the next
lemma below.  We first make some (obvious) definitions:

If $s_0$, $s_1$, \dots, and $s_{n-1}$ are symbols, then the \defn{length}
of the string $s_0s_1\dotsb s_{n-1}$ is $n$; and the 
string \defn{begins} with $s_0$.  An
\defn{initial segment} of the string is one of the strings
$s_0s_1\dotsb s_{k-1}$, where $k\leq n$.  The initial segment is
\defn{proper} if $k<n$.


\begin{lemma}\label{lem:formulas}
\mbox{}
\begin{mylist}
\item
Every formula has positive length.
\item
Every formula of length $1$ is a variable.
\item
Every formula of length greater than $1$ begins with $\lnot$ or $($.
  \item
Every formula beginning with $\lnot$ is $\lnot F$ for some
\emph{formula} $F$.
\item
Every formula beginning with $($ is $(F\to G)$ for some
  \emph{formulas} $F$ and~$G$.
\end{mylist}
\end{lemma}

\begin{proof}
By induction on formulas.  Let $N$ be the set of formulas $F$
such that: 
\begin{mylist}
\item
$F$ has positive length;
  \item
if $F$ has length $1$, then $F$ is a variable;
\item
if $F$ has length greater than $1$, then $F$ begins with $\lnot$ or
$($;
\item
if $F$ is $\lnot E$ for some string $E$, then $E$ is a formula;
\item
if $F$ begins with $($, then $F$ is $(G\to H)$ for some formulas $G$
and $H$.
\end{mylist}
Then $N$ contains the variables, and $N$ contains $\lnot F$ and $(F\to
G)$ if it contains $F$ and $G$.  Hence $N=\Fm{}{}$.
\end{proof}

Definition of functions on $\Fm{}{}$ by \defn{recursion} is
possible, because of the next theorem below.  This will use another
lemma.  Now, because formulas have lengths, this lemma---and other
facts about formulas---can 
be proved by induction (usually strong induction) \emph{on these
  lengths}:  

\begin{lemma}
  No proper initial segment of a formula is a formula.
\end{lemma}

\begin{proof}
Let $N$ be the set of formulas of which no proper
initial segment is a formula.  We shall prove by strong induction on
the lengths of formulas that
$N=\Fm{}{}$.  Suppose $N$ contains all formulas \emph{shorter} than a
formula $F$.
By Lemma~\ref{lem:formulas}, we know that $F$ is a variable $P$ or a
formula $\lnot
G$ or $(G\to H)$, where $G$ and $H$ are formulas.  The only
proper initial segment of $P$ is the empty string, which is not a
formula.  Any proper initial segment of $\lnot G$ is $\lnot
G'$ for some initial segment $G'$ of $G$; so $G'$ is not a formula, by
strong inductive hypothesis; hence $\lnot G'$ is not a formula.
Finally, and similarly, any initial segment of $(G\to H)$ is
$(G'\to H')$ for some formulas $G'$ and $H'$.  Then one of $G$ and $G'$
is an initial segment of the other.  But each one is shorter than $F$;
so by strong inductive hypothesis, $G$ and $G'$ are the same formula.
Then $H'$ is a proper initial segment of $H$; so \emph{these} formulas
must be the same.  Thus, in all cases, $F\in N$.  By strong induction,
$N=\Fm{}{}$. 
\end{proof}

We need not use induction again to prove the following:

\begin{theorem}[Unique Readability]\label{thm:UR}
  If $F$ is a formula, then $F$ satisfies exactly one of the following
  conditions:
  \begin{mylist}
    \item
$F\in V$;
\item
$F$ is $\lnot G$ for some formula $G$;
\item
$F$ is $(G\to H)$ for some \emph{unique} formulas $G$ and $H$.
  \end{mylist}
\end{theorem}

\begin{proof}
Every formula is a variable or is $\lnot F$ or $(F\to G)$ for some
formulas $F$ and $G$.  Suppose $(F\to G)$ is
also $(F'\to G')$, where $F'$ and $G'$ are also formulas.  Then (as in
the previous proof) one of $F$ and $F'$ is an initial segment of the
other.  By the last lemma, this means $F$ and $F'$ are the same, so
$G$ and $G'$ must be the same.
\end{proof}

\begin{corollary}[Recursion]%\label{thm:recursion}
  Let $f_{\lnot}$ be a unary, and $f_{\to}$ a binary, operation on
  some set.  Let $g$ be a function from $V$ into that set.  Then $g$
  extends uniquely to the domain $\Fm{}{}$ so that
  \begin{mylist}
    \item
$g(\lnot F)=f_{\lnot}(g( F))$,
\item
$g((F\to G))=f_{\to}(g(F),g(G))$
  \end{mylist}
for all $F$ and $G$ in $\Fm{}{}$.
\end{corollary}


\begin{proof}
  Not important.  The idea is to let $G$ be the set of all
  \emph{relations} with the desired properties of $g$ (except the
  property of being a function), and then to show that $\bigcap G$ is
  in $G$ and is in fact a function.  See
  \cite[Theorem~5.2.1]{111-2004}. 
\end{proof}



Notationally, we suppose:
\begin{mylist}
  \item
$P$, $Q$, $R$, \dots are in $V$;
\item
$F$, $G$, $H$, \dots are in $\Fm{}{}$;
\end{mylist}
These symbols can be called
\defn{syntactical} variables, since their possible values are symbols
and strings of symbols in the formal logic that we are studying.
(There is some discussion of this terminology in
\cite[\S08]{MR18:631a}.) 

We also let $\tuple e=(e_0,\dots,e_{n-1})\in \B^n$ for an appropriate
  $n$ in $\varN$, where $\B=\{0,1\}$.


The formula $F$ is $n$-ary if its variables come from $\{P_k:k<n\}$.
Under this definition, the $n$-ary formulas are also $(n+1)$-ary.  The
set of $n$-ary formulas can be denoted
\begin{equation*}
  \Fm n{}.
\end{equation*}
Note that this set has an inductive definition, and definition by
recursion of functions on $\Fm n{}$ is possible.  (\textbf{Exercise:}
how can the inductive definition of $\Fm{}{}$ be adapted to an inductive
definition of $\Fm n{}$?)

We can understand $\lnot$ to be the unary operation on $\B$ given by
\begin{center}
  \begin{tabular}{c | c}
$e$ & $\lnot e$\\ \hline
$0$ & $1$\\
$1$ & $0$
  \end{tabular},
\end{center}
and $\to$ to be the binary operation on $\B$ given by
\begin{center}
  \begin{tabular}{c|c|c}
    $e_0$ & $e_1$ & $e_0\to e_1$ \\ \hline
$0$ & $0$ & $1$\\
$1$ & $0$ & $0$\\
$0$ & $1$ & $1$\\
$1$ & $1$ & $1$
  \end{tabular}.
\end{center}
These agree with the definitions given on p.~\pageref{page:lnot}.
Then we have a unique function $F\mapsto\widehat F$ from $\Fm n{}$
into $\B^{\B^n}$ such that:
\begin{mylist}
  \item
$\widehat P_k$ is $\tuple e\mapsto e_k$, if $k<n$;
\item
$\widehat F(\tuple e)=\lnot (\widehat G(\tuple e))$, if $F$ is $\lnot
  G$;
\item
$\widehat F(\tuple e)=\widehat G(\tuple e)\to\widehat H(\tuple e)$, if
  $F$ is $(G\to H)$.
\end{mylist}
A \defn{truth-assignment} for an $n$-ary formula $F$ is an element
$\tuple e$ of 
$\B^n$; the element $\widehat F(\tuple e)$ of $\B$
is the
\defn{value} of $F$ at $\tuple e$.
The computation of this value is a finite procedure, and depends only
on those $e_k$ such that $P_k$ actually appears in $F$.  
\begin{example}\label{example:compute}
  Let $F$ be $(P_0\to (\lnot P_1\to P_2))$.  Let $G$ be $(\lnot P_1\to
  P_2)$.  Then
  \begin{align*}
    \widehat F(\tuple e)=1&\Iff \widehat P_0(\tuple e)\leq \widehat
    G(\tuple e)\\ 
&\Iff e_0\leq \widehat G(\tuple e)\\
&\Iff e_0=0 \text{ or } (e_1+1)\leq e_2\\
&\Iff e_0=0 \text{ or } e_1=1 \text{ or } e_2=1.
  \end{align*}
\end{example}

We write
\begin{equation*}
  \proves F
\end{equation*}
if $\widehat F(\tuple e)=1$ for all truth-assignments $\tuple e$ for
$F$; in this case, $F$ is a \defn{tautology}.  Otherwise, we write
\begin{equation*}
  \nproves F.
\end{equation*}
The question of whether $F$ is a tautology can be answered by
computing its
\defn{truth-table}, namely:
\begin{center}
  \begin{tabular}{c|c|c|c}
$P_0$ & $\dots$ & $P_{n-1}$ & $F$\\ \hline
$\vdots$ & & $\vdots$ & $\vdots$\\
$e_0$ & $\dots$ & $e_{n-1}$ & $\widehat F(\tuple e)$\\
$\vdots$ & & $\vdots$ & $\vdots$
  \end{tabular}.
\end{center}
(See also \cite[\S~2.3]{111-2004}.)

\section{Formal proofs}

Let us use $\Sigma$ as a syntactical variable for sets of formulas.
For us, a \defn{formal proof}
or a \defn{deduction}
of $F$ from $\Sigma$ will be a finite sequence
\begin{equation*}
  G_0,\dots,G_n
\end{equation*}
of formulas, where:
\begin{mylist}
  \item
$G_n$ is $F$;
\item
for each $k$ less than $n+1$,
$G_k$ is a tautology, or $G_k$ is in $\Sigma$, or there are $i$ and $j$ less
than $k$ such that $G_j$ is $(G_i\to G_k)$.
\end{mylist}
In terms of \cite[\S~2.9]{111-2004}, we are using the proof-system
whose only \defn{axioms} are the
tautologies, and whose only \defn{rule of inference} is \emph{modus
  ponens}.
If there is such a deduction, we write
\begin{equation*}
  \Sigma\proves F,
\end{equation*}
and we can say that $F$ is \defn{deducible} from $\Sigma$; we can also
say that the elements of $\Sigma$ are \defn{hypotheses} in the
deduction. 

We may write deductions vertically, so as to justify each step; but
the deduction itself is just a finite sequence of formulas:

\begin{examples}\label{examples:deductions}\mbox{}
  \begin{mylist}
    \item
$\{F,(F\to G)\}\proves G$, by the deduction
      \begin{align*}
	&F&&\text{[hypothesis]}\\
&(F\to G)&&\text{[hypothesis]}\\
&G&&\text{[\emph{modus ponens}]}
      \end{align*}
\item
If $\proves(F\to G)$, then $\{F\}\proves G$ by the deduction
\begin{align*}
  &F&&\text{[hypothesis]}\\
&(F\to G)&&\text{[axiom]}\\
&G&&\text{[\emph{modus ponens}]}
\end{align*}
(The formal proof is the same, but the justifications are not.)
\item
 $\{(P\to(Q\to R)),(P\to Q)\}\proves (P\to R)$; finding the deduction is an
 \textbf{exercise}. 
  \end{mylist}
\end{examples}

Something to think about is whether there are procedures:
\begin{mylist}
  \item
for determining whether $\Sigma\proves F$;
\item
for finding the proof, if it exists.
\end{mylist}

\begin{lemma}
  If $G_0,\dots,G_n$ is a formal proof, and $k\leq n$, then
  $G_0,\dots,G_k$ is a formal proof.
\end{lemma}

\begin{proof}
  Immediate from the definition.
\end{proof}


\begin{lemma}\label{lem:fin}
  $\Sigma\proves F$ just in case $\Sigma_0\proves F$ for some finite
  subset $\Sigma_0$ of $\Sigma$.
\end{lemma}

\begin{proof}
  ($\Rightarrow$)  Say there is a formal proof $G_0,\dots,G_n$ of $F$
  from $\Sigma$.  Let
  \begin{equation*}
    \Sigma_0=\Sigma\cap\{G_0,\dots,G_n\}.
  \end{equation*}
Then $G_0,\dots,G_n$ is a formal proof of $F$ from $\Sigma_0$, and
$\Sigma_0$ is a finite subset of $\Sigma$.

($\Leftarrow$)  A formal proof from $\Sigma_0$ is a formal proof from
any set that includes $\Sigma_0$.
\end{proof}

\begin{lemma}
  $\proves F\Iff\emptyset\proves F$.
\end{lemma}

\begin{proof}
($\Rightarrow$)  If $\proves F$, then $F$ is a one-step derivation of
  itself from $\emptyset$, so $\emptyset\proves F$.

($\Leftarrow$)  We argue by strong induction on the lengths of deductions.
  Suppose that $F$ is a tautology whenever $F$ has a deduction from
  $\emptyset$ of length less than $n+1$.  Now suppose that
  \begin{equation*}
    G_0,\dots,G_{n-1},F
  \end{equation*}
is a deduction (which has length $n+1$) of $F$.  Then either $F$ is a
tautology, or there are
$i$ and $j$ less than $n$ such that
$G_j$ is $(G_i\to F)$.  In the latter case, by inductive hypothesis,
both $G_i$ and $(G_i\to F)$ are tautologies.  But the value of
$(G_i\to F)$ at $\tuple e$ is just $\widehat F(\tuple e)$, if
$\widehat G_i(\tuple e)=1$.  Hence $F$ is a tautology.  By induction,
all formulas deducible from $\emptyset$ are tautologies.
\end{proof}

We are sometimes more interested in knowing \emph{whether} a deduction
exists than in what it is.  Towards developing this knowledge, we
have: 

\begin{lemma}\label{lem:idempotent}
Suppose $\{F:\Sigma\proves
  F\}\proves G$.  Then 
  $\Sigma\proves G$, that is, $G$ is already in the set
  $\{F:\Sigma\proves F\}$.
\end{lemma}

\begin{proof}
  Let $\Sigma^*=\{F:\Sigma\proves F\}$.  
  In a deduction of $G$ from $\Sigma^*$, if an element of
  $\Sigma^*$ appears, then replace it with its deduction from
  $\Sigma$.  The result is then itself a deduction from $\Sigma$.
\end{proof}

A useful application of the lemma is:

\begin{theorem}[\emph{Modus Ponens}]\label{thm:MP}
  If $\Sigma\proves F$ and $\Sigma\proves(F\to G)$, then
  $\Sigma\proves G$.
\end{theorem}

\begin{proof}
Let $\Sigma^*=\{H:\Sigma\proves H\}$.  If $F$ and $(F\to G)$ are in
$\Sigma^*$, then $G$ has a three-line proof from $\Sigma^*$ as in one
of the Examples~\ref{examples:deductions} above.  Hence $\Sigma\proves
G$, by the last lemma. 
\end{proof}


A set $\Sigma$ of formulas is \defn{inconsistent} if
$\Sigma\proves\lnot F$ for some $F$ in $\Sigma$; otherwise, $\Sigma$
is \defn{consistent}.
A formula $F$ is a \defn{contradiction} if $\lnot F$ is a tautology.
There are various ways to express inconsistency:

\begin{lemma}\label{lem:consistency}
  The following are equivalent:
  \begin{mylist}
    \item
$\Sigma$ is inconsistent;
\item
$\Sigma\proves F$ and $\Sigma\proves\lnot F$ for some $F$;
\item
$\Sigma\proves F$ for all $F$;
\item
a contradiction is deducible from $\Sigma$.
  \end{mylist}
\end{lemma}

\begin{proof}
$(*)\Rightarrow(\dagger)$.  If $\Sigma$ is inconsistent, then $\Sigma\proves
  \lnot F$ for some
  $F$ in $\Sigma$; but then $\Sigma\proves F$ also.

$(\dagger)\Rightarrow(\ddag)$.  Say $\Sigma\proves F$ and
  $\Sigma\proves\lnot F$.  But $\proves (F\to(\lnot F\to G))$ for all
  $G$ (by an \textbf{exercise}).  By two applications of \emph{Modus
  Ponens}, $\Sigma\proves G$.

$(\ddag)\Rightarrow(\S)$.  Immediate.

$(\S)\Rightarrow(*)$.
Suppose $F$ is a contradiction, and $\Sigma\proves F$.  Then
  $\Sigma\neq\emptyset$, since only tautologies are derivable from
  $\emptyset$.  Hence there is $G$ in $\Sigma$.  But $\proves (F\to
\lnot G)$ (by an \textbf{exercise}), so $\Sigma\proves\lnot G$ by
\emph{Modus Ponens}.
\end{proof}

\begin{lemma}\label{lem:incon-con}
\mbox{}
\begin{mylist}
  \item
    $\Sigma$ is inconsistent just in case
  some finite subset of $\Sigma$ is inconsistent.
\item
$\Sigma$ is consistent just in case $\{F:\Sigma\proves F\}$ is
  consistent.
\end{mylist}
\end{lemma}

\begin{proof}
  \textbf{Exercise}.
\end{proof}

\begin{theorem}[Deduction]
$\Sigma\proves(F\to G)$ if and only if $\Sigma\cup\{F\}\proves G$.
\end{theorem}

\begin{proof}
($\Rightarrow$)  \textbf{Exercise.}

($\Leftarrow$)
We use strong induction on the lengths of deductions.  Suppose the
claim holds when $G$ has a formal proof of length less than $n+1$.
Suppose also that
$H_0,\dots,H_{n-1},G$ is a formal proof of $G$ from
$\Sigma\cup\{F\}$.  Now,
\begin{equation*}
  \proves(G\to (F\to G))
\end{equation*}
(by an \textbf{exercise}).
Hence, if $G\in\Sigma$ or $G$ is a tautology, then
\begin{equation*}
  \Sigma\proves(F\to G)
\end{equation*}
by \emph{Modus Ponens}.  The other possibility is that $H_j$ is
$(H_i\to G)$ for some $i$ and 
$j$ in $n$. Then $\Sigma\proves(F\to
H_i)$ and $\Sigma\proves(F\to(H_i\to G))$ by inductive hypothesis.
But also 
\begin{equation*}%\label{eqn:--FH--F-HG-FG}
  \proves((F\to H_i)\to ((F\to (H_i\to G))\to(F\to G)))
\end{equation*}
(\textbf{exercise}).
By two applications of \emph{Modus Ponens}, $\Sigma\proves(F\to G)$.
\end{proof}

The Deduction Theorem gives a condition under which certain proofs
exist.  In particular, we have:

\begin{corollary}\label{cor:consistency}
\mbox{}
\begin{mylist}
  \item
  If $\Sigma\cup\{F\}$ is inconsistent, then $\Sigma\proves\lnot F$.
\item
If $\Sigma\nproves G$, then $\Sigma\cup\{\lnot G\}$ is consistent.
\end{mylist}
\end{corollary}

\begin{proof}
  Suppose  $\Sigma\cup\{F\}$ is inconsistent.  Then
  $\Sigma\cup\{F\}\proves\lnot F$ by Lemma~\ref{lem:consistency}.
  Hence
  $\Sigma\proves(F\to \lnot F)$.  But also
  \begin{equation*}
    \proves((F\to\lnot F)\to \lnot F)
  \end{equation*}
(\textbf{exercise}).
Hence $\Sigma\proves\lnot F$ by \emph{Modus Ponens}.

The remainder is an \textbf{exercise}.
\end{proof}



Recall the distinction on p.~\pageref{syntax} between \tech{syntax}
and \tech{semantics}.
The notion of formal proof can be called \defn{syntactic} because it
involves formal manipulation of symbols.  A good
proof-system will capture the notion of \tech{logical
  consequence}, a notion that can be called \defn{semantic}.  We now
develop this notion:

\section{Logical consequence}

A \defn{structure} for propositional logic is a function $\alpha$ (or
$P\mapsto\alpha(P)$) from
$V$ to $\B$.  (Alternatively, the structure is not the function $\alpha$, but
the set $\{P\in 
V:\alpha(P)=1\}$; but such a definition can cause confusion.  In any
case, the set and the function determine each other.)  Suppose
$F$ is $n$-ary, and $\tuple e$ is the truth-assignment
\begin{equation*}
  (\alpha(P_0),\dots, \alpha(P_{n-1})).
\end{equation*}
If $\widehat F(\tuple e)=1$, then we say that $F$ is \defn{true in
  $\alpha$}, and we write
\begin{equation*}
  \alpha\models F.
\end{equation*}

So far we have only introduced some new notation.  Whether $F$ is true
in $\alpha$ can be determined by finite computation.  In particular:
\begin{mylist}
  \item
$\alpha\models P\Iff \alpha(P)=1$;
\item
$\alpha\models\lnot F\Iff \alpha\nmodels F$;
\item
$\alpha\nmodels(F\to G)\Iff \alpha\models F\amp \alpha\models\lnot G$.
\end{mylist}
So truth can be computed as in the following (which can be compared
with Example~\ref{example:compute}):
\begin{example}
  The following are equivalent:
  \begin{mylist}
    \item
$\alpha\models P\to(\lnot Q\to R)$;
\item
$\alpha\models\lnot P$ or $\alpha\models(\lnot Q\to R)$;
\item
$\alpha(P)=0$ or $\alpha\models Q$ or $\alpha\models R$;
\item
$\alpha(P)=0$ or $\alpha(Q)=1$ or $\alpha(R)=1$.
  \end{mylist}
\end{example}

The notion of structures allows us to make the following definition.
If $\Sigma$ is a (possibly infinite) set of formulas, and if
$\alpha\models F$ for every $F$ in 
$\Sigma$, then $\alpha$ is a \defn{model} of $\Sigma$, and we can write
\begin{equation*}
  \alpha\models\Sigma.
\end{equation*}

Finally, $F$ is a \defn{logical consequence} of $\Sigma$, or $\Sigma$
\defn{entails} $F$, if $F$ is
true in every model of $\Sigma$.  In this case, we can write
\begin{equation*}
  \Sigma\models F.
\end{equation*}
Here, if $\Sigma$ is a finite set $\{G_0,\dots,G_{n-1}\}$, then we can
also write
\begin{equation*}
  G_0,\dots,G_{n-1}\models F
\end{equation*}
(without braces).
We consider logical consequence or entailment as a \defn{semantic}
notion, because, from its definition, it seems not to be determined
by simple
computation.  Indeed, there are infinitely many (in fact, uncountably
many) structures, and anyway a formula might be a logical consequence
of an infinite set of formulas.

It is important to note that $\models$ is used in two completely
different ways:
\begin{mylist}
\item
to express \defn{truth}, which is a relation between a structure and a
formula (or set of 
formulas); 
  \item
to express \defn{entailment}, which is a relation between a set of
formulas and a formula. 
\end{mylist}

The following is a semantic version of the Deduction Theorem; it is
easier to prove:

\begin{lemma}\label{lem:sem-ded}
  $\Sigma\cup\{F\}\models G$ just in case $\Sigma\models(F\to G)$.
\end{lemma}

\begin{proof}
  \textbf{Exercise}.
\end{proof}

Repeated application of the lemma gives
\begin{equation}\label{eqn:FFG}
  F_0,\dots,F_n\models G\Iff{} \models F_0\to\dotsb\to F_n\to
  G. 
\end{equation}
The notational convention here is that $F\to G\to H$ at the end of a
formula means $(F\to (G\to H))$; that is, grouping is from the right.
Towards an alternative expression of this equivalence, let us note:

\begin{lemma}
Suppose $F$ and $G$ are both $n$-ary.
  The following are equivalent:
  \begin{mylist}
    \item
$F\models G$;
\item
$\widehat F(\tuple e)\leq \widehat G(\tuple e)$ for all $\tuple e$.
  \end{mylist}
\end{lemma}

\begin{proof}
  \textbf{Exercise}.
\end{proof}
We can now define $F$ and $G$ to be  \defn{(logically) equivalent} if
they have the same 
truth-table, that is, $\widehat F(\tuple e)=\widehat G(\tuple e)$ for
all $\tuple e$, equivalently, $F\models G$ and $G\models F$;
we can express this by 
\begin{equation*}
F\sim G.
%  F\altequiv G.
\end{equation*}
Note the truth-table
\begin{center}
  \begin{tabular}{c|c|c|c|c}
$\lnot$ & $(P$ & $\to$ & $\lnot$ & $Q)$\\ \hline
   0    &   0  &   1   &     1   &  0\\
   0    &   1  &   1   &     1   &  0\\
   0    &   0  &   1   &     0   &  1\\
   1    &   1  &   0   &     0   &  1
  \end{tabular}.
\end{center}
As an abbreviation of $\lnot(F\to \lnot H)$, let us write 
\begin{equation*}
  F\land H;
\end{equation*}
this is the \defn{conjunction} of $F$ and $H$.

\begin{lemma}
  Show that:
  \begin{mylist}
\item
$F\land G\sim G\land F$;
    \item
  $(F\land G)\land H\sim F\land(G\land H)$;
\item
 $F\land G\to H\sim F\to G\to H$  (here $\land$ has priority
  over $\to$).
  \end{mylist}
\end{lemma}

\begin{proof}
  \textbf{Exercise.}
\end{proof}

Now we can write the equivalence \eqref{eqn:FFG} as
\begin{equation*}
  F_0,\dots,F_n\models G\Iff{} \models (F_0\land\dots \land F_n\to
  G). 
\end{equation*}
Alternatively, if $\{F_0,\dots,F_n\}=\Sigma$, then instead of
$F_0\land\dots\land F_n$, we can write
\begin{equation*}
  \bigwedge\Sigma;
\end{equation*}
this is the \defn{conjunction} of $\Sigma$.
Then
\begin{equation*}
  \Sigma\models G\Iff{}\models(\bigwedge\Sigma\to G),
\end{equation*}
provided $\Sigma$ is finite.
So we have a procedure to determine whether $\Sigma\models G$,
provided also that $\Sigma$ is finite: just check whether $\bigwedge
\Sigma\to G$ is a tautology.  What if $\Sigma$ is infinite?


\section{Soundness and Completeness}

We aim to reduce the semantic notion of entailment to the syntactic
notion of deducibility, by proving that our proof-system has the
properties of:
\begin{mylist}
  \item
\defn{soundness:} if $\Sigma\proves F$, then $\Sigma\models F$;
\item
\defn{completeness:} if $\Sigma\models F$, then $\Sigma\proves F$.
\end{mylist} 
Let us write
\begin{equation*}
  \models F
\end{equation*}
if $\alpha\models F$ for all structures
$\alpha$; in this case, $F$ can be 
called a \defn{validity}.

In the finitary case, soundness and completeness are now easy to prove:

\begin{lemma}\label{lem:taut-valid}
The tautologies are precisely the validities: 
\begin{equation*}
  \proves F\Iff{}\models F.
\end{equation*}
\end{lemma}

\begin{proof}
The following are equivalent:
\begin{mylist}
  \item
$\proves F$;
\item
$\widehat F(\tuple e)=1$ for all $\tuple e$;
\item
$\alpha\models F$ for all structures $\alpha$;
\item
$\models F$.
\end{mylist}
This completes the proof.
\end{proof}

The reverse direction of the following can be called \defn{weak
  completeness}: 

\begin{theorem}\label{thm:weak}
  If $\Sigma$ is finite, then
  \begin{equation*}
\Sigma\proves F\Iff \Sigma\models F. 
  \end{equation*}
\end{theorem}

\begin{proof}
  Suppose $\{G_0,\dots,G_{n-1}\}\models F$.  Then 
  \begin{align*}
    \Sigma\proves F&\Iff {} \proves G_0\to\dots \to G_{n-1}\to F &&\text{[by
    the Deduction Theorem]}\\
&\Iff {} \models G_0\to\dots \to G_{n-1}\to F&&\text{[by the last lemma]}\\
&\Iff \Sigma\models F&&
  \end{align*}
by Lemma~\ref{lem:sem-ded}.
\end{proof}

Another connexion between deducibility and entailment is now the
following: 

\begin{corollary}\label{cor:fin}
  $\Sigma$ is consistent if and only if every finite subset of
  $\Sigma$ has a model.
\end{corollary}

\begin{proof}
  If $\Sigma$ is not consistent, then, by Lemma~\ref{lem:incon-con},
  some finite subset $\Sigma_0$ of $\Sigma$ is inconsistent.  Then
  $\Sigma_0\proves \lnot(P\to P)$ by Lemma~\ref{lem:consistency}, so
  $\Sigma_0\models\lnot(P\to P)$.  But $\lnot(P\to P)$ has no model, so
  $\Sigma_0$ has no model.

Conversely, if $\Sigma_0$ is a finite subset of $\Sigma$ with no
model, then $\Sigma_0\models\lnot(P\to P)$, so
$\Sigma_0\proves\lnot(P\to P)$, whence $\Sigma_0$ is inconsistent by
Lemma~\ref{lem:consistency}. 
\end{proof}

Both implications in Theorem~\ref{thm:weak} are true generally:

\begin{theorem}[Soundness]
  If $\Sigma\proves F$, then $\Sigma\models F$.
\end{theorem}

\begin{proof}
Proof by strong induction on the length of deductions.  Suppose the
  claim is true when $F$ has a deduction of length less than $n+1$
  from $\Sigma$.
  Suppose $G_0,\dots,G_{n-1},F$ is a formal proof of $F$ from
  $\Sigma$.
\begin{mylist}
\item
If $\proves F$, then $\models F$ by Lemma~\ref{lem:taut-valid}, so
$\Sigma\models F$.
\item
If $F\in \Sigma$, then $\Sigma\models F$ trivially.
\item
If $G_j$ is $(G_i\to F)$ for some $i$ and $j$ less than $n$,
then $\Sigma\models G_i$ and $\Sigma\models (G_i\to F)$ by
inductive hypothesis, whence also  $\Sigma\models F$.
\end{mylist}
This completes the induction.
\end{proof}

\begin{theorem}[Completeness]
  If $\Sigma\models F$, then $\Sigma\proves F$.
\end{theorem}

\begin{proof}
  Suppose $\Sigma\nproves F$; we shall show $\Sigma\nmodels F$. 
By Corollary~\ref{cor:consistency}, $\Sigma\cup\{\lnot F\}$ is
consistent.  Our
proof, in outline, has three parts:
\begin{myenum}\setcounter{myenum}{-1}
  \item
There is a set $\Sigma^*$ of formulas such that:
\begin{myitem}
  \item
$\Sigma\cup\{\lnot F\}\included\Sigma^*$;
\item
$\Sigma^*$ is consistent;
\item
if $G\notin\Sigma^*$, then $\lnot G\in \Sigma^*$.
\end{myitem}
\item
Let the structure $\alpha$ be given by
\begin{equation*}
  \alpha(P)=1\Iff P\in\Sigma^*.
\end{equation*}
Then
\begin{equation}\label{eqn:AGGS}
  \alpha\models G\Iff G\in \Sigma^*
\end{equation}
for all formulas $G$.
\item
Hence $\alpha\models\Sigma^*$, so $\alpha\models \lnot F$.  Therefore
$\alpha\nmodels F$.  This shows $\Sigma\nmodels F$. 
\end{myenum}
Details of (0) and (1) are as follows:

\begin{myenum}\setcounter{myenum}{-1}
  \item
The infinite set $\Fm{}{}$ of formulas is countable, that is, it can be
written as $\{G_n:n\in\varN\}$ (\textbf{exercise}).  We now
recursively define a 
sequence $(\Sigma_n:n\in\varN)$ of sets of formulas:
\begin{mylist}
  \item
$\Sigma_0=\Sigma\cup\{\lnot F\}$.
\item
$\Sigma_{n+1}=
  \begin{cases}
    \Sigma_n\cup\{G_n\}, & \text{ if this is consistent;}\\
\Sigma_n,& \text{ otherwise.}
  \end{cases}$
\end{mylist}
Then $\Sigma=\Sigma_0\included\Sigma_1\included\dotsb$.
Let $\Sigma^*=\bigcup_{n\in\varN}\Sigma_n$.
We can now establish the desired points:
\begin{myitem}
\item
Obviously $\Sigma\cup\{\lnot F\}\included\Sigma^*$.
\item
Suppose if possible that  $\Sigma^*$ is inconsistent.  Then some
finite subset $\{H_0,\dots,H_k\}$ is inconsistent, by
Lemma~\ref{lem:fin}.  Each formula $H_i$ is in some set
$\Sigma_{m(i)}$.  Let
$n=\max\{m(0),\dots,m(k)\}$.  Then $\Sigma_n$ is inconsistent. 

However, by induction, each of the sets $\Sigma_n$ is consistent.

Therefore $\Sigma^*$ is consistent.
\item
Finally, suppose $G\notin\Sigma^*$.  Now, $G$ is $G_n$ for some $n$.
Then $\Sigma_n\cup\{G\}$ is inconsistent, by definition of
$\Sigma_{n+1}$ and $\Sigma^*$.  Hence:
\begin{mylist}
  \item
$\Sigma_n\proves\lnot G$, by Corollary~\ref{cor:consistency};
\item
$\Sigma^*\proves\lnot G$;
\item
$\Sigma^*\cup\{\lnot G\}$ is consistent, by
    Lemmas~\ref{lem:idempotent} and~\ref{lem:consistency}, since
    $\Sigma^*$ is consistent;
\item
$\Sigma_m\cup\{\lnot G\}$ is consistent for all $m$.
\end{mylist}
    But $\lnot G$ is $G_m$ for some $m$.  Hence $\lnot G\in
    G_{m+1}\included\Sigma^*$. 
\end{myitem}
By the consistency of $\Sigma^*$, we now have
\begin{equation*}
  G\notin\Sigma^*\Iff\lnot G\in\Sigma^*.
\end{equation*}
\item
We prove the equivalence \eqref{eqn:AGGS} by induction on $\Fm{}{}$.
It is trivially
true if $G$ is a variable, by definition of $\alpha$.  Suppose it is true
if $G$ is $H$ or $K$.  Then
\begin{equation*}
  \alpha\models\lnot H\Iff \alpha\nmodels H\Iff H\notin\Sigma^*\Iff \lnot
  H\in\Sigma^*,
\end{equation*}
and also
\begin{align*}
  \alpha\nmodels(H\to K)&\Iff \alpha\models H\amp \alpha\models\lnot K\\
&\Iff H\in\Sigma^*\amp \lnot K\in \Sigma^*\\
&\Iff (H\to K)\not\in \Sigma^*.
\end{align*}
(\textbf{Exercise:} why does the last equivalence hold?)
\end{myenum}
This completes the proof.
\end{proof}

Note well the \emph{method} of the proof:  Given a consistent set of
formulas, we extended it to a larger consistent set, $\Sigma^*$, that
determined the structure, $\alpha$, that we wanted.

A set $\Sigma$ of formulas can be called \defn{maximally consistent}
if:
\begin{mylist}
  \item
$\Sigma$ is consistent; and
\item
if $\Sigma\included\Gamma$ and $\Gamma$ is consistent, then
$\Sigma=\Gamma$. 
\end{mylist}

\begin{lemma}
  Suppose $\Sigma$ is consistent.  The following are equivalent:
  \begin{mylist}
    \item
    $\Sigma$ is maximally consistent.
\item
If $G\notin\Sigma$, then $\lnot G\in \Sigma$.
  \end{mylist}
\end{lemma}

  \begin{proof}
    \textbf{Exercise}.
  \end{proof}

Our proof of the Completeness Theorem established and used the
following result:

\begin{porism}
  Every consistent set of formulas is included in a maximally
  consistent set.
\end{porism}

The following can be proved as a corollary of Completeness:

\begin{theorem}[Compactness]
If every finite subset of $\Sigma$ has a model, then $\Sigma$ has a
model. 
\end{theorem}

\begin{proof}
Suppose every finite subset of $\Sigma$ has a model.  Then $\Sigma$ is
consistent by Lemma~\ref{cor:fin}. 
Let $F$ be a contradiction.  Then $\Sigma\nproves F$.  Hence
$\Sigma\nmodels F$.  In particular, there is a model of
$\Sigma$ in which $F$ is false.
\end{proof}

Conversely, Completeness can be proved as a corollary of the
Compactness Theorem
(\textbf{exercise}). 

\section{Additional exercises}





\begin{myenum}
\item
    Give a formal proof
of $H$ from $F$, $G$ and $(\lnot(F\to \lnot G)\to H)$.
\item
On $\Fm{}{}$, let $F\mapsto F{}'$ be the operation of `reversing the
arrows,' so that, for example, 
\begin{equation*}
  (P\to \lnot(\lnot Q\to R))'\quad\text{ is }\quad
(\lnot(R\to \lnot Q)\to P).
\end{equation*}
  What is the precise
\emph{recursive} definition of the 
function $F\mapsto F{}'$?
\item
Prove or disprove:  \emph{Either $\Sigma\models F$, or
  $\Sigma\models\lnot F$.} 
\item
      Prove or disprove: \emph{If $\Sigma\models(F\to G)$, then either
      $\Sigma\models\lnot F$ or $\Sigma\models G$.}
\end{myenum}
  We have introduced $\land$ so that $(F\land G)$ is an abbreviation of
$\lnot(F\to \lnot G)$.    
\begin{myenum}\setcounter{myenum}{4}
    \item
Show that
\begin{equation}
  (F\to G)\sim \lnot(F\land\lnot G).
\end{equation}
  \end{myenum}
Let $(\lnot F\to G)$ be abbreviated
\begin{equation*}
  (F\lor G).
\end{equation*}
  We can develop propositional logic in the signature
  $\{\land,\lor,\lnot\}$.   Let $\operatorname{Fm}'$ be the set of formulas in
  this signature.  
  \begin{myenum}\setcounter{myenum}{5}
    \item
Give a precise definition of $\operatorname{Fm}'$.
\item
Define $A\models F$ for structures $A$ and $F$ in $\operatorname{Fm}'$.
  \end{myenum}
The definition of $\Sigma\models F$ is exactly as before, when
$\Sigma$ is a set of formulas in $\operatorname{Fm}'$.
\begin{myenum}\setcounter{myenum}{7}
  \item
Prove or disprove:  \emph{If $\Sigma\models F$ or $\Sigma\models G$, then
$\Sigma\models(F\lor G)$.}
\item
Prove or disprove:  \emph{If $\Sigma\models(F\lor G)$, then $\Sigma\models
F$ or $\Sigma\models G$.}
\item
Show that
$\{\land,\lnot{}\}$ is an adequate signature. 
  \end{myenum}
Informally, we can define a unary operation $F\to
  F^*$ on $\operatorname{Fm}'$ so that $F^*$ is the result of interchanging
  $\land$ and $\lor$ in $F$ and of replacing every variable $P$ with
  $\lnot P$.
  \begin{myenum}\setcounter{myenum}{10}
    \item
Give a precise recursive definition of $F\mapsto F^*$.
\item
Show that $F^*\sim\lnot F$ for all $F$ in $\operatorname{Fm}'$.
  \end{myenum}