Have you ever been in an argument where the other person “just wasn’t being reasonable?” What were they doing that was “without reason?”

- Making “facts” up out of thin air?
- Forming connections between claims without appropriate evidence?
- Jumping between unrelated arguments?
- Not addressing the problem at hand?

How do you know that you were being reasonable and your partner was the unreasonable one? Is there an agreed-upon set of rules for what it means to operate “within reason” or is it simply a matter of perspective?

*Mathematical logic* is the study of formal logical reasoning.
Coincidentally, logic itself is one of the foundations of both
mathematics and computer science. Recall that mathematical prose
contains *propositions* that assert relationships between
definitions. These propositions are stated in terms of mathematical
logic and thus form one of the cornerstones of the discipline.

As computer scientists, we care about logic for similar reasons. We care about the properties of the algorithms we design and implement, in particular, their correctness and complexity. Logic gives us a way of stating and reasoning about these properties in a precise manner.

# Propositional Logic

Let us begin to formalize our intuition about propositions. First, how can we classify propositions? We can classify them into two buckets:

**Atomic propositions**that make elementary claims about the world. “It is beautiful today” and “it rainy today” are both elementary claims about the weather.**Compound propositions**that are composed of smaller propositions “It is either rainy today or it is beautiful today” is a single compound proposition made of up two atomic propositions.

This is not unlike arithmetic expressions that contain atomic
parts—integers—and compound parts—operators. As you learned about
arithmetic throughout grade school, you learned about each operator and
how they transformed their inputs in different ways. Likewise, we will
learn about the different logical operators—traditionally called
*connectives* in mathematical logic—and how they operate over
propositions.

We can formally define the *syntax* of a proposition \(p\) similarly to arithmetic using a
grammar:

\[ p ::= A \mid \top \mid \bot \mid \neg p \mid p_1 \wedge p_2 \mid p_1 \vee p_2 \mid p_1 \rightarrow p_2. \]

A grammar defines for a sort (the proposition \(p\)) its set of allowable syntactic forms, each written between the pipes (\(\mid\)). A proposition can take on one of the following forms:

**Atomic propositions**, elementary claims about whatever domain we are considering. When we don’t care about the particular domain (*e.g.*, we want to hold the domain*abstract*), we’ll use capital letters such as \(A\) as meta-variables for atomic propositions.**Top**, \(\top\) (LaTeX:`\top`

), pronounced “top”, the proposition which is*always provable*.**Bot**, \(\bot\) (LaTeX:`\bot`

), pronounced “bottom” or “bot”, the proposition which is*never provable*.**Logical negation**, \(\neg p\) (LaTeX:`\neg`

), pronounced “not”, which stands for proposition \(p\), but*negated*. For example, the negation of \(p\) = “It is beautiful today” is \(\neg p\) = “It is*not*beautiful today”.**Logical conjunction**, \(p_1 \wedge p_2\) (LaTeX:`\wedge`

), pronounced “and”, which stands for the proposition where both \(p_1\) and \(p_2\) are provable. For example, the conjunction of \(p_1\) = “It is beautiful today” and \(p_2\) = “The sun is out” claims that it is*both*beautiful and the sun is out.**Logical disjunction**, \(p_1 \vee p_2\) (LaTeX:`\vee`

), pronounced “or”, which stands for the proposition where at least one of \(p_1\) or \(p_2\) is provable. For example, the disjunction of \(p_1\) = “It is beautiful today” and \(p_2\) = “It is raining today” claims that it is either beautiful today or it is raining today (or both are true).**Logical implication**, \(p_1 \rightarrow p_2\) (LaTeX:`\rightarrow`

), pronounced “implies”, which stands for the proposition where \(p_2\) is provable*assuming*\(p_1\) is provable. For example, if \(p_1\) = “It is cloudy” and \(p_2\) = “It is raining”, then \(p_1 \rightarrow p_2\) claims that it is raining, assuming that it is cloudy.

Notably, logical implication are the *conditional*
propositions we have seen previously of the form “if … then … .” For
example, if we had the following program correctness claim:

**Claim**: for all natural numbers `n`

, if
`(>= n 0)`

then `(> (factorial n) 0)`

.

We might write it concisely using the formal notation above as:

**Claim**: for all natural numbers `n`

,
`(>= n 0)`

\(\rightarrow\)
`(> (factorial n) 0)`

.

This form of logic is called *propositional logic* because it
focuses on propositions and basic logic connectives between them. There
exist more exotic logics that build upon propositional logic with
additional connectives that capture richer sorts of propositions we
might consider.

## Modeling with Propositions

Recall that mathematics is the study of modeling the world. In the
case of mathematical logic, we would like to model real-world
propositions using the language of mathematical propositions we have
defined so far. This amounts to *translating* our informal
natural language descriptions into formal mathematical descriptions.

To do this, keep in mind that mathematical propositions are formed from atomic and compound propositions. We then need to:

Identify the atomic propositions in the statement.

Determine how the atomic propositions are related through various compound propositions.

As an example, let’s consider a proposition more complicated than the previous ones that we have encountered:

“If it is either the case that the grocer delivers our food on time, or I get out to the store this morning, then the party will start on time and people will be happy.

First, we identify the domain under which we are making this
proposition: *preparing for a party*. Thus, the atomic
propositions are the statements that directly talk about preparing for a
party. These propositions are:

- \(p_1\) = “The grocer delivers our food on time.”
- \(p_2\) = “I get out to the store this morning.”
- \(p_3\) = “The party will start on time.”
- \(p_4\) = “People will be happy.”

Now, we re-analyze the statement to determine how the propositions are related, translating those relations into logical connectives. You may find it helpful to replace every occurrence of the atomic propositions with variables to make the connecting language pop out:

