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)

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)

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 has been known for six years that the restriction of Girard's polymorphic system $\text{\bfseries\upshape F}$ to atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait's method of “convertibility” applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each $\beta$-reduction step of the full intuitionistic propositional calculus translates into one or more $\beta\eta$-reduction steps in the restricted Girard system. As a consequence, we obtain (...) a novel and perspicuous proof of the strong normalization property for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role to $\eta$-conversions. (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)

Commuting conversions were introduced in the natural deduction calculus as ad hoc devices for the purpose of guaranteeing the subformula property in normal proofs. In a well known book, Jean-Yves Girard commented harshly on these conversions, saying that ‘one tends to think that natural deduction should be modified to correct such atrocities.’ We present an embedding of the intuitionistic predicate calculus into a second-order predicative system for which there is no need for commuting conversions. Furthermore, we show that the redex (...) and the conversum of a commuting conversion of the original calculus translate into equivalent derivations by means of a series of bidirectional applications of standard conversions. (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 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.

Edward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is animpassable barrierin the totality of exponentiation. On the positive side, Nelson embarks on a program of investigating how much mathematics can be interpreted in Raphael Robinson's theory of arithmetic. In the shadow of this program, some very nice logical investigations and results were produced by a number of people, not only regarding what can be interpreted inbut also what cannot be so (...) interpreted. We explain some of these results and rely on them to discuss Nelson's position. (shrink)

Edward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is an impassable barrier in the totality of exponentiation. On the positive side, Nelson embarks on a program of investigating how much mathematics can be interpreted in Raphael Robinson's theory of arithmetic Q. In the shadow of this program, some very nice logical investigations and results were produced by a number of people, not only regarding what can be interpreted in Q but (...) also what cannot be so interpreted. We explain some of these results and rely on them to discuss Nelson's position. (shrink)

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

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.

Este artigo tem como principal objetivo analisar e discutir questões acerca de como à educação muitas vezes acaba por contribuir para o aumento das desigualdades sociais. Desse modo, através dessa análise pretende-se ainda destacar as contribuições e críticas do pensamento de Pierre Félix Bourdieu, Paul- Michel Foucault e Karl Marx sobre os problemas sociais que permeiam a sociedade desde o século XIX até os dias atuais e muitas vezes são fortalecidos pelos sistemas educacionais.

Suppose that it is possible to integrate real functions over a weak base theory related to polynomial time computability. Does it follow that we can count? The answer seems to be: obviously yes! We try to convince the reader that the severe restrictions on induction in feasible theories preclude a straightforward answer. Nevertheless, a more sophisticated reflection does indeed show that the answer is affirmative.

Leo Harrington showed that the second-order theory of arithmetic WKL 0 is ${\Pi^1_1}$ -conservative over the theory RCA 0. Harrington’s proof is model-theoretic, making use of a forcing argument. A purely proof-theoretic proof, avoiding forcing, has been eluding the efforts of researchers. In this short paper, we present a proof of Harrington’s result using a cut-elimination argument.

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.

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)

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)

Soren Kierkegaard's Works of Love, a series of deliberations on the commandment to love one's neighbor, has often been condemned by critics. Here, Ferreira seeks to rehabilitate Works of Love as one of Kierkegaard's most important works. He shows that Kierkegaard's deliberations on love are highly relevant to some important themes in contemporary ethics, including impartiality, duty, equality, mutuality, reciprocity, self-love, sympathy, and sacrifice. Ferreira also argues that Works of Love bears on issues peculiar to a religious ethic, (...) such as the role of God as "middle term," and the possibility of preserving the aesthetic dimensions of love in a religious ethic of relation. (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)

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)

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)

The article addresses the pervasive global challenge of delayed justice, emphasizing its role as a catalyst for widespread judicial reforms. The study defines international and national court approaches to reasonable trial durations by employing systematic and comparative legal methods. It delves into essential technology courts and parties use to ensure timely proceedings, categorizing associated risks and problems. The authors advocate for the multi-door courthouse system, illustrating its efficacy in reducing delays. Furthermore, the article classifies technologies facilitating reasonable trial durations, acknowledging (...) and offering solutions for the challenges they present. This research contributes to the dynamic landscape of judicial reform, offering a holistic perspective on the multifaceted aspects of timely justice. (shrink)

Is the dream of EU endangered? This book reviews classic and modern values and virtues, and uses them in order to rethink Europe's present politics and its future. The idea of the Republic was born with the political ethics of ancient Greece. The current international crisis obliges Europe to face the mirror of truth: What has become of the European Idea and how fares the European Constitution? It has been a long road from the Greek Politeia to the present lack (...) of values and financial monomania in Europe, who seems to have lost any harmony between the spirit, the soul and the body of her Constitution: the will and values of the people (material constitution), the text of the Lisbon Treaty (formal constitution) and its current political interpretation and action (real constitution), making Europe a two-tier or three-tier club, far from the dream of the founding fathers. Without republican values and virtues, and failing to uphold the European social model, the European Union would devolve into moral, social and democratic bankruptcy. (shrink)

Frege’s Grundgesetze der Arithmetik is formally inconsistent. This system is, except for minor differences, second-order logic together with an abstraction operator governed by Frege’s Axiom V. A few years ago, Richard Heck showed that the ramified predicative second-order fragment of the Grundgesetze is consistent. In this paper, we show that the above fragment augmented with the axiom of reducibility for concepts true of only finitely many individuals is still consistent, and that elementary Peano arithmetic (and more) is interpretable in this (...) extended system. (shrink)

In today's global marketplace, the Philippines provide a unique example of an Asian culture with established economic ties to the West. In this study, Philippine and United States undergraduate business students responded to 13 vignettes describing questionable ethical actions in business situations. Results reveal significant differences between groups for 9 of the 13 vignettes. For 4 vignettes, Philippine participants were more disapproving of the actions, and for another 5, United States participants were more disapproving. The study suggests that cultural differences (...) continue and the implications of these differences should be considered in today's global economy. (shrink)

An advanced introduction to the new philosophical anthropology and an understanding of the most contemporary developments in it.

Soren Kierkegaard's Works of Love, a series of deliberations on the commandment to love one's neighbor, has often been condemned by critics. Here, Ferreira seeks to rehabilitate Works of Love as one of Kierkegaard's most important works. He shows that Kierkegaard's deliberations on love are highly relevant to some important themes in contemporary ethics, including impartiality, duty, equality, mutuality, reciprocity, self-love, sympathy, and sacrifice. Ferreira also argues that Works of Love bears on issues peculiar to a religious ethic, (...) such as the role of God as "middle term," and the possibility of preserving the aesthetic dimensions of love in a religious ethic of relation. (shrink)