The question of finding a suitable formal account of meaning for the logical signs has troubled many philosophers and logicians since the early days of formal logic, whenever it is even recognised as a problem. Here I attempt to show how two operational approaches to the problem can still be shown to be ‘technically’ equivalent, despite having emerged from two different readings of a single philosophical account, and being essentially distinct with respect to the rôle of ‘will’ in the mathematical (...) activity: on the one hand, the ‘semantics of use’, my own reformulation of P. Martin‐Löf's Intuitionistic Type Theory canonical‐values based semantics by taking the normalisation rules as the key semantical device; and, on the other hand, J. Hintikka's Game‐Theoretical Semantics, where the meaning of logical signs is given via semantical games. The philosophical account from which both emerge is precisely Wittgenstein's later account of propositions, where the notion of ‘language‐games’ is introduced as a key semantical device. Observing that the normalisation rules seem to be able to formalise the explanation of the consequences one can draw from a proposition,3 thus showing the function/purpose/usefulness of its main connective in the calculus of language, it seems reasonable to advocate that such a meta‐mathematical device can be a semantically useful notion which would lead to a more reasonable account of the problem of formulating the meaning of logical constants. (shrink)

Utilizando el argumento de la novela Bouvard y Pécuchetde Flaubert, como posible refutación del Mundo 3 de Popper, analizamos algunas de las principales consecuencias que para la filosofía de la mente, así como para la ciencia y el conocimiento, tiene el pensamiento popperiano sobre el llamado mundo del conocimiento objetivo.

The purpose of this paper is studying the importance of the antithetical pair sympathy-antipathy, as an interpretive instrument of the human phýsis in the Hippocratic medical epistemology. His study aims to be a contribution to the understanding of the methods of inference developed by ancient medicine, in parallel to the demonstrative method.

Este artículo pretende establecer la importancia del Proyecto de una psicología para neurólogos en el conjunto de la obra de Freud, señalando aquellos puntos en los que anticipa la teoría que, unos años más tarde, revolucionará el pensamiento humano, es decir, aquella que define el campo del psicoanálisis y que tiene a los conceptos de aparato psíquico y de inconsciente como ejes centrales.

One takes advantage of some basic properties of every homotopic \(\lambda\)-model (e.g. extensional Kan complex) to explore the higher \(\beta\eta\)-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher \(\lambda\)-terms, whose equality rules would be contained in the theory of any \(\lambda\)-homotopic model.

The intention here is that of giving a formal underpinning to the idea of 'meaning-is-use' which, even if based on proofs, it is rather different from proof-theoretic semantics as in the Dummett-Prawitz tradition. Instead, it is based on the idea that the meaning of logical constants are given by the explanation of immediate consequences, which in formalistic terms means the effect of elimination rules on the result of introduction rules, i. e. the so-called reduction rules. For that we suggest an (...) extension to the Curry-Howard interpretation which draws on the idea of labelled deduction, and brings back Frege's device of variable-abstraction to operate on the labels (i. e., proof-terms) alongside formulas of predicate logic. (shrink)

The clinical empiricism of Thomas Sydenham (1624–1689) and his definition of especie morbosae represented a substantial turn in the medicine of his time. This turn supposed the shift towards an ontological conception of diseases, from a qualitative to quantitative interpretation. Sydenham’s clinical proposal had a great influence on empiricism philosophical thinking, particularly in John Locke and his delimitation of knowledge. The dialogue between medicine and philosophy, set out by Sydenham-Locke, reactivates the problem of the clinical and theoretical foundations of medical (...) thought, as well as the limits of scientific knowledge. Similar to problem exposed in the Hippocratic treatise On ancient medicine, seventeenth-century medicine seeks its epistemological foundations and the solution to its difficulties in clinical experience, probability and analogy. The aim of this work is to show the Sydenham’s contribution to one of the great controversies between medicine and philosophy. (shrink)

The conception of contagious disease that Girolamo Fracastoro provides in his work De contagione et contagiosis morbis, marks the origin of modern epidemiology and microbiology. This conception puts into play the Galenic and Aristotelian traditions of research, faced with its own conceptual limitations of the growing mechanistic thought of the time. According to Fracastoro, epidemic diseases spread by invisible living germs called seminaria, begotten by corrupted humours. Fracastoro resorted to the old notions of "sympathy" and "antipathy" to respond to questions (...) about how seminaria is transmitted from one body to another, and what is the specificity that limits its transmission to certain species and organs. Like Galileo and Descartes, Fracastoro tries to establish a dialogue in the field of medicine between the Aristotelian vitalism and the modern mechanistic perspective. The purpose of this paper is to highlight the ideological, theoretical and conceptual assumptions, both philosophical and scientific, assumed by Fracastoro with regard to the problem of contagion. (shrink)

Dividing chains have been used as conditions to isolate adequate subclasses of simple theories. In the first part of this paper we present an introduction to the area. We give an overview on fundamental notions and present proofs of some of the basic and well-known facts related to dividing chains in simple theories. In the second part we discuss various characterizations of the subclass of low theories. Our main theorem generalizes and slightly extends a well-known fact about the connection between (...) dividing chains and Morley sequences (in our case: independent sequences). Moreover, we are able to give a proof that is shorter than the original one. This result motivates us to introduce a special property of formulas concerning independent dividing chains: For any dividing chain there exists an independent dividing chain of the same length. We study this property in the context of low, short and ω -categorical simple theories, outline some examples and define subclasses of low and short theories, which imply this property. The results give rise to further studies of the relationships between some subclasses of simple theories. (shrink)