“If it is either the case that \(p_1\) or \(p_2\) then \(p_3\) and \(p_4\).”

From this reformulation of the statement, we can see that:

- \(p_1\) and \(p_2\) are related by the word “or” which implies disjunction.
- \(p_3\) and \(p_4\) are related by the word “and” which implies conjunction.
- These previous two compound conjunctions are related by the words “if” and “then” which implies implication.

Thus we arrive at our full formalization of the statement:

\[ p_1 \vee p_2 \rightarrow p_3 \wedge p_4. \]

(Note that \((\rightarrow)\) has lower precedence than \((\vee)\) or \((\wedge)\) so the statement written as-is is not ambiguous.)

When translating statements in this manner, it is useful to keep in mind some key words that usually imply the given connective:

- \((\neg)\): “not”
- \((\wedge)\): “and”
- \((\vee)\): “or”
- \((\rightarrow)\): “implies”, “if …then”

## Reasoning with Propositions

Recall that our goal is to formally model reasoning. While
equivalences allow us to show that two propositions are equivalent, they
do not tell us how to *reason* with propositions. That is, how do
we *prove* propositions once they have been formally stated?

First, we must understand the reasoning process itself so that we can understand its parts. From there, we can state rules in terms of manipulating these parts. When we are trying to prove a proposition, whether it is in the context of a debate, an argument with a friend, or a mathematical proof, our proving process can be broken up into two parts:

- A set of
*assumptions*, propositions that we are assuming are true. - The proposition that we are currently trying to prove, our
*proof goal*.

We call this pair of objects our *proof state*. Our ultimate
goal when proving a proposition is to *transform* the proof goal
into an “obviously” correct statement through valid applications of
*proof rules*.

For example, if we are in the midst of a political debate, we might be tasked with proving the statement:

“80s-era Reaganomics is the solution to our current economic crisis.”

Our proof goal is precisely this statement and our set of assumptions
includes our knowledge of Reaganomics and the current economy. We might
take a step of reasoning—*unfolding* the definition of
Reaganomics, for example—to refine our goal:

“

Economic policies associated with tax reduction and the promotion of the free-marketare the solution to our current economic crisis.”

We can then apply additional assumptions and logical rules to transform this statement further. Once our logical argument has transformed the statement into a self-evident form, for example:

“Everyone needs money to live.”

Then, if everyone agrees this is a true statement, we’re done!
Because the current proof goal follows logically from assumptions and
appropriate uses of logical rules, we know that if this proposition is
true, then our original proposition is true. In a future reading, we
will study these rules in detail in a system called *natural
deduction*.

## Propositional Logic Versus Boolean Algebra

Throughout this discussion, you might have noted similarities between
propositions and a concept you have encountered previously in
programming: booleans. Values of *boolean type* take on one of
two forms, `true`

and `false`

, and there are
various operators between booleans, `&&`

and
`||`

,logical-AND and logical-OR, respectively. It seems like
we can draw the following correspondence between propositions and
booleans (using the boolean operators found in a C-like language):

- \(\top\) is
`true`

. - \(\bot\) is
`false`

. - \((\neg)\) is
`!`

. - \((\wedge)\) is
`&&`

. - \((\vee)\) is
`||`

.

This correspondence is quite accurate! In particular, the equivalences we discussed in the previous section for propositions also work for boolean expressions. The only caveat is that there is no analog to implication for the usual boolean expressions, but the equivalence:

\[ p_1 \rightarrow p_2 \equiv \neg p_1 \vee p_2 \]

Allows us to translate an implication into an appropriate boolean expression.

So why do we talk about propositions when booleans exist? It turns out they serve subtle, yet distinct purposes!

- A proposition is a statement that may be proven.
- A boolean expression is an expression that evaluates to
`true`

or`false`

.

Note that a proposition does not say anything about whether the claim
is true or false. It also doesn’t say anything *computational* in
nature, unlike a boolean expression which carries with it an
*evaluation semantics* for how to evaluate it in the context of a
larger computer program.

Furthermore, the scope of a boolean expression is narrow: we care
about booleans values insofar as they assist in controlling the flow of
a program, *e.g.*, with conditionals and loops. We don’t need to
complicate booleans any further! In contrast, propositions concern
arbitrary statements, and our language of propositions may need to be
richer than the corresponding language of booleans to capture the
statements we have in mind.

**Exercise (Translation, ‡)**: Consider the following
propositions

- \(p_1\) = “The sky is cloudy.”
- \(p_2\) = “I will go running today.”
- \(p_3\) = “I’m going to eat a cheeseburger.”

Write down English translations of these formal statements:

- \(p_2 \vee p_3\).
- \(p_1 \rightarrow p_3 \rightarrow
p_2\). (
*Note*: implication is a right-associative operator! This means that this statement is equivalent to \(p_1 → (p_3 → p_2)\)). - \(p_1 \rightarrow p_2 \wedge \neg p_3\).

**Exercise (Funny Nesting)**: Recall that implication is
*right-associative*. That is, sequences of \((→)\) operators parenthesize “to the
right”, *i.e.*,

\[ p_1 → p_2 → p_3 ≡ p_1 → (p_2 → p_3). \]

Now, consider the abstract proposition where we instead parenthesize to the left:

\[ (p_1 → p_2) → p_3. \]

Come up with concrete instantiations of \(p_1\), \(p_2\), and \(p_3\) and write down the English translation of this proposition.

# First-order Logic

Propositional logic gives us a formal language for expressing
propositions about mathematical objects. However, is it sufficiently
*expressive*? That is, can we write down *any* proposition
we might have in mind using propositional logic?

On the surface, this seems to be the case because we can instantiate our atomic propositions to be whatever we would like. For example, consider the following proposition:

