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 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)

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)

During the last few decades, the historical turn within the tradition of the analytic tradition has experienced growing enthusiasm concerning the procedure of rational reconstruction, whose validity or importance, despite its paradigmatic examples in Frege and Russell, has not always enjoyed a consensus. Among the analytic philosophers who are the frontrunners of this movement, Robert Brandom is one of a kind: his work on Hegel as well as on German Idealism has been increasing interest in, as well as awareness of, (...) Hegel´s possible contributions to some current problems in that tradition, and connecting Hegel scholars to current questions. Thus, this work aims to explore Brandom´s methodology of rational reconstruction, as well as his dialogue with history of Philosophy, mainly exposed in his Tales of the mighty dead (2002). As we will see, Brandom´s distinction between a de dicto and a de re approach intends to present a way of identifying and analyzing a given philosopher´s theoretical (hidden) commitments that can be useful to improve the quality of the dialogue with past philosophers. From such methodological exposition, I to turn to Kierkegaard in order to make explicit some of his ontological commitments and presenting Brandom’s approach as a valuable tool for doing history of philosophy. (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)

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)

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

Em 1845, ainda durante o período de redação da obra que seria o Pós-Escrito Conclusivo Não-Científico às Migalhas Filosóficas – trabalhado sob o título provisório de Problemas Lógicos –, Kierkegaard esboça em seus Papirer (IV A 145) um curioso esquete que se passaria nos Infernos – ou Submundo – envolvendo um diálogo entre Sócrates e Hegel. Neste diálogo acerca do famigerado problema do início da filosofia hegeliana, Kierkegaard descreve Hegel fazendo a leitura da página 198 do segundo volume das Logische (...) Untersuchungen, de F. A. Trendelenburg. A citação precisa da página, feita por Kierkegaard, não poderia ser senão uma indicação da relevância de seu conteúdo para o tema debatido entre os dois filósofos no diálogo imaginário. De fato, está aí presente, entre outros argumentos, a acusação da intromissão da Anschauung no reino do pensamento puro, em especial no início da Lógica de Hegel. Assim, pretendemos neste trabalho (1) explicitar o argumento trendelenburguiano relativo à Anschauung, bem como (2) fazer alguns apontamentos da recepção kierkegaardiana do argumento a partir das relações deste com as teses centrais do Pós-Escrito. (shrink)

Resumo: Mesmo que neguemos qualquer tipo de excepcionalismo à filosofia como empreendimento intelectual (ver Williamson, 2007), parece fácil conceder que, pelo menos no que diz respeito às relações com sua própria história, a filosofia é diferente de outros campos do conhecimento (ver Williamson, 2018). No entanto, questões relacionadas ao escopo, papel e validade da história da filosofia para a atividade filosófica são tão antigas quanto a própria filosofia, além de se tornarem relevantes no chamado parting of ways entre as tendências (...) analítica e hermenêutico-fenomenológica. No entanto, é possível dizer que, pelo menos desde a segunda metade do último século, temos visto uma inflexão importante sobre o lugar e a importância da história da filosofia na filosofia contemporânea: tanto por causa da “virada histórica” na filosofia analítica, com obras de Strawson, Sellars e, mais recentemente, Brandom, servindo como bons exemplos desse movimento, quanto pelo interesse recentemente renovado em questões de metafilosofia. Um exemplo desse segundo movimento é o debate entre os chamados apropriacionistas e os contextualistas. Portanto, este artigo tem como objetivo analisar os dois principais argumentos contra as reconstruções racionais - o GTRC e a acusação de anacronismo - e oferecer uma defesa de uma abordagem inferencialista para a história da filosofia, com base no trabalho de Robert Brandom, que é simultaneamente aberto a certo contextualismo, bem como estabelece parâmetros para as reconstruções racionais. (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)

Byung-Chul Han escreve sobre uma nova forma de niilismo que emerge principalmente a partir do século XXI na _sociedade da informação_. A partir disso, analiso como esse niilismo decorre da eliminação da verdade como critério orientativo individual e coletivo. Para Han, isso decorreria da emergência da informação como o novo critério de conhecimento, que se impõe como um dispositivo da sociedade atual por meio de sua grande produtibilidade rápida e quantitativa, voltada à aceleração, produção e exploração. Desse modo, as informações (...) passam a assumir o lugar da verdade como narratividade, além de eliminar a diferença entre verdade e mentira, o que tem como principal consequência o abandono de modelos orientativos. Neste artigo, proponho apresentar as características do niilismo da sociedade da informação e classificá-lo, com base em referenciais teóricos de Deleuze sobre tema, como um niilismo ativo, posto que ao passo que nega os modelos de verdade conhecidos e existentes, tem uma postura e ação propositiva na produção de um novo modelo individual e social baseado no poder de afirmar. (shrink)

