By using some classical reasoning we show that any countably presented formal topology, namely, a formal topology with a countable axiom set, is spatial.

We characterise the collections of infinite binary sequences that, when barred by a set of finite binary sequences, are also barred by a finite subset of such a set.

Abstract.Formal topologies are today an established topic in the development of constructive mathematics. One of the main tools in formal topology is inductive generation since it allows to introduce inductive methods in topology. The problem of inductively generating formal topologies with a cover relation and a unary positivity predicate has been solved in [CSSV]. However, to deal both with open and closed subsets, a binary positivity predicate has to be considered. In this paper we will show how to adapt to (...) this framework the method used to generate inductively formal topologies with a unary positivity predicate; the main problem that one has to face in such a new setting is that, as a consequence of the lack of a complete formalization, both the cover relation and the positivity predicate can have proper axioms. (shrink)

In this paper we show that the usual intuitionistic characterization of the decidability of the propositional function B prop [x : A], i. e. to require that the predicate ∨ ¬ B) is provable, is equivalent, when working within the framework of Martin-Löf's Intuitionistic Type Theory, to require that there exists a decision function ψ: A → Boole such that = Booletrue) ↔ B). Since we will also show that the proposition x = Booletrue [x: Boole] is decidable, we can (...) alternatively say that the main result of this paper is a proof that the decidability of the predicate Bprop [x : A] can be effectively reduced by a function ψ A → Boole to the decidability of the predicate ψ = Booletrue [x : A]. All the proofs are carried out within the Intuitionistic Type Theory and hence the decision function ψ, together with a proof of its correctness, is effectively constructed as a function of the proof of ∨ ¬ B). (shrink)

We prove a generalization of the hyper-game theorem by using an abstract version of inductively generated formal topology. As applications we show proofs for Cantor theorem, uncountability of the set of functions from N to N and Gödel theorem which use no diagonal argument.

This work deals with the exponential fragment of Girard's linear logic without the contraction rule, a logical system which has a natural relation with the direct logic . A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a special treatment of the propositional constants, so that the process of cut-elimination can be performed using only “local” reductions. Hence a typed calculus, which admits only local rewriting rules, can be (...) introduced in a natural manner. Its main properties — normalizability and confluence — has been investigated; moreover this calculus has been proved to satisfy a Curry-Howard isomorphism with respect to the logical system in question. MSC: 03B40, 03F05. (shrink)

Formal topology is today an established topic in the development of constructive mathematics and constructive proofs for many classical results of general topology have been obtained by using this approach. Here we analyze one of the main concepts in formal topology, namely, the notion of formal point. We will contrast two classically equivalent definitions of formal points and we will see that from a constructive point of view they are completely different. Indeed, according to the first definition the formal points (...) of the formal topology of the real numbers can be indexed by a set whereas this is not possible according to the second one. (shrink)

In this short note we show that any proof of a general spatiality theorem for inductively generated formal topologies requires full classical logic. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

We analyze some extensions of Martin-Löf 's constructive type theory by means of extensional set constructors and we show that often the most natural requirements over them lead to classical logic or even to inconsistency.

In this paper we prove that any quantale Q is a quantale of suitable relations on Q. As a consequence two isomorphism theorems are also shown with suitable sets of functions of Q into Q. These theorems are the mathematical background one needs in order to give natural and complete semantics for Linear Logic using relations.

In this paper a proof of the normal form theorem for the closed terms of Girard's system F is given by using a computability method à la Tait. It is worth noting that most of the standard consequences of the normal form theorem can be obtained using this version of the theorem as well. From the proof-theoretical point of view the interest of the proof is that the definition of computable derivation here used does not seem to be well founded. (...) MSC: 03F05, 03B15. (shrink)

In 1996, Krivine applied Friedman's A-translation in order to get an intuitionistic version of Gödel completeness result for first-order classical logic and countable languages and models. Such a result is known to be intuitionistically underivable 559), but Krivine was able to derive intuitionistically a weak form of it, namely, he proved that every consistent classical theory has a model. In this paper, we want to analyze the ideas Krivine's remarkable result relies on, ideas which where somehow hidden by the heavy (...) formal machinery used in the original proof. We show that the ideas in Krivine's proof can be used to intuitionistically derive some crucial mathematical results, which were supposed to be purely classical up to now: the Ultrafilter Theorem for countable Boolean algebras, and the maximal ideal theorem for countable rings. (shrink)

