Predicate functor logic

In mathematical logic, predicate functor logic (or PFL) is one of several ways to express first order logic (formerly known as predicate logic) by purely algebraic means, i.e., without quantified variables. PFL employs a small number of algebraic devices called predicate functors (or predicate modifiers) that operate on terms to yield terms. PFL owes a great deal to the logician and philosopher Willard Quine.

Motivation

This source for this section, as well as for much of this entry, is Quine (1976). Quine proposed PFL as a way of algebraizing first order logic in a manner analogous to how Boolean algebra algebraizes sentential logic. He designed PFL to have exactly the expressive power of first order logic with identity. Hence the metamathematics of PFL are exactly those of first order logic with no interpreted predicate letters: both are sound, complete, and undecidable.

Quine defined functor as follows:

"The word functor, grammatical in import but logical in habitat... is a sign that attaches to one or more expressions of given grammatical kind(s) to produce an expression of a given grammatical kind." (Quine 1982: 129)

Quine took "functor" from the writings of his friend Rudolf Carnap, the first to employ it in philosophy and mathematical logic.

Ways other than PFL to algebraize first order logic include:

Cylindric algebra by Alfred Tarski and his American students. The modified cylindric algebra proposed in Bernays (1959) led Quine to write the paper containing the first use of the phrase "predicate functor";
The polyadic algebra of Paul Halmos. By virtue of its economical primitives and axioms, this algebra most resembles PFL;
Relation algebra algebraizes the fragment of first order logic consisting of formulas whose quantifiers do not nest more than three deep. That fragment suffices, however, for Peano arithmetic and the axiomatic set theory ZFC; hence relation algebra, unlike PFL, is incompletable. Most work on relation algebra since about 1920 has been due to Tarski and his American students. The power of relation algebra did not become manifest until the monograph Tarski and Givant (1987).
Combinatory logic builds on combinators, higher functions whose domain is another combinator or function, and whose range is yet another combinator. Hence combinatory logic has the expressive power of set theory, and like naïve set theory, is vulnerable to paradoxes. A predicate functor, on the other hand, simply maps predicates (also called terms) into predicates.

PFL is arguably the simplest of these formalisms, yet is also the one about which the least has been written.

Quine had a lifelong fascination with combinatory logic, attested to by Quine (1976) and his introduction to the translation in Van Heijenoort (1967) of the paper by the Russian logician Moses Schonfinkel that founded combinatory logic. But Quine had ample reason to believe that combinatory logic was a failure and to push on with his PFL, reasons such as:

Until Dana Scott began writing on the model theory of combinatory logic in the late 1960s, nearly all work on that logic was by Haskell Curry, his students, or by Robert Feys in Belgium;
In the 1930s, it was discovered that some formulations of combinatory logic were inconsistent. Curry discovered the Curry paradox, peculiar to combinatory logic. Satisfactory axiomatic formulations of combinatory logic were slow in coming;
The lambda calculus, whose expressive power is the same as combinatory logic, was seen as a superior formalism.

Nearly everything Quine published on logic and mathematics in the last 30 year of his life involved PFL in some way.

Kuhn's axiomatization

This PFL syntax, primitives, and axioms in this section are in good part due to Kuhn (1983). The semantics of the functors are from Quine (1982). The rest of this entry incorporates some terminology from Bacon (1985).

Syntax

An atomic term is a capital letter other than I and S, followed by a numerical superscript called its degree, or by concatenated lower case variables, collectively known as an argument list. The degree of a term conveys the same information as the number of variables following a predicate letter. An atomic term of degree 0 denotes a Boolean variable or a truth value. The degree of I is invariably 2 and so need not be indicated.

