A brief explanation of propositional calculus

It is impossible in this short introduction to teach you propositional calculus if you don't already know it!

A typical use of propositional calculus is to observe that

(implies (endp z) (implies (true-listp z) (equal (rev (rev z)) z)))

is equivalent to:

(implies (and (endp z) (true-listp z)) (equal (rev (rev z)) z))

If this is surprising and you know propositional calculus, then the problem might be our notation. We're exploiting the tautology

(p ---> (q ---> r)) <---> ((p & q) ---> r)

where *--->* and *<--->* are meant to be the traditional
arrows denoting logical implication and logical equivalence.

If you don't know propositional calculus, we'll say just a few things to help ease your journey.

A *propositional formula*, in ACL2, is any formula written entirely in
terms of variable symbols,

(IFF (IMPLIES P (IMPLIES Q R)) (IMPLIES (AND P Q) R)).

If you have a formula like

(implieshypconcl)

then we say that formula is an *implication*, that *hyp* is the
*hypothesis*, and that *concl* is the conclusion. If the hypothesis
is an

(implies (andhyp1hyp2...)concl)

then we call *hyp1* is the *first hypothesis*, *hyp2* is the
*second hypothesis*, etc.

If a term is of the form

(andterm1term2...)

we say it is a *conjunction* and that *term1* is the *first
conjunct*, *term2* is the *second conjunct*, etc. We treat an
*disjunction* and its arguments
are *disjuncts*.

A *tautology* is any propositional formula that can be proved by
testing it under all combinations of Boolean assignments to its variables. We
give an example of such a *truth-table proof* below, but hasten to add
that ACL2 does not generally use truth tables to recognize tautologies. It
primarily uses normalization and BDDs to recognize tautologies, which
can be seen as a mix of symbolic manipulation and case analysis.

Many tautologies have names, but ACL2 doesn't refer to them by name because it derives them from first principles. We list a few here because we sometimes use the names in our documentation; more importantly, you should look at these formulas and convince yourself that they're always true for all Boolean values of the variables:

Double Negation: (iff (not (not p)) p)DeMorgan: (iff (not (and p q)) (or (not p) (not q)))Distributivity: (iff (and p (or q r)) (or (and p q) (and p r)))Promotion: (iff (implies p (implies q r)) (implies (and p q) r))Implicative Disjunction: (iff (implies p q) (or (not p) q))Contrapositive: (iff (implies p q) (implies (not q) (not p)))Generalized Contrapositive: (iff (implies (and p r) q) (implies (and p (not q)) (not r)))

There are, of course, many others, even with these same names! For
example, there is a dual version of DeMorgan showing how

Dealing with propositional calculus will not generally be a problem for you
because it is decidable and ACL2 has procedures that decide propositional
formulas. However, propositional calculus can lead to exponential explosion
and can thus explain why ACL2 has ``gone out to lunch.'' In addition,
sometimes if you are curious as to *why* ACL2 is working on a certain
subgoal the reason can be traced back to propositional calculus.

The most common example of this is that to prove a formula of the form

(implies (implies p1 q1) (implies p2 q2))

propositional calculus will convert it to

(and (implies (and p2 (not p1)) q2) (implies (and p2 q1) q2))

Many users are surprised that the first conjunct above does not have

Now we illustrate the truth table method for deciding tautologies, even though that is not what ACL2 generally uses. Consider the formula called Promotion above:

(IFF (IMPLIES P (IMPLIES Q R)) (IMPLIES (AND P Q) R))

The formula above is a tautology. It contains three variables,

formula1: (IMPLIES P (IMPLIES Q R))formula2: (IMPLIES (AND P Q) R)

then we wish to test the formula *formula1
formula2*

P Q Rformula1formula2(IFFformula1formula2) --------- T T T T T T T T NIL NIL NIL T T NIL T T T T T NIL NIL T T T NIL T T T T T NIL T NIL T T T NIL NIL T T T T NIL NIL NIL T T T

So we see that the formula always returns

Recall that in the original example at the top of this page we were trying to prove the formula

(implies (endp z) (implies (true-listp z) (equal (rev (rev z)) z)))

This formula is an

(implies p (implies q r)).

The substitution required by the match is

sigma: ((p (endp z)) (q (true-listp z)) (r (equal (rev (rev z)) z)))

Since we know the tautology:

(iff (implies p (implies q r)) (implies (and p q) r)).

is always true no matter what Boolean values *sigma* above) is always true:

(iff (implies (endp z)formula1'(implies (true-listp z) (equal (rev (rev z)) z))) (implies (and (endp z)formula2'(true-listp z)) (equal (rev (rev z)) z))).

Thus, if we're trying to prove *formula1'* it is permitted to try to
to prove *formula2'* instead, because they return the same
truthvalue.

This sketch of propositional reasoning in ACL2 is a little suspect because
we didn't address the possibility that the substitution might replace the
propositional variables by non-propositional terms. But the tautology was
verified only on Boolean values for those variables. This actually works out
because in ACL2 all propositional testing is done against

A very simple example of this is with Double Negation.

(iff (not (not p)) p)

is a tautology. This means that if we were trying to prove

(implies (not (not p)) ...)

we could transform it to

(implies p ...).

But if we were trying to prove:

(equal (not (not p)) p)

we could not prove it by using Double Negation! The formula above claims
that *That* is what Double
Negation says.

As long as you only use propositional formulas in propositional places this aspect of ACL2 should not affect you.

Now please use your browser's **Back Button** to return to the example
proof in logic-knowledge-taken-for-granted.