O pensamento do filósofo britânico Michael Oakeshott é frequentemente recrutado no debate entre conservadorismo e posições progressistas, no qual algumas de suas distinções e explicitações são postas a serviço da crítica a determinados aspectos dessa última. Um de seus principais movimentos argumentativos consiste em apontar que posições políticas fundamentalmente revolucionárias pressupõem certa concepção de racionalidade que, por sua vez, estaria em desacordo com uma visão clássica acerca da faculdade intelectiva humana ao mesmo tempo em que privilegia tal concepção em relação (...) a outras esferas da experiência humana. No entanto, embora usual, tal reconstrução não apenas não faz justiça aos objetivos e à argumentação de Oakeshott, como parece ignorar uma compreensão mais genuína do racionalismo nos séculos XVII e XVIII. Assim, o objetivo deste artigo é explorar a argumentação de Oakeshott tal qual exposta na seção III de seu Rationalism in Politics a fi m de, simultaneamente, precisar seus objetivos e colocá-los em perspectiva em relação à gênese histórico-temática do racionalismo. (shrink)

O presente artigo tem por meta analisar a possibilidade de conciliação entre a determinação e a liberdade em Espinosa. Dessa maneira, o artigo iniciará tratando das duas séries causais indicadas por Espinosa no §100 do TIE: a “série das coisas fixas e eternas” e a “série das coisas singulares mutáveis”. A abordagem dessas duas séries causais tem por meta compreender o que as distingue e as implicações dessa distinção para a filosofia de Espinosa. Em seguida analisar-se-ão as noções de essência (...) objetiva e essência formal evidenciando que o que está em jogo em EIIP7 é a adequação entre essas duas essências, e não uma adequação entre a essência e a existência. Nesse momento também será evidenciado que o tipo de causalidade que está em jogo em EIIP7 e EIIP8 é uma causalidade imanente, do tipo todo-parte, a qual se faz entre o conjunto e seus subconjuntos: ser parte é ser um subconjunto de Deus. Feito isso, mostrar-se-á que no âmbito da existência dos subconjuntos — e não no âmbito de sua essência — é possível autonomia relativa interpares, desde que essa autonomia seja concebida como subordinada aos conjuntos anteriores. Nesse momento também será evidenciado em que medida os modos finitos podem ser deduzidos da substância infinita sem que isso implique a negação de sua liberdade. (shrink)

Em Totalidade e Infinito, Lévinas descreve cuidadosamente a separação do Mesmo e do Outro, recorrendo diversas vezes ao termo “ensinamento” para definir o acolhimento num Eu interior, daquilo que lhe é exterior. Mas para Lévinas, na absoluta alteridade, o outro é Outrem, outra pessoa, irredutível à minha posse, exterioridade absoluta que me encara a partir de um rosto, como um ser que me fala e, por isso, é o único capaz de me ensinar. Acolher outrem, nesse sentido, é responder-lhe e, (...) assim, ser responsável por ele, numa relação que é, essencialmente, ética. Com isso em mente, é possível refletir sobre o sentido mais profundo da relação educativa que, para além dos papéis que assumem professores e alunos numa totalidade sistemática, Eu e Outro constituem uma frente a frente que dá sentido ao mundo do qual vivem, se apropriam e compartilham. A relação entre os sujeitos na educação, portanto, extrai sua significação do ensinamento, não como prioridade de um conteúdo comunicável, mas como responsabilidade infinita por outrem, como relação ética. (shrink)

This paper aims to establish theoretical guidelines for understanding the relationship between ethics and anthropology in Kant's thought. Contrary to a particular line of interpretation dominant in specialized research on Kant, this article seeks to promote a historical-philosophical investigation, which contextualizes in Kant's thought the moment when three philosophical currents intersected, causing the guidelines of his debate about the concept of autonomy and perfectibility, namely: the philosophies of Hutcheson, Wolff and Rousseau. In this first part, Kant's discussion with Hutcheson and (...) Wolff is discussed. From a more specific point of view, in this first part, the present article goes through Kant's reflections between 1755 and 1764 in order to present how the need to think about a relation between ethics and anthropology is constituted within Kantian thought. (shrink)

No artigo O mito da atitude estética, dentre outros trabalhos, o filósofo George Dickie se opõe a teses que circunscrevem a apreciação das obras de arte a determinados estados psicológicos centrados na noção de desinteresse prático e que fundamentariam o único espaço onde elas teriam significado enquanto tais. Nosso propósito aqui, num primeiro momento, será explicitar um dos aspectos pontuais desta crítica, qual seja, a análise e objeção ao conceito de “atitude estética” defendido por Jerome Stolnitz. Num segundo momento, questionaremos (...) se, de modo geral, a objeção àquele conceito pode ser estendida ao valor da estética, considerada irrelevante para a teoria institucional da arte, o centro da filosofia de Dickie. Nesta direção, retomaremos a antiga discussão sobre a demarcação de fronteiras entre estética e filosofia da arte, mas o faremos a partir da perspectiva de Dickie e, longe de esgotá-la, apenas indicaremos possíveis caminhos para a relação entre estas duas instâncias. (shrink)

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.

