Negative facts get a bad press. One reason for this is that it is not clear what negative facts are. We provide a theory of negative facts on which they are no stranger than positive atomic facts. We show that none of the usual arguments hold water against this account. Negative facts exist in the usual sense of existence and conform to an acceptable Eleatic principle. Furthermore, there are good reasons to want them around, including their roles in causation, chance-making (...) and truth-making, and in constituting holes and edges. (shrink)

It is well known that the circumflex notation used by Russell and Whitehead to form complex function names in Principia Mathematica played a role in inspiring Alonzo Church's “lambda calculus” for functional logic developed in the 1920s and 1930s. Interestingly, earlier unpublished manuscripts written by Russell between 1903–1905—surely unknown to Church—contain a more extensive anticipation of the essential details of the lambda calculus. Russell also anticipated Schönfinkel's combinatory logic approach of treating multiargument functions as functions having other functions as value. (...) Russell’s work in this regard seems to have been largely inspired by Frege’s theory of functions and “value-ranges”. This system was discarded by Russell due to his abandonment of propositional functions as genuine entities as part of a new tack for solving Russell’s paradox. In this article, I explore the genesis and demise of Russell’s early anticipation of the lambda calculus. (shrink)

We present a survey of the recent applications of continuous domains for providing simple computational models for classical spaces in mathematics including the real line, countably based locally compact spaces, complete separable metric spaces, separable Banach spaces and spaces of probability distributions. It is shown how these models have a logical and effective presentation and how they are used to give a computational framework in several areas in mathematics and physics. These include fractal geometry, where new results on existence and (...) uniqueness of attractors and invariant distributions have been obtained, measure and integration theory, where a generalization of the Riemann theory of integration has been developed, and real arithmetic, where a feasible setting for exact computer arithmetic has been formulated. We give a number of algorithms for computation in the theory of iterated function systems with applications in statistical physics and in period doubling route to chaos; we also show how efficient algorithms have been obtained for computing elementary functions in exact real arithmetic. (shrink)

We show how to encode context-free string grammars, linear context-free tree grammars, and linear context-free rewriting systems as Abstract Categorial Grammars. These three encodings share the same constructs, the only difference being the interpretation of the composition of the production rules. It is interpreted as a first-order operation in the case of context-free string grammars, as a second-order operation in the case of linear context-free tree grammars, and as a third-order operation in the case of linear context-free rewriting systems. This (...) suggest the possibility of defining an Abstract Categorial Hierarchy. (shrink)

Monism is the claim that only one object exists. While few contemporary philosophers endorse monism, it has an illustrious history – stretching back to Bradley, Spinoza and Parmenides. In this paper, I show that plausible assumptions about the higher-order logic of property identity entail that monism is true. Given the higher-order framework I operate in, this argument generalizes: it is also possible to establish that there is a single property, proposition, relation, etc. I then show why this form of monism (...) is inconsistent; because all propositions are identical, p is identical to ~p – and so they have the same truth-value. At least one of the assumptions that generate higher-order monism must be rejected. (shrink)

There are two dominant approaches to quantification: the Fregean and the Tarskian. While the Tarskian approach is standard and familiar, deep conceptual objections have been pressed against its employment of variables as genuine syntactic and semantic units. Because they do not explicitly rely on variables, Fregean approaches are held to avoid these worries. The apparent result is that the Fregean can deliver something that the Tarskian is unable to, namely a compositional semantic treatment of quantification centered on truth and reference. (...) We argue that the Fregean approach faces the same choice: abandon compositionality or abandon the centrality of truth and reference to semantic theory. Indeed, we argue that developing a fully compositional semantics in the tradition of Frege leads to a typographic variant of the most radical of Tarskian views: variabilism, the view that names should be modeled as Tarskian variables. We conclude with the consequences of this result for Frege's distinction between sense and reference. (shrink)

