Predicate Logic

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:

facts, which are ground atomic formulas

      male(Adam)
      female(Ann)
      parent(Adam,Barney)

rules, which are the conjunction of one or more atomic formulae that imply another atomic formula
```
      parent(y,x) AND male(x) -> son(x,y)
      parent(y,x) AND female(x) -> daughter(x,y)
      
```
The left-hand side of a rule contains hypotheses (called the body of the rule); each atomic formula is a hypothesis or subgoal. The right-hand side is the goal (or head of the rule).

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

Assert a rule that is known to be true (that is, the body of the rule implies the head of the rule)
Find facts that (via substitution) match the atomic formulae of the body of the rule
Make consistent variable substitutions in the body and the head of the rule
Assert the head (or goal) as proven

Example Database of Facts and Rules

Facts

male(Adam)
male(Barney)
male(Bob)
male(Carl)
female(Ann)
female(Beth)
female(Barb)
female(Carol)
parent(Adam,Barney)
parent(Ann,Barney)
parent(Adam,Beth)
parent(Ann,Beth)
parent(Adam,Bob)
parent(Ann,Bob)
parent(Adam,Barb)
parent(Barney,Carl)
parent(Carol,Carl)

Rules

parent(y,x) AND male(x) -> son(x,y)
parent(y,x) AND female(x) -> daughter(x,y)
male(x) AND (E z)(parent(z,x) AND parent(z,y)) -> brother(x,y)
female(x) AND (E z)(parent(z,x) AND parent(z,y)) -> sister(x,y)
male(x) AND (E y)(parent(x,y) AND parent(y,z)) -> grandfather(x,z)
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).

There's only one rule that allows us to infer the son relationship, so we included that rule.
We need facts about the parent relationship that include reference to Adam and Barney.
We need facts about the male relationship that include (possibly) Adam and Barney.

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.