The "combinatory" (the word is Quine's) predicate functors, all monadic and peculiar to PFL, are Inv, inv, ∃, +, and p. A term is either an atomic term, or constructed by the following recursive rule. If τ is a term, then Invτ, invτ, ∃τ, +τ, and pτ are terms. A functor with a superscript n, n a natural number > 1, denotes n consecutive applications (iterations) of that functor.

A formula is either a term or defined by the recursive rule: if α and β are formulas, then αβ and ~(α) are likewise formulas. Hence "~" is another monadic functor, and concatenation is the sole dyadic predicate functor. Quine called these functors "alethic." The natural interpretation of "~" is negation; that of concatenation is any connective that, when combined with negation, forms a functionally complete set of connectives. Quine's preferred functionally complete set was conjunction and negation. Thus concatenated terms are taken as conjoined. The notation + is Bacon's (1985); all other notation is Quine's (1976; 1982). The alethic part of PFL is identical to the Boolean term schemata of Quine (1982).

As is well known, the two alethic functors could be replaced by a single dyadic functor with the following syntax and semantics: if α and β are formulas, then (αβ) is a formula whose semantics are "not (α and/or β)" (see NAND and NOR).

Semantics, axioms, rules

This section lists the primitive predicate functors and a few defined ones. The alethic functors can be axiomatized by any set of axioms for sentential logic whose primitives are negation and one of ∧ or ∨. Equivalently, all tautologies of sentential logic can be taken as axiomatic.

For each combinatory functor, we give its semantics, as per Quine (1982), stated in terms of abstraction (set builder notation), followed by the relevant axiom, if any, from Kuhn (1983), or its definition as per Quine (1976).

Identity, I, is reflexive (Ixx), symmetric (Ixy→Iyx), transitive (Ixy&Iyz → Ixz), and obeys the substitution property:

(Fx_{1}...x_{n}\land Ix_{1}y)\rightarrow Fyx_{2}...x_{n}.

Padding, +, adds a variable to the left of any argument list.

\ +F^{n}=_{def}\{x_{0},x_{1}...x_{n}:F^{n}x_{1}...x_{n}\}.

+Fx_{1}...x_{n}\leftrightarrow Fx_{2}...x_{n}.

+ maps a term of degree n into one of degree n+1.

Cropping, ∃, erases the leftmost variable in any argument list.

\exists F^{n}=_{def}\{x_{2}...x_{n}:\exists x_{1}F^{n}x_{1}...x_{n}\}.

Fx_{1}...x_{n}\rightarrow \exists Fx_{2}...x_{n}.

∃ maps a term of degree n into one of degree n-1, by eliminating the first variable in an argument list.

Cropping enables defining two useful functors:

Reflection, S:

\ SF^{n}=_{def}\{x_{2}...x_{n}:F^{n}x_{2}x_{2}...x_{n}\}.

SF^{n}\leftrightarrow \exists IF^{n}.

S generalizes the notion of reflexivity to all terms of any finite degree greater than 2. N.B: S should not be confused with the primitive combinator S of combinatory logic.

Cartesian product, $\times$ ;

F^{m}\times G^{n}\leftrightarrow F^{m}\exists ^{m}G^{n}.

The next three functors enable reordering argument lists at will.

Major inversion, Inv, swaps the first and last variable in an argument list.

\ InvFx_{1}...x_{n}=_{def}\{x_{1}...x_{n}:F^{n}x_{n}x_{1}...x_{n-1}\}.

InvFx_{1}...x_{n}\leftrightarrow Fx_{n}x_{1}...x_{n-1}.

Minor inversion, inv, swaps the first two variables in an argument list.

\ invFx_{1}...x_{n}=_{def}\{x_{1}...x_{n}:F^{n}x_{2}x_{1}...x_{n}\}.

invFx_{1}...x_{n}\leftrightarrow Fx_{2}x_{1}...x_{n}.

Permutation, p, swaps the second and last variables in an argument list, so that:

\ pF^{n}=_{def}\{x_{1},x_{2}...x_{n}:F^{n}x_{1}x_{3}...x_{n}x_{2}\}.

pFx_{1}...x_{n}\leftrightarrow InvinvFx_{1}x_{3}...x_{n}x_{2}.

Given an argument list consisting of n variables, p implicitly treats the last n-1 variables like a bicycle chain, with each variable constituting a link in the chain. One application of p advances the chain by one link. k consecutive applications of p to Fⁿ moves the k+1 variable to the second argument position in F.

When n=2, Inv and inv merely interchange x₁ and x₂. When n=1, they have no effect. Hence p has no effect when n<3.

Kuhn (1983) takes Major inversion and Minor inversion as primitive. The notation p in Kuhn corresponds to inv; he has no analog to Permutation and hence has no axioms for it. If, following Quine (1976), p is taken as primitive, Inv and inv can be defined as nontrivial combinations of +, ∃, and iterated p.

All instances of a predicate letter may be replaced by another predicate letter of the same degree, without affecting validity. The rules are:

Modus ponens;
Let α and β be PFL formulas in which $x_{1}$ does not appear. Then if $(\alpha \land Fx_{1}...x_{n})\rightarrow \beta$ is a PFL theorem, then $(\alpha \land \exists Fx_{2}...x_{n})\rightarrow \beta$ is likewise a PFL theorem.

Kuhn (1983) proves the above axioms and rules sound and complete.

Quine conjectures

Quine (1976) did not axiomatize PFL, but invited others to do so; the results include Kuhn (1983) and Bacom (1985). Quine did assert the following purely algebraic results without proof. Their utility should be evident:

$\exists I$

$F^{n}\rightarrow +\exists F^{n}$
$\lnot \exists F^{n}\rightarrow \exists \lnot F^{n}$
$+\lnot F^{n}\leftrightarrow \lnot +F^{n}$
$+(F^{n}G^{m})\leftrightarrow (+F^{n}+G^{m})$

$F^{n}\leftrightarrow \exists +F^{n}$
$p\lnot F^{n}\leftrightarrow \lnot pF^{n}$
$F^{n}\leftrightarrow p^{n-1}F^{n}$
$p(F^{n}G^{m})\leftrightarrow (pF^{n}pG^{m})$

$IF^{n}\rightarrow (p^{n-2}\exists p+F^{n})$

Quine also postulated the rule:

If $\ \alpha$ is a theorem, then so are $\ p\alpha$ , $\ +\alpha$ , and $\lnot \exists \lnot \alpha$ .

Bacon's work

Bacon (1985) takes the conditional, negation, Identity, Padding, and Major and Minor inversion as primitive, and Cropping as defined. Employing terminology and notation differing somewhat from the above, Bacon (1985) sets out two formulations of PFL:

A natural deduction formulation in the style of Frederick Fitch. Bacon proves this formulation sound and complete in full detail.
An axiomatic formulation which Bacon asserts, but does not prove, equivalent to the preceding one. Some of the axioms are Quine conjectures in different notation.

Bacon also:

Discusses the relation of PFL to the term logic of Sommers (1982), and argues that recasting PFL using a syntax proposed in Lockwood's appendix to Sommers, should make PFL easier to "read, use, and teach";
Touches on the group theoretic structure of Inv and inv;
Mentions that sentential logic, monadic logic, the modal logic S5, and the Boolean logic of (un)permuted relations, are all fragments of PFL.

From first order logic to PFL

See Quine (1976: 300-2). Given a closed formula in first order logic, rename all variables as x (say) with a numerical subscript. Then recast the formula using only negation, conjunction, and existential quantification. The quantifiers should not be left in prenex position, but instead "driven in" by freely invoking the rules of passage (Quine 1982: 119, chpt. 23). Let Q denote either of ∀ or ∃, and β a closed formula in which x does not appear. The rules of passage then are:

$\forall x[\lnot \alpha (x)]\leftrightarrow \lnot \exists x\alpha (x).$
$\ Qx[\beta \land \alpha (x)]\leftrightarrow (\beta \land Qx\alpha (x)).$
$\exists x[\alpha (x)\lor \gamma (x)]\leftrightarrow (\exists x\alpha (x)\lor \exists x\gamma (x)).$

$\exists x[\lnot \alpha (x)]\leftrightarrow \lnot \forall x\alpha (x).$
$\ Qx[\beta \lor \alpha (x)]\leftrightarrow (\beta \lor Qx\alpha (x)).$
$\exists x[\alpha (x)\land \gamma (x)]\rightarrow (\exists x\alpha (x)\land \exists x\gamma (x)).$

The objective is to give all conjoined atomic terms the same argument list, a procedure Quine calls homogenization. This is achieved by employing Padding to add variables to argument lists, and Inv and inv to reorder argument lists as needed. Then use S to eliminate any duplicate variables. Once all conjoined atomic terms have a common argument list, add numerical superscripts to the predicate letters to indicate their degree, then erase the variables.

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

Mathematics does not require the full generality of PFL. The canonical foundation of mathematics is axiomatic set theory. Set theory is commonly expressed using first order logic with identity, whose universe consists entirely of sets. There is a single predicate letter of degree 2, interpreted as set membership. The canonical axiomatic set theory is ZFC. No ZFC axiom requires more than 6 variables. Tarski and Givant (1987) show that no ZFC axiom requires that the quantified variables nest more than 3 deep.

References

Bacon, John, 1985, "The completeness of a predicate-functor logic," Journal of Symbolic Logic 50: 903-26.
Paul Bernays, 1959, "Uber eine naturliche Erweiterung des Relationenkalkuls" in Heyting, A., ed., Constructivity in Mathematics. North Holland: 1-14.
Kuhn, Stephen T., 1983, "An Axiomatization of Predicate Functor Logic," Notre Dame Journal of Formal Logic 24: 233-41.
Willard Quine, 1976, "Algebraic Logic and Predicate Functors" in Ways of Paradox and Other Essays, enlarged ed. Harvard Univ. Press: 283-307.
--------, 1982. Methods of Logic, 4th ed. Harvard Univ. Press. Chpt. 45.
Sommers, Fred, 1982. The Logic of Natural Language. Oxford Univ. Press.
Alfred Tarski and Givant, Steven, 1987. A Formalization of Set Theory Without Variables. AMS.
Jean Van Heijenoort, 1967. From Frege to Godel: A Source Book on Mathematical Logic. Harvard Univ. Press.