Humans communicate with different modalities. We offer an account of multi-modal meaning coordination, taking speech-gesture meaning coordination as a prototypical case. We argue that temporal synchrony (plus prosody) does not determine how to coordinate speech meaning and gesture meaning. Challenging cases are asynchrony and broadcasting cases, which are illustrated with empirical data. We propose that a process algebra account satisfies the desiderata. It models gesture and speech as independent but concurrent processes that can communicate flexibly with each other and exchange (...) the same information more than once. The account utilizes the ψ-calculus, allowing for agents, input-output-channels, concurrent processes, and data transport of typed λ-terms. A multi-modal meaning is produced integrating speech meaning and gesture meaning into one semantic package. Two cases of meaning coordination are handled in some detail: the asynchrony between gesture and speech, and the broadcasting of gesture meaning across several dialogue contributions. This account can be generalized to other cases of multi-modal meaning. (shrink)

Presenting the first comprehensive, in-depth study of hyperintensionality, this book equips readers with the basic tools needed to appreciate some of current and future debates in the philosophy of language, semantics, and metaphysics. After introducing and explaining the major approaches to hyperintensionality found in the literature, the book tackles its systematic connections to normativity and offers some contributions to the current debates. The book offers undergraduate and graduate students an essential introduction to the topic, while also helping professionals in related (...) fields get up to speed on open research-level problems. (shrink)

We present the system SUBSEXPL used for simulating and comparing explicit substitutions calculi. The system allows the manipulation of expressions of the λ-calculus and of three different styles of explicit substitutions: the λσ, the λse and the suspension calculus. A variation of the suspension calculus, which allows for combination of steps of β-contraction is included too. Implementations of the η-reduction are provided for each style. Other explicit substitutions calculi can be easily incorporated into the system due to its modular structure. (...) The uses of the system include: the visualization of the contractions of the λ-calculus in de Bruijn notation, and of guided one-step reductions as well as normalization via each of the associated substitution calculi. Many useful facilities are included: reductions can be easily recorded as text files, LATEX outputs can be generated and several examples for dealing with arithmetic operations and computational operators such as conditionals and repetitions in the λ-calculus are available. The system can be executed over Emacs using the x-symbol mode in such a way that λ-terms and terms of the explicit substitutions calculi are represented in its natural syntax avoiding the necessity of repeatedly generating LATEX outputs. The system has been of great help for systematically comparing explicit substitutions calculi, as well as for understanding properties of explicit substitutions such as the Preservation of Strong Normalization. In addition, it has been used for teaching basic properties of the λ-calculus such as: computational adequacy, the usefulness of de Bruijn's notation and of making explicit substitutions in real implementations. (shrink)

Abramsky, S., Domain theory in logical form, Annals of Pure and Applied Logic 51 1–77. The mathematical framework of Stone duality is used to synthesise a number of hitherto separate developments in theoretical computer science.• Domain theory, the mathematical theory of computation introduced by Scott as a foundation for detonational semantics• The theory of concurrency and systems behaviour developed by Milner, Hennesy based on operational semantics.• Logics of programsStone duality provides a junction between semantics and logics . Moreover, the underlying (...) logic is geometric, which can be computationally interpreted as the logic of observable properties—i.e., properties which can be determined to hold of a process on the basis of a finite amount of information about its execution.These ideas lead to the following programme. A metalanguage is introduced, comprising• types = universes of discourse for various computational situations;• terms = PROGRAMS = syntactic intensions for models or points. A standard denotational interpretation of the metalanguage is given, assigning domains to types and domain elements to terms. The metalanguage is also given a logical interpretation, in which types are interpreted as propositional theories and terms are interpreted via a program logic, which axiomatises the properties they satisfy. The two interpretations are related by showing that they are Stone duals of each other. Hence, semantics and logic are guaranteed to be in harmony with each other, and in fact each determines the other up to isomorphism. This opens the way to a whole range of applications. Given a denotational description of a computational situation in our metalanguage, we can turn the handle to obtain a logic for that situation. (shrink)

We show that the problem of deciding if a finite set of closed terms in normal form is a basis is recursively unsolvable. The restricted problem concerning one element sets is still recursively unsolvable. MSC: 03B40, 03D35.

