forallx-yyc-preface.tex

\chapter{Preface}\label{preface}

\paragraph{About this book}

As the title indicates, this is a textbook on formal logic.  Formal logic concerns the study of a certain kind of language which, like any language, can serve to express states of affairs.  It is a formal language, i.e., its expressions (such as sentences) are defined formally.  This makes it a very useful language for being very precise about the states of affairs its sentences describe. In particular, in formal logic it is impossible to be ambiguous. The study of these languages centres on the relationship of entailment between sentences, i.e., which sentences follow from which other sentences.  Entailment is central because by understanding it better we can tell when some states of affairs must obtain provided some other states of affairs obtain.  But entailment is not the only important notion. We will also consider the relationship of being satisfiable, i.e., of not being mutually contradictory.  These notions can be defined semantically, using precise definitions of entailment based on interpretations of the language---or proof-theoretically, using formal systems of deduction.

Formal logic is of course a central sub-discipline of philosophy, where the logical relationship of assumptions to conclusions reached from them is important.  Philosophers investigate the consequences of definitions and assumptions and evaluate these definitions and assumptions on the basis of their consequences. It is also important in mathematics and computer science. In mathematics, formal languages are used to describe not ``everyday'' states of affairs, but mathematical states of affairs. Mathematicians are also interested in the consequences of definitions and assumptions, and for them it is equally important to establish these consequences (which they call ``theorems'') using completely precise and rigorous methods. Formal logic provides such methods.  In computer science, formal logic is applied to describe the state and behaviours of computational systems, e.g., circuits, programs, databases, etc.  Methods of formal logic can likewise be used to establish consequences of such descriptions, such as whether a circuit is error-free, whether a program does what it's intended to do, whether a database is consistent or if something is true of the data in it.

The book is divided into nine parts. \Cref{ch.intro} introduces the topic and notions of logic in an informal way, without introducing a formal language yet.  \Crefrange{ch.TFL}{ch.NDTFL} concern truth-functional languages. In it, sentences are formed from basic sentences using a number of connectives (`or', `and', `not', `if \dots then') which just combine sentences into more complicated ones.  We discuss logical notions such as entailment in two ways: semantically, using the method of truth tables (in \cref{ch.TruthTables}) and proof-theoretically, using a system of formal derivations (in \cref{ch.NDTFL}). \Crefrange{ch.FOL}{ch.NDFOL} deal with a more complicated language, that of first-order logic. It includes, in addition to the connectives of truth-functional logic, also names, predicates, identity, and the so-called quantifiers. These additional elements of the language make it much more expressive than the truth-functional language, and we'll spend a fair amount of time investigating just how much one can express in it.  Again, logical notions for the language of first-order logic are defined semantically, using interpretations, and proof-theoretically, using a more complex version of the formal derivation system introduced in \cref{ch.NDTFL}.  \Cref{ch.ML} discusses the extension of TFL by non-truth-functional operators for possibility and necessity: modal logic. \Cref{ch.normalform} covers two advanced topics: that of conjunctive and disjunctive normal forms and the functional completeness of the truth-functional connectives, and the soundness of natural deduction for TFL.

In the appendices you'll find a discussion of alternative notations for the languages we discuss in this text, of alternative derivation systems, and a quick reference listing most of the important rules and definitions. The central terms are listed in a glossary at the very end.

\paragraph{Credits} This book is based on a text originally written by
P.~D. Magnus in the version revised and expanded by Tim Button. It
also includes some material (mainly exercises) by J.~Robert Loftis.
The material in \cref{ch.ML} is based on notes by Robert Trueman (but
rewritten to use Fitch's original natural deduction rules for modal
logic), and the material in
\cref{c:NormalForms,c:FunctionalCompleteness,ch:Soundness} on two
chapters from Tim Button's open text \textit{Metatheory}. Aaron
Thomas-Bolduc and Richard Zach have combined elements of these texts
into the present version, changed some of the terminology and
examples, rewritten some sections, and added material of their own. In
particular, Richard Zach rewrote \cref{s:Arguments,s:Valid}, and added
\cref{s:AmbiguityTFL,s:stratTFL,s:ambiguityFOL,ch:PropRelations,ch:equivalences}.
As of the Fall 2019 edition, the part on FOL uses the syntax more
common in advanced texts (such as those based on the
\href{https://openlogicproject.org/}{Open Logic Project}) where
arguments to predicate symbols are enclosed in parentheses (i.e.,
`$R(a,b)$' instead of `$Rab$'). This version of \forallx{} also uses
the standard definition of syntax for FOL which allows vacuous
quantification, and Gentzen's original introduction and elimination
rules for natural deduction (i.e., double negation elimination and
excluded middle rules are derived rules, and indirect proof is the
only classical rule). The resulting text is licensed under a Creative
Commons Attribution 4.0 license. There are
\href{https://github.com/OpenLogicProject/OpenLogic/wiki/Other-Logic-Textbooks}{several
other} ``remixes'' of \forallx, including translations of this
version.

\paragraph{Notes for instructors} The material in this book is suitable for a semester-long introduction to formal logic. I cover \crefrange{ch.intro}{ch.NDFOL} plus \cref{c:NormalForms,c:FunctionalCompleteness,ch:equivalences} in 12 weeks, although I leave out partial truth tables and derived inference rules.

The most recent version of this book is available in PDF at
\href{https://forallx.openlogicproject.org}{forallx.openlogicproject.org},
but changes frequently.  The CC BY license gives you the right to
download and distribute the book yourself. In order to ensure that all
your students have the same version of the book throughout the term
you're using it, you should do so: upload the PDF you decide to use to
your LMS rather than merely give your students the link. The book is
also available in an
\href{https://forallx.openlogicproject.org/html/}{HTML version}. This
version has been prepared with
\href{https://forallx.openlogicproject.org/html/A4.html}{special
attention to accessibility issues} and should be more suitable for
users who rely on screen readers, e.g., students with low vision or
complete loss of vision. You can download a SCORM bundle including the
HTML and PDF versions for upload to your LMS. You are also free to
have the PDFs printed by your bookstore, but some bookstores may be
able to purchase and stock the softcover books available on Amazon.

Note that solutions to many exercises in the book are available at the
above site as well (to everyone, including your students). The
solutions are not (yet) part of the HTML version or the SCORM bundle.

The syntax and proof systems (except those for modal logic) are supported by Graham Leach-Krouse's free, online logic teaching software application \textit{Carnap} (\href{https://carnap.io}{carnap.io}). This allows for submission and automated marking of exercises such as symbolization, truth tables, and natural deduction proofs.  Instructors on carnap.io will be able to find \href{https://carnap.io/shared/rzach@ucalgary.ca/forall%20x:%20Calgary.md}{samples of additional exercises} they may wish to adapt or assign as-is.