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)

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)

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)

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)

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)

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

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

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)

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.

Many philosophers have been attracted to the idea of using the logical form of a true sentence as a guide to the metaphysical grounds of the fact stated by that sentence. This paper looks at a particular instance of that idea: the widely accepted principle that disjunctions are grounded in their true disjuncts. I will argue that an unrestricted version of this principle has several problematic consequences and that it’s not obvious how the principle might be restricted in order to (...) avoid them. My suggestion is that, instead of trying to restrict the principle, we should distinguish between metaphysical and conceptual grounds and take the principle to apply exclusively to the latter. This suggestion, if correct, carries over to other prominent attempts at using logical form as a guide to ground. (shrink)

Objet d'une captation indue par une certaine extrême gauche, l'écologie a été très souvent délaissée par la droite radicale européenne, dont la phobie envers l'écologauchisme l'a poussée à oublier une part pourtant essentielle de son propre héritage. Réunissant deux essais qui abordent la même problématique sous des angles différents, cet ouvrage est donc aussi une redécouverte d'un continent englouti. Dans le sillage de l'oeuvre de Julius Evola, Giovanni Monastra rappelle le caractère empathique et holistique de l'approche traditionnelle de la (...) nature, par opposition à l'approche moderne, exclusivement tournée vers l'utile et l'exploitable, et qui finit par considérer l'homme lui-même comme un cobaye. Il réaffirme, conformément à la parole d'Héraclite ("Il faut éteindre la démesure"), que la mentalité prométhéenne ou faustienne est foncièrement incompatible avec le païen "sens de la Terre" cher à Nietzsche. En tant qu'elle respecte certaines "limites", la véritable écologie relève fondamentalement de l'esprit de conservation et d'une forme de conservatisme, ainsi que s'attache à le démontrer Philippe Baillet dans une étude qui fait une très large place aux sources allemandes de l'écologie, du romantisme au biocentrisme de Ludwig Klages et de certains nationaux-socialistes, en passant par le mouvement völkisch et ses prolongements jusqu'à nos jours. Parce qu'il lie de manière indissociable défense de l'environnement, défense des espèces animales et défense du pays natal (Heimat), l'écologisme conservateur allemand s'est voulu, dès l'origine, identitaire. Il s'est agi ici de poser les premiers jalons théoriques, dans l'espace francophone, de la redéfinition d'une écologie profonde nourrie par l'immémoriale piété indo-européenne pour le cosmos. (shrink)

There are two intuitions about time. The first is that there's something special about the present that objectively differentiates it from the past and the future. Call this intuition Specialness. The second is that the time at which we happen to live is just one among many other times, all of which are ‘on a par’ when it comes to their forming part of reality. Call this other intuition Egalitarianism. Tradition has it that the so-called ‘A-theories of time’ fare well (...) at addressing the first intuition, but rather badly when it comes to the second. The goal of this article is to offer advice to A-theorists about how to reconcile their view with Egalitarianism. (shrink)

Solving the meta-problem of consciousness requires, among other things, explaining why we are so reluctant to endorse various forms of illusionism about the phenomenal. I will try to tackle this task in two steps. The first consists in clarifying how the concept of consciousness precludes the possibility of any distinction between 'appearance' and 'reality'. The second consists in spelling out our reasons for recognizing the existence of something that satisfies that concept.

The first essay is one of the most influential papers ever written on Lonergan; it and the second one inquire into the notion of the a priori. The third essay presents a detailed analysis of Kantian intuitionism and contrasts it with the 'knowledge as structure' position of Lonergan's critical realism. In this essay intuitionism is generalized, to allow Sala to address representatives of neoscholasticism as well. The argument with neoscholasticism continues in the fourth essay.

This paper defends the view that one's own mental states are metaphysically privileged vis-à-vis the mental states of others, even if only subjectively so. This is an instance of a more general view called Subjectivism, according to which reality is only subjectively the way it is. After characterizing Subjectivism in analogy to two relatively familiar views in the metaphysics of modality and time, I compare the Subjectivist View of the Mental with Egocentric Presentism, a version of Subjectivism recently advocated by (...) Caspar Hare. I argue that the Subjectivist View of the Mental goes a considerable way towards solving certain long-standing philosophical puzzles having to do with the unity of consciousness, the contents of self-awareness and the intransmissibility of experiential knowledge through testimony. (shrink)

Ecological-enactive approaches to cognition aim to explain cognition in terms of the dynamic coupling between agent and environment. Accordingly, cognition of one’s immediate environment (which is sometimes labeled “basic” cognition) depends on enaction and the picking up of affordances. However, ecological-enactive views supposedly fail to account for what is sometimes called “higher” cognition, i.e., cognition about potentially absent targets, which therefore can only be explained by postulating representational content. This challenge levelled against ecological-enactive approaches highlights a putative explanatory gap between (...) basic and higher cognition. In this paper, we examine scientific cognition—a paradigmatic case of higher cognition—and argue that it shares fundamental features with basic cognition, for enaction and affordance selection are central to the scientific enterprise. Our argument focuses on modeling, and on how models promote scientific understanding. We base our argument on a non-representational account of scientific understanding and on the material engagement theory, for models are hereby conceived as material objects designed for scientific engagements. Having done so, we conclude that the explanatory gap is significantly less threatening to the ecological-enactive approach than it might appear. (shrink)

Computational systems are traditionally approached from control-oriented perspectives; however, as soon as we move from centralized to decentralized computational infrastructures, direct control needs to be replaced by distributed coordination mechanisms that are on par with institutional constructs observable in human societies (contracts, agreements, enforcement mechanisms, etc.). This paper presents a formalization of Hohfeld's framework building upon a logic whose language includes primitive operators of ability and parametric deontic operators. The proposal is meant to highlight the fundamental interaction between deontic and (...) potestative concepts and contains proofs of soundness and completeness with respect to a class of relational models. (shrink)

Assuming a radical stance on embodied cognition, according to which the information ac- quired through basic cognitive processes is not contentful (Hutto and Myin, 2013), and as- suming that perception is a source of rationally grounded knowledge (Pritchard, 2012), a pluralistic account of perceptual knowledge is developed. The paper explains: (i) how the varieties of perceptual knowledge fall under the same broader category; (ii) how they are subject to the same kind of normative constraints; (iii) why there could not be (...) a conflict between the different varieties of perceptual knowledge; and (iv) why the traditional episte- mological inquiry is inclined to overestimate the role of propositional perceptual knowledge. (shrink)