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)

The aim of this paper is to look from the point of view of admissibility of inference rules at intermediate logics having the finite model property which extend Heyting's intuitionistic propositional logic H. A semantic description for logics with the finite model property preserving all admissible inference rules for H is given. It is shown that there are continuously many logics of this kind. Three special tabular intermediate logics λ, 1 ≥ i ≥ 3, are given which describe all (...) tabular logics preserving admissibility: a tabular logic λ preserves all admissible rules for H iff 7λ has width not more than 2 and is not included in each λ. MSC: 03B55, 03B20. (shrink)

ZusammenfassungDie Arbeit enthält Bemerkungen über den Intuitionismus and über seine Beziehungen zu anderen Gebieten der Grundlagenforschung. Innerhalb der intuitionistischen Mathematik werden, im Anschluss an die Kritik von Griss gegen den Gebrauch der Negation, Evidenzstufen unterschieden, abhängend von der Art, in der bedingte Konstruktionen zugelassen werden. Auch werden gewisse Schwierigkeiten in der Theorie der endlichen Spezies diskutiert. Was die Grundlagenforschung im Aligemeinen betrifft, wird bemerkt, dass sie die klassische Mathematik weitgehend in ihre intuitiven, formalen and platonischen Bestandteile zerlegt hat. Es wird (...) näher eingegangen auf die These von Church in der Theorie der rekursiven Funktionen.RésuméL'article contient des remarques sur l'intuitionisme et sur ses rapports avec les autres directions dans la recherche des fondements. Dans la mathématique intuitioniste, et en connexion avec la critique de Griss contre l'usage de la négation, on distingue des degrés d'évidence, dépendant de l'espèce de constructions conditionnées qui est admise. En outre, on discute certaines difficultés dans la théorie des espèces finies. Concernant la recherche des fondements en général, on remarque que les mathématiques classiques ont été scindées en leurs éléments intuitifs, formels et platonistes. Quelques remarques sur la thèse de Church dans la théorie des fonctions récursives terminent l'article.The paper contains remarks on intuitionism and its relations with other domains of foundational research. Inside the intuitionistic mathematics, in connection with Griss' criticism against the use of negation, different degrees of evidence are distinguished, depending upon the way in which conditioned constructions are admitted. Some difficulties in the theory of finite species are discussed. Concerning the foundational research in general it is observed that it has separated intuitive, formal and platonistic constituents in classical mathematics. Some remarks are made on Church's thesis in the theory of recursive functions. (shrink)

In reaction to Doret De Ruyter's recent defence of the importance of ideals in education, I advocate cautiousness in three respects. First, I explain the importance of distinguishing ideals more sharply from goals by demonstrating the problems of considering ideals even approximately realisable. Second, I substantiate my doubts about their indispensability in human motivation, and question the desirability of encouraging the motivational use of ideals. Third, I question whether ideals could or should be ‘passed on’ in education, drawing attention to (...) their non-objective, personally created nature. (shrink)

This is the Spanish translation, by María Gabriela Fulugonio, of Arend Heyting’s classical text “Die logizistische Grundlegung der Mathematik”, which was originally presented at the Königsberg’s Symposium on Philosophy of Mathematics in 1930, and finally published in Erkenntnis in 1931.

Differential academic language proficiency is an issue of major educational concern, bearing on problems varying from pupil performance, to social prospects, and citizenship. In this paper we develop a conception of the language-acquiring subject, and we discuss the consequences for understanding differential language proficiency in schools. Starting from Wittgenstein's meaning-as-use theory we show that learning a language requires an activity that relates the subject both to the community of language users, and to the things language is about. In opposition to (...) Luntley, we contend that this does not mean that linguistic development involves linguistic adjustment to the world 'as it is'. It is argued that, in as far as linguistic development involves a process of adjustment, this concerns conceptions about the world as it is presupposed to be—a 'world' that is subjected to doubt and revision time and again. With respect to dealing with differential academic language proficiency, this approach to linguistic development suggests bringing pupils into situations which require active participation in processes of 'negotiating meaning', including negotiating the prevailing presuppositions about what the world is like. This also puts novices in a different position—less assimilatory—recognising their co-constructive potencies at a more fundamental level. (shrink)

