Proofs from assumptions are amongst the most fundamental reasoning techniques. Yet the precise nature of assumptions is still an open topic. One of the most prominent conceptions is the placeholder view of assumptions generally associated with natural deduction for intuitionistic propositional logic. It views assumptions essentially as holes in proofs, either to be filled with closed proofs of the corresponding propositions via substitution or withdrawn as a side effect of some rule, thus in effect making them an auxiliary notion subservient (...) to proper propositions. The Curry–Howard correspondence is typically viewed as a formal counterpart of this conception. I will argue against this position and show that even though the Curry–Howard correspondence typically accommodates the placeholder view of assumptions, it is rather a matter of choice, not a necessity, and that another more assumption-friendly view can be adopted. (shrink)

Mathematics is about proofs, that is the derivation of correct statements; and calculations, that is the production of results according to well-defined sets of rules. The two notions are intimately related. Proofs can involve calculations, and the algorithm underlying a calculation should be proved correct. The aim of the author is to explore this relationship. The book itself forms an introduction to simple type theory. Starting from the familiar propositional calculus the author develops the central idea of an applied lambda-calculus. (...) This is illustrated by an account of Gödel's T, a system which codifies number-theoretic function hierarchies. Each of the book's 52 sections ends with a set of exercises, some 200 in total. These are designed to help the reader get to grips with the subject, and develop a further understanding. An appendix contains complete solutions of these exercises. (shrink)

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof (...) normalization corresponds to term reduction, etc. But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transforms proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq). This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic. Key features - The Curry-Howard Isomorphism treated as common theme - Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics - Thorough study of the connection between calculi and logics - Elaborate study of classical logics and control operators - Account of dialogue games for classical and intuitionistic logic - Theoretical foundations of computer-assisted reasoning · The Curry-Howard Isomorphism treated as the common theme. · Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics · Thorough study of the connection between calculi and logics. · Elaborate study of classical logics and control operators. · Account of dialogue games for classical and intuitionistic logic. · Theoretical foundations of computer-assisted reasoning. (shrink)

This paper introduces a natural deduction calculus for intuitionistic logic of belief \ which is easily turned into a modal \-calculus giving a computational semantics for deductions in \. By using that interpretation, it is also proved that \ has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in \ showing the general structure of such a modality for belief in an intuitionistic framework.

The Curry-Howard isomorphism is a proof-theoretic result that establishes a connection between derivations in natural deduction and terms in typed lambda calculus. It is an important proof-theoretic result, but also underlies the development of type systems for programming languages. This fact suggests a potential importance of the result for a philosophy of code.

In order to allow the use of axioms in a second‐order system of extracting programs from proofs, we define constant terms, a form of Curry‐Howard terms, whose types are intended to correspond to those axioms. We also define new reduction rules for these new terms so that all consequences of the axioms can be represented. We finally show that the extended Curry‐Howard terms are strongly normalizable.

A comparison is given between two conditions used to define logical constants: Belnap's uniqueness and Hacking's deducibility of identicals. It is shown that, in spite of some surface similarities, there is a deep difference between them. On the one hand, deducibility of identicals turns out to be a weaker and less demanding condition than uniqueness. On the other hand, deducibility of identicals is shown to be more faithful to the inferentialist perspective, permitting definition of genuinely proof-theoretical concepts. This kind of (...) analysis is driven by exploiting the Curry–Howard correspondence. In particular, deducibility of identicals is shown to correspond to the computational property of eta expansion, which is essential in the characterization of propositional identity. (shrink)

In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the (...) natural deduction system of Wansing's bi-intuitionistic logic 2Int, which I will turn into a term-annotated form. Therefore, we need a type theory that extends to a two-sorted typed lambda-calculus. I will present such a term-annotated proof system for 2Int and prove a Dualization Theorem relating proofs and refutations in this system. On the basis of these formal results I will argue that this gives us interesting insights into questions about sense and denotation as well as synonymy and identity of proofs from a bilateralist point of view. (shrink)

We present a proof system for a multimode and multimodal logic, which is based on our previous work on modal Martin-Löf type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e., a small 2-category. The logic is extended to a lambda calculus, establishing a Curry–Howard correspondence.