We present and study the category of formal topologies and some of its variants. Two main results are proven. The first is that, for any inductively generated formal cover, there exists a formal topology whose cover extends in the minimal way the given one. This result is obtained by enhancing the method for the inductive generation of the cover relation by adding a coinductive generation of the positivity predicate. Categorically, this result can be rephrased by saying that inductively generated formal (...) topologies are coreflective into inductively generated formal covers. The second result is that unary formal covers are exponentiable in the category of inductively generated formal covers and hence, thanks to the coreflection, unary formal topologies are exponentiable in the category of inductively generated formal topologies. From a localic point of view the exponentiability of unary formal topologies means that algebraic dcpos are exponentiable in the category of open locales. But, the coreflection theorem states that open locales are coreflective in locales and hence, as a consequence of well-known impredicative results on exponentiable locales, it allows to prove that locally compact open locales are exponentiable in the category of open locales. (shrink)

An intuitionistic version of Cantor's theorem, which shows that there is no surjective function from the type of the natural numbers N into the type N → N of the functions from N into N, is proved within Martin-Löf's Intuitionistic Type Theory with the universe of the small types.

In this paper we analyze an extension of Martin-Löf s intensional set theory by means of a set contructor P such that the elements of P are the subsets of the set S. Since it seems natural to require some kind of extensionality on the equality among subsets, it turns out that such an extension cannot be constructive. In fact we will prove that this extension is classic, that is “ true holds for any proposition A.

In this paper we propose an approach to vagueness characterised by two features. The first one is philosophical: we move along a Kantian path emphasizing the knowing subject’s conceptual apparatus. The second one is formal: to face vagueness, and our philosophical view on it, we propose to use topology and formal topology. We show that the Kantian and the topological features joined together allow us an atypical, but promising, way of considering vagueness.

We propose a formal representation of objects , those being mathematical or empirical objects. The powerful framework inside which we represent them in a unique and coherent way is grounded, on the formal side, in a logical approach with a direct mathematical semantics in the well-established field of constructive topology, and, on the philosophical side, in a neo-Kantian perspective emphasizing the knowing subject’s role, which is constructive for the mathematical objects and constitutive for the empirical ones.

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 provide a new and elementary proof of strong normalization for the lambda calculus of intersection types. It uses no strong method, like for instance Tait-Girard reducibility predicates, but just simple induction on type complexity and derivation length and thus it is obviously formalizable within first order arithmetic. To obtain this result, we introduce a new system for intersection types whose rules are directly inspired by the reduction relation. Finally, we show that not only the set of strongly normalizing terms (...) of pure lambda calculus can be characterized in this system, but also that a straightforward modification of its rules allows to characterize the set of weakly normalizing terms. (shrink)

This article provides a conceptual map of the debate on ideal and non‐ideal theory. It argues that this debate encompasses a number of different questions, which have not been kept sufficiently separate in the literature. In particular, the article distinguishes between the following three interpretations of the ‘ideal vs. non‐ideal theory’ contrast: (i) full compliance vs. partial compliance theory; (ii) utopian vs. realistic theory; (iii) end‐state vs. transitional theory. The article advances critical reflections on each of these sub‐debates, and highlights (...) areas for future research in the field. (shrink)

Following a Weltanschaaung that involves a concept of life, Hitler has organized one of central chapiters of his autobiography My Struggle, named “Nation and Race”. Three human groups – to know, the founders of culture, the bearers of culture, the destroyers of culture – would be organized as forms of life. These three groups cohabit in competition for the territory of living space. With Hitler´s interpretations, come up then a living economic, that justifies the Total State or the Total War. (...) In front of this horizon, appear critiques as Marcuse, which efforts intend to face the usurpation of concepts as life, nature and racionality by Nazi myth of race and nation. Into this field, Marcuse meets psychoanalysis. Someone considers this meeting as a return to some naturalism too far from the critical exigencies of this time; however, it is possible to insist that this resourse to Freud makes evident a straight critic to a living economic operated from a totalitarian Weltanschauung. (shrink)

This paper explores how some Italian HR managers narrate the changes imposed by the COVID-19 threat in the workplace. Events since December 2019 have presented exceptional circumstances to which HR managers have reacted in very different ways. This study explored how HR managers came to introduce organizational changes aimed at coping with the emergency, as well as how employees were involved in those organizational changes. The article is based on a thematic analysis of some interviews with Italian HR managers whose (...) companies decided to switch working from home on a massive scale. We wanted to offer some reflections on the actions taken by a few HR managers and Italian companies to keep working at a time when most workers were forced to respect the lockdown. (shrink)

