We present a proof of the equivalence between two deductive systems for constructive necessity, namely an axiomatic characterisation inspired by Hakli and Negri's system of derivations from assumptions for modal logic , a Hilbert-style formalism designed to ensure the validity of the deduction theorem, and the judgmental reconstruction given by Pfenning and Davies by means of a natural deduction approach that makes a distinction between valid and true formulae, constructively. Both systems and the proof of their equivalence are formally verified (...) using the state-of-the-art proof assistant Coq. The proof approach taken throughout the paper unveils the use of some alternative proof methods that allow for a smooth transition from the high-level mathematical proofs to their mechanised counterparts. (shrink)

Laurent Le Bon, directeur du Centre Pompidou-Metz, dévoile au cours d’un entretien avec Roland Huesca l’histoire, les atours et les enjeux de l’écriture de plusieurs catalogues d’expositions : à l’affiche Dada, Chefs-d’œuvre ?..

En este artículo se pretende poner de manifiesto las restricciones impuestas por el Estado español a la libertad de movimiento. Una vez descritas estas restricciones en las tres primeras olas de la pandemia de la Covid-19, se reflexiona sobre los posibles excesos del gobierno aumentando su control sobre una ciudadanía preocupada y con temor hacia la pandemia. Sin embargo, existe una consecuencia inesperada en las actitudes políticas de las personas: una reducción de las preferencias hacia la democracia, a favor del (...) autoritarismo. (shrink)

Equational reasoning arises in many areas of mathematics and computer science. It is a cornerstone of algebraic reasoning and results essential in tasks of specification and verification in functional programming, where a program is mainly a set of equations. The usual manipulation of identities while conducting informal proofs obviates many intermediate steps that are neccesary while developing them using a formal system, such as the equationally complete Birkhoff calculus ${\mathcal{B}}$. This deductive system does not fit in the common manner of (...) doing mathematical proofs, and it is not compatible with the mechanisms of proof assistants. The aim of this work is to provide a deductive system ${\mathcal{B}}^{\textrm{GOAL}}$ for equality, equivalent to ${\mathcal{B}}$ but suitable for constructing equational proofs in a backward fashion. This feature makes it adequate for interactive proof-search in the approach of proof assistants. This will be achieved by turning ${\mathcal{B}}^{\textrm{GOAL}}$ into a transition system of formal tactics in the style of Edinburgh LCF, such transformation allows us to give a direct formal definition of backward proof in equational logic. (shrink)

Spanish translation of Jussi Backman, "Divine and Mortal Motivation: On the Movement of Life in Aristotle and Heidegger,” Continental Philosophy Review 38 (2005): 241–261. -/- Translated by Fernando Huesca Ramón, translation revised by Jean Orejarena Torres and César Mora Alonso.

On propose une biographie de Petrus Alfonsi de Huesca. On reproduit notre déduction mathématique de l'icone Trinitaire d'un parchemin de Chartres, du Xlll siècle, depuis la figure précabalistique de Petrus Alfonsi, qu'il a introduit dans son oeuvre Dialogue contre les juifs en l'année 1110. On presente aussi trois matérialisations de I'enlacement alterné de trois anneaux deux à deux non enlacés.A Biography of Pedro Alfonso es proposed from the information today known. There is repruduced our mathematical deduction of the icon (...) Trinitario of a parchment of Chartres of the XIIIth century from a figure precabalistica introduced in 1110 by Pedro of Huesca and it is presented three other materializations of the "alternated link of three any two nost linked". (shrink)

Dos corrientes principales dividen el debate sobre la relación entre Joaquín de Fiore, Pedro Alfonso de Huesca y la cábala judaica. Gershon Scholem firma la hipótesis de que el abad de Fiore y los cabalistas españoles del siglo XII, a la vez y sin conocerse, han producido trabajos similares. Esta hipótesis será parcialmente rechazada por una segunda que pone en evidencia algunos aspectos de la obra joaquinita derivados del filósofo judío-aragonés, converso al cristianismo, Pedro Alfonso de Huesca. Esta (...) segunda hipótesis permite afirmar que la explicación de la Trinidad asumida por Pedro Alfonso de acuerdo con el Tetragrama YHWH tomado del Secretum secretorum de los judíos fue incorporada por Joaquín de Fiore, y que utilizará especialmente en la composición de la Figura XIII – el Salterio de diez cuerdas, y de la Figura XI – los Tres círculos trinitarios del Liber Figurarum. Desde esta perspectiva, añadimos una tercera hipótesis: que la relación entre Joaquín de Fiore y la cábala, además de tener como punto de apoyo la explicación trinitaria de Pedro Alfonso, se refleja directamente en la confección de sus principales figurae. Y de forma complementaria, entendemos que la fuente que nutre Pedro Alfonso, e indirectamente la de Joaquín de Fiore –el llamado Secretum secretorum de los judíos– es una compilación de tres textos cabalistas principales: el Sefer Yetsirah, el Sefer al-Raziel y el Libro de Salomón. (shrink)

A biography of Pedro Alfonso is proposed from the information today known. There is reproduced our mathematical deduction of the icon Trinitario of a parchment of Chartres of the XIIIth century from a figure precabalística introduced in 1110 by Pedro Alfonso of Huesca and it is presented three other materializations of the «alternated link of three rings any two not linked».