Every month has a day in which it rains.

We can certainly take this *entire* proposition to be an
atomic proposition, *i.e.*,

\[ P = \text{Every month has a day in which it rains}. \]

However, this is not an ideal encoding of the proposition in logic!
Why is this the case? We can see that there is *structure* to the
claim that is lost by taking the whole proposition to be atomic. In this
case, the notion of “every” month is not distinguished from the rest of
the proposition. This is a common idea in propositions, for example:

- For every natural number \(n\), \(n > 0\).
- For any boolean expression \(e\), \(e ⟶^* \mathsf{true}\).
- For any pair of people in the group, they are friends with each other.

We would like our formal language of logic to capture this idea of “every” as a distinguished form so that we can reason about it precisely. However, propositional logic has no such form!

To this end, we introduce a common extension to proposition logic,
*predicate logic* (also known as *first-order-logic*),
which introduces a notion of *quantification* to propositions.
Quantification captures precisely this concept of “every” we have
identified, and more!

## Introducing Quantification

When we express the notion of “every month” or “any pair of people,”
we are really introducing unknown quantities, *i.e.*, variables,
into our propositions. For example, our sample proposition above
introduces two such variables, months and days. At first glance, we
might try expressing the proposition as an abstract proposition,
*i.e.*, a function that expects a month and day and produces a
proposition:

\[ P(x, y) = x\;\text{has}\;y ∧ \text{it rains during}\;y. \]

We call such functions that produce propositions
*predicates*.

However, this encoding of our proposition is not quite accurate! If we think carefully about the situation, we will note that the interpretation of \(x\) and \(y\) are subtlety different! We can make this more clear by a slight rewriting of our original proposition:

For every month, there exists a day in which it rains.

Note how we are interested in “every month.” However, we are not
interested in “every day”; we only identify a *single* day in
which the property holds. The property may hold for more than one day
for any given month, but we only care that there is at least one such
day.

Thus, we find ourselves needing to *quantify* our variables in
two different ways:

- Any value (of a given type).
- At least one value (of a given type).

Observe that our predicate notation \(P(x, y)\) does not tell us which quantification we are using!

First-order logic extends propositional logic with two additional connectives that make explicit this quantification:

\[ p ::= \ldots \mid A(x) \mid \forall x.\,p \mid \exists x.\,p \]

**Universal quantification of a proposition**, written \(\forall x.\,p\) (pronounced “for all \(x\), \(p\)”, LaTeX:`\forall`

) introduces a universally quantified variable \(x\) that may be mentioned inside of \(p\).**Existential quantification of a proposition**, written \(\exists x.\,p\) (pronounced “there exists \(x\), \(p\)”, LaTeX:`\exists`

) introduces an existentially quantified variable \(x\) that may be mentioned inside of \(p\).

These quantified variables may then appear inside of our atomic
propositions. We write \(A(x)\) to
remind ourselves that our atomic propositions may be
*parameterized* by these quantified variables.

With quantifiers, we can now fully specify our example in first-order logic:

\[ P = ∀x \ldotp ∃y \ldotp x\;\text{has}\;y ∧ \text{it rains during}\;y. \]

The first quantifier \(∀x\)
introduces a new variable \(x\) that is
interpreted *universally*. That is, the following proposition
holds *for every possible value of \(x\)*. The second quantifier \(∃y\) introduces a new variable \(y\) that is interpreted
*existentially*. That is, the following proposition holds *for
at least one possible value of \(y\)*. When taken together, our English
pronunciation of this formal proposition now lines up with our
intuition:

For all months \(x\), there exists a day \(y\) where \(x\) has \(y\) and it rains during \(y\).

## Variables and Scope in Mathematics

Like function headers in a programming language, quantifiers
*introduce* variables into our propositions. For example,
consider the following Racket function definition:

```
(define length
(lambda (lst)
(match lst
['() 0]
[(cons head tail) (+ 1 (length tail))])))
```

Here, the `lambda`

form introduces a new program variable
`lst`

that may be used anywhere inside of the function bound
to `length`

. However, `lst`

has no meaning outside
of `length`

. The location where a variable has meaning is
called its *scope*:

**Definition (Scope)**: the *scope* of a variable
is the region in which that variable has meaning.

In the case of functions, the scope of a parameter is the body of its
enclosing function. So if we try to evaluate `lst`

outside of
the definition of `length`

, we receive an error:

```
> (length (list 1 2 3))
3
> lst
lst: undefined;
cannot reference an identifier before its definition
```

The same principles hold for logical variables. The quantifiers \(∀x \ldotp p\) and \(∃x \ldotp p\) introduce an appropriately quantified variable \(c\) that has scope inside of \(p\). \(x\) does not have meaning outside of \(p\). For example, the proposition:

\[ P = x > 5 ∧ ∀x \ldotp x ≠ 0. \]

Is malformed because the \(x\) outside the quantifier is not well-scoped.

## Implicit Types and Quantification

Variables are always quantified according to a particular set of
values, its *type*. However, you may have noticed that we never
mention the type of a variable in its quantification. How do we know
what the type of \(x\) is in \(∀x \ldotp p\)? Traditionally, we
*infer* the types of variables based on their usage.

For example, in the proposition:

\[ ∀x \ldotp ∃y \ldotp x > y. \]

We can see that \(x\) and \(y\) are used in a numeric comparison \((>)\), so we assume that the quantified
variables range over numbers. Could the variables be quantified more
specifically? Certainly! \(x\) and
\(y\) could certainly be real numbers,
integers, or even the natural numbers (*i.e.*, the positive
integers or zero). We would need to look at more surrounding context,
*e.g.*, how this proposition is used in a larger mathematical
text, to know whether the variables can be typed in more specific
ways.

