Predicate Functor Logic - From First-order Logic To PFL

From First-order Logic To PFL

The following algorithm is adapted from Quine (1976: 300-2). Given a closed formula of first-order logic, first do the following:

• Attach a numerical subscript to every predicate letter, stating its degree;
• Translate all universal quantifiers into existential quantifiers and negation;
• Restate all atomic formulas of the form x=y as Ixy.

Now apply the following algorithm to the preceding result:

1. Translate the matrices of the most deeply nested quantifiers into disjunctive normal form, consisting of disjuncts of conjuncts of terms, negating atomic terms as required. The resulting subformula contains only negation, conjunction, disjunction, and existential quantification.

2. Distribute the existential quantifiers over the disjuncts in the matrix using the rule of passage (Quine 1982: 119):

3. Replace conjunction by Cartesian product, by invoking the fact:

4. Concatenate the argument lists of all atomic terms, and move the concatenated list to the far right of the subformula.

5. Use Inv and inv to move all instances of the quantified variable (call it y) to the left of the argument list.

6. Invoke S as many times as required to eliminate all but the last instance of y. Eliminate y by prefixing the subformula with one instance of ∃.

7. Repeat (1)-(6) until all quantified variables have been eliminated. Eliminate any disjunctions falling within the scope of a quantifier by invoking the equivalence:

The reverse translation, from PFL to first-order logic, is discussed in Quine (1976: 302-4).

The canonical foundation of mathematics is axiomatic set theory, with a background logic consisting of first-order logic with identity, with a universe of discourse consisting entirely of sets. There is a single predicate letter of degree 2, interpreted as set membership. The PFL translation of the canonical axiomatic set theory ZFC is not difficult, as no ZFC axiom requires more than 6 quantified variables.