The duality between general frames and modal algebras allows to transfer a problem about the relational (Kripke) semantics into algebraic terms, and conversely. We here deal with the conjecture: the modal algebra A is subdirectly irreducible (s.i.) if and only if the dual frame A* is generated. We show that it is false in general, and that it becomes true under some mild assumptions, which include the finite case and the case of K4. We also prove that a Kripke frame (...) F is generated if and only if the dual algebra F* is s.i. The technical result is that A is s.i. when the set of points which generate the dual frame A* is not of zero measure. (shrink)

We introduce a sequent calculus B for a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic, quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterize B positively: reflection, symmetry and visibility. A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with (...) a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection. To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube. (shrink)

We introduce a sequent calculusBfor a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic. quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterizeBpositively: reflection, symmetry and visibility.A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with a metalinguistic link between assertions, (...) and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection.To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube. (shrink)

Pretopologies were introduced in [S], and there shown to give a complete semantics for a propositional sequent calculus BL, here called basic linear logic, as well as for its extensions by structural rules,ex falso quodlibetor double negation. Immediately after Logic Colloquium '88, a conversation with Per Martin-Löf helped me to see how the pretopology semantics should be extended to predicate logic; the result now is a simple and fully constructive completeness proof for first order BL and virtually all its extensions, (...) including the usual, or structured, intuitionistic and classical logic. Such a proof clearly illustrates the fact that stronger set-theoretic principles and classical metalogic are necessary only when completeness is sought with respect to a special class of models, such as the usual two-valued models.To make the paper self-contained, I briefly review in §1 the definition of pretopologies; §2 deals with syntax and §3 with semantics. The completeness proof in §4, though similar in structure, is sensibly simpler than that in [S], and this is why it is given in detail. In §5 it is shown how little is needed to obtain completeness for extensions of BL in the same language. Finally, in §6 connections with proofs with respect to more traditional semantics are briefly investigated, and some open problems are put forward. (shrink)

Within the technical frame supplied by the algebraic variety of diagonalizable algebras, defined by R. Magari in [2], we prove the following: Let T be any first-order theory with a predicate Pr satisfying the canonical derivability conditions, including Löb's property. Then any formula in T built up from the propositional variables $q,p_{1},...,p_{n}$ , using logical connectives and the predicate Pr, has the same "fixed-points" relative to q (that is, formulas $\psi (p_{1},...,p_{n})$ for which for all $p_{1},...,p_{n}\vdash _{T}\phi (\psi (p_{1},...,p_{n}),p_{1},...,p_{n})\leftrightarrow \psi (...) (p_{1},...,p_{n})$ ) of a formula $\phi ^{\ast}$ of the same kind, obtained from φ in an effective way. Moreover, such $\phi ^{\ast}$ is provably equivalent to the formula obtained from φ substituting with $\phi ^{\ast}$ itself all the occurrences of q which are under Pr. In the particular case where q is always under Pr in φ, $\phi ^{\ast}$ is the unique (up to provable equivalence) "fixed-point" of φ. Since this result is proved only assuming Pr to be canonical, it can be deduced that Löb's property is, in a sense, equivalent to Gödel's diagonalization lemma. All the results are proved more generally in the intuitionistic case. (shrink)

The search for a synthesis between formalism and constructivism, and meditation on Gödel incompleteness, leads in a natural way to conceive mathematics as dynamic and plural, that is the result of a human achievement, rather than static and unique, that is given truth. This foundational attitude, called dynamic constructivism, has been adopted in the actual development of topology and revealed some deep structures that had remained hidden under other views. After motivations for and a brief introduction to dynamic constructivism, an (...) overview is given of the changes it induces in the practice of mathematics and in its foundation, and of the new results it allows to obtain. (shrink)