The Lambek-Grishin calculus is a symmetric version of categorial grammar obtained by augmenting the standard inventory of type-forming operations (product and residual left and right division) with a dual family: coproduct, left and right difference. Interaction between these two families is provided by distributivity laws. These distributivity laws have pleasant invariance properties: stability of interpretations for the Curry-Howard derivational semantics, and structure-preservation at the syntactic end. The move to symmetry thus offers novel ways of reconciling the demands of (...) natural language form and meaning. (shrink)

The paper is devoted to an examination of the epistemic account of the notion of deductive inference recently provided by D. Prawitz, and based on the notion of ground. This is part of the general scenario constituted by the “Proof-theoretic semantics”, presented since the ’70s of the last century as an alternative to the standard model-theoretic explication of the notion of logical consequence.Our argument pivots on the so-called “Curry–Howard Correspondence”, which exploited the idea of considering proofs as (...) proper mathematical objects in a remarkable way. A sort of rational reconstruction of this idea is outlined, tracing it back to Hilbert and Husserl’s investigations. (shrink)

This paper investigates whether the fundamental linguistic insights and intuitions of Lexical Functional Grammar, which is usually presented as a constraint-based linguistic theory, can be reformulated in a resource sensitive framework using a substructural modal logic. In the approach investigated here, LFG's f-descriptions are replaced with expressions from a multi-modal propositional logic. In effect, the feature structure unification basis of LFG's f-structures is replaced with a very different resource based mechanism. It turns out that some linguistic analyses that required non-monotonic (...) devices in LFG analysis of Icelandic) can be straightforwardly expressed in the framework presented here. Moreover, a Curry– Howard correspondence between proofs in this logic and -terms provides a semantic interpretation as a by-product of the process of showing syntactic well-formedness. (shrink)

In this paper we discuss a new perspective on the syntax-semantics interface. Semantics, in this new set-up, is not ‘read off’ from Logical Forms as in mainstream approaches to generative grammar. Nor is it assigned to syntactic proofs using a Curry-Howard correspondence as in versions of the Lambek Calculus, or read off from f-structures using Linear Logic as in Lexical-Functional Grammar (LFG, Kaplan & Bresnan [9]). All such approaches are based on the idea that syntactic objects (trees, (...) proofs, fstructures) are somehow prior and that semantics must be parasitic on those syntactic objects. We challenge this idea and develop a grammar in which syntax and semantics are treated in a strictly parallel fashion. The grammar will have many ideas in common with the (converging) frameworks of categorial grammar and LFG, but its treatment of the syntax-semantics interface is radically different. Also, although the meaning component of the grammar is a version of Montague semantics and although there are obvious affinities between Montague’s conception of grammar and the work presented here, the grammar is not compositional, in the sense that composition of meaning need not follow surface structure. (shrink)

, which uses the intuitionistic propositional calculus, with the only connective →. It is very important, because the well known Curry-Howard correspondence between proofs and programs was originally discovered with it, and because it enjoys the normalization property: every typed term is strongly normalizable. It was extended to second order intuitionistic logic, in 1970, by J.-Y. Girard [4], under the name of system F, still with the normalization property.More recently, in 1990, the Curry-Howard correspondence (...) was extended to classical logic, following Felleisen and Griffin [6] who discovered that the law of Peirce corresponds to control instructions in functional programming languages. It is interesting to notice that, as early as 1972, Clint and Hoare [1] had made an analogous remark for the law of excluded middle and controlled jump instructions in imperative languages.There are now many type systems which are based on classical logic; among the best known are the system LC of J.-Y. Girard [5] and the λμ-calculus of M. Parigot [11]. We shall use below a system closely related to the latter, called the λ c -calculus [8, 9]. Both systems use classical second order logic and have the normalization property.In the sequel, we shall extend the λ c -calculus to the Zermelo-Frænkel set theory. The main problem is due to the axiom of extensionality. To overcome this difficulty, we first give the axioms of ZF in a suitable (equivalent) form, which we call ZF ɛ. (shrink)

