Showing 1–10 of 10 results for author: Levy, P B

The Price of Mathematical Scepticism

Authors: Paul Blain Levy

Abstract: This paper argues that, insofar as we doubt the bivalence of the Continuum Hypothesis or the truth of the Axiom of Choice, we should also doubt the consistency of third-order arithmetic, both the classical and intuitionistic versions. Underlying this argument is the following philosophical view. Mathematical belief springs from certain intuitions, each of which can be either accepted or doubted in… ▽ More This paper argues that, insofar as we doubt the bivalence of the Continuum Hypothesis or the truth of the Axiom of Choice, we should also doubt the consistency of third-order arithmetic, both the classical and intuitionistic versions. Underlying this argument is the following philosophical view. Mathematical belief springs from certain intuitions, each of which can be either accepted or doubted in its entirety, but not half-accepted. Therefore, our beliefs about reality, bivalence, choice and consistency should all be aligned. △ Less

Submitted 25 May, 2022; v1 submitted 27 July, 2021; originally announced July 2021.

Comments: Accepted for publication in Phiilosophia Mathematica. 17 pages plus bibliography

MSC Class: 03A05 03A30

Broad Infinity and Generation Principles

Authors: Paul Blain Levy

Abstract: We introduce Broad Infinity, a new set-theoretic axiom scheme based on the slogan "Every time we construct a new element, we gain a new arity." It says that three-dimensional trees whose growth is controlled by a specified class function form a set. Such trees are called "broad numbers". Assuming the axiom of choice, or at least the weak version known as WISC (Weakly Initial Set of Covers), we s… ▽ More We introduce Broad Infinity, a new set-theoretic axiom scheme based on the slogan "Every time we construct a new element, we gain a new arity." It says that three-dimensional trees whose growth is controlled by a specified class function form a set. Such trees are called "broad numbers". Assuming the axiom of choice, or at least the weak version known as WISC (Weakly Initial Set of Covers), we show that Broad Infinity is equivalent to Mahlo's principle, which says that the class of all regular limit ordinals is stationary. Broad Infinity also yields a convenient principle for generating a subset of a class using a "rubric" (family of rules). This directly gives the existence of Grothendieck universes, without requiring a detour via ordinals. In the absence of choice, Broad Infinity implies that the derivations of elements from a rubric form a set. This yields the existence of Tarski-style universes. Additionally, we reveal a pattern of resemblance between "Wide" principles, that are provable in ZFC, and "Broad" principles, that go beyond ZFC. Note: this paper uses a base theory that is weaker than ZF but includes classical first-order logic and Replacement. △ Less

Submitted 3 August, 2024; v1 submitted 5 January, 2021; originally announced January 2021.

Comments: 61 pages + bibliography

MSC Class: 03E30; 03E25 (Primary) 03E70; 03E55 (Secondary)

A Theory of Particular Sets

Authors: Paul Blain Levy

Abstract: ZFC has sentences that quantify over all sets or all ordinals, without restriction. Some have argued that sentences of this kind lack a determinate meaning. We propose a set theory called TOPS, using Natural Deduction, that avoids this problem by speaking only about particular sets. ZFC has sentences that quantify over all sets or all ordinals, without restriction. Some have argued that sentences of this kind lack a determinate meaning. We propose a set theory called TOPS, using Natural Deduction, that avoids this problem by speaking only about particular sets. △ Less

Submitted 13 June, 2019; v1 submitted 7 May, 2019; originally announced May 2019.

Comments: 12 pages

Formulating Categorical Concepts using Classes

Authors: Paul Blain Levy

Abstract: We examine the use of classes to formulate several categorical notions. This leads to two proposals: an explicit structure for working with subobjects, and a hierarchy of $k$-classes. We apply the latter to both ordinary and higher categories. We examine the use of classes to formulate several categorical notions. This leads to two proposals: an explicit structure for working with subobjects, and a hierarchy of $k$-classes. We apply the latter to both ordinary and higher categories. △ Less

Submitted 26 July, 2018; v1 submitted 25 January, 2018; originally announced January 2018.

Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method (Long Version)

Authors: Ugo Dal Lago, Francesco Gavazzo, Paul Blain Levy

Abstract: We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value $λ$-calculi with algebraic effects. We first of all endow a computational $λ$-calculus with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which… ▽ More We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value $λ$-calculi with algebraic effects. We first of all endow a computational $λ$-calculus with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which applicative bisimilarity is a congruence, thus a sound methodology for program equivalence. This is done by studying Howe's method in the abstract. △ Less

Submitted 15 April, 2017; originally announced April 2017.

Comments: 30 pages

A monad for full ground reference cells

