solidot新版网站常见问题,请点击这里查看。
消息
本文已被查看4711次
Implicative algebras: a new foundation for realizability and forcing. (arXiv:1802.00528v1 [math.LO])
来源于:arXiv
We introduce the notion of implicative algebra, a simple algebraic structure
intended to factorize the model constructions underlying forcing and
realizability (both in intuitionistic and classical logic). The salient feature
of this structure is that its elements can be seen both as truth values and as
(generalized) realizers, thus blurring the frontier between proofs and types.
We show that each implicative algebra induces a (Set-based) tripos, using a
construction that is reminiscent from the construction of a realizability
tripos from a partial combinatory algebra. Relating this construction with the
corresponding constructions in forcing and realizability, we conclude that the
class of implicative triposes encompass all forcing triposes (both
intuitionistic and classical), all classical realizability triposes (in the
sense of Krivine) and all intuitionistic realizability triposes built from
total combinatory algebras. 查看全文>>