Focused sequent calculi are a refinement of sequent calculi, where additional side-conditions on the applicability of inference rules force the implementation of a proof search strategy. Focused cut-free proofs exhibit a special normal form that is used for defining identity of sequent calculi proofs. We introduce a novel focused display calculus fD.LG and a fully polarized algebraic semantics FP.LG\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbb {FP.LG}$$\end{document} for Lambek–Grishin logic by generalizing the theory of multi-type calculi and their (...) algebraic semantics with heterogenous consequence relations. The calculus fD.LG has strong focalization and it is sound and complete w.r.t. FP.LG\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbb {FP.LG}$$\end{document}. This completeness result is in a sense stronger than completeness with respect to standard polarized algebraic semantics, insofar as we do not need to quotient over proofs with consecutive applications of shifts over the same formula. We also show a number of additional results. fD.LG is sound and complete w.r.t. LG-algebras: this amounts to a semantic proof of the so-called completeness of focusing, given that the standard (display) sequent calculus for Lambek–Grishin logic is complete w.r.t. LG-algebras. fD.LG and the focused calculus fLG of Moortgat and Moot are equivalent with respect to proofs, indeed there is an effective translation from fLG-derivations to fD.LG-derivations and vice versa: this provides the link with operational semantics, given that every fLG-derivation is in a Curry–Howard correspondence with a directional λ¯μμ~\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\overline{\lambda }\mu \widetilde{\mu }$$\end{document}-term. (shrink)

Les mathématiques telles qu’elles se sont développées entre 1935 et 1970 jouent un rôle très important dans La Méthode. Ce rôle est explicite en ce qui concerne la logique, plus implicite en ce qui concerne la théorie du contrôle, l’incertitude, et certaines notions vues hors du champ mathématique et particulièrement probabiliste . Sur un exemple de résultats récents de la logique mathématique, la correspondance de Curry-Howard et les travaux de Jean-Louis Krivine nous montrent la pertinence des idées et (...) des intuitions d’Edgar Morin concernant la logique, la réalité et le cerveau.Mathematics as they are developed between 1935 and 1970 played a very important role in the method. This role is explicit with respect to the logical, implied regarding control theory, uncertainty, and some notions out of the field and especially mathematical probability . On a recent example of results of mathematical logic, the Curry-Howard correspondence and the work of Jean-Louis Krivine show the relevance of the ideas and insights of Edgar Morin on logic, reality and brain. (shrink)

Game semantics extends the Curry–Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. The system is expressive: it contains all of the connectives of Intuitionistic Linear Logic, and first-order quantification. Use of Lairdʼs sequoid operator allows proofs with imperative behaviour to be expressed. Thus, we (...) can embed first-order Intuitionistic Linear Logic into this system, Polarized Linear Logic, and an imperative total programming language.The proof system has a tight connection with a simple game model, where games are forests of plays. Formulas are modelled as games, and proofs as history-sensitive winning strategies. We provide a strong full completeness result with respect to this model: each finitary strategy is the denotation of a unique analytic proof. Infinite strategies correspond to analytic proofs that are infinitely deep. Thus, we can normalise proofs, via the semantics. (shrink)

Most type systems are agnostic regarding the evaluation strategy for the underlying languages, with the value restriction for ML which is absent in Haskell as a notable exception. As type systems become more precise, however, detailed properties of the operational semantics may become visible because properties captured by the types may be sound under one strategy but not the other. For example, intersection types distinguish between call-by-name and call-by-value functions, because the subtyping law ∩≤A→ is unsound for the latter in (...) the presence of effects.In this paper we develop a proof-theoretic framework for analyzing the interaction of types with evaluation order, based on the notion of polarity. Polarity was discovered through linear logic, but we propose a fresh origin in Dummett’s program of justifying the logical laws through alternative verificationist or pragmatist “meaning-theories”, which include a bias towards either introduction or elimination rules. We revisit Dummett’s analysis using the tools of Martin-Löf’s judgmental method, and then show how to extend it to a unified polarized logic, with Girard’s “shift” connectives acting as intermediaries. This logic safely combines intuitionistic and dual intuitionistic reasoning principles, while simultaneously admitting a focusing interpretation for the classical sequent calculus.Then, by applying the Curry–Howard isomorphism to polarized logic, we obtain a single programming language in which evaluation order is reflected at the level of types. Different logical notions correspond directly to natural programming constructs, such as pattern-matching, explicit substitutions, values and call-by-value continuations. We give examples demonstrating the expressiveness of the language and type system, and prove a basic but modular type safety result. We conclude with a brief discussion of extensions to the language with additional effects and types, and sketch the sort of explanation this can provide for operationally sensitive typing phenomena. (shrink)