SummaryLooking at proof theory as an attempt to ‘code’ the general pattern of the logical steps of a mathematical proof, the question of what kind of rules can make the meaning of a logical connective completely explicit does not seem to have been answered satisfactorily. The lambda calculus seems to have been more coherent simply because the use of ‘λ’ together with its projection 'apply' is specified by what can be called a 'reduction' rule: β‐conversion. We attempt to analyse the (...) role of proof rules, making use of a set of formal rules designed to capture both the notions of proof theory and those of the lambda‐calculus: Martin‐Löf's Intuitionistic Type Theory.RésuméSi on considère la théorie de la démonstration comme une tentative de ‘codifier’ les pas logiques d'une démonstration mathématique, on se rendra compte qu'on n'a pas répondu de façon satisfaisante à la question suivante: quelles sont les règies qui rendent complètement explicite le sens d'un connecteur logique? Le lambda‐calcul a été apparemment plus cohérent, tout simplement parce que l'utilisation du‘λ’ avec sa projection 'apply' est spécifiée par une regie de 'réduction': β‐conversion. Nous essayons d'analyser le rôle des règies de démonstration, en utilisant un système formel de règies conçu pour englober à la fois les notions de la théorie de la démonstration et celles du lambda‐calcul: la Théorie Intuitionniste des Types de Martin‐Löf.ZusammenfassungWenn man Beweistheorie als einen Versuch, ein allgemeines Muster der logischen Schritte in einem mathematischen Beweis zu kodifizieren, betrachtet, so scheint die Frage nach der Art von Regeln , die die Bedeutung von logischen Operatoren vollständig beschreiben, nicht zufriedenstellend beantwortet. Der Lambda‐Kalkül erscheint, kohärenter, einfach deshalb weil der Gebrauch von ‘λ’ zusammen mit dessen Projektion 'apply' durch Regeln bestimmt wird, die man 'Reduktions'‐Regeln nennen kann: β‐Konversion. Wir versuchen, die Rolle von Beweisregeln zu analysieren, indem wir ein Regelsystem verwenden, das sowohl die Begriffe der Beweistheorie als auch diejenigen des Lambda‐Kalküls erfasst, nämlich die Martin‐Löfsche Typentheorie. (shrink)

The intention here is that of giving a formal underpinning to the idea of ‘meaning-is-use’ which, even if based on proofs, it is rather different from proof-theoretic semantics as in the Dummett–Prawitz tradition. Instead, it is based on the idea that the meaning of logical constants are given by the explanation of immediate consequences, which in formalistic terms means the effect of elimination rules on the result of introduction rules, i.e. the so-called reduction rules. For that we suggest an extension (...) to the Curry– Howard interpretation which draws on the idea of labelled deduction, and brings back Frege’s device of variable-abstraction to operate on the labels (i.e., proof-terms) alongside formulas of predicate logic. (shrink)

The lambda calculus is a universal programming language. It can represent the computable functions, and such offers a formal counterpart to the point of view of functions as rules. Terms represent functions and this allows for the application of a term/function to any other term/function, including itself. The calculus can be seen as a formal theory with certain pre-established axioms and inference rules, which can be interpreted by models. Dana Scott proposed the first non-trivial model of the extensional lambda calculus, (...) known as $ D_{\infty }$, to represent the $\lambda $-terms as the typical functions of set theory, where it is not allowed to apply a function to itself. Here we propose a construction of an $\infty $-groupoid from any lambda model endowed with a topology. We apply this construction for the particular case $D_{\infty }$, and we see that the Scott topology does not provide enough information about the relationship between higher homotopies. This motivates a new line of research focused on the exploration of $\lambda $-models with the structure of a non-trivial $\infty $-groupoid to generalize the proofs of term conversion to higher-proofs in $\lambda $-calculus. (shrink)

As a celebration of theTractatus100th anniversary it might be worth revisiting its relation to the later writings. From the former to the latter, David Pears recalls that “everyone is aware of the holistic character of Wittgenstein’s later philosophy, but it is not so well known that it was already beginning to establish itself in theTractatus” (The False Prison, 1987). From the latter to the former, Stephen Hilmy’s (The Later Wittgenstein, 1987) extensive study of theNachlasshas helped removing classical misconceptions such as (...) Hintikka’s claim that “Wittgenstein in thePhilosophical Investigationsalmost completely gave up the calculus analogy.” Hilmy points out that even in theInvestigationsone finds the use of the calculus/game paradigm to the understanding of language, such as “in operating with the word” (Part I, §559) and “it plays a different part in the calculus”. Hilmy also quotes from a late (1946) unpublished manuscript (MS 130) “this sentence has use in the calculus of language”, which seems to be compatible with “asking whether and how a proposition can be verified is only a particular way of asking ‘How do you mean?’” Central in this back and forth there is an aspect which seems to deserve attention in the discussion of a semantics for the language of mathematics which might be based on (normalisation of) proofs and/or Hintikka/Lorenzen game-dialogue: the explication of consequences. Such a discussion is substantially supported by the use of the open and searchableThe Wittgenstein Archives at the University of Bergen. These findings are framed within the discussion of the meaning of logical constants in the context of natural deduction style rules of inference. (shrink)

An appropriate framework is put forward for the construction of $$\lambda $$ -models with $$\infty $$ -groupoid structure, which we call homotopic $$\lambda $$ -models, through the use of an $$\infty $$ -category with cartesian closure and enough points. With this, we establish the start of a project of generalization of Domain Theory and $$\lambda $$ -calculus, in the sense that the concept of proof (path) of equality of $$\lambda $$ -terms is raised to higher proof (homotopy).