SI242: Finishing off First-order logic deductions

First order theories

A theory is a collection of constants/functions/predicates, along with formulas that define their behavior, which are called the theory axioms. Think of a theory as being like a library in a programming language. You "#include" the theory, and then you get some pre-defined predicates/functions/constants, and perhaps also some formulas about them, the axioms, which you can take as "givens" in your proofs.

The theory of equality

Working with "the theory of equality" means that we will assume that we always have predicate Equal(·,·) that works like we expect equality to work, which means we have the following two axioms:

Equality Axioms

reflexivity of equality: ∀x[Equal(x,x)]
subsitutivity of equality: if Equal($e_1$,$e_2$) is true for two function/constant/variable expressions $e_1$ and $e_2$, and $F_1$ is a formula and formula $F_2$ is the result of replacing some (but not necessarily all) occurences of expression $e_1$ in $F_1$ with $e_2$, then $F_1 \Leftrightarrow F_2$.

Note: So as not to go completely crazy, we will allow ourselves to write "$e_1 = e_2$" to mean "Equal($e_1$,$e_2$)" and "$e_1 \neq e_2$" to mean "¬Equal($e_1$,$e_2$)".

an example proof using the theory of equality	the same proof with the "=" operator as syntactic sugar
Given Equal(bruce,batman), prove equal(mother(bruce),mother(batman)). 1: Equal(bruce,batman) [Given] 2: ∀x[Equal(x,x)] [Refelxivity of equality] 3: Equal(mother(bruce),mother(bruce)) [Specialization of 2 with x=mother(bruce)] 4: Equal(mother(bruce),mother(batman)) [Substitutivity of equality on 3 (using 1)]	Given bruce = batman, prove mother(bruce) = mother(batman). 1: bruce=batman [Given] 2: ∀x[x=x] [Refelxivity of equality] 3: mother(bruce)=mother(bruce) [Specialization of 2 with x=mother(bruce)] 4: mother(bruce)=mother(batman) [Substitutivity of equality on 3 (using 1)]

an example proof using the theory of equality

the same proof with the "=" operator as syntactic sugar

Given Equal(bruce,batman), prove equal(mother(bruce),mother(batman)).  
1: Equal(bruce,batman)                 [Given]	
2: ∀x[Equal(x,x)]                      [Refelxivity of equality]
3: Equal(mother(bruce),mother(bruce))  [Specialization of 2 with x=mother(bruce)]
4: Equal(mother(bruce),mother(batman)) [Substitutivity of equality on 3 (using 1)]

Given bruce = batman, prove mother(bruce) = mother(batman).
1: bruce=batman                 [Given]	
2: ∀x[x=x]                      [Refelxivity of equality]
3: mother(bruce)=mother(bruce)  [Specialization of 2 with x=mother(bruce)]
4: mother(bruce)=mother(batman) [Substitutivity of equality on 3 (using 1)]

Note: Usually we will go straight from line #1 in the above to line #3, without explictly writing line #2, and just call that "reflexivity of equality". After all, any time we introduce the reflexivity axiom into a proof, we will want to immediately specialize it.

ACTIVITY
Using first-order logic + the theory of equality, we add ...
Predicates: ismid(.), inDTA(.)
constants: bancroft, jones
functions: home(.)

Given: ∀x[ismid(x) => bancroft=home(x)], inDTA(bancroft), and ismid(jones)
Prove: inDTA(home(jones))

Note: Break up into groups and solve at the board.

SOLUTION
Given: ∀x[ismid(x) => home(x)=bancroft], inDTA(bancroft), and ismid(jones)
Prove: inDTA(home(jones))
1: ∀x[ismid(x) => bancroft=home(x)]	[Given]
2: inDTA(bancroft)                      [Given]
3: ismid(jones)                         [Given]
4: ismid(jones) => bancroft=home(jones) [Specialization of 1 with x=jones]
5: bancroft=home(jones)                 [Modus ponens 4, 3]
6: inDTA(home(jones))                   [Substitutivity of equality on 2 (using equality 5)]

Disclaimers:

Important: We will only talk about first order logic with equality. In other words, we will always assume we have the Equal(.,.) predicate and the two axioms of equality.

This might not mean a lot to you right now, but for completeness I feel compelled to make this clear: We will not attempt to formally describe a a complete set of rules of deduction for first order logic, as one would in a course dedicated to formal logic. Our goal is to learn what one might call "practical" first-order logic, which is how we use first-order logic to model the world and to produce proofs. A more theoretically oriented course would actually prove things about first-order logic, e.g. is it consistent, is it complete, what is the smallest, simplest set of deduction rules that suffice for first-order logic, etc.

Deduction in first order logic: Part 3

