Derivation Systems — Source and provenance

Source and provenance

All 6 files in the exact Derivation Systems source boundary appear line by line and are copied byte-for-byte for download. All 137 formulas link to exact source coordinates.

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

31 lines; SHA-256 85b8a0fca16c329ad16b3c17975735c159e0cf9d38e8dfc7501acba84171fb6c. Open the preserved source file.

% Part: first-order-logic
% Chapter: proof-systems
\documentclass[../../../include/open-logic-chapter]{subfiles}
\begin{document}
\iftag{FOL}
{\olchapter{fol}{prf}{\usetoken{S}{derivation} Systems}}
{\olchapter{pl}{prf}{\usetoken{S}{derivation} Systems}}
\begin{editorial}
This chapter collects general material on !!{derivation} systems. A
textbook using a specific system can insert the introduction section
plus the relevant survey section at the beginning of the chapter
introducing that system.
\end{editorial}
\olimport{introduction}
\olimport{sequent-calculus}
\olimport{natural-deduction}
\olimport{tableaux}
\olimport{axiomatic-deduction}
\OLEndChapterHook
\end{document}

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

101 lines; SHA-256 5172343625a0d66971257858a1a6e359805ffeec979bd5afdc0377864799a756. Open the preserved source file.

% Part: first-order-logic
% Chapter: proof-systems
% Section: introduction
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{prf}{int}}
{\olfileid{pl}{prf}{int}}
\olsection{Introduction}
Logics commonly have both a semantics and !!a{derivation}
system. The semantics concerns concepts such as truth, satisfiability,
validity, and entailment. The purpose of !!{derivation} systems is to
provide a purely syntactic method of establishing entailment and
validity. They are purely syntactic in the sense that a
!!{derivation} in such a system is a finite syntactic object, usually
a sequence (or other finite arrangement) of !!{sentence}s or
!!{formula}s. Good !!{derivation} systems have the property that any
given sequence or arrangement of !!{sentence}s or !!{formula}s can be
verified mechanically to be ``correct.''
The simplest (and historically first) !!{derivation} systems for
first-order logic were \emph{axiomatic}. A sequence of !!{formula}s
counts as !!a{derivation} in such a system if each individual
!!{formula} in it is either among a fixed set of ``axioms'' or follows
from !!{formula}s coming before it in the sequence by one of a fixed
number of ``inference rules''---and it can be mechanically verified if
!!a{formula} is an axiom and whether it follows correctly from other
!!{formula}s by one of the inference rules. Axiomatic !!{derivation}
systems are easy to describe---and also easy to handle
meta-theoretically---but !!{derivation}s in them are hard to read and
understand, and are also hard to produce.
Other !!{derivation} systems have been developed with the aim of
making it easier to construct !!{derivation}s or easier to understand
!!{derivation}s once they are complete. Examples are natural
deduction, truth trees, also known as tableaux proofs, and the sequent
calculus. Some !!{derivation} systems are designed especially with
mechanization in mind, e.g., the resolution method is easy to
implement in software (but its !!{derivation}s are essentially
impossible to understand). Most of these other !!{derivation} systems
represent !!{derivation}s as trees of !!{formula}s rather than
sequences. This makes it easier to see which parts of !!a{derivation}
depend on which other parts.
So for a given logic, such as first-order logic, the different
!!{derivation} systems will give different explications of what it is
for !!a{sentence} to be a \emph{theorem} and what it means for
!!a{sentence} to be !!{derivable} from some others. However that is
done (via axiomatic !!{derivation}s, natural deductions, sequent
!!{derivation}s, truth trees, resolution refutations), we want these
relations to match the semantic notions of validity and
entailment. Let's write $\Proves !A$ for ``$!A$~is a theorem'' and
``$\Gamma \Proves !A$'' for ``$!A$~is !!{derivable} from~$\Gamma$.''
However $\Proves$~is defined, we want it to match up with $\Entails$,
that is:
\begin{enumerate}
\item $\Proves !A$ if and only if $\Entails !A$
\item $\Gamma \Proves !A$ if and only if $\Gamma \Entails !A$
\end{enumerate}
The ``only if'' direction of the above is called
\emph{soundness}. !!^a{derivation} system is sound if !!{derivability}
guarantees entailment (or validity). Every decent !!{derivation}
system has to be sound; unsound !!{derivation} systems are not useful
at all. After all, the entire purpose of !!a{derivation} is to provide
a syntactic guarantee of validity or entailment. We'll prove soundness
for the !!{derivation} systems we present.
The converse ``if'' direction is also important: it is called
\emph{completeness}. A complete !!{derivation} system is strong enough
to show that $!A$~is a theorem whenever $!A$~is valid, and that
$\Gamma \Proves !A$ whenever $\Gamma \Entails !A$.
Completeness is harder to establish, and some logics have no complete
!!{derivation} systems. First-order logic does. Kurt G\"odel was the
first one to prove completeness for !!a{derivation} system of
first-order logic in his 1929 dissertation.
Another concept that is connected to !!{derivation} systems is that of
\emph{consistency}. A set of !!{sentence}s is called inconsistent if
anything whatsoever can be !!{derive}d from it, and consistent
otherwise. Inconsistency is the syntactic counterpart to
unsatisfiablity: like unsatisfiable sets, inconsistent sets of
!!{sentence}s do not make good theories, they are defective in a
fundamental way. Consistent sets of !!{sentence}s may not be true or
useful, but at least they pass that minimal threshold of logical
usefulness. For different !!{derivation} systems the specific
definition of consistency of sets of !!{sentence}s might differ, but
like~$\Proves$, we want consistency to coincide with its semantic
counterpart, satisfiability. We want it to always be the case that
$\Gamma$ is consistent if and only if it is satisfiable. Here, the
``only if'' direction amounts to completeness (consistency guarantees
satisfiability), and the ``if'' direction amounts to soundness
(satisfiability guarantees consistency). In fact, for classical
first-order logic, the two versions of soundness and completeness are
equivalent.
\end{document}