Differential academic language proficiency is an issue of major educational concern, bearing on problems varying from pupil performance, to social prospects, and citizenship. In this paper we develop a conception of the language‐acquiring subject, and we discuss the consequences for understanding differential language proficiency in schools. Starting from Wittgenstein's meaning‐as‐use theory we show that learning a language requires an activity that relates the subject both to the community of language users, and to the things language is about. In opposition to (...) Luntley, we contend that this does not mean that linguistic development involves linguistic adjustment to the world ‘as it is’. It is argued that, in as far as linguistic development involves a process of adjustment, this concerns conceptions about the world as it is presupposed to be—a ‘world’ that is subjected to doubt and revision time and again. With respect to dealing with differential academic language proficiency, this approach to linguistic development suggests bringing pupils into situations which require active participation in processes of ‘negotiating meaning’, including negotiating the prevailing presuppositions about what the world is like. This also puts novices in a different position—less assimilatory—recognising their co‐constructive potencies at a more fundamental level. (shrink)

Writings by a thinker—a psychiatrist, a philosopher, a cybernetician, and a poet—whose ideas about mind and brain were far ahead of his time. Warren S. McCulloch was an original thinker, in many respects far ahead of his time. McCulloch, who was a psychiatrist, a philosopher, a teacher, a mathematician, and a poet, termed his work “experimental epistemology.” He said, “There is one answer, only one, toward which I've groped for thirty years: to find out how brains work.” Embodiments of Mind, (...) first published more than fifty years ago, teems with intriguing concepts about the mind/brain that are highly relevant to recent developments in neuroscience and neural networks. It includes two classic papers coauthored with Walter Pitts, one of which applies Boolean algebra to neurons considered as gates, and the other of which shows the kind of nervous circuitry that could be used in perceiving universals. These first models are part of the basis of artificial intelligence. Chapters range from “What Is a Number, that a Man May Know It, and a Man, that He May Know a Number,” and “Why the Mind Is in the Head,” to “What the Frog's Eye Tells the Frog's Brain” (with Jerome Lettvin, Humberto Maturana, and Walter Pitts), “Machines that Think and Want,” and “A Logical Calculus of the Ideas Immanent in Nervous Activity” (with Walter Pitts). Embodiments of Mind concludes with a selection of McCulloch's poems and sonnets. This reissued edition offers a new foreword and a biographical essay by McCulloch's one-time research assistant, the neuroscientist and computer scientist Michael Arbib. (shrink)

Because of the “all-or-none” character of nervous activity, neural events and the relations among them can be treated by means of propositional logic. It is found that the behavior of every net can be described in these terms, with the addition of more complicated logical means for nets containing circles; and that for any logical expression satisfying certain conditions, one can find a net behaving in the fashion it describes. It is shown that many particular choices among possible neurophysiological assumptions (...) are equivalent, in the sense that for every net behaving under one assumption, there exists another net which behaves under the other and gives the same results, although perhaps not in the same time. Various applications of the calculus are discussed. (shrink)

In this paper we shall prove that certain subvarieties of the variety of Salgebras (Heyting algebras with successor) has amalgamation. This result together with an appropriate version of Theorem 1 of [L. L. Maksimova, Craig’s theorem in superintuitionistic logics and amalgamable varieties of pseudo-boolean algebras, Algebra i Logika, 16(6):643-681, 1977] allows us to show interpolation in the calculus IPC S (n), associated with these varieties.We use that every algebra in any of the varieties of S-algebras studied in this work (...) has a canonical extension, to show completeness of the calculus IPC S (n) with respect to appropriate Kripke models. (shrink)