We give here a model-theoretical solution to the problem, raised by J.L: Krivine, of the consistency of λβη+U(G)+Ω=t, wheret is an arbitrary λ-term,G an arbitrary finite group of order, sayn, andU(G) the theory which expresses the existence of a surjectiven-tuple notion, such that each element ofG behaves simultaneously as a permutation of the components of then-tuple and as an automorphism of the model. This provides in particular a semantic proof of the βη-easiness of the λ-term Ω.

In the proof-theoretic semantics approach to meaning, harmony , requiring a balance between introduction-rules (I-rules) and elimination rules (E-rules) within a meaning conferring natural-deduction proof-system, is a central notion. In this paper, we consider two notions of harmony that were proposed in the literature: 1. GE-harmony , requiring a certain form of the E-rules, given the form of the I-rules. 2. Local intrinsic harmony : imposes the existence of certain transformations of derivations, known as reduction and expansion . We propose (...) a construction of the E-rules (in GE-form) from given I-rules, and prove that the constructed rules satisfy also local intrinsic harmony. The construction is based on a classification of I-rules, and constitute an implementation to Gentzen’s (and Pawitz’) remark, that E-rules can be “read off” I-rules. (shrink)

We introduce a certain extension of -calculus, and show that it has the Church-Rosser property. The associated open-term extensional combinatory algebra is used as a basis to construct models for theories of Explict Mathematics (formulated in the language of "types and names") with positive stratified comprehension. In such models, types are interpreted as collections of solutions (of terms) w.r. to a set of numerals. Exploiting extensionality, we prove some consistency results for special ontological axioms which are refutable under elementary comprehension.

The “DNA is a program” metaphor is still widely used in Molecular Biology and its popularization. There are good historical reasons for the use of such a metaphor or theoretical model. Yet we argue that both the metaphor and the model are essentially inadequate also from the point of view of Physics and Computer Science. Relevant work has already been done, in Biology, criticizing the programming paradigm. We will refer to empirical evidence and theoretical writings in Biology, although our arguments (...) will be mostly based on a comparison with the use of differential methods (in Molecular Biology: a mutation or alike is observed or induced and its phenotypic consequences are observed) as applied in Computer Science and in Physics, where this fundamental tool for empirical investigation originated and acquired a well-justified status. In particular, as we will argue, the programming paradigm is not theoretically sound as a causal(as in Physics) or deductive(as in Programming) framework for relating the genome to the phenotype, in contrast to the physicalist and computational grounds that this paradigm claims to propose. (shrink)

Using the programming-language concept of continuations, we propose a new, multimodal analysis of quantification in Type Logical Grammar. Our approach provides a geometric view of in-situ quantification in terms of graphs, and motivates the limited use of empty antecedents in derivations. Just as continuations are the tool of choice for reasoning about evaluation order and side effects in programming languages, our system provides a principled, type-logical way to model evaluation order and side effects in natural language. We illustrate with an (...) improved account of quantificational binding, weak crossover, wh-questions, superiority, and polarity licensing. (shrink)

Mitchell, J.C. and E. Moggi, Kripke-style models for typed lambda calculus, Annals of Pure and Applied Logic 51 99–124. The semantics of typed lambda calculus is usually described using Henkin models, consisting of functions over some collection of sets, or concrete cartesian closed categories, which are essentially equivalent. We describe a more general class of Kripke-style models. In categorical terms, our Kripke lambda models are cartesian closed subcategories of the presheaves over a poset. To those familiar with Kripke models of (...) modal or intuitionistic logics, Kripke lambda models are likely to seem adequately ‘semantic’. However, when viewed as cartesian closed categories, they do not have the property variously referred to as concreteness, well- pointedness or having enough points. While the traditional lambda calculus proof system is not complete for Henkin models that may have empty types, we prove strong completeness for Kripke models. In fact, every set of equations that is closed under implication is the theory of a single Kripke model. We also develop some properties of logical relations over Kripke structures, showing that every theory is the theory of a model determined by a Kripke equivalence relation over a Henkin model. We discuss cartesian closed categories but present the main definitions and results without the use of category theory. (shrink)