Authors: Ohad Kammar, Paul B. Levy, Sean K. Moss, Sam Staton

Abstract: We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer t… ▽ More We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations. △ Less

Submitted 19 April, 2017; v1 submitted 16 February, 2017; originally announced February 2017.

A Ghost at $ω_1$

Authors: Paul Blain Levy

Abstract: In the final chain of the countable powerset functor, we show that the set at index $ω_1$, regarded as a transition system, is not strongly extensional because it contains a "ghost" element that has no successor even though its component at each successor index is inhabited. The method, adapted from a construction of Forti and Honsell, also gives ghosts at larger ordinals in the final chain of oth… ▽ More In the final chain of the countable powerset functor, we show that the set at index $ω_1$, regarded as a transition system, is not strongly extensional because it contains a "ghost" element that has no successor even though its component at each successor index is inhabited. The method, adapted from a construction of Forti and Honsell, also gives ghosts at larger ordinals in the final chain of other subfunctors of the powerset functor. This leads to a precise description of which sets in these final chains are strongly extensional. △ Less

Submitted 25 July, 2018; v1 submitted 30 December, 2016; originally announced December 2016.

MSC Class: 03E75

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 3 (July 26, 2018) lmcs:2626

Coproducts of Monads on Set

Authors: Jiří Adámek, Nathan Bowler, Paul B. Levy, Stefan Milius

Abstract: Coproducts of monads on Set have arisen in both the study of computational effects and universal algebra. We describe coproducts of consistent monads on Set by an initial algebra formula, and prove also the converse: if the coproduct exists, so do the required initial algebras. That formula was, in the case of ideal monads, also used by Ghani and Uustalu. We deduce that coproduct embeddings of c… ▽ More Coproducts of monads on Set have arisen in both the study of computational effects and universal algebra. We describe coproducts of consistent monads on Set by an initial algebra formula, and prove also the converse: if the coproduct exists, so do the required initial algebras. That formula was, in the case of ideal monads, also used by Ghani and Uustalu. We deduce that coproduct embeddings of consistent monads are injective; and that a coproduct of injective monad morphisms is injective. Two consistent monads have a coproduct iff either they have arbitrarily large common fixpoints, or one is an exception monad, possibly modified to preserve the empty set. Hence a consistent monad has a coproduct with every monad iff it is an exception monad, possibly modified to preserve the empty set. We also show other fixpoint results, including that a functor (not constant on nonempty sets) is finitary iff every sufficiently large cardinal is a fixpoint. △ Less

Submitted 11 September, 2014; originally announced September 2014.

Comments: Presented at the conference "27th Annual Symposium on Logic in Computer Science (LICS 2012)". The current version contains proofs of some of the results in the appendix

Exploring the Boundaries of Monad Tensorability on Set

Authors: Nathan Bowler, Sergey Goncharov, Paul Blain Levy, Lutz Schröder

Abstract: We study a composition operation on monads, equivalently presented as large equational theories. Specifically, we discuss the existence of tensors, which are combinations of theories that impose mutual commutation of the operations from the component theories. As such, they extend the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts;… ▽ More We study a composition operation on monads, equivalently presented as large equational theories. Specifically, we discuss the existence of tensors, which are combinations of theories that impose mutual commutation of the operations from the component theories. As such, they extend the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We present two main results: we show that the tensor of two monads need not in general exist by presenting two counterexamples, one of them involving finite powerset (i.e. the theory of join semilattices); this solves a somewhat long-standing open problem, and contrasts with recent results that had ruled out previously expected counterexamples. On the other hand, we show that tensors with bounded powerset monads do exist from countable powerset upwards. △ Less

Submitted 17 September, 2013; v1 submitted 9 September, 2013; originally announced September 2013.

Journal ref: Logical Methods in Computer Science, Volume 9, Issue 3 (September 18, 2013) lmcs:740

Proceedings Fourth Workshop on Mathematically Structured Functional Programming

Authors: James Chapman, Paul Blain Levy

Abstract: This volume contains the proceedings of the Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012), taking place on 25 March, 2012 in Tallinn, Estonia, as a satellite event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012. MSFP is devoted to the derivation of functionality from structure. It highlights concepts from algebra, semantic… ▽ More This volume contains the proceedings of the Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012), taking place on 25 March, 2012 in Tallinn, Estonia, as a satellite event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012. MSFP is devoted to the derivation of functionality from structure. It highlights concepts from algebra, semantics and type theory as they are increasingly reflected in programming practice, especially functional programming. The workshop consists of two invited presentations and eight contributed papers on a range of topics at that interface. △ Less

Submitted 10 February, 2012; originally announced February 2012.

ACM Class: D.3.3; F.3.3

Journal ref: EPTCS 76, 2012