add intro to FOL chapter (issue #69), split syntax & semantics into t…

…wo chapters. Should also help with issue #173

bib/open-logic.bib

@@ -347,6 +347,19 @@ @misc{MacFarlane2015
   url =		 {http://johnmacfarlane.net/church.html}
 }
 
+
+@book{Magnus2021,
+  title = {Forall {\emph{x}}: {{Calgary}}. {{An}} Introduction to Formal Logic},
+  author = {Magnus, P. D. and Button, Tim and Loftis, J. Robert and {Thomas-Bolduc}, Aaron and Trueman, Robert and Zach, Richard},
+  year = {2021},
+  edition = {F21},
+  publisher = {{Open Logic Project}},
+  address = {{Calgary}},
+  url = {https://forallx.openlogicproject.org/},
+  copyright = {All rights reserved},
+  keywords = {textbook}
+}
+
 @article{Matijasevich1992,
   title =	 {My Collaboration with {J}ulia {R}obinson},
   author =	 {Matijasevich, Yuri},

content/first-order-logic/first-order-logic.tex

@@ -29,7 +29,11 @@
   (\gitissue{69}).
 \end{editorial}
 
-\olimport[syntax-and-semantics]{syntax-and-semantics}
+\olimport[introduction]{introduction}
+
+\olimport[syntax-and-semantics]{syntax}
+
+\olimport[syntax-and-semantics]{semantics}
 
 \olimport[models-theories]{models-theories}
 

content/first-order-logic/introduction/first-order-logic.tex

@@ -0,0 +1,87 @@
+% Part: first-order-logic
+% Chapter: introduction
+% Section: first-order-logic
+
+\documentclass[../../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{fol}{int}{fol}
+
+\olsection{First-Order Logic}
+
+You are probably familiar with first-order logic from your first
+introduction to formal logic.\footnote{In fact, we more or less assume
+you are!{} If you're not, you could review a more elementary textbook,
+such as \emph{forall x} \citep{Magnus2021}.} You may know it as
+``quantificational logic'' or ``predicate logic.''  First-order
+logic, first of all, is a formal language.  That means, it has a
+certain vocabulary, and its expressions are strings from this
+vocabulary.  But not every string is permitted.  There are different
+kinds of permitted expressions: terms, !!{formula}s, and
+!!{sentence}s.  We are mainly interested in !!{sentence}s of
+first-order logic: they provide us with a formal analogue of sentences
+of English, and about them we can ask the questions a logician
+typically is interested in. For instance: 
+\begin{itemize}
+    \item Does $!B$ follow from~$!A$ logically?
+    \item Is $!A$ logically true, logically false, or
+contingent?
+    \item Are $!A$ and $!B$ equivalent?
+\end{itemize}
+
+These questions are primarily questions about the ``meaning'' of
+!!{sentence}s of first-order logic.  For instance, a philosopher would
+analyze the question of whether $!B$ follows logically from~$!A$ as
+asking: is there a case where $!A$ is true but~$!B$ is false ($!B$
+doesn't follow from~$!A$), or does every case that makes $!A$ true
+also make~$!B$ true ($!B$ does follow from~$!A$)?  But we haven't been
+told yet what a ``case'' is---that is the job of \emph{semantics}.  The
+semantics of first-order logic provides a mathematically precise model
+of the philosopher's intuitive idea of ``case,'' and also---and this
+is important---of what it is for !!a{sentence}~$!A$ to be \emph{true
+in} a case. We call the mathematically precise model that we will
+develop !!a{structure}. The relation which makes ``true in'' precise,
+is called the relation of \emph{satisfaction}.  So what we will define
+is ``$!A$ is satisfied in~$\Struct{M}$'' (in symbols: $\Sat{M}{!A}$)
+for !!{sentence}s~$!A$ and !!{structure}s~$\Struct{M}$. Once this is
+done, we can also give precise definitions of the other semantical
+terms such as ``follows from'' or ``is logically true.'' These
+definitions will make it possible to settle, again with mathematical
+precision, whether, e.g., $\lforall[x][(!A(x) \lif !B(x)),
+\lexists[x][!A(x)] \Entails \lexists[x][!B(x)]]$. The answer will, of
+course, be ``yes.'' If you've already been trained to symbolize
+sentences of English in first-order logic, you will recognize this as,
+e.g., the symbolizations of, say, ``All ants are insects, there are
+ants, therefore there are insects.'' That is obviously a valid
+argument, and so our mathematical model of ``follows from'' for our
+formal language should give the same answer.
+
+Another topic you probably remember from your first introduction to
+formal logic is that there are \emph{formal proofs}.  If you have
+taken a first formal logic course, your instructor will have made you
+practice finding such proofs, perhaps even a proof that shows that the
+above entailment holds.  There are many different ways to give formal
+proofs: you may have done something called ``natural deduction'' or
+``truth trees,'' but there are many others.  The purpose of proof
+systems is to provide tools using which the logicians' questions above
+can be answered: e.g., a natural deduction proof in which
+$\lforall[x][(!A(x) \lif !B(x))$ and $\lexists[x][!A(x)]$ are premises
+and $\lexists[x][!B(x)]]$ is the conclusion (last line)
+\emph{verifies} that $\lexists[x][!B(x)]]$ logically follows from
+$\lforall[x][(!A(x) \lif !B(x))]$ and $\lexists[x][!A(x)]$.  
+
+But why is that?  On the face of it, proof systems have nothing to do
+with semantics: giving a formal proof merely involves arranging symbols
+in certain rule-governed ways; they don't mention ``cases'' or ``true
+in'' at all.  The connection between proof systems and semantics has
+to be established by a meta-logical investigation. What's needed is a
+mathematical proof, e.g., that a formal proof of $\lexists[x][!B(x)]$
+from premises $\lforall[x][(!A(x) \lif !B(x))]$ and
+$\lexists[x][!A(x)]$ is possible, if, and only if, $\lforall[x][(!A(x)
+\lif !B(x))$ and $\lexists[x][!A(x)]$ together
+entails~$\lexists[x][!B(x)]]$.  Before this can be done, however, a
+lot of painstaking work has to be carried out to get the definitions
+of syntax and semantics correct.
+
+\end{document}

content/first-order-logic/introduction/formulas.tex

@@ -0,0 +1,88 @@
+% Part: first-order-logic
+% Chapter: introduction
+% Section: formulas
+
+\documentclass[../../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{fol}{int}{fml}
+
+\section{\usetoken{P}{formula}}
+
+Here is the approach we will use to rigorously specify !!{sentence}s
+of first-order logic and to deal with the issues arising from the use
+of !!{variable}s. We first define a \emph{different} set of
+expressions: !!{formula}s. Once we've done that, we can consider the
+role !!{variable}s play in them---and on the basis of some other
+ideas, namely those of ``free'' and ``bound'' !!{variable}s, we can
+define what !!a{sentence} is (namely, !!a{formula} without free
+!!{variable}s). We do this not just because it makes the definition of
+``!!{sentence}'' more manageable, but also because it will be crucial
+to the way we define the semantic notion of satisfaction.
+
+Let's define ``!!{formula}'' for a simple first-order language, one
+containing only a single !!{predicate}~$\Obj P$ and a single
+!!{constant}~$\Obj a$, and only the logical symbols $\lnot$, $\land$,
+and~$\lexists$. Our full definitions will be much more general:
+we'll allow infinitely many !!{predicate}s and !!{constant}s. In fact,
+we will also consider !!{function}s which can be combined with
+!!{constant}s and !!{variable}s to form ``terms.'' For now, $\Obj a$
+and the variables will be our only terms.  We do need infinitely many
+!!{variable}s.  We'll officially use the symbols $\Obj v_0$, $\Obj
+v_1$, \dots, as variables.
+
+\begin{defn}
+The set of \emph{!!{formula}s}~$\Frm$ is defined as follows:
+\begin{enumerate}
+\item\ollabel{fmls-atom} $\Atom{\Obj P}{\Obj a}$ and $\Atom{\Obj
+  P}{\Obj v_i}$ are !!{formula}s ($i \in \Nat$).
+
+\tagitem{prvNot}{If $!A$ is !!a{formula}, then $\lnot !A$ is
+  !!{formula}.}{}
+
+\tagitem{prvAnd}{If $!A$ and $!B$ are !!{formula}s, then $(!A \land
+  !B)$ is !!a{formula}.}{}
+
+\tagitem{prvEx}{If $!A$ is !!a{formula} and $x$ is !!a{variable},
+  then $\lexists[x][!A]$ is !!a{formula}.}{}
+
+\tagitem{limitClause}{\ollabel{fmls-limit}Nothing else is !!a{formula}.}{}
+\end{enumerate}
+\end{defn}
+
+\olref{fmls-atom} tell us that $\Atom{\Obj P}{\Obj a}$ and $\Atom{\Obj
+P}{\Obj v_i}$ are !!{formula}s, for any $i \in \Nat$. These are
+the so-called \emph{atomic} !!{formula}s. They give us something to
+start from.  The other clauses give us ways of forming new
+!!{formula}s from ones we have already formed. So for instance, we get
+that $\lnot \Atom{\Obj P}{\Obj v_2}$ is !!a{formula}, since
+$\Atom{\Obj P}{\Obj v_2}$ is already !!a{formula} by
+\olref{fmls-atom}, and then we get that $\lexists[\Obj v_2][\lnot
+\Atom{\Obj P}{\Obj v_2}]$ is another !!{formula}, and so on.
+\olref{fmls-limit} tells us that \emph{only} strings we can form in
+this way count as !!{formula}s. In particular, $\lexists[\Obj
+v_0][\Atom{\Obj P}{\Obj a}]$ and $\lexists[\Obj v_0][\lexists[\Obj
+v_0][\Atom{\Obj P}{\Obj a}]]$ \emph{do} count as !!{formula}s, and
+$(\lnot \Atom{\Obj P}{\Obj a})$ does not.
+
+This way of defining !!{formula}s is called an \emph{inductive
+definition}, and it allows us to prove things about !!{formula}s using
+a version of proof by induction called \emph{structural induction}.
+These are discussed in a general way in \olref[mth][ind][idf]{sec} and
+\olref[mth][ind][sti]{sec}, which you should review before delving
+into the proofs later on. Basically, the idea is that if you want to
+give a proof that something is true for all !!{formula}s you show
+first that it is true for the atomic !!{formula}s, and then that
+\emph{if} it's true for any !!{formula}~$!A$ (and~$!B$), it's
+\emph{also} true for $\lnot !A$, $(!A \land !B)$, and
+$\lexists[x][!A]$. For instance, this proves that it's true for
+$\lexists[\Obj v_2][\lnot \Atom{\Obj P}{\Obj v_2}]$: from the first
+part you know that it's true for the atomic !!{formula}~$\Atom{\Obj
+P}{\Obj v_2}$. Then you get that it's true for $\lnot \Atom{\Obj
+P}{\Obj v_2}$ by the second part, and then again that it's true for
+$\lexists[\Obj v_2][\lnot \Atom{\Obj P}{\Obj v_2}]$ itself. Since all
+!!{formula}s are inductively generated from atomic !!{formula}s, this
+works for any of them.
+
+\end{document}

content/first-order-logic/introduction/introduction.tex

@@ -0,0 +1,30 @@
+% Part: first-order-logic
+% Chapter: introduction
+
+\documentclass[../../../include/open-logic-chapter]{subfiles}
+
+\begin{document}
+
+\olchapter{fol}{int}{Introduction to First-Order Logic}
+
+\olimport{first-order-logic}
+
+\olimport{syntax}
+
+\olimport{formulas}
+
+\olimport{satisfaction}
+
+\olimport{sentences}
+
+\olimport{semantic-notions}
+
+\olimport{substitution}
+
+\olimport{models-theories}
+
+\olimport{soundness-completeness}
+
+\OLEndChapterHook
+
+\end{document}

content/first-order-logic/introduction/models-theories.tex

@@ -0,0 +1,70 @@
+% Part: first-order-logic
+% Chapter: introduction
+% Section: models-theories
+
+\documentclass[../../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{fol}{int}{mod}
+
+\olsection{Models and Theories}
+
+Once we've defined the syntax and semantics of first-order logic, we
+can get to work investigating the properties of !!{structure}s, of the
+semantic notions, we can define proof systems, and investigate those.
+For a set of !!{sentence}s, we can ask: what !!{structure}s make all
+the !!{sentence}s in that set true?  Given a set of
+!!{sentence}s~$\Gamma$, !!a{structure}~$\Struct{M}$ that satisfies
+them is called a \emph{model of~$\Gamma$}.  We might start
+from~$\Gamma$ and try find its models---what do they look like? How
+big or small do they have to be? But we might also start with a single
+!!{structure} or collection of !!{structure}s and ask: what
+!!{sentence}s are true in them?  Are there !!{sentence}s that
+\emph{characterize} these !!{structure}s in the sense that they, and
+only they, are true in them? These kinds of questions are the domain
+of \emph{model theory}.  They also underlie the \emph{axiomatic
+method}: describing a collection of !!{structure}s by a set of
+!!{sentence}s, the axioms of a theory. This is made possible by the
+observation that exactly those !!{sentence}s entailed in first-order
+logic by the axioms are true in all models of the axioms.
+
+As a very simple example, consider preorders. A preorder is a
+relation~$R$ on some set~$A$ which is both reflexive and transitive.
+A set~$A$ with a two-place relation $R \subseteq A \times A$ on it is
+exactly what we would need to give !!a{structure} for a first-order
+language with a single two-place relation symbol~$\Obj P$: we would
+set $\Domain{M} = A$ and $\Assign{\Obj P}{M} = R$.  Since $R$~is a
+preorder, it is reflexive and transitive, and we can find a
+set~$\Gamma$ of !!{sentence}s of first-order logic that say this:
+\begin{align*}
+  & \lforall[\Obj v_0][\Atom{\Obj P}{\Obj v_0,\Obj v_0}]\\
+  & \lforall[\Obj v_0][\lforall[\Obj v_1][\lforall[\Obj v_2][((\Atom{\Obj P}{\Obj v_0,\Obj v_1} \land \Atom{\Obj P}{\Obj v_1,\Obj v_2}) \lif \Atom{\Obj P}{\Obj v_0,\Obj v_2})]]]
+\end{align*}
+These !!{sentence}s are just the symbolizations of ``for any~$x$,
+$Rxx$'' ($R$ is reflexive) and ``whenever $Rxy$ and $Ryz$ then also
+$Rxz$'' ($R$ is transitive). We see that !!a{structure}~$\Struct{M}$
+is a model of these two !!{sentence}s~$\Gamma$ iff $R$ (i.e.,
+$\Assign{\Obj P}{M}$), is a preorder on~$A$ (i.e., $\Domain{M}$). In
+other words, the models of $\Gamma$ are exactly the preorders. Any
+property of all preorders that can be expressed in the first-order
+language with just~$\Obj P$ as !!{predicate} (like reflexivity and
+transitivity above), is entailed by the two !!{sentence}s in~$\Gamma$
+and vice versa.  So anything we can prove about models of~$\Gamma$ we
+have proved about all preorders.
+
+For any particular theory and class of models (such as $\Gamma$ and
+all preorders), there will be interesting questions about what can be
+expressed in the corresponding first-order language, and what cannot
+be expressed. There are some properties of !!{structure}s that are
+interesting for all languages and classes of models, namely those
+concerning the size of the !!{domain}.  One can always express, for
+instance, that the !!{domain} contains exactly $n$~!!{element}s, for
+any~$n \in \PosInt$.  One can also express, using a set of infinitely
+many !!{sentence}s, that the !!{domain} is infinite.  But one cannot
+express that the domain is finite, or that the domain is
+!!{nonenumerable}. These results about the limitations of first-order
+languages are consequences of the compactness and L\"owenheim-Skolem
+theorems.
+
+\end{document}