In addition to implicit types, sometimes quantification is also implicit. For example, the standard statement of the Pythagorean theorem is:

\[ a^2 + b^2 = c^2 \]

Where the quantification of \(a\),
\(b\), and \(c\) is implicit. What is the implied
quantification of these variables? It turns out that when a quantifier
is omitted, we frequently intend for the variables to be
*universally* quantified, *i.e.*, the Pythagorean theorem
holds for any \(a\), \(b\), and \(c\) of appropriate types.

When writing mathematics, you should always explicitly quantify your variables so your intent is clear. However, you should be aware that implicit typing and quantification is pervasive in mathematical texts, so you will need to use inference and your best judgment to make sense of a variable.

**Exercise (Quantified Translation, ‡)**:

Consider the following parameterized propositions:

- \(A_1(x)\) = “\(x\) is a kitty.”
- \(A_2(x, y)\) = “\(x\) likes \(y\).”
- \(A_3(x)\) = “\(x\) is a dog.”

Translate these formal propositions into informal English descriptions:

- \(\exists x.\,\exists y.\,A_1(x) \wedge A_3(y)\).
- \(\forall x.\,\exists y.\,A_1(y) \rightarrow A_2(x, y)\).
- \(\forall x.\,\forall y.\,(A_1(x) \wedge A_3(y)) \rightarrow \neg A_2(x, y)\).

# Natural Deduction

So far we have discussed the objects of study of logic, the
*proposition*, defined recursively as:

\[ p ::= A(x) \mid \top \mid \bot \mid \neg p \mid p_1 \wedge p_2 \mid p_1 \vee p_2 \mid p_1 \rightarrow p_2 \mid \forall x.\,p \mid \exists x.\,p \]

However, recall that our purpose for studying propositional logic was
to develop rules for developing logically sound arguments. Equivalences,
while convenient to use in certain situations, *e.g.*, rewriting
complex boolean equations, do not translate into what we would consider
to be “natural” deductive reasoning.

Now, we present a system for performing *deductive reasoning*
within propositional logic. This system closely mirrors our intuition
about how we would prove propositions, thus giving it the name
*natural deduction*. As we explore how we formally define
deductive reasoning in this chapter, keep in mind your intuition about
how these connectives ought to work to help you navigate the symbols
that we use to represent this process.

## The Components of a Proof

To understand what are the components proof that we capture in natural deduction, let us scrutinize a basic proof involving the even numbers. First we remind ourselves what it means for a number to be even.

**Definition (Evenness)**: call a natural number \(n\) even if \(n =
2k\) for some natural number \(k \geq
0\).

In other words, an even number is a multiple of two. This intuition informs how we prove the following fact:

**Claim**: For any natural number \(n\), if \(n\) is even then \(4n\) is also even.

*Proof*. Let \(n\) be an even
natural number. Because \(n\) is even,
by the definition of evenness, \(n =
2k\) for some natural number \(k\). Then:

\[ 4n = 4(2k) = 8k = 2(4k). \]

So we can conclude that \(2n\) is also even by the definition of evenness because it can be expressed as \(2m\) where \(m = 4k\).

From the above proof, we can see that there is an overall proposition
that we must prove, called the **goal proposition**:

For any natural number \(n\), if \(n\) is even then \(4n\) is also even.

As the proof evolves, our goal proposition *changes* over time
according to the **steps of reasoning** that we take. For
example, implicit in the equational reasoning we do in the proof:

\[ 4n = 4(2k) \]

Is a *transformation* of our goal proposition, “\(4n\) is even,” to another proposition
“\(4(2k)\) is even.” Ultimately, our
steps of reasoning transform our goal repeatedly until the goal
proposition is “obviously” provable. In the proof above, we transform
our goal from “\(4n\) is even” to
“\(2(4k)\) is even” by the rules of
arithmetic. At this point, we can apply the definition of evenness
directly which says that a number is even if it can be expressed as a
multiple of two.

However, in addition to the goal proposition, there are also
**assumptions** that we acquire and use in the proof. For
example, the proposition “\(n\) is
even” becomes an assumption of our proof after we process the initial
goal proposition which is stated in the form of an implication, \(P \rightarrow Q\), where:

- \(P =\) “\(n\) is even”
- \(Q =\) “\(4n\) is even”

We then *utilize* this assumption in our steps of reasoning.
In particular, it is the assumption that \(n\) is even coupled with the definition of
evenness that allows us to conclude that \(n =
2k\) for some natural number \(k\). There exists other assumptions in our
proof as well, *e.g.*, \(n\) and
\(k\) are natural numbers, that we use
implicitly in our reasoning.

### Proof States and Proofs

We can crystallize these observations into the following definition of “proof.”

**Definition (Proof State)**: the **state of a
proof** or **proof state** is a pair of a *set of
assumptions* and a *goal proposition* to prove.

**Definition (Proof)**: a **proof** is a
sequence of logical steps that manipulate a proof state towards a final,
provable result.

In our above example, we initially started with a proof state consisting of:

- No assumptions.
- The initial claim as our goal proposition: “For any natural number \(n\), if \(n\) is even then \(4n\) is also even.”

After some steps of reasoning that breaks apart this initial goal, we arrived at the following proof state:

- Assumptions: “\(n\) is a natural number,” “\(n\) is even”
- Goal: “\(4n\) is even.”

At the end of the proof, we rewrote the goal in terms of a new variable \(m\) and performed some factoring, leading to the final proof state:

- Assumptions: “\(n\) and \(m\) are natural numbers,” “\(n\) is even,” “\(m = 4k\)”
- Goal: “\(2m\) is even”

This final goal is provable directly from the definition of evenness since the quantity \(2m\) is precisely two times a natural number.

## Rules of Natural Deduction

