Abstraction in Fitch's Basic Logic

Abstract

Fitch's basic logic is an untyped illative combinatory logic with unrestricted principles of abstraction effecting a type collapse between properties (or concepts) and individual elements of an abstract syntax. Fitch does not work axiomatically and the abstraction operation is not a primitive feature of the inductive clauses defining the logic. Fitch's proof that basic logic has unlimited abstraction is not clear and his proof contains a number of errors that have so far gone undetected. This paper corrects these errors and presents a reasonably intuitive proof that Fitch's system K supports an implicit abstraction operation. Some general remarks on the philosophical significance of basic logic, especially with respect to neo-logicism, are offered, and the paper concludes that basic logic models a highly intensional form of logicism.

Acknowledgements

The present study is the first part of an ongoing research program on Fitch's basic logic. I thank Aldo Antonelli, Jeff Barrett and Kai Wehmeier for their comments on an earlier version of this work, and for their strong encouragement and support for what is sometimes a frustrating endeavor. I must also thank Wayne Aitken for introducing me to Fitch's program (which he re-discovered in the course of developing algorithmic logic, in collaboration with Jeff Barrett), and from whom I learned a great deal about abstraction as understood by a native mathematician. Finally, I thank the two anonymous referees for their very helpful suggestions.

Notes

¹Fitch's first paper on basic logic was published in 1942 and the last was published in 1984, with many intermediary contributions. See Anderson et al. 1975 for a partial bibliography of Fitch's work.

²The extended form of the base system of basic logic has this property. Truth is reflective in the sense that the truth operator (and its dual) can (truly) apply to itself.

³ Myhill 1950 established a completeness theorem for a system fairly similar to basic logic. Future work will show how to modify Myhill's completeness proof with the notion of a ‘structured variable’ to establish a completeness theorem for Fitch's system K, which was the first formulation of basic logic. The phrase ‘abstract syntax’ is from Cantini 1996 .

⁴So far as I know Cantini 2009 is the first systematic attempt to include Fitch's work on type-free foundations for logic and mathematics within the broader history of mathematical logic. Cantini also wonders why Fitch's work on logic is forgotten today. Cantini speculates that Fitch's peers took his work as primarily relevant to a formalist foundational project and to illative combinatory logic in particular (p. 937). However, Fitch seems to have understood propositions in the sense of Russell and if the constituency relation (of an object in a proposition) finds an exact analogue in the part/whole relation of syntax then formalist philosophical scruples may instead betray a thoroughgoing commitment to logical realism rather than to a crude formalism. Here as in other areas Fitch does not give a great deal of guidance but some hints may be found in his ‘Propositions as the Only Realities’ published in 1971.

⁵ Körner 1976 records some such attitude from Geach and McDowell in their respective responses to a talk by Fitch on a combinatory logic similar to basic logic. Haack, in her review 1978 of the proceedings recorded in the Körner volume, calls their comments ‘somewhat chilly’.

⁶There are a few exceptions to the general lack of interest in Fitch's program. The Frege structures of Aczel 1980, the systems of Apostoli 2000 , the minimal framework of Cantini 1996 , and the work on type-free logics in Feferman 1984 , all bear fruitful comparisons to basic logic. Scott and Myhill (especially the latter) devoted important papers to basic logic and Gilmore 1968 (and Gilmore's later work on partial set theory) is somewhat in the tradition of basic logic. The algorithmic logic of Aitken and Barrett 2004 , 2007a,b is closely allied with the philosophical program of basic logic.

⁷The base system for basic logic, Fitch's system K, is complete with respect to what is essentially the theory of pairing (see Myhill 1950 for a proof of this type) though Fitch did not develop basic logic in order to exemplify this kind of completeness.

⁸Basic logic does have resources sufficient to establish interesting results in metalogic, in particular, a kind of -incompleteness result, which generalizes Gödel's first incompleteness theory, will be established in forthcoming work.

⁹In subsequent papers on basic logic Fitch refers to the first paper for the proof of abstraction so he evidently thought he had established its proof beyond doubt.

¹⁰A precise definition of representation-in-K will be given later in this section.

¹¹Basic logic is richer than apparently similar projects involving universal grammar or universal notational systems such as Backus-Naur notation in theoretical computer science. K contains a fragment of set theory (the extent of this is discussed later) and extensions of K contain considerably more (perhaps all that is needed for ordinary mathematics). Indeed, from the proof-theoretic point of view K is able to match the deductive power of any finitary theory, including ZFC. This is so since K can represent every finitary inductive definition, indeed, every recursively enumerable set of natural numbers (the former was essentially established in Fitch 1942 , Theorem 5.16, the latter in Fitch 1944b , as Theorem III).

¹²Prospects for such a program obviously depends on the extent to which the axiomatic method is applicable in philosophy, including ethics and aesthetics, of which there is substantial doubt after the demise of logical positivism. Fitch was entirely serious about the role of logic in philosophy and in 1968 he anticipated the objection that value theory, of all things, can find no use for symbolic logic:

Naturally [symbolic logic] meets with strong opposition from those who do not have the technical training to understand it, and from those who feel that, though science has made great advances by use of mathematics, no analogous advance, by similar use of exact methods, is to be expected in philosophy. There is also the mistaken supposition that value concepts (e.g., those of ethics and [a]esthetics) cannot be handled by symbolic logic and that all use of symbolic logic indicates a return to a hopeless materialism and skepticism. Quite the reverse is actually the case. The only way that mankind can develop an ethics and a philosophy commensurate with its achievement in building the atomic bomb is to make full use of symbolic logic in criticizing and correcting the past systems of ethics and philosophy and in constructing new and better ones. (Fitch 1968, p. 545)

Similar sentiments are also found among advocates of the Unity of Science Movement, as detailed in Reisch 2005 .

¹³The combinators were extensively investigated by Curry and were first introduced in Schönfinkel 1924. Quine's preface to Schonfinkel's article in the van Heijenoort collection is a useful primer on the combinators. More advanced treatments may be found in Curry and Feys 1958 and Curry et al. 1972 .

¹⁴In combinatory logic these combinators satisfy the equations Kxy=x and Sxyz=xz(yz). K (the constant function) allows the system to introduce novel terms and S is carefully engineered to effect a substitution operation while simultaneously eliminating duplications of terms.

¹⁵Fitch's extension of basic logic to his system K′, which adds universal quantification to K, can quantify over all finite sequences by using Quine's method of framed ingredients given in Quine 1981 .

¹⁶It might be thought that this last point is simply too obvious to bear mention. However, basic logic is arguably a system for the description of syntax, in particular, a description of general sign-shapes. That ‘σ’ is to be free of any further syntactical analysis in terms of simpler components must be explicitly assumed in advance.

¹⁷Fitch presents basic logic using a number of notations original with Peano. I've modified Fitch's notation to promote clarity, where I thought such was needed.

¹⁸For example, one finds these combinators characterized in this way in substructural logics.

¹⁹It is assumed that the object theory is presented as a combinatorial calculus, so that ϕ(x, x) is written as ((ϕ x)x), that is, ϕ is a Curried relation.

²⁰A proof of this type will appear in a forthcoming work.

²¹Cantini proves this fact for a system quite similar to basic logic by applying Gordeev's paradox (Cantini 1996 , p. 74). A modification of this proof can be used to derive a similar result for basic logic, indeed, from the point of view of basic logic there are many non-identical empty classes.

²²For Fitch the term structure of abstracts is a reliable guide to the metaphysical structure of attributes (as assigned to objects by propositions) so the structure of terms mirrors the ontological structure of higher-order entities. Fitch did not mark this distinction explicitly – he seemed to have thought abstracts (which are linguistic items) just are attributes, rather than denoting them.

²³‘ϕ’ will be a 𝒰-expression which, in a particular application, may be a combinatory analog to a sentence in some formal language. Parameters may be drawn from 𝒰 but in principle they may be assumed to be members of some set (possibly with ur-elemente). The clauses of basic logic will treat parameters as syntactic simples when they are not themselves 𝒰-expressions.

²⁴See for example the papers in Hale and Wright's co-edited volume The Reason's Proper Study: Essays towards a Neo-Fregean Philosophy of Mathematics which outline the neo-logicist position in detail and attempts to make the case for the logicality of Hume's principle, and the non-logicality of others apparently in the same company.

²⁵See Schönfinkel 1924, republished in the van Heijenoort volume, for the original presentation of the combinators and its motivation in developing the minimum basis necessary for presenting a logic; Quine's commentary is also very useful.

²⁶These variables will, despite certain appearances, never occur as bound in a 𝒰-expression.

²⁷A similar convention is adopted by Humberstone 2000 .

²⁸The notation ϕ<texlscub>x↦ a</texlscub><texlscub>y↦ b</texlscub>is sequential substitution: first substitute a for x in ϕ, then substitute b for y in ϕ<texlscub>x↦ a</texlscub>. If a contains y then ϕ<texlscub>x↦ a</texlscub><texlscub>y↦ b</texlscub>may be distinct from ϕ<texlscub>x↦ a, y↦ b</texlscub>.

²⁹Fitch's notation for abstracts should be familiar to readers of Principia.

³⁰This fact is used in combinatory logic to model Church's lambda-calculus.

³¹We could of course apply ϵ again, and so on ad nauseum.

³²This is not quite right, since we have presented neither K nor K _λ proof theoretically – hence the appeal to proofs in the unspecified metatheory. However, the point should be clear enough.

³³Another reason why variables like x, y must not be 𝒰-expressions is that the lemma may fail otherwise. To see this, suppose x, y∈𝒰 where x and y \:do not occur as parts of each other (so, in particular, x≠y). Let ϕ=yx. Then ŷ.[ϕ]=ϵ x. So, ŷ.[ϕ]<texlscub>x↦ y</texlscub>=ϵ y but ŷ.[ϕ<texlscub>x↦ y</texlscub>]=ŷ.[(yy)]=Wϵ, and Wϵ≠ϵ y as W≠ϵ. Fitch did not seem to be aware of this problem. Because of this we must either work in a system like K _λ and then show by an induction that an analogue to the lemma also holds for K or treat x, y as 𝒰-expressions which function as free variables (and these variables do not occur as parts of each other) and where we must stipulate that in the lemma a≠x, y. This is a restriction on the substitution operation (and implicitly a restriction on abstraction).