In 1990, J. L. Krivine introduced the notion of storage operator to simulate, for Church integers, the “call by value” in a context of a “call by name” strategy. In the present paper we define for every λ-term S which realizes the successor function on Church integers the notion of S-storage operator. We prove that every storage operator is an S-storage operator. But the converse is not always true.

We investigate a theory of Frege structures extended by the Myhill-Flagg hierarchy of implications. We study its relation to a property theory with an approximation operator and we give a proof theoretical analysis of the basic system involved. MSC: 03F35, 03D60.

The relation between least and diagonal fixed points is a well known and completely studied question for a large class of partially ordered models of the lambda calculus and combinatory logic. Here we consider this question in the context of algebraic recursion theory, whose close connection with combinatory logic recently become apparent. We find a comparatively simple and rather weak general condition which suffices to prove the equality of least fixed points with canonical (corresponding to those produced by the Curry (...) combinator in lambda calculus) diagonal fixed points in a class of partially ordered algebras which covers both combinatory spaces of Skordev and operative spaces of Ivanov. Especially, this yields an essential improvement of the axiomatization of recursion theory via combinatory spaces. (shrink)

Inλ-calculus, the strategy of leftmost reduction (“call-by-name”) is known to have good mathematical properties; in particular, it always terminates when applied to a normalizable term. On the other hand, with this strategy, the argument of a function is re-evaluated at each time it is used.To avoid this drawback, we define the notion of “storage operator”, for each data type. IfT is a storage operator for integers, for example, let us replace the evaluation, by leftmost reduction, ofϕτ (whereτ is an integer, (...) andϕ anyλ-term) by the evaluation oftτϕ. Then, this computation is the same as the following: first computeτ up to some reduced formτ 0, and then applyϕ toτ 0. So, we have simulated “call-by-value” evaluation within the strategy of leftmost reduction.The main theorem of the paper (Corollary of Theorem 4.1) shows that, in a second orderλ-calculus, using Gödel's translation of classical intuitionistic logic, we can find a very simple type (or specification) for storage operators. Thus, it gives a way to get such operators, which is to prove this type in second order intuitionistic predicate calculus. (shrink)

Children learn their native language by exposure to their linguistic and communicative environment, but apparently without requiring that their mistakes be corrected. Such learning from “positive evidence” has been viewed as raising “logical” problems for language acquisition. In particular, without correction, how is the child to recover from conjecturing an over-general grammar, which will be consistent with any sentence that the child hears? There have been many proposals concerning how this “logical problem” can be dissolved. In this study, we review (...) recent formal results showing that the learner has sufficient data to learn successfully from positive evidence, if it favors the simplest encoding of the linguistic input. Results include the learnability of linguistic prediction, grammaticality judgments, language production, and form-meaning mappings. The simplicity approach can also be “scaled down” to analyze the learnability of specific linguistic constructions, and it is amenable to empirical testing as a framework for describing human language acquisition. (shrink)

In [7], a naive set theory is introduced based on a polynomial time logical system, Light Linear Logic (LLL). Although it is reasonably claimed that the set theory inherits the intrinsically polytime character from the underlying logic LLL, the discussion there is largely informal, and a formal justification of the claim is not provided sufficiently. Moreover, the syntax is quite complicated in that it is based on a non-traditional hybrid sequent calculus which is required for formulating LLL.In this paper, we (...) consider a naive set theory based on Intuitionistic Light Affine Logic (ILAL), a simplification of LLL introduced by [1], and call it Light Affine Set Theory (LAST). The simplicity of LAST allows us to rigorously verify its polytime character. In particular, we prove that a function over {0, 1}* is computable in polynomial time if and only if it is provably total in LAST. (shrink)

