PREFACEProf. Göran Sundholm of Leiden University inspired the group of Logic at Lille and Valparaíso to start a fundamental review of the dialogical conception of logic by linking it to constructive type logic. One of Sundholm's insights was that inference can be seen as involving an implicit interlocutor. This led to several investigations aimed at exploring the consequences of joining winning strategies to the proof-theoretical conception of meaning. The leading idea is, roughly, that while introduction rules lay down the conditions (...) under which a winning strategy for the Proponent may be built, the elimination rules lay down those elements of the Opponent's assertions that the Proponent has the right to use for building winning strategy. It is the pragmatic and ethical features of obligations and rights that naturally lead to the dialogical interpretation of natural deduction.During the Visiting Professorship of Prof. Sundholm at Lille in (2012) the group of Lille started delving into the ways of implementing Per Martin-Löf's Constructive Type Theory with the dialogical perspective. In particular, Aarne Ranta's (1988) paper, the first publication on the subject, was read and discussed during Sundholm’s seminar. The discussions strongly suggested that the game-theoretical conception of quantifiers as deploying interdependent moves provide a natural link between CTT and dialogical logic. This idea triggered several publications by the group of Lille in collaboration with Nicolas Clerbout and Juan Redmond at the University of Valparaíso, including the publication of the book (2015) by Clerbout / Rahman that provides a systematic development of this way of linking CTT and the dialogical conception of logic. However the Clerbout / Rahman book was written from the CTT perspective on dialogical logic, rather than the other way round. The present book should provide the perspective from the other side of the dialogue between the Dialogical Framework and Constructive Type Theory. The main idea of our present study is that Sundholm's (1997) notion of epistemic assumption is closely linked to the Copy-Cat Rule or Socratic Rule that distinguishes the dialogical framework from other game-theoretical approaches. One way to read the present book is as a further development of Sundholm’s extension of Austin's (1946, p. 171) remark on acts of assertion to inference. Indeed, Sundholm (2013, p. 17) gave the following forceful formulation: When I say therefore, I give others my authority for asserting the conclusion, given theirs for asserting the premisses.Per Martin-Löf, in recent lectures, have utilized the dialogical perspective on epistemic assumptions to get out of a certain circle that threatens the explanation of the notions of inference and demonstration. A demonstration may be explained as a chain of (immediate) inferences starting from no premisses. That an inference J1... Jn—————Jis valid means that the conclusion J can be made evident on the assumption that J1, …, Jn are known. The notion of epistemic assumption thus enters in the explanation of valid inference. We cannot, however, in this explanation understand 'known' in the sense of demonstrated, for then we are explaining the notion of inference in terms of demonstration, whereas demonstration has been explained in terms of inference. Martin-Löf suggests that we here understand 'known' in the sense of asserted, so that epistemic assumptions are judgements others have made, judgements for which others have taken the responsibility; that the inference is valid then means that, given that others have taken responsbility for the premisses, I can take responsibility for the conclusion:The circularity problem is this: if you define a demonstration to be a chain of immediate inferences, then you are defining demonstration in terms of inference. Now we are considering an immediate inference and we are trying to give a proper explanation of that; but, if that begins by saying: Assume that J1, …, Jn have been demonstrated – then you are clearly in trouble, because you are about to explain demonstration in terms of the notion of immediate inference, hence when you are giving an account of the notion of immediate inference, the notion of demonstration is not yet at your disposal. So, to say: Assume that J1, …, Jn have already been demonstrated, makes you accusable of trying to explain things in a circle. The solution to this circularity problem, it seems to me now, comes naturally out of this dialogical analysis. […]The solution is that the premisses here should not be assumed to be known in the qualified sense, that is, to be demonstrated, but we should simply assume that they have been asserted, which is to say that others have taken responsibility for them, and then the question for me is whether I can take responsibility for the conclusion. So, the assumption is merely that they have been asserted, not that they have been demonstrated. That seems to me to be the appropriate definition of epistemic assumption in Sundholm's sense. One of the main tenets of the present study is that the further move of relating the Socratic Rule rule with judgemental equality provides both a simpler and more direct way to implement the constructive type theoretical approach within the dialogical framework. Such a reconsideration of the Socratic Rule, roughly speaking, amounts to the following. 1.A move from P that brings-forward a play-object in order to defend an elementary proposition A can be challenged by O. 2.The answer to such a challenge, involves P bringing forward a definitional equality that expresses the fact that the play-object chosen by P copies the one O has chosen while positing A. For short, the equality expresses at the object-languaje level that the defence of P relies on the authority given to O to be able to produce the play-objects she brings forward. More generally, according to this view, a definitional equality established by P and brought forward while defending the proposition A, expresses the equality between a play-object (introduced by O) and the instruction for building a play-object deployed by O while affirming A. So it can be read as a computation rule that indicates how to compute O's instructions. Let us recall that from the strategic point of view, O's moves correspond to elimination rules of demonstrations. Thus, the dialogical rules that prescribe how to introduce a definitional equality – correspond – at the strategic level – to the definitional equality rules for CTT as applied to the selector-functions involved in the elimination rules. So, what we are doing here is extending the dialogical interpretation of Sundholm's epistemic assumption to the rules that set up the definitional equality of a type.The present work is structured in the following way:•In the Introduction we state the main tenets that guide our book•Chapter II contains a brief overview of Constructive Type Theory penned by Ansten Klev with exercises and their solutions. •Chapter III offers a novel presentation of the dialogical conception of logic. In fact, the first two sections of the chapter provide an overview of standard dialogical logic – including solved exercises, slightly adapted to the content of the present volume. The rest of the sections develop a new dialogical approach to Constructive Type Theory. •Chapters IV and V contain the main body of our study, namely the relation between the Socratic Rule, epistemic assumptions, and equality. The chapter provides the reader with thoroughly worked out examples with comments. •After the Final Remarks the book containsa.An appendix containing a an overview of all the rules for the new formulation of dialogical approach to constructive type theory developed in the book; b.a brief outline of Per Martin-Löf's informal presentation of the demonstration of the axiom of choice.c.two examples of a tree-shaped graph of an extensive strategy. Acknowledgments: Many thanks to Mark van Atten (Paris1), Giuliano Bacigalupo (Zürich), Charles Zacharie Bowao (Univ. Ma Ngouabi de Brazzaville, Congo), Christian Berner (Lille3), Michel Crubellier (Lille3), Pierre Cardascia (Lille3), Oumar Dia (Dakar), Marcel Nguimbi ((Univ. Marien Ngouabi de Brazzaville, Congo), Adjoua Bernadette Dango (Lille3 / Alassane Ouattara de Bouaké, Côte d'Ivoire), Steephen Rossy Eckoubili (Lille3), Johan Georg Granström (Zürich), Gerhard Heinzmann (Nancy2), Muhammad Iqbal (Lille3), Matthieu Fontaine (Lille3), Radmila Jovanovic (Belgrad), Hanna Karpenko (Lille3), Laurent Keiff (Lille3), Sébastien Magnier (Saint Dennis, Réunion), Clément Lion (Lille3), Gildas Nzokou (Libreville), Fachrur Rozie (Lille3), Helge Rückert (Mannheim), Mohammad Shafiei (Paris1), and Hassan Tahiri (Lisbon), for rich interchanges, suggestions on the main claims of the present study and proof-reading of specific sections of the text. Special thanks to Gildas Nzokou (Libreville), Steephen Rossy Eckoubili (Lille3) and Clément Lion (Lille3), with whom a Pre-Graduate Textbook in French on dialogical logic and CTT is in the process of being worked out – during the visiting-professorship in 2016 of the former. Eckoubili is the author of the sections on exercises for dialogical logic, Nzokou cared of those involving the development of CTT-demonstrations out of winning-strategies. Special thanks also to Ansten Klev (Prague) for helping with technical details and conceptual issues on CTT, particularly so as author of the chapter introducing CTT. (shrink)