content/first-order-logic/proof-systems/sequent-calculus.tex

67 lines; SHA-256 9a847c7bd45afe0d177230807fb2ba9dda820b4c0551a9274002db8776182003. Open the preserved source file.

% Part: first-order-logic
% Chapter: proof-systems
% Section: seqeunt-calculus
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{prf}{seq}}
{\olfileid{pl}{prf}{seq}}
\olsection{The Sequent Calculus}
While many !!{derivation} systems operate with arrangements of
!!{sentence}s, the sequent calculus operates with \emph{sequents}. A
sequent is an expression of the form
\[
!A_1, \dots, !A_m \Sequent !B_1, \dots, !B_m,
\]
that is a pair of sequences of !!{sentence}s, separated by the sequent
symbol~$\Sequent$. Either sequence may be empty. !!^a{derivation} in
the sequent calculus is a tree of sequents, where the topmost sequents
are of a special form (they are called ``initial sequents'' or
``axioms'') and every other sequent follows from the sequents
immediately above it by one of the rules of inference. The rules of
inference either manipulate the !!{sentence}s in the sequents (adding,
removing, or rearranging them on either the left or the right), or
they introduce a complex !!{formula} in the conclusion of the rule.
For instance, the $\LeftR{\land}$ rule allows the inference from $!A,
\Gamma \Sequent \Delta$ to $!A \land !B, \Gamma \Sequent \Delta$, and
the $\RightR{\lif}$ allows the inference from $!A, \Gamma \Sequent
\Delta, !B$ to $\Gamma \Sequent \Delta, !A \lif !B$, for any $\Gamma$,
$\Delta$, $!A$, and~$!B$. (In particular, $\Gamma$ and~$\Delta$ may be
empty.)
The $\Proves$ relation based on the sequent calculus is defined as
follows: $\Gamma \Proves !A$ iff there is some sequence $\Gamma_0$
such that every $!A$ in $\Gamma_0$ is in~$\Gamma$ and there is a
!!{derivation} with the sequent~$\Gamma_0 \Sequent !A$ at its root.
$!A$ is a theorem in the sequent calculus if the sequent~$\Sequent !A$
has !!a{derivation}. For instance, here is !!a{derivation} that shows
that $\Proves (!A \land !B) \lif !A$:
\begin{prooftree}
\Axiom$!A \fCenter !A$
\RightLabel{\LeftR{\land}}
\UnaryInf$!A \land !B \fCenter !A$
\RightLabel{\RightR{\lif}}
\UnaryInf$\fCenter (!A \land !B) \lif !A$
\end{prooftree}
A set $\Gamma$ is inconsistent in the sequent calculus if there is
!!a{derivation} of $\Gamma_0 \Sequent$ (where every $!A \in \Gamma_0$
is in~$\Gamma$ and the right side of the sequent is empty). Using the
rule \RightR{\Weakening}, any !!{sentence} can be !!{derive}d from an
inconsistent set.
The sequent calculus was invented in the 1930s by Gerhard Gentzen.
Because of its systematic and symmetric design, it is a very useful
formalism for developing a theory of !!{derivation}s. It is relatively
easy to find !!{derivation}s in the sequent calculus, but these
!!{derivation}s are often hard to read and their connection to proofs
are sometimes not easy to see. It has proved to be a very elegant
approach to !!{derivation} systems, however, and many logics have
sequent calculus systems.
\end{document}