Modus ponens provides the central theme. There are laws, of the form A→C. A logic L collects such laws. Any datum A provides input to the laws of L. The central ternary relation R relates theories L,T and U, where U consists of all of the outputs C got by applying modus ponens to major premises from L and minor premises from T. Underlying this relation is a modus ponens product operation on theories L and T, whence RLTU iff LTU. (...) These ideas have been expressed, especially with Routley, as worlds semantics for relevant and other substructural logics.Worlds are best demythologized as theories, subject to truth-functional and other constraints. The chief constraint is that theories are taken as closed under logical entailment, which clearly begs the question if we are using the semantics to determine which theory L is Logic itself. Instead we draw the modal logicians’ conclusion—there are many substructural logics, each with its appropriate ternary relational postulates.Each logic L gives rise to a Calculus of L-theories, on which particular candidate logical axioms have the combinatorial properties expected from the well-known Curry–Howard isomorphism . We apply their bubbling lemma, updating the Fools Model of Combinatory Logic at the pure → level for the system BT. We make fusion an explicit connective, proving a combinator correspondence theorem. Having taken relevant → as a left residual for , we explore its right residual mate →r. Finally we concentrate on and prove a finite model property for the classical minimal relevant logic CB, a conservative extension of the minimal positive relevant logic B+. (shrink)

Introduction. Il est bien connu que la correspondance de Curry-Howard permet d'associer un programme, sous la forme d'un λ-terme, à toute preuve intuitionniste, formalisée dans le calcul des prédicats du second ordre. Cette correspondance a été étendue, assez récemment, à la logique classique moyennant une extension convenable du λ-calcul. Chaque théorème formalisé en logique du second ordre correspond donc à une spécification de programme.Il se pose alors le problème, en général tout à fait non trivial, de trouver la (...) spécification associée à un théorème donné; autrement dit, de déterminer le comportement opérationnel commun aux λ-termes associés aux diverses démonstrations formelles du théorème considéré.Cette question est résolue ici pour le théorème de complétude de la logique classique.La première étape consiste à formaliser convenablement ce théorème en logique du second ordre. Ce travail est fait complètement dans la section 1. Il a comme sous-produit, peut-être inattendu, de montrer que ce théorème est prouvable en logique intuitionniste du second ordre. Ceci, toutefois, à condition d'introduire une légère variante de la notion de modèle, en admettant un modèle supplémentaire trivial, où toute formule est satisfaite.On notera, à ce sujet, que des preuves intuitionnistes du théorème de complétude de la logique intuitionniste, utilisant des variantes de la notion de modele de Kripke, ont été données par H. Friedman [7] et W. Veldman [8]. On remarquera également qu'un argument de G. Kreisel [2] montre que le théorème de complétude habituel de la logique intuitionniste n'a pas de preuve intuitionniste. (shrink)

In this paper it is shown how simple texts that can be parsed in a Lambek Categorial Grammar can also automatically be provided with a semantics in the form of a Discourse Representation Structure in the sense of Kamp [1981]. The assignment of meanings to texts uses the Curry-Howard-Van Benthem correspondence.

The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources.This paper introduces a typed functional language Λ! and a categorical model for it.The terms of (...) Λ! encode a version of natural deduction for Intuitionistic Linear Logic such that linear and non linear assumptions are managed multiplicatively and additively, respectively. Correspondingly, the terms of Λ! are built out of two disjoint sets of variables. Moreover, the λ-abstractions of Λ! bind variables and patterns. The use of two different kinds of variables and the patterns allow a very compact definition of the one-step operational semantics of Λ!, unlike all other extensions of Curry-Howard Isomorphism to Intuitionistic Linear Logic. The language Λ! is Church-Rosser and enjoys both Strong Normalizability and Subject Reduction.The categorical model induces operational equivalences like, for example, a set of extensional equivalences.The paper presents also an untyped version of Λ! and a type assignment for it, using formulas of Linear Logic as types. The type assignment inherits from Λ! all the good computational properties and enjoys also the Principal-Type Property. (shrink)