This book intends to show that radical naturalism, nominalism and strict finitism account for the applications of classical mathematics in current scientific theories. The applied mathematical theories developed in the book include the basics of calculus, metric space theory, complex analysis, Lebesgue integration, Hilbert spaces, and semi-Riemann geometry. The fact that so much applied mathematics can be developed within such a weak, strictly finitistic system, is surprising in itself. It also shows that the applications of those classical theories to the (...) finite physical world can be translated into the applications of strict finitism, which demonstrates the applicability of those classical theories without assuming the literal truth of those theories or the reality of infinity. Both professional researchers and students of philosophy of mathematics will benefit greatly from reading this book. (shrink)

In the present paper, the Fregean conception of proof-theoretic semantics that I developed elsewhere will be revised so as to better reflect the different roles played by open and closed derivations. I will argue that such a conception can deliver a semantic analysis of languages containing paradoxical expressions provided some of its basic tenets are liberalized. In particular, the notion of function underlying the Brouwer–Heyting–Kolmogorov explanation of implication should be understood as admitting functions to be partial. As argued in previous (...) work, the correctness of an inference rule should not be defined in terms of transmission of provability, but rather should be grounded on weaker principles, which I show that are motivated by consideration about the content of the inversion principle. In the conclusion, I briefly address the issue of compositionality, arguing that the violation of compositionality induced by paradoxes are no worse than others that are regarded, at least by Dummett, as wholly unproblematic. (shrink)

Substantial facts are not well-understood entities. Many philosophers object to their existence on this basis. Yet facts, if they can be understood, promise to do a lot of philosophical work: they can be used to construct theories of property possession and truthmaking, for example. Here, I give a formal theory of facts, including negative and logically complex facts. I provide a theory of reduction similar to that of the typed λ -calculus and use it to provide identity conditions for facts. (...) This theory validates truthmaker maximalism : it provides truthmakers for all truths. I then show how the usual truth-in-a-model relation can be replaced by two relations: one between models and facts, saying that a given fact obtains relative to the model, and the other between facts and propositions: the truthmaking relation. (shrink)

In the first part ("Determination"), I consider different notions of determination, contrast and compare modal with non-modal accounts and then defend two a-modality theses concerning essence and supervenience. I argue, first, that essence is a a-modal notion, i.e. not usefully analysed in terms of metaphysical modality, and then, contra Kit Fine, that essential properties can be exemplified contingently. I argue, second, that supervenience is also an a-modal notion, and that it should be analysed in terms of constitution relations between properties. (...) In the second part ("A Theory of Truthmaking"), I first review the literature on ontological commitment, and argue that the notion of truthmaking is better suited to play its explanatory rôle. I then argue that we should take truthmaker theory seriously, and that we should provide actual truthmakers for all truths there are. In the last chapter of this part, I review Armstrong's truthmaker theories and argue that they are unsatisfactory. I generalise my criticism to an argument against truthmaker necessitarianism, the view that truthmakers necessarily make true the truths they are truthmakers of. In the third part ("Properties and their Kind(s)"), I discuss qualitative determination. I present and endorse the truthmaker argument for universals, and defend universalism against friends of tropes, states of affairs and facts. I then give a novel characterisation of the important class of intrinsic properties, building on Lewis' work. With a workable notion of intrinsicness at hand, I argue that relations are ontologically – but not "ideologically" – dispensable: qualitative determination in general is a matter of intrinsic structure. In the future, I plan to add two parts and to publish my thesis as a book: In the fourth part ("Exemplification"), I argue for the existence of an exemplification relation tying universals and particulars together. I derive theoretical benefits from this relation by providing adverbialist theories of modality and tense and identify exemplification with a type of parthood. In the fifth part ("Qua qua qua"), I investigate the curious and interesting ontological category of so-called "qua-objects" (Picasso-as-a-painter, for example) and argue that they exist, are not identical with transworld indidivuals or modal parts and that they provide (contingent) truthmakers for all true predications. (shrink)

