Conjunction and Disjunction

PRL Home Introduction Math Library Publications Projects System

Seminar People The Book Lectures Other Groups

Logical Investigations, with the Nuprl Proof Assistant

4. Conjunction and Disjunction

Next we step out of the minimal implicational calculus and add to our logic the operators of conjunction (∧, "and") and disjunction (∨, "or").

For two propositions P and Q, evidence for (P ∧ Q) means that we have evidence for P and also evidence for Q. To have evidence for the logical statement (P ∨ Q), we only require evidence for at least one of the propositions, P or Q. We may have evidence for both propositions, but this is not required. In logic there is also an "exclusive or" operator which requires evidence for either P or Q but not both; however, we will not be discussing this operator further.

As with implication, we have a construction rule for constructing each operator and an application rule for using each operator to prove a goal. To differentiate among the rules, we will start including the logical operator in front of the rule name.

Conjunction Rules

∧ Construction:
H ⊢ P ∧ Q by < ___ , ___ >

H ⊢ P by ___
H ⊢ Q by ___

To prove (P ∧ Q) from a list of hypotheses H, we need to provide evidence for both P and Q. In Nuprl, we apply the tactic D 0 which decomposes the goal into two subgoals, one for proving P and one for proving Q. The evidence for the conjunction is then represented as a pair containing the evidence of each subgoal. The completed rule takes the following form, where p is evidence for P, and q is evidence for Q:

H ⊢ P ∧ Q by < p, q >

H ⊢ P by p
H ⊢ Q by q

∧ Application:
H, f : P ∧ Q ⊢ G by ___

H, p : P, q : Q ⊢ G by ___

If we need to prove a goal G and we have a conjunction (P ∧ Q) among our hypotheses, this means that we have evidence for P and also evidence for Q. In Nuprl, a conjunction is treated as a pair. The tactic D i, where i is the index of the hypothesis, will decompose this conjunction into two separate hypotheses so that we can access each member of the pair. The completed rule takes the following form, where g(p, q) is evidence for the goal G:

H, f : P ∧ Q ⊢ G by let p, q = f in g(p, q)

H, p : P, q : Q ⊢ G by g(p, q)

Disjunction Rules

∨ Construction:
H ⊢ P ∨ Q by ___

To prove (P ∨ Q) from a list of hypotheses H, we only need to provide evidence for P or evidence for Q:

H ⊢ P ∨ Q by ___

H ⊢ Q by ___

H ⊢ P ∨ Q by ___

H ⊢ P by ___

To prove the left side of the disjunction in Nuprl, we apply the tactic OrLeft to inject the left side to form the disjunction. To prove the right side instead, we apply the tactic OrRight to inject the right side. In the extracted evidence these steps are abbreviated as inl and inr, respectively. The completed rule takes the following form, where p is evidence for P, and q is evidence for Q:

H ⊢ P ∨ Q by inr (q)

H ⊢ Q by q

H ⊢ P ∨ Q by inl (p)

H ⊢ P by p

∨ Application:
H, f : P ∨ Q ⊢ G by ___

H, p : P ⊢ G by ___
H, q : Q ⊢ G by ___

This rule shows us how to apply a disjuntion (P ∨ Q) to prove a goal G. By definition, if we have evidence for (P ∨ Q), we might only have evidence for P or only have evidence for Q. Thus in order to use this disjunction, we must prove G assuming we only have evidence for P and then also assuming we only have evidence for Q. In Nuprl, the tactic D i, where i is the index of the hypothesis, will decompose a disjunction to create two subgoals to prove. The extracted evidence will then show the evidence for both cases. The completed rule takes the following form, where g₁(p) and g₂(q) are both evidence for G:

H, f : P ∨ Q ⊢ G by case f of inl(p) → g₁(p) | inr(q) → g₂(q)

H, p : P ⊢ G by g₁(p)
H, q : Q ⊢ G by g₂(q)

Finitary Mathematical Worlds and Boolean Semantics

Our first intuitive experience with the logic of mathematical statements occurs in the everyday world, where we usually assume that for any proposition P that we understand, we can either find evidence for P or evidence for ∼P, i.e. (P ∨ ∼P). We say that such propositions are decidable. This is very plausible for a world of finite kinds of mathematical objects like natural numbers, finite lists of numbers, finite graphs, and the data types used in computations. When in addition the propositions are all decidable, we call these finitary worlds.

We informally say that propositions for which we have evidence are "true" and those for which we know that there is no evidence, hence for which we know ∼P, are "false." We are accustomed to thinking that every proposition about finite mathematics is either true or false, e.g. it is either true or false that a given natural number is positive or even or prime, that a particular prime is a factor of another number, and so forth.

This assumption about finitary world leads to a simple semantics for formulas of propositional logic, called Boolean semantics. Based on the decidability assumption, we know that every formula is either true or false. We can thus base the whole semantics of propositions on a very simple data type of Boolean values whose values are tt for true and ff for false. This is the semantics typically used in textbooks and around which Tarski built up his theory of truth [Tar56] which has become extremely influential in certain areas of logic and mathematics.

Once we start to think about unbounded mathematical objects such as real numbers or functions from natural numbers to natural numbers, we are no longer confident that we can know for any proposition P whether it is true or false, i.e. whether we can find evidence for P or evidence for ∼P. The fact that very basic questions about numbers have remained open for decades and the prodigious effort involved in resolving some of the major results of mathematics reveals how difficult it is to find evidence one way or another when we are thinking about propositions about the unbounded world of natural numbers and real numbers. For objects like real numbers we strongly believe that we cannot even effectively decide equality.

One way that we imagine a world beyond our existing understanding of operational semantics is to imagine computations that have access to certain "oracles" that can perform operations that are only imaginary at present. But computer scientists are usually less fascinated than other scientists by imaginary computations that are highly unlikely to ever become realizable. This might be because they live in a world where there are so many fascinating questions about real computations; moreover these real computations have proven to be stunningly important not only in mathematics and science but in ordinary daily life.

Examples

We prove the following theorems on the next few pages:

The next three theorems are part of De Morgan's laws:

We leave these theorems as exercises:

Table of Contents