5.5. Every topos is linguistic: the equivalence theorem.

Alongside the analogy between maximal ideals and complete theories, the Jacobson radical carries over from ideals of commutative rings to theories of propositional calculi. This prompts a variant of Lindenbaum’s Lemma that relates classical validity and intuitionistic provability, and the syntactical counterpart of which is Glivenko’s Theorem. The Jacobson radical in fact turns out to coincide with the classical deductive closure. As a by-product we obtain a possible interpretation in logic of the axioms-as-rules conservation criterion for a multi-conclusion Scott-style entailment (...) relation over a single-conclusion one. (shrink)

The topic of this article is the formal topology abstracted from the Zariski spectrum of a commutative ring. After recollecting the fundamental concepts of a basic open and a covering relation, we study some candidates for positivity. In particular, we present a coinductively generated positivity relation. We further show that, constructively, the formal Zariski topology cannot have enough points.

This paper provides a constructive topological semantics for non-deducibility of a first order intuitionistic formula. Formal topology theory, in particular the recently introduced notion of a binary positivity predicate, and co-induction are two needful tools.

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.

Entailment relations, introduced by Scott in the early 1970s, provide an abstract generalisation of Gentzen’s multi-conclusion logical inference. Originally applied to the study of multi-valued logics, this notion has then found plenty of applications, ranging from computer science to abstract algebra. In particular, an entailment relation can be regarded as a constructive presentation of a distributive lattice and in this guise it has proven to be a useful tool for the constructive reformulation of several classical theorems in commutative algebra. In (...) this paper, motivated by these concrete applications, we state and prove a cut-elimination result for inductively generated entailment relations. We analyse some of its consequences and describe the existing connections with analogous results in the literature. (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.