This paper is an historical study of Tarski's methodology of deductive sciences (in which a logic S is identified with an operator Cn S, called the consequence operator, on a given set of expressions), from its appearance in 1930 to the end of the 1970s, focusing on the work done in the field by Roberto Magari, Piero Mangani and by some of their pupils between 1965 and 1974, and comparing it with the results achieved by Tarski and the Polish school (...) (Łoś, Suszko, Słupecki, Pogorzelski, Wójcicki). In the last section of the paper we will then compare these works with some recent developments in algebraic logic: this will lead to a better understanding of the results of the methodology of deductive science, but at the same time will show some intrinsic limits to such an approach to logic. Even if Magari's work on diagonizable algebras and universal algebra and Mangani's axiomatization of MV-algebras and results in model theory are rather famous, the articles on closure operators, published in the 1960s, are almost totally unknown outside Italy (mainly because of a linguistic limitation, the papers we analyse having been written and published in Italian). This paper aims to fill the gap in the literature and to enable the international community to get acquainted with this part of Italian logic. The same applies to some works published in Barcelona (in Catalan) at the end of the 1970s, analysed in the last section. (shrink)

There is a simple technique, due to Dragalin, for proving strong cut-elimination for intuitionistic sequent calculus, but the technique is constrained to certain choices of reduction rules, preventing equally natural alternatives. We consider such a natural, alternative set of reduction rules and show that the classical technique is inapplicable. Instead we develop another approach combining two of our favorite tools—Klop’s ι-translation and perpetual reductions. These tools are of independent interest and have proved useful in a variety of settings; it (...) is therefore natural to investigate, as we do here, what they have to offer the field of sequent calculus. (shrink)

Interest has been recently devoted to historical and philosophical aspects about fractional calculus and its adoption as additional mathematical tool in different physics areas as well as in other scientific applications. However, potential application of FC towards relativity is still lacking. In relativity theory, Lorentz transformation of time and position coordinates plays a major role while the corresponding outcomes still defy our ‘common sense’. As some problems in physics can be solved by following different mathematical routes leading to the (...) same result, the present paper suggests an alternative method to relativity. Instead of converting time and position data from different inertial reference frames through Lorentz transformation, it is here envisaged to numerically adjust relativistic results with the help of FC. Bearing in mind well established postulates from relativity, we intend to fill up this gap by addressing and discussing the main arguments in favour of the prospective use of FC as emergent and alternative tool applied to relativity. (shrink)

How do we measure happiness? Focusing on subjective measures as a proxy for welfare and well-being, this book finds ways to do that. Subjective measures have been used by psychologists, sociologists, political scientists, and, more recently, economists to answer a variety of scientifically and politically relevant questions. Van Praag, a pioneer in this field since 1971, and Ferrer-i-Carbonell present in this book a generally applicable methodology for the analysis of subjective satisfaction. Drawing on a range of surveys on people's satisfaction (...) with their jobs, income, housing, marriages, and government policy, among other areas of life, this book shows how satisfaction with life "as a whole" is an aggregate of these domain satisfactions. Using German, British, Dutch, and Russian data, the authors cover a wide range of topics. This groundbreaking book presents a new and fruitful methodology that constitutes a welcome addition to the social sciences. The paperback edition has been revised to bring the literature review up-to-date and the chapter on poverty has been revised and extended to take account of new research. (shrink)

Emergence of the requirement of justice -- Justice's major platforms -- Justice within human rights -- Judges' balancing exercise -- The calculus of social harmonization -- Equilibrating the forces of attraction and repulsion -- Principles of justice and the reasons for their mixing -- Metrics and dialectics for a reflective equilibrium -- Social institutions as equilibrium setting tools.

We consider language models for the Lambek calculus that allow empty antecedents and enrich them with constants for the empty language and for the language containing only the empty word. No complete calculi are known with respect to these semantics, and in this paper we consider several trivalent systems that arise as fragments of these models? logics.

This paper contributes to the generalization of lattice-valued models of set theory to non-classical contexts. First, we show that there are infinitely many complete bounded distributive lattices, which are neither Boolean nor Heyting algebra, but are able to validate the negation-free fragment of \. Then, we build lattice-valued models of full \, whose internal logic is weaker than intuitionistic logic. We conclude by using these models to give an independence proof of the Foundation axiom from \.

