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)

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)

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)

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)

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

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.

Nada hay más confortable para el hombre, ni más peligroso, que las certezas. Nuestra mejor defensa es la filosofía, que consiste engran medida en el arte de cuestionarlas, de atreverse a pensar, de interpelar las verdades establecidas y ver qué esconden. En estepaseo por la historia de la filosofía, Fernando Savater nos presenta a los grandes personajes que con sus preguntas, y en ocasiones con sus respuestas, han marcado el pensamiento occidental. Platón, Aristóteles, Hobbes, Tomás de Aquino, Nietzsche, Marx, (...) Ortega, Wittgenstein y hasta dieciocho filósofos más desfilan por estas páginas de la mano de Savater, que con su habitual estilo lúcido, ameno e inteligente explica sus ideas más importantes y resume sus trayectorias. Un canto al irrenunciable ejercicio de la libertad intelectual, este libro es en realidad una invitación a huir de los tópicos y a compartir con los grandes filósofos la maravillosa aventura de pensar. (shrink)

Heritage values are basic in conservation, nevertheless there is not a methodology to analyze their variation over time and how it has affected the conservation of heritage assets. Therefore, a methodology that allows us to determine their variation in written descriptions about a specific heritage site was needed. In this article we have addressed the concept of heritage values and stressed their importance and their variability over time, but also analyzed different methods from the field of linguistics that would better (...) adapt to determine heritage values variation and their application in the heritage field. (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)

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)

Las sugerentes problemáticas de la obra y pensamiento de Paul Ricoeur, enunciadas en este artículo, no buscan dar un trabajo apologético ni una descripción acusativa; de lo que se trata, por consiguiente, es de estructurar la subjetividad como acción y hermenéutica. En este contexto, el lenguaje y la acción contienen en sí inherentes interrogantes que fomentan una especie de dedicación cuidadosa y pertinente sobre el sujeto. Los interrogantes que suscitan estas dos temáticas pueden ser: ¿qué es lenguaje?, ¿cuál es la (...) relación del lenguaje con el sujeto y la hermenéutica?, ¿cuál es la necesidad del texto?, ¿cuál es la importancia del discurso? y, sobre todo, ¿qué queremos interpretar por “teoría de la acción subjetiva e intersubjetiva para el hombre actual”? (shrink)