## 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*_{1}(*p*) and*g*_{2}(*q*) are both evidence for*G*:H,

*f*:*P*∨*Q*⊢*G*by case*f*of inl(*p*) →*g*_{1}(*p*) | inr(*q*) →*g*_{2}(*q*)

H,*p*:*P*⊢*G*by*g*_{1}(*p*)

H,*q*:*Q*⊢*G*by*g*_{2}(*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:

- Theorem 11: ((∼
*P*) ∨ (∼*Q*)) ⇒ ∼(*P*∧*Q*) - Theorem 12: ∼(
*P*∨*Q*) ⇒ ((∼*P*) ∧ (∼*Q*)) - Theorem 13: ((∼
*P*) ∧ (∼*Q*)) ⇒ ∼(*P*∨*Q*)

We leave these theorems as exercises:

- Theorem 14: ((∼
*P*) ∨*Q*) ⇒ (*P*⇒*Q*) - Theorem 15: (
*P*⇒*Q*) ⇒ ∼∼((∼*P*) ∨*Q*) - Theorem 16: ((
*P*⇒*Q*) ∧ ((*P*∨ ∼*P*) ∨ (*Q*∨ ∼*Q*))) ⇒ ((∼*P*) ∨*Q*)

Table of Contents