SI242: First-order logic standard rules

Standard deduction rules for first-order logic

specialization: "if F is true for all possible values of x, then it must be true for x taking on the value e specifically".
If ∀x [F] is known to be true, where no quantifiers in F introduce a new scope for the name x, and e is a function/constant expression such that no constant contained in e has the same name as a variable introduced by a quantifier in F, then the formula we get by replacing all occurences of x with e inside of F is true.
```
1: ∀x[inClass(x,HH215) => isSleepy(x)]
2: inClass(Joe,HH215) => isSleepy(Joe)     [specializing x to Joe in 1]	  
```
existential introduction: "If F is true and contains expression e, then ∃x[G] is true where G is F with e's replaced with x's".
If formula F is known to be true, exp is a function/constant expression in F, and x is a new variable (i.e. does not occur inside F), then letting F* be the result of replacing some or all occurences of exp with the variable x, the formula ∃x[F*] is true. For example, if F := P(f(a),b) => Q(c,f(a)) ∧ R(f(a)) is known to be true, and we let exp := f(a) and our new variable is z, then we could deduce ∃z[P(z,b) => Q(c,z) ∧ R(z)].
```
1: friends(alice,mother(bob)) ∧ enemies(mother(bob),cathy)  [Given]
2: ∃z[friends(alice,z) ∧ enemies(z,cathy)]                  [Existential intro. on 1 using z for mother(bob)]	  
```
existential instantiation (simple version): "if there exists an object for x that makes F true, then let c be that object". 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!
```
1: ∃x[P(x,c)]   [Given]
2: P(k,c)       [Existential instantiation of 1 with new constant k for x]	  
```
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.
```
1: ∀x[P(f(x))]           [Given]
2: ∀x[P(x) => Q(f(x))]   [Given]
3:                       [let u be arbitrary but fixed]
4: P(f(u))               [Specialization of 1 with x = u]
5: P(f(u)) => Q(f(f(u))) [Specialization of 2 with x = f(u)] 
6: Q(f(f(u)))            [Modus ponens on 5 and 4]
7: ∀u[Q(f(f(u)))]        [u arbitrary but fixed from 3]	  
```