This volume would not exist without the help of all those who contributed to the organisation of the MacColl centenary meeting (Boulogne-sur-Mer, 9--10 October 2009). We are especially grateful to Bruno Béthouart, Jacques Dubucs, Gerhard Heinzmann, and Shahid Rahman. We would also like to thank Michael Astroh, Sandrine Avril, Anny Bégard, Christian Berner, Pierre-Édouard Bour, Peggy Cardon, Emmanuelle Jablonsky, Christian Mac Coll, Tony Mann, Gildas Nzokou, Max Papyle, Bernard Quéh...

Carta escrita por Gilda de Mello e Souza, remetida ao colega Oswaldo Porchat, que se encontrava em Berkeley, quando a ditadura civil-militar brasileira, recrudescida desde a implantação, em agosto de 1968, do AI-5, representava uma verdadeira ameaça a estudantes e docentes da Universidade de São Paulo, especialmente se lhe fizessem qualquer tipo de oposição. Porchat trocou uma sequência de cartas com Gilda nessa época, nas quais relata sua desilusão com a Faculdade de Filosofia, e com os acontecimentos políticos no Brasil. (...) Ao mesmo tempo, confessa estar encantado com a descoberta de novos elementos da Lógica, e com a atmosfera mais amena dos Estados Unidos. Porchat sabe que Gilda enfrenta momentos difíceis, tendo de assumir a Presidência do curso em meio à tentativa do reitor Miguel Reale de submetê-lo a um interventor. Enfrentando a dúvida sobre se valeria a pena retornar ao Brasil naquele momento, Porchat escreve à amiga. A carta a seguir expressa, dentro do que era possível na época, quando as correspondências eram vigiadas, o parecer de Gilda sobre as indagações do amigo, sobre os rumos da ditadura, e sobre o que ela pensava de sua própria atitude de resistência naquele contexto. A carta original, assim como a sequência de correspondências da qual faz parte, está depositada no Fundo Gilda de Mello e Souza, no Instituto de Estudos Brasileiros (IEB/USP). Agradeço à família de Gilda, especialmente a Ana Luisa Escorel e a Laura Escorel, pela disponibilização desse documento para a presente publicação. (shrink)