³⁴The proof of this fact is greatly facilitated by the availability of relational abstraction in K; otherwise, the proof is nearly unmanageable.

³⁵The expression ‘◯ ₁ ◯ ₂… ◯ _n .[ϕ(x ₁, x ₂, …, x _n )]′ is an abbreviation for ◯ ₁.[◯ ₂.[… ◯ _n .[ϕ]…]].

³⁶Neo-logicists have not, to my knowledge, seriously examined illative combinatory logic as a way to recover some of the Fregean standpoint, indeed, Burgess (2005) does not seem to take the idea too seriously in his reconstruction and evaluation of their program.

³⁷Curry's early work on the combinators was intended to give a precise analysis of the role of substitution in Principia. According to Landini the relevant analysis of substitution is found in Russell's substitutional theory though some of the relevant work on this topic was only available posthumously, as first reported in Grattan-Guinness 1974 .

³⁸Fitch's work on systems which contain their own truth-predicate, nearly unacknowledged by contemporary philosophers, preceded Kripke's own work by over a decade though it must be admitted that Kripke's work is elegant and clear while Fitch's formal work is unusually complex.

³⁹The argument clearly has a transcendental flavor and basic logic under this interpretation is a novel mixing of Fregean and Kantian themes. Note that this is not a version of the Maddy–Putnam–Quine indispensability arguments given in, for example, Maddy 1992 , where the practical use of numbers in the sciences gives them a utility which is sufficient to imply their (merely contingent?) existence.

⁴⁰The version of logicism that basic logic instantiates is in this sense closer to Russell's version than Frege's.

⁴¹This could be explicitly modeled by using polymorphic typing as in Gilmore 2005 .

⁴²For Frege a concept is signified by incomplete predicate expressions and predicates are linguistic items. On the Fregean model concepts are propositional functions but it is not clear to me that Frege intended all arbitrary maps from the domain of individuals to the truth values to form the space of all concepts, though it is often said that the Russell paradox reveals this to be the case. This is wrong. The Russell paradox (and the generalized form of Cantor's paradox) have easily derived analogues in theories with a substitution operator (and no corresponding theory of sets), as can be checked by examining their derivations.

⁴³The distinction between concepts and individuals is not metaphysical but is made relative to a choice of individuals. What are concepts in one framework may function as individuals in another.

⁴⁴This definition is taken from Antonelli 2010 (p. 3).

⁴⁵The problem with adding order types as logical objects is finding a principled way to avoid the Burali–Forti paradox while also admitting transfinite order types as genuine entities.

⁴⁶This criterion is supposed to ensure the independence of a logical principle from the nature of the individuals, insuring the priority of logic over metaphysics.

⁴⁷The cardinal notion of number can also be developed within basic logic by using the techniques of Myhill 1952 .

⁴⁸Presumably the space of witnessing functions is ‘all of them’, where ‘all’ is not relativized.

⁴⁹Antonelli (2010) presents a very clear explication of permutation invariance as a principled way to pick out a distinguished class of abstraction principles as logical. He distinguishes several ways in which permutation invariance may be applied in an analysis of abstraction. In his philosophical assessment of his results Antonelli describes abstraction principles as applying inflationary pressure on the size of the first-order domain but also deflationary pressure (running the abstraction principle in reverse, metaphorically speaking) on the size of the second-order domain. Finding the right balance (between hyper-fine grained abstraction like Frege's inconsistent Law V) and coarser grained notions (like Hume's principle) yields an instrumentalist, not logical, conception of abstraction. The objects yielded by abstraction are simply representatives from some equivalence class – the choice among representatives is simply an instrument for coordinating between the size of the first- and second-order domains. We are then free, according to Antonelli, to effect whatever instrumental choices have the desired mathematical outcomes – there are no worries about things like the ‘Bad Company’ objection in this form of instrumentalism. The so-called abstracts play no privileged ontological or epistemological role. Antonelli's commentary liberates abstraction from service to particular philosophical conceptions of it, including neo-Fregean philosophy of mathematics, a separation perhaps long overdue. If Antonelli is correct I cannot see neo-logicism continuing as a distinct philosophy of mathematics – it has not been refuted, of course, but from the mathematical point of view its contribution is absorbed into a much larger mathematical project classifying consistent abstraction principles with respect to proof-theoretic strength (in the spirit, I take it, of the analysis of subsystems of second-order arithmetic). This would be a most worthy project.

⁵⁰Consistent fragments of Frege's theory have been calibrated against the analytic hierarchy, see especially the paper by Ferreira and Wehmeier Ferreira and Wehmeier 2002 ‘On the Consistency of the -CA Fragment of Frege's Grundgesetze’.

⁵¹Fitch's teacher was F. S. C. Northrop.