In 1990, J.L. Krivine introduced the notion of storage operator to simulate 'call by value' in the 'call by name' strategy. J.L. Krivine has shown that, using Gödel translation of classical into intuitionitic logic, we can find a simple type for the storage operators in AF2 type system. This paper studies the $forall$-positive types (the universal second order quantifier appears positively in these types), and the Gödel transformations (a generalization of classical Gödel translation) of TTR type system. We generalize, by (...) using syntaxical methods, the J.L. Krivine's Theorem about these types and for these transformations. We give a proof of this result in the case of the type of recursive integers. (shrink)

In 1990, J. L. Krivine introduced the notion of storage operator to simulate “call by value” in the “call by name” strategy. J. L. Krivine has showed that, using Gödel translation of classical into intuitionistic logic, one can find a simple type for the storage operators in AF2 type system. This paper studies the ∀-positive types and the Gödel transformations of TTR type system. We generalize by using syntactical methods Krivine's theorem about these types and for these transformations. We give (...) a proof of this result in the case of the type of recursive integers. (shrink)

The storage operators were introduced by J.L. Krivine ([6]); they are closed λ-terms which, for some fixed data type (the integers for example), allow to simulate “call by value” while using “call by name”. J.L. Krivine showed that such operators can be typed, in the type system, using Gödel's translation from classical to intuitionistic logic ([8]).This paper studies the existence of storage operators which give a normal form as result (strong storage operators) for recursive and iterative representation of data in (...) λ-calculus. We obtain the following result:We can find typed strong storage operators for the recursive representations of data type, but that is not the case for the iterative representations of an infinite data type.We give the proof of this result in the case of integers. (shrink)

We define an applicative theoryCL 2 similar to combinatory logic which can be interpreted in classes of functions possessing an enumerating function. In contrast to the models of classical combinatory logic, it is not necessarily assumed that the enumerating function itself belongs to that function class. Thereby we get a variety of possible models including e. g. the classes of primitive recursive, recursive, elementary, polynomial-time comptable ofɛ 0-recursive functions.We show that inCL 2 a major part of the metatheory of enumerated (...) classes of functions can be developed. Namely, a kind of λ-abstraction can be defined and abstract versions of theS n m - and (Primitive) Recursion Theorems are proved. Thereby, a closer analysis of the phenomenon of the different recursion theorems is achieved.A theory closely related toCL 2 can be used to replace the applicative part of Feferman's theories for explicit mathematics. So this work can be seen as an answer to Feferman's question to formulate a theory for explicit mathematics in which operations can be interpreted as primitive recursive or even more feasible ones.Finally it is shown that the proof-theoretical strength of various theoreies for explicit mathematics is preserved when replacing the applicative part of the theories by our theory together with an operation for primitive recursion. (shrink)

We define the paraconsistent supra-logic Pσ by a type-shift from the booleans o of propositional logic Po to the supra-booleans σ of the propositional type logic P obtained as the propositional fragment of the transfinite type theory Q defined by Peter Andrews (North-Holland Studies in Logic 1965) as a classical foundation of mathematics. The supra-logic is in a sense a propositional logic only, but since there is an infinite number of supra-booleans and arithmetical operations are available for this and other (...) types, virtually anything can be specified. The supra-logic is a generalization of Lukasiewicz's three-valued logic, with the intermediate value duplicated many times and ordered such that none of the copies of this value imply other ones, but it differs from Lukasiewicz's many-valued logics as well as from logics based on bilattices. There are several automated theorem provers for classical higher order logic (finite type theory) and it should be possible to modify these to our needs. (shrink)