Our proof rules manipulate proof states, ultimately driving them
towards goal propositions that are directly provable through our
assumptions. Because of the syntax of our propositions breaks up
propositions into a finite set of cases, our rules operate by case
analysis on the syntax or *shape* of the propositions contained
in the proof state. Specifically, these propositions can either appear
as *assumptions* or in the *goal proposition*. Therefore,
for each kind of proposition, we give one or more rules describing how
we “process” that proposition depending on where it appears in the proof
goal.

- Rules that operate on propositions in the goal proposition are
called
*introduction rules*. This is because we typically first*introduce*various propositions when they initially appear in our goal. - Rules that operate on propositions in assumptions are called
*elimination rules*. These rules use or “consume” assumptions, resulting in more assumptions and/or an updated set of goals.

### A Note on the Presentation of Proof Rules

When we talk about *rules of proof* we really mean the set of
“allowable actions” that we can take on the current proof state. We
describe these rules in the following form:

To prove a proof state of the form … we can prove proof state(s) of the form …

One of our proof rules *applies* when it has the form
specified by the rule, *e.g.*, the goal proposition is a
conjunction or there is an implication in the assumption list. The
result of the proof rule is one or more *new* proof states that
we must now prove instead of the current state. In effect, the proof
rule *updates* the current state to be a new state (or set of
states) that becomes the new proof state under consideration.

In terms of notation, we will use \(p\) and \(q\) to denote arbitrary propositions.
Similarly, for assumptions, we will use the traditional metavariable
\(\Gamma\) (*i.e.*, Greek
uppercase Gamma, \(\LaTeX\):
`\Gamma`

) to represent an arbitrary set of assumptions. When
writing down our proof rules, it is very onerous to describe the
components of proof states in prose:

If our proof state contains assumptions \(\Gamma\) and goal proposition \(p\) … .

Instead, we will write down a proof state as a *pair* of a set
of assumptions and a proof state. Traditionally, we write pairs using
parentheses, separating the components of the pair with commas,
*e.g.*, a coordinate pair \((x,
y)\). However, in logic, we traditionally write this pair as a
stylized pair called a *sequent*:

\[ \Gamma \vdash p. \]

The turnstile symbol (\(\LaTeX\),
`\vdash`

) acts like the comma in the coordinate pair; it
merely creates visual separation between the assumptions \(\Gamma\) and the goal proposition \(p\).

### Conjunction and Assumptions

A conjunction, \(p_1 \wedge p_2\),
is a proposition that asserts that *both* propositions \(p_1\) and \(p_2\) are provable. For example, the
proposition “I’m running out of cheeseburgers and the sky is falling” is
a conjunction of two propositions: “I’m running out of cheeseburgers”
and “the sky is falling.” We call each of the sub-propositions of a
conjunction a *conjunct*.

First, let’s consider how we *prove* a proposition that is a
conjunction. If we have to prove the example proposition above, our
intuition tells that we must prove both “sides” of the conjunction. That
is, to show that the proposition “I’m running out of cheeseburgers and
they sky is falling”, we must show that both

- “I’m running out of cheeseburgers” and
- “the sky is falling”

Are true *independently* of each other. In particular, we
don’t get to rely on fact being true when going to prove the other
fact.

We can codify this intuition into the following *proof rule*
describing how we can process a conjunction when it appears as our proof
goal:

**Proof Rule [intro-∧]**: To prove \(\Gamma \vdash p_1 \wedge p_2\), we may
prove the following two proof states separately:

- \(\Gamma \vdash p_1\).
- \(\Gamma \vdash p_2\).

Recall that \(\Gamma \vdash p_1 \wedge p_2\) represents the following proof state:

- We assume that the assumptions in set \(\Gamma\) are provable.
- Our goal proposition we must prove is \(p_1 \wedge p_2\).

Our proof rule says that whenever we have a proof state of this form,
we can prove it by proving \(\Gamma \vdash
p_1\) and \(\Gamma \vdash p_2\)
as two separate cases. More generally, our *introduction rules*
describe, for each kind of proposition, how to prove that proposition
when it appears as a goal.

Note that this proof rule applies only when the *overall goal
proposition is of the form of a conjunction*. For example:

- If our goal is \(A \wedge B\), then the intro-∧ rule applies with \(p_1 = A\) and \(p_2 = B\).
- If our goal is \((A \rightarrow B) \wedge (C \wedge D)\), then the intro-∧ rule applies with \(p_1 = A \rightarrow B\) and \(p_2 = C \wedge D)\).

This rule cannot be applied if only a *sub-component* of the
goal proposition is a conjunction. For example, if our goal is \(A \rightarrow (B \wedge C)\), the rule does
not apply even though \(B \wedge C\) is
part of the goal.

Now, what happens if the conjunction appears to the left of the
turnstile, *i.e.*, as an assumption? From our
**intro-∧** rule, we know that if the conjunction is
provable, then *both* conjuncts are provable individually. So if
we know that “I’m running out of cheeseburgers and the sky is falling”
is provable, then we know that both conjuncts are true, *i.e.*,
“I’m running out of chesseburgers” and “the sky is falling.” The
following pair of rules captures this idea:

**Proof Rule [elim-∧-left]**: To prove \(\Gamma \vdash p\), if \(p_1 \wedge p_2 \in \Gamma\), then we may
prove \(p_1, \Gamma \vdash p\).

**Proof Rule [elim-∧-right]**: To prove \(\Gamma \vdash p\), if \(p_1 \wedge p_2 \in \Gamma\), then we may
prove \(p_2, \Gamma \vdash p\).

If we are trying to prove some proposition \(p\) and we assume that a conjunction \(p_1 \wedge p_2\) is true, then the two
rules say we can continue trying to prove \(p\), *but with an additional assumption
gained from the conjunction*. In terms of the new notation in these
rules:

- To state that \(p_1 \wedge p_2\) is
contained in \(\Gamma\), we write \(p_1 \wedge p_2 \in Gamma\) where the \((\in)\) symbol (\(\LaTeX\),
`\in`

) is pronounced “in.” - To add a new assumption to the set of assumptions \(\Gamma\), we “cons” on the new assumption,
*e.g.*, \(p_1\) in the elim-∧-left rule, by adding it to the front of \(\Gamma\) with a comma,*i.e.*, \(p_1, \Gamma\).

The **elim-∧-left** rule allows us to add the left
conjunct to our assumptions, and the **elim-∧-right** rule
allows us to add the right conjunct. In effect, these *elimination
rules* allow us to *decompose* or *extract
information* from assumptions. However, how do we use these
assumptions to prove a goal? The **assumption** rule allows
us to prove a goal proposition directly if it is one of our
assumptions.

**Proof Rule [assumption]**: If \(p \in \Gamma\), then \(\Gamma \vdash p\) is proven
immediately.

### Proofs in Natural Deduction

First-order logic and natural deduction give us all the definitions necessary for rigorously defining every step of reasoning in a proof. Let’s see this in action with a simple claim within formal propositional logic.

**Claim**: \(A, B \vdash A
\wedge B\).

First, let’s make sure we understand what the claim says. To the left of the turnstile are our set of assumptions. Here we assume that propositions \(A\) and \(B\) are provable. To the right of the turnstile is our goal. We are trying to prove that \(A \wedge B\) is provable.

Next, let’s develop a high-level proof strategy. Because we are working at such a low-level of proof, it is important to ask ourselves:

- Is the proof state as I understand it provable?
- How do the different parts of the proof state relate to each other?

In our example claim, we see that the proposition consists of atomic
propositions \(A\) and \(B\) joined by conjunction and those same
propositions appear as assumptions in the initial sequent. Thus, our
overall strategy in our proof will be to *decompose* the proof
goal into cases where we need to prove these individual cases directly
via our hypotheses.

With this in mind, let’s see what the formal proof looks like:

**Claim**: \(A, B \vdash A
\wedge B\).

*Proof*. By the intro-∧ rule, we must prove two new goals:

- Case \(A, B ⊢ A\). \(A\) is an assumption, so we are done.
- Case \(A, B ⊢ B\). \(B\) is an assumption, so we are done.

Because each proof rule creates *zero or more* additional
proof states that we must prove or *discharge*, our proofs take
on a *tree-like shape*. In a diagram, our reasoning would look as
follows:

```
A, B |- A /\ B
/ \
[intro-∧ (1)] [intro-∧ (2)]
/ \
A, B |- A A, B |- B
/ \
[assumption: A] [assumption: B]
```

Because the **intro-∧** rule creates two sub-goals we
must prove, we have two branches of reasoning emanating from our initial
proof state, one for each goal (labeled `(1)`

and
`(2)`

, respectively). We then prove each branch immediately
by invoking the appropriate assumption. *Every* proof, not just
in formal logic but in any context, has a hierarchical structure like
this.

We can write this hierarchical structure in linear prose with a bulleted list where indentation levels correspond to branching. Whenever we perform case analysis, we should be clear when we are entering different cases, usually through some kind of sub-heading or bullet-like structure.

Finally, note that we cite *every* step of our proof. This
“luxury” is afforded to us because our proof rules are now explicit and
precise—we can justify every step of reasoning as an invocation of one
of our proof rules!

**Exercise (Adaption):** Formally prove the following
claim in propositional logic:

**Claim**: \(A, B \vdash A
\wedge B \wedge A.\)

(*Hint*: remember that \((\wedge)\) is a left-associative
operator!)

### Implication

Next, let’s look at implication. An implication, \(p_1 \rightarrow p_2\), is a proposition
that asserts that whenever \(p_1\) is
provable, then \(p_2\) is provable as
well. For example, the proposition “If I’m running out of cheeseburgers
then the sky is falling” is an implication where “I’m running out of
cheeseburgers” is the *premise* of the implication and “the sky
is falling” is the *conclusion*.

Implication is closely related to the preconditions and
postconditions we analyzed in our study of program correctness. Pre- and
postconditions form an implication where the preconditions are premises
and the postcondition is a conclusion. When we went to prove a claim
that involved pre- and postconditions, we assumed that preconditions
held and went on to prove the postcondition. Likewise here, to prove an
implication, we *assume* the premises and then go on to
*prove* the conclusion.

**Proof Rule [intro-→]**: To prove \(\Gamma \vdash p_1 \rightarrow p_2\) we must
prove \(p_1, \Gamma \vdash p_2\).

What do we do if the implication appears as a hypothesis,
*i.e.*, to the left of the turnstile, rather than the right? We
saw this process, too, in our discussion of program correctness. If we
had an auxiliary claim that we proven that was the form of a
conditional, or if our induction hypothesis was a conditional, we needed
to first prove the preconditions and then we could assume that the
conclusion held. Thus, to use an assumed implication, we must first
prove its *premise* and then we can *assume* the
conclusion as a new hypothesis:

**Proof Rule [elim-→]**: To prove \(\Gamma \vdash p\), if \(p_1 \rightarrow p_2 \in \Gamma\), then we
may prove both \(\Gamma \vdash p_1\)
and \(p_2, \Gamma \vdash p\).

After using **elim-→**, we must prove two proof
goals:

- The first requires us to prove that the premise of the assumed implication is provable.
- The second requires us to prove our original goal, but with the additional information of the conclusion of implication.

If you are familiar with logic already, *e.g.*, from a
symbolic logic class, you should recognize **elim-→** as
the *modus ponens* rule that says:

