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).
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).
The simplest proofs in predicate logic consist of:
male(Adam) female(Ann) parent(Adam,Barney)
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.
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).
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.