**Home** / **first order logic proof calculator** / First-Order Logic and Proofs - Stanford University

CS103 Handout 13

Fall 2016 October 14, 2016

First-Order Logic and Proofs

Now that we're starting to explore more complex discrete structures, we're starting to see more and

more definitions phrased in first-order logic. One major advantage of this approach is that first-order

definitions, in some sense, give both a formal definition of a term and a sketch for how you might go

about proving it.

Below is a table of all the quantifiers and connectives in first-order logic and how you should try to

prove statements with each form:

Statement Form Proof Approach

x. P Direct proof: Consider an arbitrary x, then prove P is true for that choice of x.

By contradiction: Suppose for the sake of contradiction that there is some x

where P is false. Then derive a contradiction.

x. P Direct proof: Do some exploring and find a choice of x where P is true. Then,

write a proof explaining why P is true in that case.

By contradiction: Suppose for the sake of contradiction that P is false for any

choice of x and derive a contradiction.

?P Direct proof: Simplify your formula by pushing the negation deeper, then

apply the appropriate rule.

By contradiction: Suppose for the sake of contradiction that P is true, then

derive a contradiction.

P Q Direct proof: Prove each of P and Q independently.

By contradiction: Assume ?P ?Q. Then, try to derive a contradiction.

P Q Direct proof: Prove that ?P Q, or prove that ?Q P.

By contradiction: Assume ?P ?Q. Then, try to derive a contradiction.

P Q Direct proof: Assume P is true, then prove Q.

By contradiction: Assume P is true and Q is false, then derive a contradiction.

By contrapositive: Assume Q is false, then prove P is false.

P Q Prove both P Q and Q P.

2 / 3

The above might seem pretty abstract, so let's make things more concrete. Suppose that we have a

binary relation ~ over the set defined as follows: we'll say that x~y if x + y is even. Now, suppose

that we want to prove that this relation is transitive. How exactly would we prove this? And what ex -

actly is it that we need to prove?

Well, we happen to have the following formal definition for transitivity:

a A. b A. c A. (aRb bRc aRc)

If we want to prove that ~ is transitive, we need to show that the above statement is true with respect

to the ~ relation over the set . Plugging in ~ and , we need to prove this statement:

a . b . c . (a~b b~c a~c)

Now, how do we go about proving this? This formula is a universal statement:

a . b . c . (a~b b~c a~c)

Consulting the table on the previous page, we see that the way to prove a statement like this is to

choose arbitrary choices of a, b, c , then to go and prove the inside of the statement is true given

those choices. Therefore, we could start our proof off like this:

To prove that ~ is transitive, consider any arbitrary a, b, c .

We now need to prove that, for these choices of a, b, and c, that the following statement is true:

a~b b~c a~c.

So how do we prove this? Consulting our table, we see that for a formula of the form P Q, we

should assume P and prove Q. Here, this means assuming a~b and b~c, then proving a~c. Let's write

that out:

To prove that ~ is transitive, consider any arbitrary a, b, c where a~b and b~c. We need to prove

that a~c.

From here, the rest of the job is just showing that this statement is indeed true. To do so, it's proba-

bly best to expand out the definition of ~ to more specifically articulate what we're assuming and

what we're going to prove:

To prove that ~ is transitive, consider any arbitrary a, b, c where a~b and b~c. In other words,

we assume that a+b is even and that b+c is even. We need to prove that a~c, meaning that we need

to show that a+c is even.

Now, we've got a clear statement of what we need to prove. The rest of the proof is then just about

filling in the details:

3 / 3

To prove that ~ is transitive, consider any arbitrary a, b, c where a~b and b~c. In other words,

we assume that a+b is even and that b+c is even. We need to prove that a~c, meaning that we need

to show that a+c is even.

Notice that (a+b) + (b+c) = a + c + 2b. Rearranging terms, we see that a+c = (a+b) + (b+c) - 2b.

Now, we know that a+b and b+c are even, so there are integers r and s such that a+b = 2r and

b+c = 2s. Therefore, we see that a+c = 2r + 2s - 2b = 2(r + s - b), which means that a+c is even, as

required.

Notice how the first-order definition of the terms in question leads us to the shape of the proof we

need to write. Without knowing anything about the ~ relation, we could still see what we needed to

assume, what we needed to prove, and what values were chosen arbitrarily. It's amazing that all of

this information was packed into the small set of instructions "prove that ~ is transitive," but that's

often how math works: begin by "rehydrating" the statement to prove into something more concrete,

then use that to determine how to approach the problem.

Similarly, notice how the above proof does not contain any first-order logic symbols; even though

the statement we're proving is giving in first-order logic, the proof we ultimately ended up writing

does not contain any quantifiers or connectives. This is deliberate! Remember that our proofs are

supposed to be written in plain English and, therefore, that the argumentative structure should be

written using natural language.

Author: Gerald Cain

Creator: Writer

Producer: LibreOffice 5.1

CreationDate: Fri Oct 14 14:42:49 2016

Tagged: no

Form: none

Pages: 3

Encrypted: no

Page size: 612 x 792 pts (letter) (rotated 0 degrees)

File size: 77555 bytes

Optimized: no

PDF version: 1.4