View source for Predicate functor logic

{{Short description|Algebraization of first-order logic}}
In [[mathematical logic]], '''predicate functor logic''' ('''PFL''') is one of several ways to express [[first-order logic]] (also known as [[predicate logic]]) by purely algebraic means, i.e., without [[Quantification (logic)|quantified variable]]s. PFL employs a small number of algebraic devices called '''predicate functors'''<!--boldface per WP:R#PLA--> (or '''predicate modifiers'''<!--boldface per WP:R#PLA-->)<ref>Johannes Stern, ''Toward Predicate Approaches to Modality'', Springer, 2015, p. 11.</ref> that operate on terms to yield terms. PFL is mostly the invention of the [[logic]]ian and [[philosopher]] [[Willard Quine]].

==Motivation==
The 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 (logic)|Boolean algebra]] algebraizes [[propositional logic]]. He designed PFL to have exactly the [[First-order logic#Expressiveness|expressive power]] of [[first-order logic]] with [[Identity (mathematics)|identity]]. Hence the [[metamathematics]] of PFL are exactly those of first-order logic with no interpreted predicate letters: both logics are [[consistency proof|sound]], [[Completeness (logic)|complete]], and [[undecidable problem|undecidable]]. Most work Quine published on logic and mathematics in the last 30 years of his life touched on PFL in some way.{{citation needed|date=August 2014}}

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:
<blockquote>
"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)
</blockquote>

Ways other than PFL to algebraize [[first-order logic]] include:
*[[Cylindric algebra]] by [[Alfred Tarski]] and his American students. The simplified 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 [[axiom]]s, this algebra most resembles PFL;
*[[Relation algebra]] algebraizes the fragment of [[first-order logic]] consisting of formulas having no atomic formula lying in the scope of more than three [[Quantifier (logic)|quantifier]]s. That fragment suffices, however, for [[Peano arithmetic]] and the [[axiomatic set theory]] [[ZFC]]; hence relation algebra, unlike PFL, is [[Gödel's incompleteness theorem|incompletable]]. Most work on relation algebra since about 1920 has been by Tarski and his American students. The power of relation algebra did not become manifest until the monograph Tarski and Givant (1987), published after the three important papers bearing on PFL, namely Bacon (1985), Kuhn (1983), and Quine (1976);
*[[Combinatory logic]] builds on [[combinator]]s, [[higher order function]]s whose [[domain of a function|domain]] is another combinator or function, and whose [[range of a function|range]] is yet another combinator. Hence [[combinatory logic]] goes beyond first-order logic by having the expressive power of [[set theory]], which makes combinatory logic vulnerable to [[paradox]]es. A predicate functor, on the other hand, simply maps predicates (also called [[Term (logic)|terms]]) into predicates.
PFL is arguably the simplest of these formalisms, yet also the one about which the least has been written.

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:
* Until [[Dana Scott]] began writing on the [[model theory]] of combinatory logic in the late 1960s, almost only [[Haskell Curry]], his students, and [[Robert Feys]] in Belgium worked on that logic;
*Satisfactory axiomatic formulations of combinatory logic were slow in coming. In the 1930s, some formulations of combinatory logic were found to be [[consistency proof|inconsistent]]. Curry also discovered the [[Curry paradox]], peculiar to combinatory logic;
*The [[lambda calculus]], with the same expressive power as [[combinatory logic]], was seen as a superior formalism.

==Kuhn's formalization==
The PFL [[syntax]], primitives, and axioms described in this section are largely [[Steven Kuhn]]'s (1983). The [[semantics]] of the functors are Quine's (1982). The rest of this entry incorporates some terminology from Bacon (1985).

===Syntax===
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. An atomic term of degree 0 denotes a [[Boolean variable]] or a [[truth value]]. The degree of ''I'' is invariably 2 and so is not 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 [[Logical connective|connective]] that, when combined with negation, forms a [[functional completeness|functionally complete]] set of connectives. Quine's preferred functionally complete set was [[Logical conjunction|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 (&alpha; and/or &beta;)" (see [[Sheffer stroke|NAND]] and [[Logical NOR|NOR]]).

===Axioms and semantics===
Quine set out neither axiomatization nor proof procedure for PFL. The following axiomatization of PFL, one of two proposed in Kuhn (1983), is concise and easy to describe, but makes extensive use of [[free variable]]s and so does not do full justice to the spirit of PFL. Kuhn gives another axiomatization dispensing with free variables, but that is harder to describe and that makes extensive use of defined functors. Kuhn proved both of his PFL axiomatizations [[consistency proof|sound]] and [[Completeness (logic)|complete]].

This section is built around 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 [[tautology (logic)|tautologies]] of sentential logic can be taken as axioms.

Quine's (1982) semantics for each predicate functor are stated below in terms of [[abstraction]] (set builder notation), followed by either the relevant axiom from Kuhn (1983), or a definition from Quine (1976). The notation <math>\{x_1\cdots x_n : Fx_1\cdots x_n\}</math> denotes the set of [[n-tuple|''n''-tuple]]s satisfying the atomic formula <math>Fx_1\cdots x_n.</math>

*''Identity'', {{mvar|I}}, is defined as:
:<math> IFx_1x_2\cdots x_n \leftrightarrow (Fx_1x_1\cdots x_n \leftrightarrow Fx_2x_2\cdots x_n)\text{.}</math>
Identity is [[reflexive relation|reflexive]] ({{mvar|Ixx}}), [[symmetric]] ({{math|''Ixy''→''Iyx''}}), [[transitive relation|transitive]] ({{math|(''Ixy''∧''Iyz'') → ''Ixz''}}), and obeys the substitution property:
:<math>(Fx_1\cdots x_n \land Ix_1y) \rightarrow Fyx_2\cdots x_n.</math>
*''Padding'', '''+''', adds a variable to the left of any argument list.
:<math>\ +F^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_0x_1\cdots x_n : F^n x_1\cdots x_n\}.</math>
:<math>+Fx_1\cdots x_n \leftrightarrow Fx_2\cdots x_n.</math>
*''Cropping'', '''∃''', erases the leftmost variable in any argument list.
:<math> \exist F^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_2\cdots x_n : \exist x_1 F^n x_1\cdots x_n\}.</math>
:<math>Fx_1\cdots x_n \rightarrow \exist Fx_2\cdots x_n.</math>

''Cropping'' enables two useful defined functors:
* ''Reflection'', '''S''':
:<math>SF^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_2\cdots x_n : F^n x_2x_2\cdots x_n\}.</math>
:<math>SF^n \leftrightarrow \exist IF^n.</math>
'''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 [[combinatory logic|primitive combinator]] '''S''' of combinatory logic.
*''[[Cartesian product]]'', <math>\times</math>;
:<math>F^m \times G^n \leftrightarrow F^m \exist^m G^n.</math> 
Here only, Quine adopted an infix notation, because this infix notation for Cartesian product is very well established in mathematics. Cartesian product allows restating conjunction as follows:
:<math>F^mx_1\cdots x_mG^nx_1\cdots x_n \leftrightarrow (F^m \times G^n)x_1\cdots x_mx_1\cdots x_n.</math>
Reorder the concatenated argument list so as to shift a pair of duplicate variables to the far left, then invoke '''S''' to eliminate the duplication. Repeating this as many times as required results in an argument list of length max(''m'',''n'').

The next three functors enable reordering argument lists at will.  
*''Major inversion'', '''Inv''', rotates the variables in an argument list to the right, so that the last variable becomes the first.
:<math>\operatorname{Inv} F^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_1\cdots x_n : F^nx_nx_1\cdots x_{n-1}\}.</math>
:<math>\operatorname{Inv} Fx_1\cdots x_n \leftrightarrow Fx_nx_1\cdots x_{n-1}.</math>
*''Minor inversion'', '''inv''', swaps the first two variables in an argument list.
:<math>\operatorname{inv} F^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_1\cdots x_n : F^n x_2x_1\cdots x_n\}.</math>
:<math>\operatorname{inv} Fx_1\cdots x_n \leftrightarrow Fx_2x_1\cdots x_n.</math>
*''Permutation'', '''p''', rotates the second through last variables in an argument list to the left, so that the second variable becomes the last.
:<math>\ pF^n \ \overset{\underset{\mathrm{def}}{}}{=}\ \{x_1\cdots x_n : F^n x_1x_3\cdots x_nx_2\}.</math>
:<math> pFx_1\cdots x_n \leftrightarrow \operatorname{Inv} \operatorname{inv} Fx_1x_3\cdots x_nx_2.</math>
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''<sup>''n''</sup> moves the ''k''+1 variable to the second argument position in ''F''.

When ''n''=2, '''Inv''' and '''inv''' merely interchange ''x''<sub>1</sub> and ''x''<sub>2</sub>. 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'''.

The following table summarizes how the functors affect the degrees of their arguments.
{| class="wikitable" style="text-align: center;"
!Expression
!Degree
|-
|<math>p;\operatorname{Inv};\operatorname{inv};\ \lnot;\ I</math>
|no change
|-
|<math>+F^{n-1};\ \exist F^{n+1}; \ SF^{n+1}</math> || {{mvar|n}}
|-
|<math>\alpha^m\beta^n;\ F^m \times G^n</math> || {{math|max(''m'', ''n'')}}
|}

===Rules===
All instances of a predicate letter may be replaced by another predicate letter of the same degree, without affecting validity. The [[first-order logic|rules]] are:
* [[Modus ponens]];
* Let ''α'' and ''β'' be PFL formulas in which <math>x_1</math> does not appear. Then if <math>(\alpha \land Fx_1...x_n) \rightarrow \beta </math> is a PFL theorem, then <math>(\alpha \land \exist Fx_2...x_n) \rightarrow \beta </math> is likewise a PFL theorem.

===Some useful results===
Instead of axiomatizing PFL, Quine (1976) proposed the following conjectures as candidate axioms.

: <math>\exist I</math>
''n''&minus;1 consecutive iterations of '''p''' restores the ''status quo ante'':
: <math>F^n \leftrightarrow p^{n-1}F^n</math>
'''+''' and '''∃''' annihilate each other:

: <math>\begin{cases}F^n \rightarrow +\exist F^n\\
F^n \leftrightarrow \exist +F^n\end{cases}</math>

Negation distributes over '''+''', '''∃''', and '''p''':

: <math>\begin{cases}+\lnot F^n \leftrightarrow \lnot +F^n\\
\lnot\exist F^n \rightarrow \exist \lnot F^n\\
p\lnot F^n \leftrightarrow \lnot pF^n\end{cases}</math>

'''+''' and '''p''' distributes over conjunction:

: <math>\begin{cases}+(F^nG^m) \leftrightarrow (+F^n+G^m)\\
p(F^nG^m) \leftrightarrow (pF^npG^m)\end{cases}</math>

Identity has the interesting implication:
: <math>IF^n \rightarrow p^{n-2} \exist p+F^n</math>

Quine also conjectured the rule: If {{mvar|&alpha;}} is a PFL theorem, then so are {{math|''p&alpha;'', +&alpha;}}, and <math>\lnot \exist \lnot \alpha</math>.

==Bacon's work==
Bacon (1985) takes the [[Material conditional|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 [[consistency proof|sound]] and [[Completeness (logic)|complete]] in full detail.
*An axiomatic formulation, which Bacon asserts, but does not prove, equivalent to the preceding one. Some of these axioms are simply Quine conjectures restated in Bacon's 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 theory|group theoretic]] structure of '''Inv''' and '''inv''';
*Mentions that [[sentential logic]], [[monadic predicate logic]], the [[modal logic]] [[S5 (modal logic)|S5]], and the Boolean logic of (un)permuted [[relation (mathematics)|relation]]s, are all fragments of PFL.

==From first-order logic to PFL==
The following [[algorithm]] is adapted from Quine (1976: 300–2). Given a [[sentence (mathematical logic)|closed formula]] of [[first-order logic]], first do the following:
* Attach a numerical subscript to every predicate letter, stating its degree;
* Translate all [[universal quantifier]]s into [[existential quantifier]]s and negation;
* Restate all [[atomic formula]]s of the form {{math|''x''{{=}}''y''}} as {{mvar|Ixy}}.

Now apply the following algorithm to the preceding result:
{{ordered list
|Translate the matrices of the most deeply nested quantifiers into [[disjunctive normal form]], consisting of [[logical OR|disjuncts]] of [[logical AND|conjuncts]] of terms, negating atomic terms as required. The resulting subformula contains only negation, conjunction, disjunction, and existential quantification.

|Distribute the existential quantifiers over the disjuncts in the matrix using the [[rules of passage (logic)|rule of passage]] (Quine 1982: 119):
:<math>\exist x[\alpha (x) \lor \gamma (x)] \leftrightarrow (\exist x \alpha (x) \lor \exist x \gamma (x)).</math>

|Replace conjunction by [[Cartesian product]], by invoking the fact:
:<math>(F^m \land G^n) \leftrightarrow (F^m \times G^n) \leftrightarrow (F^m \exist^m G^n); m<n.</math>

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

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

|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 '''∃'''.

|Repeat (1)-(6) until all quantified variables have been eliminated. Eliminate any disjunctions falling within the scope of a quantifier by invoking the equivalence:
:<math> (\alpha \lor \beta \lor ...) \leftrightarrow \lnot(\lnot\alpha \land \lnot\beta \land ...).</math>
}}
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 (mathematics)|identity]], with a [[universe of discourse]] consisting entirely of sets. There is a single [[first-order logic|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.<ref>[http://us.metamath.org/mpegif/mmset.html#staxioms Metamath axioms.]</ref>

==See also==
*[[Algebraic logic]]

==Footnotes==
{{reflist}}

==References==
*Bacon, John, 1985, "[https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/completeness-of-a-predicatefunctor-logic/B29F706DB4A28C5EB7E4661535FBD85A The completeness of a predicate-functor logic]," ''[[Journal of Symbolic Logic]] 50'': 903–26.
*[[Paul Bernays]], 1959, "[https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/paul-bernays-uber-eine-naturliche-erweiterung-des-relationenkalkus-constructivity-in-mathematics-proceedings-of-the-colloquium-held-at-amsterdam-1957-edited-by-a-heyting-studies-in-logic-and-the-foundations-of-mathematics-northholland-publishing-company-amsterdam1959-pp-114/05AC676B63D15A328BB080C7EA1730A3 Uber eine naturliche Erweiterung des Relationenkalkuls]" in Heyting, A., ed., ''Constructivity in Mathematics''. North Holland: 1–14.
*[[Steven Kuhn|Kuhn, Steven T.]], 1983, "[https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-24/issue-2/An-axiomatization-of-predicate-functor-logic/10.1305/ndjfl/1093870313.full An Axiomatization of Predicate Functor Logic]," ''[[Notre Dame Journal of Formal Logic]] 24'': 233–41.
*[[Willard Quine]], 1976, "Algebraic Logic and Predicate Functors" in [https://www.hup.harvard.edu/books/9780674948372 ''Ways of Paradox and Other Essays'', revised and enlarged ed.] Harvard Univ. Press: 283–307.
*Willard Quine, 1982. [https://www.hup.harvard.edu/books/9780674571761 ''Methods of Logic'', 4th ed.] Harvard Univ. Press. Chpt. 45.
*[[Fred Sommers|Sommers, Fred]], 1982. ''The Logic of Natural Language''. Oxford Univ. Press.
*[[Alfred Tarski]] and Givant, Steven, 1987. ''[https://bookstore.ams.org/coll-41 A Formalization of Set Theory Without Variables]''. [[American Mathematical Society|AMS]].
*[[Jean Van Heijenoort]], 1967. ''[https://www.hup.harvard.edu/books/9780674324497 From Frege to Gödel: A Source Book on Mathematical Logic]''. Harvard Univ. Press.

==External links==
* [http://stp.ling.uu.se/~matsd/pub/pfl.ps ''An introduction to predicate-functor logic''] (one-click download, PS file) by Mats Dahllöf (Department of Linguistics, Uppsala University)

[[Category:Algebraic logic]]
[[Category:Mathematical axioms]]
[[Category:Predicate logic]]