The aim of this paper is to distinguish between, and examine, three issues surrounding Humphreys's paradox and interpretation of conditional propensities. The first issue involves the controversy over the interpretation of inverse conditional propensities — conditional propensities in which the conditioned event occurs before the conditioning event. The second issue is the consistency of the dispositional nature of the propensity interpretation and the inversion theorems of the probability calculus, where an inversion theorem is any theorem of probability that makes (...) explicit (or implicit) appeal to a conditional probability and its corresponding inverse conditional probability. The third issue concerns the relationship between the notion of stochastic independence which is supported by the propensity interpretation, and various notions of causal independence. In examining each of these issues, it is argued that the dispositional character of the propensity interpretation provides a consistent and useful interpretation of the probability calculus. (shrink)

A connection between Aristotle's syllogistic and the calculus of relations is investigated. Aristotle's and Gergonne's syllogistics are considered as some algebraic structures. It is proved that Gergonne's syllogistic is isomorphic to closed elements algebra of a proper approximation relation algebra. This isomorphism permits to evaluate Gergonne's syllogisms and also Aristotle's syllogisms, laws of conversion and relations in the "square of oppositions" by means of regular computations with Boolean matrices.

A sequent calculus methodology for systems of agency based on branching-time frames with agents and choices is proposed, starting with a complete and cut-free system for multi-agent deliberative STIT; the methodology allows a transparent justification of the rules, good structural properties, analyticity, direct completeness and decidability proofs.

The present paper studies formal properties of so-called modal information logics (MILs)—modal logics first proposed in (van Benthem 1996 ) as a way of using possible-worlds semantics to model a theory of information. They do so by extending the language of propositional logic with a binary modality defined in terms of being the supremum of two states. First proposed in 1996, MILs have been around for some time, yet not much is known: (van Benthem 2017, 2019 ) pose two central (...) open problems, namely (1) axiomatizing the two basic MILs of suprema on preorders and posets, respectively, and (2) proving (un)decidability. The main results of the first part of this paper are solving these two problems: (1) by providing an axiomatization [with a completeness proof entailing the two logics to be the same], and (2) by proving decidability. In the proof of the latter, an emphasis is put on the method applied as a heuristic for proving decidability ‘via completeness’ for semantically introduced logics; the logics lack the FMP w.r.t. their classes of definition, but not w.r.t. a generalized class. These results are build upon to axiomatize and prove decidable the MILs attained by endowing the language with an ‘informational implication’—in doing so a link is also made to the work of (Buszkowski 2021 ) on the Lambek Calculus. (shrink)

Global properties of canonical derivability predicates in Peano Arithmetic) are studied here by means of a suitable propositional modal logic GL. A whole book [1] has appeared on GL and we refer to it for more information and a bibliography on GL. Here we propose a sequent calculus for GL and, by exhibiting a good proof procedure, prove that such calculus admits the elimination of cuts. Most of standard results on GL are then easy consequences: completeness, decidability, finite (...) model property, interpolation and the fixed point theorem. (shrink)

Intuitionistic logic is presented here as part of familiar classical logic which allows mechanical extraction of programs from proofs. to make the material more accessible, basic techniques are presented first for propositional logic; Part II contains extensions to predicate logic. This material provides an introduction and a safe background for reading research literature in logic and computer science as well as advanced monographs. Readers are assumed to be familiar with basic notions of first order logic. One device for making this (...) book short was inventing new proofs of several theorems. The presentation is based on natural deduction. The topics include programming interpretation of intuitionistic logic by simply typed lambda-calculus (Curry-Howard isomorphism), negative translation of classical into intuitionistic logic, normalization of natural deductions, applications to category theory, Kripke models, algebraic and topological semantics, proof-search methods, interpolation theorem. The text developed from materal for several courses taught at Stanford University in 1992-1999. (shrink)