This essay examines an argument of perennial importance against naive Leibnizian absolute identity theory, originating with Ruth Barcan in 1947 (Barcan, R. 1947. ?The identity of individuals in a strict functional 3 calculus of second order?, Journal of Symbolic Logic, 12, 12?15), and developed by Arthur Prior in 1962 (Prior, A.N. 1962. Formal Logic. Oxford: The Clarendon Press), presented here in the form offered by Nicholas Griffin in his 1977 book, Relative Identity (Griffin, N. 1977. Relative Identity. Oxford: The Clarendon (...) Press). The objection considers the property of being necessarily identical to a specific object a as a counterexample to Leibnizian identity conditions, and more particularly to the indiscernibility of identicals, when it is only contingently true that a=b. The inquiry eliminates necessity and reference to a specifically designated object as responsible for the counterexample, leaving only identity. The requirements for an exact reinterpretation of Leibniz's Law in light of counterexamples involving converse intentional properties and the family of properties suggested by the property of being necessarily identical to a where a=b (or an equivalent definite descriptor variation) is only logically contingently true, are formalized in a more powerful, counterexample-resistant version of Leibniz's Law that does not succumb to relative identity as a necessary alternative motivated by desperation over the failure of the absolute identity principle. (shrink)

This paper is dedicated to Alonzo Church, who died in August 1995 after a long life devoted to logic. To Church we owe lambda calculus, the thesis bearing his name and the solution to the Entscheidungsproblem.His well-known book Introduction to Mathematical LogicI, defined the subject matter of mathematical logic, the approach to be taken and the basic topics addressed. Church was the creator of the Journal of Symbolic Logicthe best-known journal of the area, which he edited for several decades This (...) paper is in three sections. The first is written in journalistic style:the story of the life of AlonzoChurch is told, including some of the many anecdotes I have collected from different sources. The secondpart is devoted to his work, but is far from being exhaustive. The last part is more original; in it I attempto show that Church’s great discovery was lambda calculus and that his remaining contributions weremainly inspired afterthoughts in the sense that most of his contributions as well as some of his pupils derivefrom that initial achievement. Included are Kleene’s Recursion Theory and the completeness proof ofHenkin. I have added an appendix in which is presented the typed lambda calculus and a proof of theundecidability of first-order logic. (shrink)

In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910-1912) and Church's simply typed λ-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's (...) Grundgesetze der Arithmetik for which Russell applied his famous paradox and this led him to introduce the first theory of types, the Ramified Type Theory (RTT). We present RTT formally using the modern notation for type theory and we discuss how Ramsey, Hilbert and Ackermann removed the orders from RTT leading to the simple theory of types STT. We present STT and Church's own simply typed λ-calculus (λ → C) and we finish by comparing RTT, STT and λ → C. (shrink)

We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typedλ-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews' higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratethe parallels and differences of the extensionality treatment of these approachesand demonstrate that extensional higher-order resolution is the sole approach thatcan completely avoid (...) additional extensionality axioms. (shrink)

Inside a combinatory algebra, there are ‘internal’ versions of the finite type structure over ω, which form models of various systems of finite type arithmetic. This paper compares internal representations of the intensional and extensional functionals. If these classes coincide, the algebra is called ft-extensional. Some criteria for ft-extensionality are given and a number of well-known ca's are shown to be ft-extensional, regardless of the particular choice of representation for ω. In particular, DA, Pω, Tω, Hω and certain D∞-models all (...) share the property of ft-extensionality. It is also shown that ft-extensionality is by no means an intrinsic property of ca's i.e., that there exists a very concrete class of ca's—the class of reflexive coherence spaces—no member of which has this property. This leads to a comparison of ft-extensionality with the well-studied notions of extensionality and weak extensionality. Ft-extensionality turns out to be completely independent. (shrink)

A closed λ-term E is called an enumerator if M ε /gL/dg /gTn ε N E/drn/dl = β M. Here Λ° is the set of closed λ-terms, N is the set of natural numbers and the /drn/dl are the Church numerals λfx./tfnx. Such an E is called reducing if moreover M ε /gL/dg /gTn ε N E/drn/dl /a/gb M. In 1983 I conjectured that every enumerator is reducing. An ingenious recursion theoretic proof of this conjecture by Statman is presented in (...) Barendregt . The proof is not intuitionistically valid, however. Dirk van Dalen has encouraged me to find intuitionistic proofs whenever possible. In the lambda calculus this is usually not difficult. In this paper an intuitionistic version of Statmans proof will be given. It took me somewhat longer to find it than in other cases. (shrink)