The lambdaPi-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the lambdaPi-calculus and prove the cut-elimination theorem. The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The (...) type-theoretic setting considered here elegantly illustrates the distinction between the processes of normalization in a natural deduction system and cut-elimination in a Gentzen-style sequent calculus. (shrink)

The logical system P-W is an implicational non-commutative intuitionistic logic defined by axiom schemes B = (b → c) → (a → b) → a → c, B' = (a → b) → (b → c) → a → c, I = a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α = β holds if α → β and β → α are both provable in P-W. The answer is (...) affirmative. The first to prove this was E. P. Martin by a semantical method. In this paper, we give the first proof of Martin's theorem based on the theory of simply typed λ-calculus. This proof is obtained as a corollary to the main theorem of this paper, shown without using Martin's Theorem, that any closed hereditary right-maximal linear (HRML) λ-term of type α → α is βη-reducible to λ x.x. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style. (shrink)

In this paper we 1. provide a natural deduction system for full first-order linear logic, 2. introduce Curry-Howard-style terms for this version of linear logic, 3. extend the notion of substitution of Curry-Howard terms for term variables, 4. define the reduction rules for the Curry-Howard terms and 5. outline a proof of the strong normalization for the full system of linear logic using a development of Girard's candidates for reducibility, thereby providing an alternative to (...) Girard's proof using proof-nets. (shrink)

We present a categorical/denotational semantics for the Lambek Syntactic Calculus , indeed for a λlD-typed version Curry-Howard isomorphic to it. The main novelty of our approach is an abstract noncommutative construction with right and left adjoints, called sequential product. It is defined through a hierarchical structure of categories reflecting the implicit permission to sequence expressions and the inductive construction of compound expressions. We claim that Lambek's noncommutative product corresponds to a noncommutative bi-endofunctor into a category, which encloses all (...) categories of such hierarchical structure. A soundness theorem for LSC is shown with respect to this semantical framework. (shrink)

This paper discusses the relation between the minimal positive relevant logic B and intersection and union type theories. There is a marvelous coincidence between these very differently motivated research areas. First, we show a perfect fit between the Intersection Type Discipline ITD and the tweaking BT of B, which saves implication and conjunction but drops disjunction . The filter models of the -calculus (and its intimate partner Combinatory Logic CL) of the first author and her coauthors then become theory models (...) of these calculi. (The logician's "theory" is the algebraist's "filter".) The coincidence extends to a dual interpretation of key particles—the subtype translates to provable , type intersection to conjunction , function space to implication, and whole domain to the (trivially added but trivial) truth T. This satisfying ointment contains a fly. For it is right, proper, and to be expected that type union should correspond to the logical disjunction of B. But the simulation of functional application by a fusion (or modus ponens product) operation on theories leaves the key Bubbling lemma of work on ITD unprovable for the -prime theories now appropriate for the modeling. The focus of the present paper lies in an appeal to Harrop theories which are (a) prime and (b) closed under fusion. A version of the Bubbling lemma is then proved for Harrop theories, which accordingly furnish a model of and CL. (shrink)

Truth in a correspondence sense is objective in two ways. It is objective because the relation of correspondence is objective and because the facts to which truths correspond are objective. Truth about artifacts is problematic because artifacts are intentionally designed to perform certain functions, and so are not entirely mind independent. Against this, it is argued in this paper that truth about artifacts is perfectly objective despite the role played by intention and purpose in the production of artifacts.

Plato's dialogues may be interpreted in a number of ways. One interpretation sees Plato's concept of The Good as a precursor of maximization theory, a modern behavioral theory. Plato identifies goodness with an ideal pattern of people's overt choices under the constraints of everyday life. Correspondingly, maximization theory sees goodness (in terms of "value") as a quantifiable function of overt, constrained choices of an animal. In both conceptions goodness may be increased by expanding the temporal extent over which a behavioral (...) pattern is integrated. (shrink)