There is a simple technique, due to Dragalin, for proving strong cut-elimination for intuitionistic sequent calculus, but the technique is constrained to certain choices of reduction rules, preventing equally natural alternatives. We consider such a natural, alternative set of reduction rules and show that the classical technique is inapplicable. Instead we develop another approach combining two of our favorite tools—Klop's l-translation and perpetual reductions. These tools are of independent interest and have proved useful in a variety of settings; it (...) is therefore natural to investigate, as we do here, what they have to offer the field of sequent calculus. (shrink)

How do we measure happiness? Focusing on subjective measures as a proxy for welfare and well-being, this book finds ways to do that. Subjective measures have been used by psychologists, sociologists, political scientists, and, more recently, economists to answer a variety of scientifically and politically relevant questions. Van Praag, a pioneer in this field since 1971, and Ferrer-i-Carbonell present in this book a generally applicable methodology for the analysis of subjective satisfaction. Drawing on a range of surveys on people's satisfaction (...) with their jobs, income, housing, marriages, and government policy, among other areas of life, this book shows how satisfaction with life "as a whole" is an aggregate of these domain satisfactions. Using German, British, Dutch, and Russian data, the authors cover a wide range of topics, even some not usually considered part of economic study.The book makes a distinction between actual satisfaction levels and individual norms, and in this way complements Van Praag's earlier work within the Leyden School with his later work in "happiness research". Among the many topics covered, the authors discuss: individuals' memory and anticipation processes and the estimation of adaptation phenomena ; the effect of reference groups on income norms and satisfaction with income; the importance of climate for well-being, including the development of a climate-equivalence index; the trade-offs between chronic diseases and income when well-being is kept constant; the damage of aircraft noise on well-being; the construction of a new talent tax tariff; and inequality from a satisfaction perspective, including the definition of "satisfaction inequalities", a natural extension of income inequality and poverty.This groundbreaking book presents new and fruitful methodology that consitutes a welcome addition to the social sciences. (shrink)

Drawing upon rational choice and investor attention theories, we examine how accusations of corporate bribery and subsequent investigations shape market reactions. Using event study methodology to measure loss in firm value for public firms facing bribery investigations from 1978 to 2010, we found that total market penalties amounted to $60.61 billion. We ran moderated multiple regression analysis to examine further the degree to which the unique characteristics of bribery explain variations in market penalties. Companies committing bribery in less corrupt host (...) countries and with the involvement of compromised executives experienced greater market penalties than did other companies. After partitioning share value losses into components for regulatory penalties, class action settlements, and loss to reputation, we found that reputational penalties account for 81.8¢ of every dollar of share value loss. Omission of reputational penalties in rational choice calculus underestimates bribery costs by 4.5 times. The results suggest that firms should not underestimate the importance of market-imposed reputational penalties by merely considering regulator-imposed fines and sanctions. (shrink)

Taking Isaac Newton at his own word, historians have long agreed that the decade of the 1660s, when Newton was a young man in his twenties, was the critical period in his scientific career. In the years 1665 and 1666, he has told us, he hit on the ideas of cosmic gravitation, the composition of white light, and the fluxional calculus. The elaboration of these basic ideas constituted his scientific achievement. Nevertheless, the decade of the 1660s has remained a (...) virtual blank in our knowledge of Newton. It need not remain so always. His papers contain a wealth of manuscripts from his undergraduate years and the period immediately following. The first volume of his mathematical papers, which will soon be published, will demonstrate how extensive the information on his early mathematical development is. The development of his non-mathematical studies, especially of what I shall call his scientific studies to distinguish them from the mathematical, can be followed as well—in his reading notes, in his notebooks, above all in the passage in his philosophical notebook labelled Quaestiones quaedam Philosophicae. In this passage we see emerging into consciousness for the first time the questions on which Newton's philosophy of nature was built. (shrink)

We introduce a complete and cut-free proof system for a sufficiently expressive fragment of Metric Temporal Logic over dense time domains in which a schema of induction is provable. So doing we extend results previously obtained by Montagna et al. to unbounded temporal operators.