-
What is a monoid?
Authors:
Paul Blain Levy,
Morgan Rogers
Abstract:
In many situations one encounters a notion that resembles that of a monoid. It consists of a carrier and two operations that resemble a unit and a multiplication, subject to three equations that resemble associativity and left and right unital laws. The question then arises whether this notion in fact that of a monoid in a suitable sense. Category theorists have answered this question by providing…
▽ More
In many situations one encounters a notion that resembles that of a monoid. It consists of a carrier and two operations that resemble a unit and a multiplication, subject to three equations that resemble associativity and left and right unital laws. The question then arises whether this notion in fact that of a monoid in a suitable sense. Category theorists have answered this question by providing a notion of monoid in a monoidal category, or more generally in a multicategory. While this encompasses many examples, it is unsuitable in other cases, such as the notion of relative monad, and the modelling of call-by-push-value sequencing. In each of these examples, the leftmost and/or the rightmost factor of a multiplication or associativity law seems to be distinguished. To include such examples, we generalize the multicategorical framework in two stages. Firstly, we move to the framework of a left-skew multicategory (due to Bourke and Lack), which generalizes both multicategory and left-skew monoidal category. The notion of monoid in this framework encompasses examples where only the leftmost factor is distinguished, such as the notion of relative monad. Secondly, we consider monoids in the novel framework of a bi-skew multicategory. This encompasses examples where both the leftmost and the rightmost factor are distinguished, such as the notion of a category on a span, and the modelling of call-by-push-value sequencing. In the bi-skew framework (which is the most general), we give a coherence result saying that a monoid corresponds to an unbiased monoid, i.e. a map from the unit bi-skew multicategory.
△ Less
Submitted 16 April, 2025;
originally announced April 2025.
-
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.
-
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 AC (the axiom of choice), or at least the weak version known as WISC (Weakly Initial Set of Covers),…
▽ 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 AC (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. Assuming AC or WISC, 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 23 March, 2025; v1 submitted 5 January, 2021;
originally announced January 2021.
-
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.
-
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.
-
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.