Sheaves of Structures, Heyting-Valued Structures, and a Generalization of Łoś's Theorem

An open mapping theorem for finitely copresented Esakia spaces

We prove an open mapping theorem for the topological spaces dual to finitely presented Heyting algebras. This yields in particular a short, self-contained semantic proof of the uniform interpolation theorem for intuitionistic propositional logic, first proved by Pitts in 1992. Our proof is based on the methods of Ghilardi & Zawadowski. However, our proof does not require sheaves nor games, only basic duality theory for Heyting algebras.

具有稳定性的拓扑强制语义

Topological Forcing Semantics with Settling

人们很早就意识到拓扑可以模拟构造性系统，因为开集形成了海廷代数。在以布尔值模型的形式发展了强迫之后，很明显，就像在ZF上任何布尔值模型也满足ZF一样，海廷值模型也满足IZF，它代表直觉ZF，ZF公理的最直接的建设性改造。在本文中，我们回到拓扑结构，并介绍了一个变体模型，以及相应的修订强迫或满意度关系。目的是证明与幂集公理弱化有关的独立性结果。最初的动机是早期的工作，基于实数的集合，这表明在CZF减去子集集合的上下文中，指数化不足以证明戴德金实数形成一个集合。当前的语义是将该模型从R推广到任意拓扑空间。它的研究，集理论的原则，在这样的模型一般。此外，底层拓扑空间的自然属性表明，这意味着更强的这些原则的有效性。

自由代数、合并与多值逻辑的Vaught定理

Free algebras, amalgamation, and a theorem of Vaught for many valued logics

我们研究了自由代数的原子性，BL代数和MV代数的各种形式的合并，以及Heyting代数的原子性，尽管后者代数可能不是线性序的，所以严格地说，它们对应的直觉主义逻辑不属于多值逻辑。推广了Comer在经典一阶情形下证明的结果，给出了定义在这类代数的素谱上的Zarski拓扑的层对偶，推导出了几个可定义性定理，并得到了作为层连续截面的理论的表示定理.我们还证明了一个省略类型定理的模糊逻辑，并制定和证明其后果（在经典模型论）适应我们的情况下，这与存在性和唯一性的总理和原子模型。

有界分配格作为层连续截面的表示

Representations of bounded distributive lattices as the continuous sections of Sheaves based on the Priestly and Zarski topologies

利用Comer关于柱形代数的层对偶理论，给出了分配有界格按模态（分布在联上的函数）扩张为层的连续截面的一个表示定理.我们的表示是通过一个反变函子定义的。我们给应用程序的多值逻辑逻辑和各种修改的一阶逻辑和多模态逻辑，设置在一个代数框架。

关于伪 sheaf 模型论的一些贡献

Some contributions to presheaf model theory

本文通过改进sheaf模型论的术语解释和保持结果，证明了相关范畴在AECats框架中的包含性。

Paraconsistent models of Zermelo-Fraenkel set theory

In this paper, we build Fidel-structures valued models following the methodology developed for Heyting-valued models; recall that Fidel structures are not algebras in the universal algebra sense. Taking models that verify Leibniz law, we are able to prove that all set-theoretic axioms of ZF are valid over these models. The proof is strongly based on the existence of paraconsistent models of Leibniz law. In this setting, the difficulty of having algebraic paraconsistent models of law for formulas with negation using the standard interpretation map is discussed, showing that the existence of mod…