In his recent bookThe Idea of Justice, Amartya Sen suggests that political philosophy should move beyond the dominant, Rawls-inspired, methodological paradigm – what Sen calls ‘transcendental institutionalism’ – towards a more practically oriented approach to justice: ‘realization-focused comparison’. In this article, I argue that Sen's call for a paradigm shift in thinking about justice is unwarranted. I show that his criticisms of the Rawlsian approach are either based on misunderstandings, or correct but of little consequence, and conclude that the Rawlsian (...) approach already delivers much of what Sen himself wants from a theory of justice. (shrink)

Principles of distributive justice bind macro-level institutional agents, like the state. But what does justice require in non-ideal circumstances, where institutional agents are unjust or do not e...

We show that some common varieties of modal K4-algebras have finitary unification type, thus providing effective best solutions for equations in free algebras. Applications to admissible inference rules are immediate.

We show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.

Which standards should we employ to evaluate the global order? Should they be standards of justice or standards of legitimacy? In this article, I argue that liberal political theorists need not face this dilemma, because liberal justice and legitimacy are not distinct values. Rather, they indicate what the same value, i.e. equal respect for persons, demands of institutions under different sets of circumstances. I suggest that under real-world circumstances – characterized by conflicts and disagreements – equal respect demands basic-rights protection (...) and democratic participation, which I here call ‘political justice’. I conclude the article by considering three possible configurations of the global order – the ‘democratic world-state’, ‘independent democratic states’, and ‘mixed’ models – and argue that a commitment to political justice speaks in favour of the latter. (shrink)

A life without liberty and material resources is not a good life. Equally, a life devoid of meaningful social relationships—such as friendships, family attachments, and romances—is not a good life. From this it is tempting to conclude that just as individuals have rights to liberty and material resources, they also have rights to access meaningful social relationships. I argue that this conclusion can be defended only in a narrow set of cases. ‘Pure’ social relationship deprivation—that is, deprivation that is not (...) caused, or accompanied, by deficits in liberties and material resources— mostly generates demands of private beneficence. I suggest that social relationship deprivation is unjust, hence a rights violation, only when it is due to factors—such as one’s race—that are irrelevant to one’s being a good participant in social relationships. I thus conclude that access to meaningful social relationships is not a fundamental concern for theories of justice. (shrink)

This article suggests developing the concept of spiritual ecology into that of balanced spiritual ecosystems. Philosophies, theologies, education systems, political parties, and gender-based and ethnic identity politics need to be critiqued both from within and without so that they can finally contribute to the creation, maintenance and flourishing of balanced spiritual ecosystems.Contribution: Spiritual ecology is a concept on which converge different worldviews. This article recommends using balanced spiritual ecosystems, instead. The new concept could provoke further reflection on how our -ontologies (...) and communities co-exist and whether they do it organically and spiritually. This article befits HTS’s interest in ‘theology and nature’. (shrink)

Heideggers Kritik am Nationalsozialismus ist vor allem ab 1963 greifbar in Vorträgen, Vorlesungen (zu Nietzsche) und den "Beiträgen zur Philosophie". Entgegen Thesen der jüngsten Heidegger-Kontroverse hat sich Heidegger nach einer Phase der falschen politischen Besetzung seiner Philosophie im Jahre 1933 vor allem ab 1936 von der Bewegung des Nationalsozialismus gelöst. Er begreift den Nationalsozialismus zunehmend klar als eine Erscheinungsform des Nihilismus, der "Seinsverlassenheit" und des Herrschaftsdenkens des reinen "Willens zur Macht". Dabei geht Heideggers subtile philosophische Kritik des Nationalsozialismus über in (...) eine Kritik der neuzeitlichen Technologie als einer sich fortsetzenden Form planetarischen Herrschaftsdenkens und der Ausbeutung der Erde durch den Menschen. (shrink)

Summary Although by the mid-eighteenth century colonial American makers of mathematical instruments were producing many of the scientific instruments required in the British Colonies of North America for surveying and navigation, it was not until after the first quarter of the nineteenth century that American makers had the capability to produce sophisticated precision optical instruments for astronomy and microscopy. Until then, these had to be imported from overseas, chiefly England, at considerable cost and after long delays. Included among them were (...) historically important instruments required for establishing provincial and territorial boundaries, and for making astronomical observations. Although generally treated with the utmost care while in use, eventually one after another was misplaced, lost, destroyed by fire, or, in one instance, carefully hidden away then forgotten until it was discovered more than a century later. (shrink)