Predicate Functor Logic - Bacon's Work

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 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 theoretic structure of Inv and inv;
• Mentions that sentential logic, monadic predicate logic, the modal logic S5, and the Boolean logic of (un)permuted relations, are all fragments of PFL.