content/first-order-logic/proof-systems/natural-deduction.tex

90 lines; SHA-256 c203daa5161eed34188e9fb9022b83be4f0201904f31cef386c5b838fb9e7d49. Open the preserved source file.

% Part: first-order-logic
% Chapter: proof-systems
% Section: natural-deduction
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{prf}{ntd}}
{\olfileid{pl}{prf}{ntd}}
\olsection{Natural Deduction}
Natural deduction is !!a{derivation} system intended to mirror actual
reasoning (especially the kind of regimented reasoning employed by
mathematicians). Actual reasoning proceeds by a number of ``natural''
patterns. For instance, proof by cases allows us to establish a
conclusion on the basis of a disjunctive premise, by establishing that
the conclusion follows from either of the disjuncts. Indirect proof
allows us to establish a conclusion by showing that its negation leads
to a contradiction. Conditional proof establishes a conditional claim
``if \dots then \dots'' by showing that the consequent follows from
the antecedent. Natural deduction is a formalization of some of these
natural inferences. Each of the logical connectives and quantifiers
comes with two rules, an introduction and an elimination rule, and
they each correspond to one such natural inference pattern. For
instance, $\Intro{\lif}$ corresponds to conditional proof, and
$\Elim{\lor}$ to proof by cases. A particularly simple rule is
$\Elim{\land}$ which allows the inference from $!A \land !B$ to~$!A$
(or $!B$).
One feature that distinguishes natural deduction from other
!!{derivation} systems is its use of assumptions. !!^a{derivation} in
natural deduction is a tree of !!{formula}s. A single !!{formula}
stands at the root of the tree of !!{formula}s, and the ``leaves'' of
the tree are !!{formula}s from which the conclusion is derived. In
natural deduction, some leaf !!{formula}s play a role inside the
!!{derivation} but are ``used up'' by the time the !!{derivation}
reaches the conclusion. This corresponds to the practice, in actual
reasoning, of introducing hypotheses which only remain in effect for a
short while. For instance, in a proof by cases, we assume the truth
of each of the disjuncts; in conditional proof, we assume the truth of
the antecedent; in indirect proof, we assume the truth of the negation
of the conclusion. This way of introducing hypothetical assumptions
and then doing away with them in the service of establishing an
intermediate step is a hallmark of natural deduction. The formulas at
the leaves of a natural deduction !!{derivation} are called
assumptions, and some of the rules of inference may ``!!{discharge}''
them. For instance, if we have !!a{derivation} of~$!B$ from some
assumptions which include~$!A$, then the $\Intro{\lif}$ rule allows us
to infer~$!A \lif !B$ and discharge any assumption of the form~$!A$.
(To keep track of which assumptions are discharged at which
inferences, we label the inference and the assumptions it discharges
with a number.) The assumptions that remain !!{undischarged} at the
end of the !!{derivation} are together sufficient for the truth of the
conclusion, and so !!a{derivation} establishes that its
!!{undischarged} assumptions entail its conclusion.
The relation $\Gamma \Proves !A$ based on natural deduction holds iff
there is !!a{derivation} in which $!A$~is the last !!{sentence} in the
tree, and every leaf which is !!{undischarged} is in~$\Gamma$. $!A$~is
a theorem in natural deduction iff there is !!a{derivation} in which
$!A$~is the last !!{sentence} and all assumptions are !!{discharged}.
For instance, here is !!a{derivation} that shows that $\Proves (!A
\land !B) \lif !A$:
\begin{prooftree}
\AxiomC{$\Discharge{!A \land !B}{1}$}
\RightLabel{\Elim{\land}}
\UnaryInfC{$!A$}
\DischargeRule{\Intro{\lif}}{1}
\UnaryInfC{$(!A \land !B) \lif !A$}
\end{prooftree}
The label~$1$ indicates that the assumption $!A \land !B$ is
!!{discharged} at the \Intro{\lif} inference.
A set~$\Gamma$ is inconsistent iff $\Gamma \Proves \lfalse$ in natural
deduction. The rule \FalseInt{} makes it so that from an inconsistent
set, any !!{sentence} can be !!{derive}d.
Natural deduction systems were developed by Gerhard Gentzen and
Stanis\l{}aw Ja\'skowski in the 1930s, and later developed by Dag
Prawitz and Frederic Fitch. Because its inferences mirror natural
methods of proof, it is favored by philosophers. The versions
developed by Fitch are often used in introductory logic textbooks. In
the philosophy of logic, the rules of natural deduction have sometimes
been taken to give the meanings of the logical operators
(``proof-theoretic semantics'').
\end{document}