If \(p\) implies \(q\) and \(p\) is true, then \(q\) is true as well.

Here is a pair of simple example proofs that illustrate the basic usage of these rules:

**Claim**: \(⋅ \vdash A
\rightarrow A\).

*Proof*. By intro-→, we first assume that \(A\) is provable and go on to show that
\(A\) is provable. However, this is
simply the assumption that we just acquired.

**Claim**: \(A \rightarrow B,
A \vdash B\).

*Proof*. By elim-→, we must show that \(A\) is provable and then we may assume
\(B\) is provable. \(A\) is provable by assumption and the goal
\(B\) is provable by the assumption we
gained from eliminating the assumption.

Compare the flow of these proofs with the rules presented in this section to make sure you understand how the rules translate into actual proof steps.

### Disjunction

Now, let’s look at disjunction. A disjunction, \(p_1 \vee p_2\), is a proposition that
asserts that *one or both* of \(p_1\) and \(p_2\) are provable as well. For example,
the proposition “I’m running out of cheeseburgers or the sky is falling”
is a disjunction where at least one of “I’m running out of
cheeseburgers” and “the sky is falling” must be provable.

Again, using our intuition, we can see that if we have to
*prove* a disjunction, our job is easier than with a conjunction.
With a conjunction we must prove both conjuncts; with disjunction, we
may prove *only one* of the *disjuncts*.

**Proof Rule [intro-∨-left]**: To prove \(\Gamma \vdash p_1 ∨ p_2\), we may prove
\(\Gamma \vdash p_1\).

**Proof Rule [intro-∨-right]**: To prove \(\Gamma \vdash p_1 ∨ p_2\), we may prove
\(\Gamma \vdash p_2\).

The **intro-∨-left** and **intro-∨-right**
rules allow us to explicit choose the left- and right-hand sides of the
disjunction to prove, respectively.

We have flexibility in proving a disjunction. However, that
flexibility results in complications when we reasoning about what we
know if a disjunction is assumed to be true. As an example, suppose that
our example disjunction from above is assumed to be true. What do we
know as a result of this fact? Well, we know that *at least one*
of “I’m running out of cheeseburgers” and “the sky is falling” is true.
The problem is that *we don’t know which one* is true!

We seem to be stuck! It doesn’t seem like we can extract any
interesting information from a disjunction. Indeed, a disjunction
doesn’t give us the same *direct* access to new information like
a conjunction. However, disjunctions can be used in an *indirect*
manner to prove a claim!

Suppose that we are trying to prove the claim that “the apocalypse is now” and we know our disjunction is true. We know that at least of the disjuncts is true, so if we can do the following:

- Assume that “I’m running out of cheeseburgers” and then prove “the apocalypse is now.”
- Assume that “the sky is falling” and then prove “the apocalypse is now.”

It must be the case that apocalypse is happening because
*both* disjuncts imply the apocalypse and we know *at
least* one of the disjuncts is true!

This logic gives rise to the following left-rule for disjunction:

**Proof Rule [elim-∨]**: To prove \(\Gamma \vdash p\), if \(p_1 \vee p_2 \in \Gamma\), then we may
prove \(p_1, \Gamma \vdash p\) and
\(p_2, \Gamma \vdash p\).

In effect, a disjunction gives us *additional assumptions*
when proving a claim, but we must consider *all possible cases*
when doing so. This reasoning should sound familiar: this is precisely
the kind of reasoning we invoke when analyzing the guard of a
conditional in a computer program: “either the guard evaluates to true
or false.” This reasoning is possible because we know that the guard of
a conditional produces a boolean value and booleans can only take on two
values.

### Top, Bottom, and Negation

Finally, we arrive at our two “trivial” propositions. Recall that \(\top\) (“top”) is the proposition that is always provable and \(\bot\) (“bottom”) is the proposition that is never provable.

First let’s consider \(\top\). Since \(\top\) is always provable, its introduction is straightforward to write down:

**Proof Rule [intro-⊤]**: \(\Gamma \vdash \top\) is always
provable.

But what if we know \(\top\) holds
as an assumption? Well that doesn’t mean much because
**intro-⊤** tells us that we can always prove \(\top\)! Indeed, there is no left-rule for
\(\top\) because knowing \(\top\) holds *does not tell us anything
new*.

Similarly, because \(\bot\) is never provable, there is no introduction rule for \(\bot\) because we should never be able to prove it! But what does it means if \(\bot\) somehow becomes an assumption in our proof state? Think about what this implies:

- \(\bot\) is defined to never be provable.
- We assume that \(\bot\) is provable as a hypothesis.

This is a *logical contradiction*: we are assuming something
we know is not true! We are now in an *inconsistent state of
reasoning* where, it turns out, *anything* is provable. This
gives rise to the following elimination rule for \(\bot\):

**Proof Rule [elim-⊥]**: If \(\Gamma \vdash p\) and \(\bot \in \Gamma\) then our goal \(p\) is always provable.

Finally, how do we handle negation? It turns out rather than giving proof rules for negation, we’ll employ an equivalence, relating negation to implication:

**Definition (Negation)**: \(\neg p \equiv p \rightarrow \bot\).

\(p \rightarrow \bot\) means that whenever we can prove \(p\) we can “prove” a contradiction. Since contradictions cannot arise, it must be the case that \(\neg p\) must be true instead.

**Exercise (Follow the Rules, ‡)**: Formally prove the
following claim:

**Claim**: \(A, B \vdash A
\wedge (B \vee C)\).

## Reasoning About Quantifiers

We have given rules for all of the connectives in propositional logic. But what about the additional constructs from first-order logic: universal and existential quantification? Let’s study each of these constructs in turn.

**Universal Quantification**

