On relation between totality semantic and syntactic validity
Abstract
In this paper, we present a denotational semantic for non-wellfounded proofs of µLL ∞ , linear logic extended with least and greatest fixed points, by adapting the categorical semantics of µLL ∞ [EJ21]. Two instances of this categorical setting are REL (category of sets and relations), and NUTS (category of sets equipped with a notion of totality and relations preserving it) which is studied in [EJ21]. In particular, we relate validity condition for non-wellfounded proofs and totality of NUTS. More precisely, we show each µLL ∞ valid proof will have interpreted as a total element in NUTS.
Origin | Files produced by the author(s) |
---|