content/first-order-logic/proof-systems/tableaux.tex

89 lines; SHA-256 6abf691f97c618dd41bc0c30a21dcf74fa7025228aa378cfd9f0369a898c2966. Open the preserved source file.

% Part: first-order-logic
% Chapter: proof-systems
% Section: tableaux
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{prf}{tab}}
{\olfileid{pl}{prf}{tab}}
\olsection{\usetoken{P}{tableau}}
While many !!{derivation} systems operate with arrangements of
!!{sentence}s, !!{tableau}s operate with !!{signed formula}s.
!!^a{signed formula} is a pair consisting of a truth value sign
($\True$ or $\False$) and !!a{sentence}
\[
\sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.
\]
!!^a{tableau} consists of !!{signed formula}s arranged in a
downward-branching tree. It begins with a number of \emph{assumptions}
and continues with !!{signed formula}s which result from one of the
!!{signed formula}s above it by applying one of the rules of
inference. Each rule allows us to add one or more !!{signed formula}s
to the end of a branch, or two !!{signed formula}s side by side---in
this case a branch splits into two, with the two added !!{signed
formula}s forming the ends of the two branches.
A rule applied to a complex !!{signed formula} results in the addition
of !!{signed formula}s which are immediate sub-!!{formula}s. They come
in pairs, one rule for each of the two signs. For instance, the
$\TRule{\True}{\land}$ rule applies to $\sFmla{\True}{!A \land !B}$,
and allows the addition of both the two !!{signed formula}s
$\sFmla{\True}{!A}$ and~$\sFmla{\True}{!B}$ to the end of any branch
containing $\sFmla{\True}{!A \land !B}$, and the rule
$\TRule{\False}{!A \land !B}$ allows a branch to be split by adding
$\sFmla{\False}{!A}$ and $\sFmla{\False}{!B}$ side-by-side.
!!^a{tableau} is closed if every one of its branches contains a
matching pair of !!{signed formula}s $\sFmla{\True}{!A}$ and
$\sFmla{\False}{!A}$.
The $\Proves$ relation based on !!{tableau}s is defined as follows:
$\Gamma \Proves !A$ iff there is some finite set~$\Gamma_0 = \{!B_1,
\dots, !B_n\} \subseteq \Gamma$ such that there is a closed !!{tableau}
for the assumptions
\[
\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
\]
For instance, here is a closed !!{tableau} that shows that $\Proves
(!A \land !B) \lif !A$:
\begin{oltableau}
[\sFmla{\False}{(\formula{A} \land \formula{B}) \lif \formula{A}}, just = \TAss
[\sFmla{\True}{\formula{A} \land \formula{B}}, just = {\TRule{\False}{\lif}[1]}
[\sFmla{\False}{\formula{A}}, just = {\TRule{\False}{\lif}[1]}
[\sFmla{\True}{\formula{A}}, just = {\TRule{\True}{\lif}[2]}
[\sFmla{\True}{\formula{B}}, just = {\TRule{\True}{\lif}[2]}, close]
]
]
]
]
\end{oltableau}
A set $\Gamma$ is inconsistent in the !!{tableau} calculus if there is
a closed !!{tableau} for assumptions
\[
\{\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
\]
for some $!B_i \in \Gamma$.
!!^{tableau}s were invented in the 1950s independently by Evert
Beth and Jaakko Hintikka, and simplified and popularized by Raymond
Smullyan. They are very easy to use, since constructing !!a{tableau} is a
very systematic procedure. Because of the systematic nature of
!!{tableau}s, they also lend themselves to implementation by
computer. However, !!a{tableau} is often hard to read and their
connection to proofs are sometimes not easy to see. The approach is
also quite general, and many different logics have !!{tableau}
systems. !!^{tableau}s also help us to find !!{structure}s that
satisfy given (sets of) !!{sentence}s: if the set is satisfiable, it
won't have a closed !!{tableau}, i.e., any !!{tableau} will have an
open branch. The satisfying !!{structure} can be ``read off'' an open
branch, provided every rule it is possible to apply has been applied
on that branch. There is also a very close connection to the sequent
calculus: essentially, a closed !!{tableau} is a condensed
!!{derivation} in the sequent calculus, written upside-down.
\end{document}

content/first-order-logic/proof-systems/axiomatic-deduction.tex

83 lines; SHA-256 0269390efeb94a0522020ce00d45f1d1e752e4a32db564b7519d7a939fa13034. Open the preserved source file.

% Part: first-order-logic
% Chapter: proof-systems
% Section: axiomatic-deduction
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\iftag{FOL}
{\olfileid{fol}{prf}{axd}}
{\olfileid{pl}{prf}{axd}}
\olsection{Axiomatic \usetoken{P}{derivation}}
Axiomatic !!{derivation}s are the oldest and simplest logical
!!{derivation} systems. Its !!{derivation}s are simply sequences of
!!{sentence}s. A sequence of !!{sentence}s counts as a correct
!!{derivation} if every !!{sentence}~$!A$ in it satisfies one of the
following conditions:
\begin{enumerate}
\item $!A$ is an axiom, or
\item $!A$ is !!a{element} of a given set~$\Gamma$ of !!{sentence}s, or
\item $!A$ is justified by a rule of inference.
\end{enumerate}
To be an axiom, $!A$ has to have the form of one of a number of fixed
!!{sentence} schemas. There are many sets of axiom schemas that
provide a satisfactory (sound and complete) !!{derivation} system for
first-order logic. Some are organized according to the connectives
they govern, e.g., the schemas
\[
!A \lif (!B \lif !A) \qquad !B \lif (!B \lor !C) \qquad (!B \land !C) \lif !B
\]
are common axioms that govern $\lif$, $\lor$ and~$\land$. Some axiom systems
aim at a minimal number of axioms. Depending on the connectives that
are taken as primitives, it is even possible to find axiom systems
that consist of a single axiom.
A rule of inference is a conditional statement that gives a sufficient
condition for !!a{sentence} in !!a{derivation} to be justified. Modus
ponens is one very common such rule: it says that if $!A$ and $!A \lif
!B$ are already justified, then $!B$ is justified. This means that a
line in !!a{derivation} containing the !!{sentence}~$!B$ is justified,
provided that both $!A$ and $!A \lif !B$ (for some !!{sentence}~$!A$)
appear in the !!{derivation} before~$!B$.
The $\Proves$ relation based on axiomatic !!{derivation}s is defined
as follows: $\Gamma \Proves !A$ iff there is !!a{derivation} with the
!!{sentence}~$!A$ as its last formula (and $\Gamma$ is taken as the
set of !!{sentence}s in that !!{derivation} which are justified by~(2) above). $!A$
is a theorem if~$!A$ has !!a{derivation} where~$\Gamma$ is empty,
i.e., every !!{sentence} in the !!{derivation} is justified either by (1)
or~(3). For instance, here is !!a{derivation} that shows that $\Proves
!A \lif (!B \lif (!B \lor !A))$:
\begin{derivation}
1. & $!B \lif (!B \lor !A)$ \\
2. & $(!B \lif (!B \lor !A)) \lif (!A \lif (!B \lif (!B \lor !A)))$\\
3. & $!A \lif (!B \lif (!B \lor !A))$
\end{derivation}
The !!{sentence} on line~1 is of the form of the axiom $!A \lif (!A
\lor !B)$ (with the roles of $!A$ and $!B$ reversed). The sentence on
line~2 is of the form of the axiom $!A \lif (!B \lif !A)$. Thus, both
lines are justified. Line~3 is justified by modus ponens: if we
abbreviate it as $!D$, then line~2 has the form $!C \lif !D$, where
$!C$ is $!B \lif (!B \lor !A)$, i.e., line~1.
A set $\Gamma$ is inconsistent if $\Gamma \Proves \lfalse$. A complete
axiom system will also prove that $\lfalse \lif !A$ for any~$!A$, and
so if $\Gamma$ is inconsistent, then $\Gamma \Proves !A$ for any~$!A$.
Systems of axiomatic !!{derivation}s for logic were first given by
Gottlob Frege in his 1879 \emph{Begriffsschrift}, which for this
reason is often considered the first work of modern logic. They were
perfected in Alfred North Whitehead and Bertrand Russell's
\emph{Principia Mathematica} and by David Hilbert and his students in
the 1920s. They are thus often called ``Frege systems'' or ``Hilbert
systems.'' They are very versatile in that it is often easy to find
an axiomatic system for a logic. Because !!{derivation}s have a very
simple structure and only one or two inference rules, it is also
relatively easy to prove things \emph{about} them. However, they are
very hard to use in practice, i.e., it is difficult to find and write
proofs.
\end{document}