Proofs in Predicate Logic

A proof in predicate logic has much the same form as a proof in propositional logic.

We begin with a set of axioms (or hypotheses) A1..An, and using the rules of inference, we construct a sequence of expressions that follow from those axioms.

We can use the rules of inference from propositional logic as inference rules in predicate logic, including modus ponens, DeMorgan's laws, and the substitution of equals.

We require that each hypothesis and line in the proof be a closed expression (ie, there are no free variables whose scope extends beyond a line in the proof).


Substitution Rule

The law of variable substitution is an inference rule for use in proofs in predicate logic.

Informally, this rule states that having established that a general fact (or expression) is true, we can assert that a specific instance of that general expression is also true.

In particular, if we can prove (or assert as an axiom) a logical expression L1 containing free variables, then if we substitute constants or variables for some of the free variables in L1 to create expression L2, then the law of substitution states that
L1 -> L2 is a tautology, and we can assert L2 in the proof.

Consider the following assertion about the domain of real numbers:

      Lt(x,y) -> (E z) (Lt(x,z) AND Lt(z,y))
  
If we substitute x=2 and y=5 in the original expression, then we can assert:
      Lt(2,5) -> (E z) (Lt(2,z) AND Lt(z,5))
  
In other words, if the original expression holds for all x and y, then it must hold for x=2 and y=5.

Note that choosing x=5 and y=2 makes Lt(x,y) = false, and the entire expression is still true (since false->anything is true).


Structure of a Proof in Predicate Logic

The simplest proofs in predicate logic consist of:

Rules are general principles that we can apply to facts to prove new facts.


Example Database of Facts and Rules

Facts

  1. male(Adam)
  2. male(Barney)
  3. male(Bob)
  4. male(Carl)
  5. female(Ann)
  6. female(Beth)
  7. female(Barb)
  8. female(Carol)
  9. parent(Adam,Barney)
  10. parent(Ann,Barney)
  11. parent(Adam,Beth)
  12. parent(Ann,Beth)
  13. parent(Adam,Bob)
  14. parent(Ann,Bob)
  15. parent(Adam,Barb)
  16. parent(Barney,Carl)
  17. parent(Carol,Carl)
Rules
  1. parent(y,x) AND male(x) -> son(x,y)
  2. parent(y,x) AND female(x) -> daughter(x,y)
  3. male(x) AND (E z)(parent(z,x) AND parent(z,y)) -> brother(x,y)
  4. female(x) AND (E z)(parent(z,x) AND parent(z,y)) -> sister(x,y)
  5. male(x) AND (E y)(parent(x,y) AND parent(y,z)) -> grandfather(x,z)
  6. female(x) AND (E y)(parent(x,y) AND parent(y,z)) -> grandmother(x,z)

Example Proof using Substitution

Prove son(Barney,Adam)

  1. male(Adam)                             Fact 1
  
  2. male(Barney)                           Fact 2
  
  3. parent(Adam,Barney)                    Fact 9
  
  4. parent(y,x) AND male(x) -> son(x,y)    Rule 1
  
  5. parent(Adam,Barney) AND male(Barney)   L2,L3
  
  6. parent(Adam,Barney) AND male(Barney)
     -> son(Barney,Adam)                    L5, L4, sub.
  
  7. son(Barney,Adam)                       L5, L6, m.p.
  

Note that we selected the facts and the rule that would help us prove son(Barney,Adam).


Example Proof with Quantifiers

Prove brother(Barney,Beth):

  1. male(Barney)                        Fact 2
  
  2. parent(Adam,Barney)                 Fact 9
  
  3. parent(Adam,Beth)                   Fact 11
  
  4. male(x) AND (E z)(parent(z,x) AND
     parent(z,y)) -> brother(x,y)        Rule 3
  
  5. male(Barney) AND
     (E z)(parent(z,Barney) AND
     parent(z,Beth))
     -> brother(Barney,Beth)             L4, sub.
  
  6. male(Barney) AND
     parent(Adam,Barney) AND
     parent(Adam,Beth)                   L1, L2, L3
  
  7. brother(Barney,Beth)                L5, L6, m.p.