Martin-Löf Type Theory is both an important and practical formalization and a focus for a charismatic view of the foundations of mathematics. Per Martin-Löf's work has been of huge significance in the fields of logic and the foundations of mathematics, and has important applications in areas such as computing science and linguistics. This volume celebrates the twenty-fifth anniversary of the birth of the subject, and is an invaluable record both of areas of currentactivity and of the early development of the (...) subject. Also published for the first time is one of Per Martin-Löf's earliest papers. (shrink)

This volume draws together contributions from researchers whose work builds on the theory developed by Martin-Lof over the last twenty-five years.

We introduce the notion of infinitary preorder and use it to obtain a predicative presentation of sup-lattices by generators and relations. The method is uniform in that it extends in a modular way to obtain a presentation of quantales, as “sup-lattices on monoids”, by using the notion of pretopology.Our presentation is then applied to frames, the link with Johnstone’s presentation of frames is spelled out, and his theorem on freely generated frames becomes a special case of our results on quantales.The (...) main motivation of this paper is to contribute to the development of formal topology. That is why all our definitions and proofs can be expressed within an intuitionistic and predicative foundation, like constructive type theory. (shrink)

Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in (...) a predicative way by an inductive generation and thus their properties can be proved inductively. We show however that some natural complete Heyting algebra cannot be inductively defined. (shrink)

We give arguments explaining why, when adopting a minimalist approach to constructive mathematics as that formalized in our two-level minimalist foundation, the choice for a pointfree approach to topology is not just a matter of convenience or mathematical elegance, but becomes compulsory. The main reason is that in our foundation real numbers, either as Dedekind cuts or as Cauchy sequences, do not form a set.

We construct a Galois connection between closure and interior operators on a given set. All arguments are intuitionistically valid. Our construction is an intuitionistic version of the classical correspondence between closure and interior operators via complement.

A positive topology is a set equipped with two particular relations between elements and subsets of that set: a convergent cover relation and a positivity relation. A set equipped with a convergent cover relation is a predicative counterpart of a locale, where the given set plays the role of a set of generators, typically a base, and the cover encodes the relations between generators. A positivity relation enriches the structure of a locale; among other things, it is a tool to (...) study some particular subobjects, namely the overt weakly closed sublocales. We relate the category of locales to that of positive topologies and we show that the former is a reflective subcategory of the latter. We then generalize such a result to the category of suplattices, which we present by means of cover relations. Finally, we show that the category of positive topologies also generalizes that of formal topologies, that is, overt locales. (shrink)

Giovanni Sambin has recently introduced the notion of an overlap algebra in order to give a constructive counterpart to a complete Boolean algebra. We propose a new notion of regular open subset within the framework of intuitionistic, predicative topology and we use it to give a representation theorem for overlap algebras. In particular we show that there exists a duality between the category of set-based overlap algebras and a particular category of topologies in which all open subsets are (...) regular. (shrink)

Research in the field of management has increasingly focused on strategies and tools related to corporate sustainability. Of the tools examined, codes of ethics have been found to play a primary role. Many studies have investigated the content of such codes, as well as their capacity to condition the behaviour of people within organizations. However, few studies have considered the intrinsic quality of codes of ethics. This study aims to investigate the impact that specific factors—firm size, degree of internationalization and (...) industry effect—can have on the quality of codes of ethics. Based on a sample of 248 listed Italian companies, the results of the empirical analysis show that the quality standard is particularly high in larger companies and in those firms operating in industries in which relationships established with critical stakeholders—and disclosure to those stakeholders—play a crucial role. These results have interesting implications for both researchers and practitioners. (shrink)

Euler developed a program which aimed to transform analysis into an autonomous discipline and reorganize the whole of mathematics around it. The implementation of this program presented many difficulties, and the result was not entirely satisfactory. Many of these difficulties concerned the integral calculus. In this paper, we deal with some topics relevant to understand Euler’s conception of analysis and how he developed and implemented his program. In particular, we examine Euler’s contribution to the construction of differential equations and his (...) notion of indefinite integrals and general integrals. We also deal with two remarkable difficulties of Euler’s program. The first concerns singular integrals, which were considered as paradoxical by Euler since they seemed to violate the generality of certain results. The second regards the explicitly use of the geometric representation and meaning of definite integrals, which was gone against his program. We clarify the nature of these difficulties and show that Euler never thought that they undermined his conception of mathematics and that a different foundation was necessary for analysis. (shrink)

