اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدConstructive pointfree topology eliminates non-constructive representation theorems from Riesz space theory
273
0
0.0
(
0
)
تأليف
Bas Spitters
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
In Riesz space theory it is good practice to avoid representation theorems which depend on the axiom of choice. Here we present a general methodology to do this using pointfree topology. To illustrate the technique we show that almost f-algebras are commutative. The proof is obtained relatively straightforward from the proof by Buskes and van Rooij by using the pointfree Stone-Yosida representation theorem by Coquand and Spitters.
قيم البحث
اقرأ أيضاً
We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation theorem for f-algebras. In turn, this theorem implies the Ge
lfand representation theorem for C*-algebras of operators on Hilbert spaces as formulated by Bishop and Bridges. Our proof is shorter, clearer, and we avoid the use of approximate eigenvalues.
We provide a constructive treatment of basic results in the theory of central simple algebras. One main issue is the fact that one starting result, Wedderburns Theorem stating that a simple algebra is a matrix algebra over a skew field, is not constr
uctively valid. We solve this problem by proving instead a dynamical version of this theorem. One can use this to give constructive proofs of basic results of the theory of central simple algebras, such as Skolem-Noether Theorem. We illustrate this development by giving an elementary constructive proof of a theorem of Becher (which is itself a consequence of a celebrated theorem of Merkurjev).
We present a constructive proof of Gelfand duality for C*-algebras by reducing the problem to Gelfand duality for real C*-algebras.
In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a
linear fragment (arena net) and a parallel weakening-contraction fragment (skew fibration). In particular we provide an encoding of modal formulas by means of directed graphs (modal arenas), and an encoding of linear proofs as modal arenas equipped with vertex partitions satisfying topological criteria. The second semantics is given by means of winning innocent strategies of a two-player game over modal arenas. This is given by extending the Heijltjes-Hughes-Stra{ss}burger correspondence between intuitionistic combinatorial proofs and winning innocent strategies in a Hyland-Ong arena. Using our first result, we provide a characterisation of winning strategies for games on a modal arena corresponding to proofs with modalities.
We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive models of univalence, that can then be relativized to any presheaf model
s, and these sheaf models are obtained by localisation for a left exact modality. We provide first an abstract notion of descent data which can be thought of as a higher version of the notion of prenucleus on frames, from which can be generated a nucleus (left exact modality) by transfinite iteration. We then provide several examples.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
