CSC 208-01 (Spring 2023)

Reading: First-Order Logic

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

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:

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:

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:

  1. Identify the atomic propositions in the statement.

  2. 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:

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:

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:

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:

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-market are 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):

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!

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:

  1. \(p_2 \vee p_3\).
  2. \(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)\)).
  3. \(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:

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:

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 \]

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:

  1. \(\exists x.\,\exists y.\,A_1(x) \wedge A_3(y)\).
  2. \(\forall x.\,\exists y.\,A_1(y) \rightarrow A_2(x, y)\).
  3. \(\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:

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:

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

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:

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.

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

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:

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:

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:

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:

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:

  1. The first requires us to prove that the premise of the assumed implication is provable.
  2. 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:

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:

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:

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:

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:

  1. Proving the proposition.
  2. Utilizing the proposition as an assumption. :::