Predicate functor 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 quantified variables. PFL employs a small number of algebraic devices called predicate functors (or predicate modifiers) that operate on terms to yield terms. PFL is mostly the invention of the logician 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 algebraizes propositional 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 logics are sound, complete, and undecidable. Most work Quine published on logic and mathematics in the last 30 years of his life touched on PFL in some way.

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 1982: 129)

Ways other than PFL to algebraize first-order logic include:

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 (1976) and 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:

Kuhn's formalization

The PFL syntax, primitives, and axioms described in this section are largely 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 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).

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 variables 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 sound and 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 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 \{x_1...x_n : Fx_1...x_n\} denotes the set of n-tuples satisfying the atomic formula Fx_1...x_n.

 IFx_1x_2...x_n \leftrightarrow Fx_1x_1...x_n \leftrightarrow Fx_2x_2...x_n.

Identity is reflexive (Ixx), symmetric (IxyIyx), transitive ( (IxyIyz) → Ixz), and obeys the substitution property:

(Fx_1...x_n \and Ix_1y) \rightarrow Fyx_2...x_n.
\ +F^n =_{def} \{x_0x_1...x_n : F^n x_1...x_n\}.
+Fx_1...x_n \leftrightarrow Fx_2...x_n.
 \exist F^n =_{def} \{x_2...x_n : \exist x_1 F^n x_1...x_n\}.
Fx_1...x_n \rightarrow \exist Fx_2...x_n.

Cropping enables two useful defined functors:

\ SF^n =_{def} \{x_2...x_n : F^n x_2x_2...x_n\}.
SF^n \leftrightarrow \exist 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.

F^m \times G^n \leftrightarrow F^m \exist^m G^n.

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:

F^mx_1...x_mG^nx_1...x_n \leftrightarrow (F^m \times G^n)x_1...x_mx_1...x_n.

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.

\ InvF^n =_{def} \{x_1...x_n : F^nx_nx_1...x_{n-1}\}.
 Inv Fx_1...x_n \leftrightarrow Fx_nx_1...x_{n-1}.
\ invF^n =_{def} \{x_1...x_n : F^n x_2x_1...x_n\}.
 invFx_1...x_n \leftrightarrow Fx_2x_1...x_n.
\ pF^n =_{def} \{x_1...x_n : F^n x_1x_3...x_nx_2\}.
 pFx_1...x_n \leftrightarrow Inv  inv Fx_1x_3...x_nx_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 Fn moves the k+1 variable to the second argument position in F.

When n=2, Inv and inv merely interchange x1 and x2. 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.

Expression Degree
 p; Inv; inv; \lnot; I no change
\ +F^{n-1}; \exist F^{n+1}; \ SF^{n+1} \ n
\ \alpha^m\beta^n; F^m \times G^n \ 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 rules are:

Some useful results

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:

  • F^n \rightarrow +\exist F^n

  • F^n \leftrightarrow \exist +F^n

Negation distributes over +, , and p:

  • +\lnot F^n \leftrightarrow \lnot +F^n

  • \lnot\exist F^n \rightarrow \exist \lnot F^n

  • p\lnot F^n \leftrightarrow \lnot pF^n

+ and p distributes over conjunction:

  • +(F^nG^m) \leftrightarrow (+F^n+G^m)

  • p(F^nG^m) \leftrightarrow (pF^npG^m)

Identity has the interesting implication:

Quine also conjectured the rule: If \ \alpha is a PFL theorem, then so are \ p\alpha, \ +\alpha, and \lnot \exist \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:

Bacon also:

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:

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):

\exist x[\alpha (x) \or \gamma (x)] \leftrightarrow (\exist x \alpha (x) \or \exist x \gamma (x)).

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

(F^m \and G^n) \leftrightarrow (F^m \times G^n) \leftrightarrow (F^m \exist^m G^n); m<n.

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:

 (\alpha \or \beta \or ...) \leftrightarrow \lnot(\lnot\alpha \and \lnot\beta \and ...).

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.[1]

See also

Footnotes

  1. Metamath axioms.

References

External links

This article is issued from Wikipedia - version of the Saturday, March 05, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.