Theoria, Volume 88, Issue 4, Page 733-742, August 2022.

Riassunto: Questo lavoro sviluppa due elementi, apparentemente lontani, ma per alcuni aspetti non secondari, convergenti. Per un verso l’attenzione è rivolta all’origine delle regole che disciplinano il comportamento sociale umano, oltrepassando le regole di matrice istituzionale e convenzionale, che sono spesso considerate le più nobili e le più umane, nel tentativo di far affiorare le regole più remote del nostro agire, legate al patrimonio genetico degli individui della nostra specie, al parlamento dei nostri istinti, sviluppatisi durante l’evoluzione filogenetica. Lungo questo (...) primo tratto del percorso l’articolo fa riferimento in particolare al pensiero di Konrad Lorenz e della sua scuola. Per altro verso, si seguono le tracce del pensiero etico di Lévinas, soffermandosi su alcuni punti fondamentali: il volto dell’altro, la passività, la responsabilità, al fine di porre in evidenza come tra il filosofo e l’etologo, pur nelle evidenti differenze di linguaggio, di approccio e di orizzonti, siano ravvisabili tratti e conclusioni comuni. Parole chiave: Alterità; Relazione; Istinto; Etica; Responsabilità Autrui: Ethics and anthropology in Lévinas: This paper moves along two seemingly distant paths, that turn out to converge in some significant ways. The first path leads us to the origin of what are often considered the most noble and essentially human principles that regulate our social behaviour, going beyond institutional and conventional norms. This allows us to highlight the deepest and most evolutionarily remote rules of human behaviour, related to our genetic code and instincts, which developed over phylogenetic evolution. As we move along this first path, we pay special attention to the work of Konrad Lorenz and his school. The second path follows the traces of Lévinas’ ethical thought, dwelling on some fundamental issues: the face of the other, passivity, and responsibility, and helps us shed light on some ideas and conclusions that are common to the philosopher and the ethologist, despite their clear differences in language, approach, and horizons. We hope this will show how the insights of each can be used to support of the theories of the other. Keywords: Otherness: relationship; Instinct; Ethics; Responsibility. (shrink)

In this article, we shall study the mechanism of the Shroud body image formation with the help of both natural sciences and religion. The various possibilities can be divided into three groups of hypothesis: the first one is that of the fake, the second is the miracle and the third one of the natural event. The first hypothesis is discarded by the interdisciplinary work of the STURP team. Their results do not support the hypothesis that the blood stains and the (...) body image are due to a forger. In our opinion, even if the Miracle by God is possible, the proposed hypotheses of the supernatural event are theologically unacceptable. So, the natural one remains well supported by the “Ockham’s razor”. Obviously, this last model must be verified by experimental evidence. However, this result is not contrary to the hypothesis that the body image is the one of the Nazarene. (shrink)

As Professor of Theoretical Medicine for Surgeons at Padua University between 1824 and 1849, Giacomini achieved a position of great academic professionalism and prestige, not only in Padua, but throughout Italy and Europe. His fundamental medical thesis became part of the established field of medical practise that existed into the first decades of the 19th century. This thesis, derived directly from a vitalistic concept of biological phenomena, was based on the existence of a 'life force' that is distinct from the (...) forces of physical-chemistry, having its own specific laws, contrary to those of physical-chemistry. Using this concept Giacomini was able to distinguish two causes of death: mechanical illness and dynamic illness. The nosographic and therapeutic beliefs of Giacomini were based on his distinction between the 'mechanical' or 'dynamic' effects of drugs. Giacomini's medical philosophy is the result of an interweaving of scientific theories and metaphysical ideas. The merits and limits of this philosophy must be analysed in the light of modern epistemology to explain why Giacomini was unable to develop fully clinical anatomy. (shrink)