This study was aimed at exposing the proximity and not agonizing and not antagonistic relationship between themes and concepts as popularly known and often mistakenly understood in their relationships, such as "science" and "religion", "faith" and "reason, "" “empirical search” and “subjective understanding”. "For us, the relationship established between these concepts is a relation of completion, parallel, and not in opposition. Through a theistic argument based on history, philosophy, theology and sciences, we intend to present the misconception about the issue (...) and demonstrate the truth inherent in these relationships as productive and so poorly understood. (shrink)

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.

O artigo discute as noções de imagem e imaginação na Ética de Espinosa. A análise iniciará elencando passagens nas quais Espinosa se refere às imagens como afecções do corpo e às imaginações como afecções da mente. Em um segundo momento, o texto se encaminhará para EII P17 cor., a partir do qual será analisada a geração das imagens. Nesse momento, será posto em evidência o fato de que é o movimento — e não o vestígio — aquilo que constitui a (...) essência das imagens. Na sequência, analisar-se-á a geração das imaginações na mente e serão tecidos alguns comentários sobre a memória em Espinosa. Por fim, convém destacar que o artigo limita-se à Ética por essa obra trazer alterações significativas na maneira como Espinosa pensa o assunto em relação aos seus textos de juventude. (shrink)

'Revisão do Pensamento Conservador' apresenta alguns resultados do Projeto Temático Fapesp 'Linhagens do Pensamento Político-Social Brasileiro' desenvolvidos por seus integrantes e outros pesquisadores interlocutores do projeto. O livro procura oferecer uma visão de conjunto das configurações assumidas pelo pensamento conservador em diferentes momentos da vida intelectual brasileira, em algumas tradições políticas e em diferentes autores, como Visconde do Uruguai, José de Alencar, Alberto Torres, Gilberto Freyre, Gustavo Corção e outros.

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.

Understanding Animal Abuse and How to Intervene with Children and Young People offers a positive, compassion-based and trauma-informed approach to understanding and intervening in animal abuse. It provides an accessible cross-disciplinary synthesis of current international evidence on animal abuse, and a toolkit for professionals working with people and/or animals to help them understand, prevent, and intervene in cases of animal abuse. With contributions from experts in the field, this essential text offers ten user-friendly chapters with questions for reflection and key (...) summary points. It offers a definition of animal abuse, synthesises the latest research on children, young people and animal abuse, and explores the link between animal abuse and other forms of abuse, and legal perspectives on animal abuse. The second half of the book presents a practical toolkit for professionals, offering guidance and strategies for prevention of and intervention in cases of animal abuse. It provides multidisciplinary perspectives on interventions; from teachers' and social workers roles in detection and intervention of childhood animal abuse, to the roles of enforcement agencies and veterinarians in legal cases of adult animal abuse. Together with a final chapter proposing new directions for research, policy, and practice, this guide is for all who work with children, young people and/or animals, including psychologists, social workers, veterinarians, education professionals, and animal welfare educators. It is also key reading for those involved in legal and policy issues relating to animal welfare. (shrink)

The course delivered by Heidegger during the Summer semester of 1923, and published later under the title of Ontology – The hermeneutics of facticity, is one of the most important loci in which we can have a glimpse of Kierkegaard’s influence on and importance to Heidegger, as well as of some of his interpretations about the thought of the Dane philosopher. One of them, notwithstanding puts forward a very interesting assessment of the relation between Kierkegaard and Hegel – through F. (...) A. Trendelenburg –, one of hottest topics in the Kierkegaardian scholarship, is not usually analyzed by that scholarship. Hence, this paper aims to show and analyze Heidegger’s theses on the relation between Kierkegaard-Hegel in that work in order to evaluate their correctness. As final remarks, this paper presents some metaphilosophical reflections on the very notions of relation and dependence between philosophers. (shrink)

O percurso construído pelo pensamento de Albert Camus (1913-1960) perfaz uma unidade profunda entre Ética e Estética. Par- tindo de uma preocupação explicitamente ética, o autor acaba por ter de desenvolver uma antropologia filosófica, ou seja, um discurso sobre o homem que tem como núcleo um conceito que o reenvia àquilo que podemos chamar de dimensão estética para então, a partir daí, oferecer uma resposta àquele problema ético. Desse modo, pretendemos neste trabalho explicitar o caminho ao qual aludimos em três (...) momentos: (a) a existência humana como problema ético; (b) o discurso camusiano sobre o homem que tem como núcleo a noção de Passion e, por fim, (c) a elaboração de um novo éthos, partindo da noção de Paixão, como res- posta necessária ao problema existencial configurada como uma re-cri- ação ou correção permanente, à semelhança do ofício do Artista. (shrink)