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

---

• (1) propositional logic proof calculator
• (2) first order logic formula
• (3) first order logic generator
• (4) logic direct proof calculator

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.


• Second-order Logic - Open Logic Project
• Resolution in Propositional and First-Order Logic
• Axiom Systems for Classical 16 First-Order Logic
• First-order Proofs - The College of Engineering at the …
• First-Order Logic and Proofs - Stanford University