We show that there is a purely proof-theoretic proof of the Rasiowa–Harrop disjunction property for the full intuitionistic propositional calculus ), via natural deduction, in which commuting conversions are not needed. Such proof is based on a sound and faithful embedding of \ into an atomic polymorphic system. This result strengthens a homologous result for the disjunction property of \ and answers a question then posed by Pierluigi Minari.

The aim of this article is to offer a view of the current status of women in medical physics and biomedical engineering, while focusing on solutions towards gender balance and providing examples of current activities carried out at national and international levels. The International Union of Physical and Engineering Scientists in Medicine is committed to advancing women in science and health and has several initiatives overseen by the Women in Medical Physics and Biomedical Engineering Task Group. Some of the main (...) strategies proposed by the Task Group to attain gender balance are: (a) identify and promote female role models that achieve successful work-life balance, (b) establish programs to develop female leaders, (c) create opportunities for females to increase the international visibility within the scientific community, and (d) establish archives and databases of women in STEM. (shrink)

We show that the number-theoretic functions definable in the atomic polymorphic system are exactly the extended polynomials. Two proofs of the above result are presented: one, reducing the functions’ definability problem in ${\mathbf{F}}_{\mathbf{at}}$ to definability in the simply typed lambda calculus and the other, directly adapting Helmut Schwichtenberg’s strategy for definability in $\lambda ^{\rightarrow }$ to the atomic polymorphic setting. The uniformity granted in the polymorphic system, when compared with the simply typed lambda calculus, is emphasized.

Si Vernant est célèbre pour avoir appliqué aux mythes grecs la méthode structurale élaborée par Lévi-Strauss, on essaiera ici de montrer que l’absence de la notion de transformation dans ses travaux révèle la distance qui sépare sa psychologie historique de l’anthropologie structurale. Au lieu d’analyser les relations qui unissent les variantes d’un mythe, Vernant cherche à appréhender la cohérence interne d’une œuvre, afin de reconstituer la mentalité qu’elle exprime. Cette démarche s’oppose profondément à celle de Lévi-Strauss, qui soutient pour sa (...) part que le fonctionnement de la pensée sauvage n’apparaît qu’à travers les opérations qui permettent de traduire les uns dans les autres des mythes issus de cultures différentes. (shrink)