existential instantiation (simple version): "if there exists an object for x that makes F true, then let c be that object".
Here is how to understand existential instantiation: Suppose we have the following fact:
```
  everyone loves computer science  
```
From that can we then deduce
```
  Taylor Swift loves computer science  
```
is also a fact? Yes! This is an example of specialization, because "everyone loves computer science" is ∀x[lovesCS(x)]. Suppose we have the following fact:
```
  someone is 10 feet tall  
```
From that can we then deduce
```
  Taylor Swift is 10 feet tall  
```
is a fact? No! This is not specialization, since "someone is 10 feet tall" is ∃x[tall10ft(x)]. It is not a "∀", so specialization doesn not apply. What we do with existential instantiation is say, given a completely new name like JoeTacoOrange, that
```
  tall10ft(JoeTacoOrange)
```
where we treat "JoeTacoOrange" as an alias for this mystery 10-foot-tall giant. That allows us to more easily say things like "Go find JoeTacoOrange and offer him a lot of money to play for our basketball team."
If ∃x [F] is known to be true, where no quantifiers in F introduce a new scope for the name x and no other variables appear in F, then you may introduce a new constant symbol c and assume that the formula we get by replacing all occurences of x with c inside of F is true. Note that the "∃x" needs to be the outermost quantifier in the formula. It cannot be embedded inside another quantified variable's scope. Danger! You must choose a new constant symbol each time you apply existential instantiation, where "new" means the name absolutely does not appear anywhere else in the whole proof!
ACTIVITY - activity (do on paper in pairs, not at board). Note: Problem 2 may feel a little odd, since there are no constants, which means that there are no natural specializations to be made. This is a clue that maybe specialization should not be your first step!

Below is a proof that makes use of existential instantiation. In this case, we are proving a basic fact of mathematics, so we can see first order logic allowing us to express the kinds of deductions we require in mathematical proof.
```
Given: ∀x[Even(x) => ∃y[x = 2*y]], ∀x[∃z[x = 2*z+1] => Odd(x)] and Even(n)
Prove: Odd(n+1)
NOTE: we will use + and * as usual rather than Plus(a,b) and Times(a,b)
1:  Even(n)                     [given]
2:  ∀x[Even(x) => ∃y[x = 2*y]]  [given]	    
4:  Even(n) => ∃y[n = 2*y]      [specialize x to n in 2]
5:  ∃y[n = 2*y]                 [modus ponens with 4 and 1]
6:  n = 2*k                     [existential instantiation - new constant is k]
7:  n+1 = n+1                   [reflexivity of equality]
8:  n+1 = 2*k+1                 [substitutivity of equality]
9:  ∃z[n+1 = 2*z+1]             [existential introduction replacing k with variable z]
10: ∀x[∃z[x = 2*z+1] => Odd(x)] [given]
11: ∃z[n+1 = 2*z+1] => Odd(n+1) [specialize x to n+1 in 10]
12: Odd(n+1)                    [modus ponens on 11 and 9]
      
```