A universally quantified proposition, for example, \(\forall x \ldotp x \geq 5\) holds *for
all possible values* of its quantified variable. Here, \(x \geq 5\) means that *every possible
value of \(x\)* is greater than
five.

Because the proposition must hold for all possible values, when we go
to *prove* a universally quantified proposition, we must consider
the value as *arbitrary*. In other words, we don’t get to assume
anything about the universally quantified variable. As we discussed
during the program correctness section of the course, this amounts to
substituting an *unknown, yet constant value* for that variable
when we go to reason about the proposition. In practice, we think of the
variable as the unknown, yet constant value, but it is important to
remember that we need to *remove* the variable, either implicitly
or explicitly, from the proposition before we can continue processing
it.

In contrast, when we have a universally quantified proposition as an
assumption, we can take advantage of the fact that the proposition holds
for all values. We do so by *choosing* a particular value for the
proposition’s quantified variable, a process called
*instantiation*. We can choose whatever value we want, or even
instantiate the proposition multiple times to many variables, depending
on the situation at hand.

We can summarize this behavior as introduction and elimination rules in our natural deduction system:

**Proof Rule [intro-∀]**: To prove \(\Gamma \vdash \forall x \ldotp p\), we must
prove \(\Gamma \vdash \forall [c/x]p\)
where \([c/x]p\) is the
*substitution* of some unknown constant \(c\) for \(x\) everywhere \(x\) occurs in proposition \(p\).

**Proof Rule [elim-∀]**: To prove \(\Gamma \vdash p\), if \(\forall x \ldotp p \in \Gamma\), then we
may prove \([v/x]p, \Gamma \vdash p\)
where \([v/x]p\) is the substitution of
some chosen value \(v\) for \(x\) everywhere \(x\) occurs in \(p\).

The difference between the rules is subtle but important to summarize:

- In
**intro-∀**, we*hold the quantified variable abstract*. - In
**elim-∀**, we*choose a particular value*for the variable.

We formalize this through *substitution notation*. The
proposition \([e/x] p\) is proposition
\(p\) but every occurrence of variable
\(x\) is replaced with \(e\). Furthermore, we use the convention
that:

- \(c\) is a unknown, yet constant value.
- \(v\) is a chosen value.

From this, we see that in the **intro-∀** rule, we
substitute an unknown, constant value \(c\) for the quantified variable \(x\). In contrast, in the
**elim-∀** rule, we substitute a chosen value \(v\) for \(x\).

**Existential Quantification**

An existentially quantified proposition, for example, \(\exists x \ldotp x \geq 5\) holds *for
at least possible value* that its quantified variable can take on.
Here, \(x \geq 5\) means that *there
is at least one value* for \(x\)
such that \(x\) is greater than
five.

Since an existentially quantified proposition holds if a single value
makes the proposition true, then we get the luxury of *choosing*
such a value when going to prove an existential. For example, we might
choose \(x = 10\) and then we would be
tasked with proving that \(10 \geq 5\).
However, this flexibility comes at a price. When know an existential is
provable, we do *not* know what value(s) make the proposition
true. So the only thing we know is the existentially quantified
proposition is true for some *unknown, constant value*.

We can summarize this behavior with a pair of rules as well:

**Proof Rule [intro-∃]**: To prove \(\Gamma \vdash \exists x \ldotp p\), we must
prove \(\Gamma \vdash \exists [v/x]p\)
where \([v/x]p\) is the substitution of
some chosen \(v\) for \(x\) in \(p\).

**Proof Rule [elim-∃]**: To prove \(\Gamma \vdash p\), if \(\exists x \ldotp p \in \Gamma\), then we
may prove \([c/x]p, \Gamma \vdash p\)
where \([c/x]p\) is the substitution of
some arbitrary constant \(c\) for \(x\) everywhere \(x\) occurs in \(p\).

**Summary of Reasoning with Universals and
Existentials**

We can summarize our reasoning principles using universals and existentials with the following table:

Position/Quantifier | ∀x.p | ∃x.p |
---|---|---|

Goal | ( x ) is arbitrary | ( x ) is chosen |

Assumption | ( x ) is chosen | ( x ) is arbitrary |

Note how the rules of reasoning about universal and existential
quantification are flipped depending on whether the proposition appears
in goal or assumption position. We call mathematical objects that have a
reciprocal relationship of this nature *duals*. In other words,
universal and existential quantification are *duals* of each
other. This dual nature leads to a number of interesting properties
between the two connectives, *e.g.*, De Morgan’s law-style
reasoning:

\[ \neg \forall x \ldotp p \equiv \exists x \ldotp \neg p \qquad \neg \exists x \ldotp p \equiv \forall x \ldotp \neg p. \]

Another example of duals in logic are conjunction and disjunction. Compare their introduction and elimination rules:

Position/Connective | p ∧ q | p ∨ q |
---|---|---|

Goal | Prove both | Prove one |

Assumption | Assume one | Assume both |

Here, the duality manifests itself in whether we choose to analyze
*one or both* of the arguments to the connective.

Duals highlight an important goal of mathematical modeling. When we
model a phenomena, we are interested in understanding the
*relationship* between objects in our models. As mathematicians,
we care about these relationships so that we discover and ultimately
prove properties about these objects. As computer scientists and
programmers, we can exploit these relationships to write more efficient
or concise code.

::: **Exercise (Alternation, ‡)**: Consider the
following abstract first-order proposition:

\[ \forall x \ldotp \exists y \ldotp \forall z \ldotp p(x, y, z). \]

For each of the variables \(x\),
\(y\), and \(z\) identify whether you must *hold the
variable abstract* or when you get to *choose a value for that
variable* when you are:

- Proving the proposition.
- Utilizing the proposition as an assumption. :::