Les multiples histoires des idées qui retracent la constitution, relativement récente, de la discipline appelée «esthétique», mentionnent souvent le nom d�Alexander Gottlieb Baumgarten (1714-1762) en lui attribuant l�«invention» du néologisme «æsthetica». Très rapidement, ce terme latin, traduit en allemand, entre dans l�usage courant. De nos jours, il désigne un ensemble de discours souvent très hétérogènes sur les beaux-arts. Mais le sens originaire d�æsthetica, c�est-à-dire le contenu de l�ouvrage éponyme de 1750, demeure largement méconnu. Le présent article souhaite contribuer à souligner (...) l�importance du geste inaugural de Baumgarten, dont l�intérêt n�est pas seulement historiographique. Car ce philosophe instaure de manière durable un nouveau rapport à l��uvre d�art. Nous insisterons tout particulièrement sur l�inscription métaphysique de son projet. (shrink)

Dans cet ouvrage, Fabrice Bertin s’intéresse à un personnage assez méconnu de l’histoire des Sourds: Auguste Bébian. Sa trajectoire est atypique: né en 1789 ou en 1791 d’un père métropolitain et d’une mère guadeloupéenne, dans le village de Morne-à-l’Eau (Guadeloupe), il grandit au cœur d’une exploitation agricole dédiée au café et qui compte plusieurs dizaines d’esclaves. Le jeune Auguste Bébian grandit donc au contact de nombreux enfants d’esclaves, qui perdent leurs conditions d’esclaves e...

El presente artículo tiene como objetivo analizar la ansiedad en adultos de Quito, Ecuador; la muestra estuvo conformada por 135 hombres y mujeres de 18 a 73 años quienes no han presentado un diagnóstico previo de ansiedad. Se aplicó el Inventario de Ansiedad de Beck (BAI) y se identificó que el 14% de los participantes presentan ansiedad grave, 17% moderada, 36% mínima y el 33% leve, siendo los jóvenes quienes presentan mayor nivel de ansiedad de tipo grave en comparación con (...) los adultos. En relación con la sintomatología física y emocional se considera la preocupación, miedo y dificultades del sueño. (shrink)

Résumé — En assignant la notion de création ex nihilo à la « représentation » , Hegel affirme son caractère non pleinement rationnel : en user, c’est selon lui voir des substances là où il faut discerner des moments. Figeant et isolant les termes en jeu, la représentation déboucherait sur le dialectique , sans permettre de passer au spéculatif . Ainsi, posant créateur et créature comme des substances distinctes, elle donnerait lieu à une « dialectique du fini et de l’infini (...) », où chaque terme « passerait en son opposé ». Mais Hegel omet de distinguer le couple fini/infini du couple esprit fini / esprit infini, ce qui le conduit à traiter ce dernier comme un couple de contraires ; et c’est ce qui ne semble pas tenable. Autant la stricte séparation des termes du premier couple débouche bien sur une dialectique ruineuse , autant la nette distinction des termes du second couple est la condition d’authentiques relations spirituelles, de personne à personne. En fait, la notion de création est, telle quelle, pleinement adéquate à la désignation d’un originer dont le fruit est un être à part entière,libre – et non un simple moment.— In assigning the notion of creation ex nihilo to « representation » , Hegel asserts its character not fully rational. According to him, in using this notion, one sees substances where one should discern moments. By fixing and isolating the terms at stake, representation leads to a dialectic type of reasoning , without allowing speculative reasoning . Hence, establishing creator and creature as distinct entities, it produces a « dialectic of the finite and the infinite » in which each term « would be interchangeable ». Yet, Hegel fails to distinguish the pair of concepts finite/infinite from the pair finite spirit / infinite spirit, which leads him to consider the two terms of the latter as opposite ; and that is precisely what is questionable. Although the strict separation of the terms of the first pair of notions leads to a self-annihilating dialectic , making a clear-cut distinction between the terms of the second couple is the necessary condition to deal with authentic relations from person to person. Actually, the notion of creation as such perfectly matches the designation of a gesture giving birth to a free and independent being instead of a simple moment. (shrink)