assumptions ... reprising a deduction rule from propositional logic.
In class 11 we decribed assumptions in propositional logic proofs. Basically, if you assume A is true, then prove B using that assumption, you can deduce A => B. (We call that last move "closing the assumption.) We can do the same thing with the previous proof, in which case we demonstrate Even(n) => Odd(n+1). Using assumptions like this is handy for proving implications.

Given: ∀x[Even(x) => ∃y[x = 2*y]], ∀x[∃z[x = 2*z+1] => Odd(x)] and Even(n)
Prove: Odd(n+1) Even(n) => Odd(n+1)
NOTE: we will use + and * as usual rather than Plus(a,b) and Times(a,b)
A1:  Even(n)                     [new assumption A]
A2:  ∀x[Even(x) => ∃y[x = 2*y]]  [given]	    
A4:  Even(n) => ∃y[n = 2*y]      [specialize x to n in A2]
A5:  ∃y[n = 2*y]                 [modus ponens with A4 and A1]
A6:  n = 2*k                     [existential instantiation - new constant is k A5]
A7:  n+1 = n+1                   [reflexivity of equality]
A8:  n+1 = 2*k+1                 [substitutivity of equality on A7 using A6]
A9:  ∃z[n+1 = 2*z+1]             [existential introduction replacing k with new var z in A8]
A10: ∀x[∃z[x = 2*z+1] => Odd(x)] [given]
A11: ∃z[n+1 = 2*z+1] => Odd(n+1) [specialize x to n+1 in A10]
A12: Odd(n+1)                    [modus ponens on A11 and A9]
13:  Even(n) => Odd(n+1)         [closing assumption A]

arbitrary but fixed: "If a proof of F involves an arbitrary constant c, then we can deduce ∀c[F]." Notice that the constant n in the previous poof is sort of out of nowhere. There is no special information about it that constrains it, unlike the first version, where we were given Even(n). We refer to this as "arbitrary but fixed". It's "fixed" because it is a constant, and "arbitrary" because there's no special information about it. When a proof of some fomula F has an arbitrary but fixed constant c, we can deduce ∀c[F]. Why? Because the proof we gave of F didn't use any specific information about c, so the same proof would work for any object in the domain of discourse.

Given: ∀x[Even(x) => ∃y[x = 2*y]], ∀x[∃z[x = 2*z+1] => Odd(x)]
Prove: Even(n) => Odd(n+1) ∀n[Even(n) => Odd(n+1)]
NOTE: we will use + and * as usual rather than Plus(a,b) and Times(a,b)
0:                               [let n be arbitrary but fixed]
A1:  Even(n)                     [new assumption A]
A2:  ∀x[Even(x) => ∃y[x = 2*y]]  [given]	    
A4:  Even(n) => ∃y[n = 2*y]      [specialize x to n in A2]
A5:  ∃y[n = 2*y]                 [modus ponens with A4 and A1]
A6:  n = 2*k                     [existential instantiation - new constant is k is k A5]
A7:  n+1 = n+1                   [reflexivity of equality]
A8:  n+1 = 2*k+1                 [substitutivity of equality]
A9:  ∃z[n+1 = 2*z+1]             [existential introduction replacing k with new var z in A8]
A10: ∀x[∃z[x = 2*z+1] => Odd(x)] [given]
A11: ∃z[n+1 = 2*z+1] => Odd(n+1) [specialize x to n+1 in A10]
A12: Odd(n+1)                    [modus ponens on A11 and A9]
13:  Even(n) => Odd(n+1)         [closing assumption A]
14:  ∀n[Even(n) => Odd(n+1)]     [arbitrary but fixed n to ∀]

An important theorem of equality

A property of equality that we definitely expect to hold is that it is "symmetric". So if $a = b$, it should follow that $b = a$. This is not one of our axioms, however. Why not!?!?!? The answer is that we can prove the symmetric property from our two existing axioms, and there is a fundamental philosophy in logic and mathematics that we should keep the set of axioms as small and simple as possible.

In the larger world of philosophy and science, this idea of preferring the smallest, simplest set of axioms is called Occam's Razor.

Why? Because the axioms are things we must simply accept (or, of course, we are free to reject them). Anything we can prove from the axioms are things we are forced to acknowledge are true

∀x,y[Equal(x,y) $\Rightarrow$ Equal(y,x)]. (Alternatively, ∀x,y[x=y $\Rightarrow$ y=x]) In other words, equality is symmetric.

In our proof, we use the syntactic sugar of the "=" operator.

  1:                        [Let x be arbitrary but fixed]
  2:                        [Let y be arbitrary but fixed]
A.1: x = y                  [new assumption A] 
A.2: ∀z[z = z]              [Reflexivity of equality]
A.3: x = x                  [Specialization of z to x in A.2]
A.4: y = x                  [Substitutivity of equality on A.3 using A.1]
  3: x = y => y = x         [Closing assumption A]
  4: ∀y[x = y => y = x]     [arbitrary but fixed y to ∀ on 3]
  5: ∀x[∀y[x = y => y = x]] [arbitrary but fixed x to ∀ on 4]

note: ∀x,y[x = y => y = x] is shorthand for #5.

Looking forward

Looking forward to how we use deduction rules like specialization, existential instantiation, existential introduction, reflexivity and substitutivity of equality, we will prove important (if basic, in this case) mathematical facts. Moving forward, we will start giving proofs as mathematicians and computer scientists normally do - mostly in english, less structured, and much less detailed. What's important though, is that these proofs should provide a sketch of the full first-order-logic proof. Here's a mathematician-style proof that n being even means that n+1 is odd.

Given that n is even, n+1 is odd.

Since n is even, by the definition of "even", n = 2*k for some integer k. Thus, n+1 = 2*k + 1. By the definition of "odd", this means that n+1 is odd.

Hopefully you see the correspondence:

"Since n is even ..." - line 1 from the original proof
"the definition of "even", n = 2*k for some integer k" - lines 2-6 of the original proof
Thus, n+1 = 2*k + 1. - line 8 of the original proof
By the definition of "odd", this means that n+1 is odd. - lines 9-12 of the original proof

So as we encounter mathematician-style proofs, we should be confident that each step could be fleshed out in first-order logic to provide all the details ... even if we are too lazy to actually do it. If we lack that confidence, the proof isn't a complete proof and, worse, it may be invalid!