The third author gave a natural deduction style proof system called the \-calculus for implicational fragment of classical logic in. In -calculus, 2015, Post-proceedings of the RIMS Workshop “Proof Theory, Computability Theory and Related Issues”, to appear), the fourth author gave a natural subsystem “intuitionistic \-calculus” of the \-calculus, and showed the system corresponds to intuitionistic logic. The proof is given with tree sequent calculus, but is complicated. In this paper, we introduce some reduction rules for the \-calculus, and give (...) a simple and purely syntactical proof to the theorem by use of the reduction. In addition, we show that we can give a computation model with rich expressive power with our system. (shrink)

Discussion at the symposium, and subsequent correspondence with participants, have raised a series of critical questions that seem to me to merit discussion. The issues raised have also led me to consider further some of the literature commenting on Newton’s work and on related matters in the history of optics. What was initially intended as a brief supplement to the foregoing paper [On Metaphysics and Method in Newton, item 10631] has thus evolved into a new article of considerable length.

The reduction of the lambda calculus to the theory of combinators in [Sch¨ onfinkel, 1924] applies to positive implicational logic, i.e. to the typed lambda calculus, where the types are built up from atomic types by means of the operation A −→ B, to show that the lambda operator can be eliminated in favor of combinators K and S of each type A −→ (B −→ A) and (A −→ (B −→ C)) −→ ((A −→ B) −→ (A −→ C)), (...) respectively.1 I will extend that result to the case in which the types are built up by means of the general function type ∀x : A.B(x) as well as the disjoint union type ∃x : A.B(x)– essentially to the theory of [Howard, 1980]. To extend the treatment of −→ to ∀ we shall need a generalized form of the combinators K and S, and to deal with ∃ we will need to introduce a new form of the combinator S.. (shrink)

What is the relation between method and truth? Are we justified in accepting a theory that satisfies the rules of scientific method as true? Such questions divide realism from anti-realism in the philosophy of science. Scientific realists take the methods of science to promote the realist aim of correspondence truth. Anti-realists either claim that the methods of science promote lesser epistemic goals than realist truth, or else they reject the realist conception of truth altogether. In this paper, I propose (...) a realist theory of the relation between method and truth. The theory consists of three basic elements: (a) a naturalistic treatment of epistemic normativity, (b) an instrumentalist conception of the nature of methodological rules, and (c) an abductive argument for the truth-conduciveness of the rules of scientific method. (shrink)

Hegel indicates toward the end of his Phenomenology of Spirit that there would be a parallelism in the categories of his later system to the various configurations of consciousness in the Phenomenology. Some general correspondences have been indicated by Otto Pöggeler and suggested by Robert Grant McRae, but I argue in this paper that there are at least four important and more specific parallels, bringing out simultaneously a similarity of content and a difference of approach and methodology in the two (...) works: 1) in the philosophical construal of “categories”; 2) in the conceptualization of a “phenomenology”; 3) in the analysis of the dialectical relationship of religion and art; and 4) in the relationship of the history of philosophy to the Absolute. (shrink)

Hegel indicates toward the end of his Phenomenology of Spirit that there would be a parallelism in the categories of his later system to the various configurations of consciousness in the Phenomenology. Some general correspondences have been indicated by Otto Pöggeler and suggested by Robert Grant McRae, but I argue in this paper that there are at least four important and more specific parallels, bringing out simultaneously a similarity of content and a difference of approach and methodology in the two (...) works: 1) in the philosophical construal of “categories”; 2) in the conceptualization of a “phenomenology”; 3) in the analysis of the dialectical relationship of religion and art; and 4) in the relationship of the history of philosophy to the Absolute. (shrink)

The essence of a mental event such as self-deception lies in its function – its place in the life of an animal. But the function of self-deception corresponds to that of interpersonal deception. Therefore self-deception, contrary to Mele's thesis, is essentially isomorphic with interpersonal deception.

Gray's account is remarkable in its depth and scope but too little attention is paid to poor correspondences with the literature on hippocampal/subicular damage, the theta rhythm, and novelty detection. An alternative account, focusing on hippocampal involvement in organizing memories in a way that makes them accessible to conscious recollection but not in access to consciousness per se, avoids each of these limitations.