We present a refinement ofthe bounded modified realizability which provides both upper and lower bounds for witnesses. Our interpretation is based on a generalisation of Howard/Bezem's notion of strong majorizability. We show how the bounded modified realizability coincides with our interpretation in the case when least elements exist . The new interpretation, however, permits the extraction of more accurate bounds, and provides an ideal setting for dealing directly with data types whose natural ordering is not well-founded.

Realizability notions in mathematical logic have a long history, which can be traced back to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations of intuitionistic logic. Kleene’s initial realizability laid the ground for more sophisticated notions such as Kreisel’s modified realizability and various modern approaches. In this context, our work aligns with the lineage of realizability strategies that emphasize the accumulation, rather than the propagation of precise witnesses. In this paper, we introduce a new notion (...) of realizability, namely herbrandized modified realizability. This novel form of (cumulative) realizability, presented within the framework of semi-intuitionistic logic is based on a recently developed star combinatory calculus, which enables the gathering of witnesses into nonempty finite sets. We also show that the previous analysis can be extended from logic to (Heyting) arithmetic. (shrink)

Given the recent interest in the fragment of system $\mathbf{F}$ where universal instantiation is restricted to atomic formulas, a fragment nowadays named system ${\mathbf{F}}_{\textbf{at}}$, we study directly in system $\mathbf{F}$ new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: they help achieving strict simulation of proof reduction by means of the Russell–Prawitz embedding of $\textbf{IPC}$ into system $\mathbf{F}$, they are not stronger than a certain ‘dinaturality’ conversion known to generate a consistent (...) equality of proofs, they provide the bridge between the Russell–Prawitz embedding and another translation, due to the authors, of $\textbf{IPC}$ directly into system ${\mathbf{F}}_{\textbf{at}}$ and they give means for explaining why the Russell–Prawitz translation achieves strict simulation whereas the translation into ${\mathbf{F}}_{\textbf{at}}$ does not. (shrink)

It is known that there is a sound and faithful translation of the full intuitionistic propositional calculus into the atomic polymorphic system F at, a predicative calculus with only two connectives: the conditional and the second-order universal quantifier. The faithfulness of the embedding was established quite recently via a model-theoretic argument based in Kripke structures. In this paper we present a purely proof-theoretic proof of faithfulness. As an application, we give a purely proof-theoretic proof of the disjunction property of the (...) intuitionistic propositional logic in which commuting conversions are not needed. (shrink)

We introduce a new typed combinatory calculus with a type constructor that, to each type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma$$\end{document}, associates the star type σ∗\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma ^*$$\end{document} of the nonempty finite subsets of elements of type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma$$\end{document}. We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this star combinatory (...) calculus, we define a functional interpretation of first-order predicate logic and prove a corresponding soundness theorem. It is seen that each theorem of classical first-order logic is connected with certain formulas which are tautological in character. As a corollary, we reprove Herbrand’s theorem on the extraction of terms from classically provable existential statements. (shrink)

We study an alternative embedding of IPC into atomic system F whose translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity. As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at the levels of provability and preservation of proof identity, but it produces shorter derivations and shorter simulations of reduction sequences. Lambda-terms are employed in the technical development so that the algorithmic (...) content is made explicit, both for the alternative and the original embeddings. The investigation of preservation of proof-reduction steps by the alternative embedding enables the analysis of generation of “administrative” redexes. These are the key, on the one hand, to understand the difference between the two embeddings; on the other hand, to understand whether the final word on the embedding of IPC into atomic system F has been said. (shrink)

This paper describes the first study of vasectomized men in Latin America; it is based on personal interviews with 172 men who had undergone the operation at least 3 months previously.

We give an elementary proof of the strong normalization of the atomic polymorphic calculus Fat.