He designed PFL to have exactly the expressive power of first-order logic with identity.
Most work Quine published on logic and mathematics in the last 30 years of his life touched on PFL in some way.
[citation needed] Quine took "functor" from the writings of his friend Rudolf Carnap, the first to employ it in philosophy and mathematical logic, and defined it 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 had a lifelong fascination with combinatory logic, attested to by his introduction to the translation in Van Heijenoort (1967) of the paper by the Russian logician Moses Schönfinkel founding combinatory logic.
When Quine began working on PFL in earnest, in 1959, combinatory logic was commonly deemed a failure for the following reasons: The PFL syntax, primitives, and axioms described in this section are largely Steven Kuhn's (1983).
An atomic term is an upper case Latin letter, I and S excepted, 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.
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).
Kuhn gives another axiomatization dispensing with free variables, but that is harder to describe and that makes extensive use of defined functors.
The alethic functors can be axiomatized by any set of axioms for sentential logic whose primitives are negation and one of ∧ or ∨.
Identity is reflexive (Ixx), symmetric (Ixy→Iyx), transitive ((Ixy∧Iyz) → Ixz), and obeys the substitution property: Cropping enables two useful defined functors: S generalizes the notion of reflexivity to all terms of any finite degree greater than 2.
Repeating this as many times as required results in an argument list of length max(m,n).
The notation p in Kuhn corresponds to inv; he has no analog to Permutation and hence has no axioms for it.
The rules are: Instead of axiomatizing PFL, Quine (1976) proposed the following conjectures as candidate axioms.
n−1 consecutive iterations of p restores the status quo ante: + and ∃ annihilate each other: Negation distributes over +, ∃, and p: + and p distributes over conjunction: Identity has the interesting implication: Quine also conjectured the rule: If α is a PFL theorem, then so are pα, +α, and
Bacon (1985) takes the conditional, negation, Identity, Padding, and Major and Minor inversion as primitive, and Cropping as defined.