Abstract. Solovay defined the inner model in the context of by using it to define the supercompactness measure on naturally given by . Solovay speculated that stronger versions of this inner model should exist, corresponding to stronger versions of the measure . Woodin, in his unpublished work, defined which is arguably the ultimate version of the supercompactness measure that Solovay had defined. I will talk about in the context of and the axiom .

The event will be followed by another talk on the subject of extensions of the axiom of determinacy. Douglas Blue, from the University of Pittsburgh, will talk about The iterability problem and the transfinite generalization of AD for the Logic Seminar at the Mathematical Institute at 5PM in the lecture room L3.

• P. Antonino, A. Derek, and W. A. Wołoszyn, “Flexible remote attestation of pre-snp sev vms using sgx enclaves,” Ieee access, vol. 11, pp. 90839-90856, 2023.
  [Bibtex]

  @article{Antonino-Derek-Woloszyn23:Flexible-remote-attestation-of-pre-SNP-SEV-VMs-using-SGX-enclaves,
  author={Antonino, Pedro and Derek, Ante and Wołoszyn, Wojciech Aleksander},
  journal={IEEE Access},
  title={Flexible Remote Attestation of Pre-SNP SEV VMs Using SGX Enclaves},
  year={2023},
  volume={11},
  number={},
  pages={90839-90856}}

Abstract. We propose a protocol that explores a synergy between two TEE implementations: it brings SGX-like remote attestation to SEV VMs. We use the notion of a trusted guest owner, implemented as an SGX enclave, to deploy, attest, and provision an SEV VM. This machine can, in turn, rely on the trusted owner to generate SGX-like attestation proofs on its behalf. Our protocol combines the application portability of SEV with the flexible remote attestation of SGX. We formalise our protocol and prove that it achieves the intended guarantees using the Tamarin prover. Moreover, we develop an implementation for our trusted guest owner together with example SEV machines, and put those together to demonstrate how our protocol can be used in practice; we use this implementation to evaluate our protocol in the context of creating accountable machine-learning models. We also discuss how our protocol can be extended to provide a simple remote attestation mechanism for a heterogeneous infrastructure of trusted components.

Find the article at The Blockhouse Technology Limited and access the source code at GitHub.

• P. Antonino, A. Derek, and W. A. Wołoszyn, “Flexible remote attestation of pre-snp sev vms using sgx enclaves,” Ieee access, vol. 11, pp. 90839-90856, 2023.
  [Bibtex]

  @article{Antonino-Derek-Woloszyn23:Flexible-remote-attestation-of-pre-SNP-SEV-VMs-using-SGX-enclaves,
  author={Antonino, Pedro and Derek, Ante and Wołoszyn, Wojciech Aleksander},
  journal={IEEE Access},
  title={Flexible Remote Attestation of Pre-SNP SEV VMs Using SGX Enclaves},
  year={2023},
  volume={11},
  number={},
  pages={90839-90856}}

From Mishap to Marvel: The Unintended Discovery

Let me start with some history. The story begins with a big announcement of a (false) theorem that Joel David Hamkins and I proved (we thought we did but we did not).

Just before a formal announcement at an event in Amsterdam, Joel found a flaw in our argument. But the “great news” have remained on the slides online. And so a MathOverflow thread ensued, where Joel finally published a retraction. This has left everyone with an open question: for what upper bound on the modal validities do buttons actually suffice? Ultimately, at the beginning of my DPhil at the University of Oxford, I showed that the answer is Grz.2. I presented the result at the National University of Singapore in 2022, and additionally shared some details on MathOverflow beforehand.

The draft of the paper I am presenting to you today is key in demonstrating that buttons are sufficient for the upper bounds to be Grz.2. It includes a proof of this fact for propositional Kripke models. The relevant arguments are easily adaptable to the case of any arbitrary potentialist system or a Kripke category, with details appearing in my pre-print The modal theory of the category of sets.

The Grzegorczyk axiom

At first glance, the Grz axiom is very scary. It says that if always it is the case that if always we have that p implies that always p, then p, then p.

However, I provide an easy understanding of the axiom by introducing the concept of penultimacy of p: the truth-value of p is false but if it ever flips, it will never flip again—thus staying necessarily true from that point on. The Grzegorczyk axiom simply says that p is either true or possibly penultimate.

The modal logic Grz.2

The modal logic Grz.2 is the smallest normal modal logic that contains the axiom Grz and the axiom .2, which says that everything that is possibly necessary is also necessarily possible.

Abstract. The article offers an accessible exposition of the Grzegorczyk axiom and provides a new characterization of the modal logic Grz.2, establishing that it is complete for the set of finite Boolean algebras. Thereby, it enhances the utility of the control statement technique of establishing upper bounds on the modal validities of a potentialist system [HL08; HL19; HW20].

Update

The article will be published on my blog soon again in a revised and expanded form, under a new title.

What are the propositional modal validities of group theory?

The reader who is closely acquainted with my work will realize that this inquiry was a subject of my 2019 research, during my time as a Recognised Student under the supervision of Professor Joel David Hamkins at the Faculty of Philosophy, University of Oxford.

And so, given my inclination to ponder mathematics with enthusiasm but sometimes delay in documenting it systematically (though I guess I am in a good company considering that the results of Berger, Block, and Löwe date back to 2015), and the multitude of inquiries I have received regarding the propositional modal validities of groups, I have decided to offer a preview of this segment of my work ahead of releasing the entire preprint.

Let’s commence with the foundation:

We define that a group satisfies the assertion ◇ϕ if it can be embedded in a larger group where ϕ holds (and □ϕ if ϕ is true in all such groups).

A group validates a propositional modal assertion ϕ(p₀, p₁, …, pₙ) if, for all substitution instances pᵢ ↦ ψᵢ in the language of groups, the resulting assertion ϕ(ψ₀, ψ₁, …, ψₙ) holds true in that group.

The propositional modal theory of interest today is known as S4.2, and it is defined as the smallest propositional modal theory containing the axioms for S4.2, which are:

1. □p → p
2. □p → □□p
3. ◇□p → □◇p,

and that is closed under modus ponens, substitution, and necessitation (□).

Lemma. Every group validates the propositional modal theory S4.2.

Proof. Based on the work of Hamkins and Löwe (with a minor correction in Hamkins and Wołoszyn), a commuting directed system of L-structures validates the propositional modal theory S4.2. It’s evident that the cone above any group G, that is the cocone of G, forms such a commuting directed system. Indeed, a free product with amalgamation of a pair of overgroups over any group within the cone remains within the cone. Furthermore, the definition of the product ensures that the diagram formed by these groups and their embeddings commute.

Dealing with the lower bounds was straightforward. The real challenge lay in determining the upper bounds on propositional modal validities, which was the essence of Berger, Block, and Löwe’s question. In particular, a crucial result by Hamkins and Löwe underpins this problem.

Lemma. Suppose M belongs to a family of L-structures in a common first-order language L. If M admits arbitrarily large families of independent buttons independent of arbitrarily long dials, then the propositional modal validities of M constitute precisely the propositional modal theory S4.2.

I should clarify what buttons and dials are and what it means to be independent. Buttons and dials are control statements, a technology used by a multiverse traveler to control the modal nature of a world they are about to visit. In our context, of groups, an unpushed button is an assertion not yet true in a given group but becomes true in some overgroup and all subsequent groups that extend it. Once such a button becomes necessarily true, it is considered pushed. On the other hand, a dial is a list of assertions dᵢ where exactly one assertion is true in any given group within the cone above the base group, but for any other assertion on the list, there is always an overgroup where it becomes true. Control statements are independent if their underlying assertions do not interfere with one another. For instance, buttons are independent of each other and independent of a dial if one can push a selected subset of buttons and set the dial value to any assertion dᵢ without interfering with other buttons.

Theorem. Suppose G is a group. The propositional modal validities of G precisely constitute the propositional modal theory S4.2.

Proof. The lower bound on the propositional modal validities follows from the lemma. To complete the proof, we must establish the existence of an arbitrarily large family of independent buttons independent of an arbitrarily long dial. The choice of buttons is straightforward: we take assertions bₙ expressing the existence of an element of order n, where n is the nth prime number. For the dial, let dᵢ state that the group’s center has size m, where m is much larger than any of the primes used for the buttons. We can introduce as many distinct values of m as needed, modifying the last dᵢ to be the negation of the disjunction of the former ones. It’s clear that each bₙ constitutes a button since once an element of a given order exists, it continues to exist in all overgroups. Moreover, there is no interference with the dial if we realize bₙ by embedding the base group G in the group (G ⊕ Cₚ). Similarly, dᵢs form a dial that does not interfere with the buttons, as witnessed by the embeddings G ↦ Cᵢ ⊕ (G*Z). This concludes the proof.

Since the argument applies regardless of the choice of G, we deduce the following corollary.

Corollary. The propositional modal validities of groups precisely constitute the propositional modal theory S4.2.

Let me end the post by noting that there exist individual groups that validate more than S4.2, a topic I delve into further in my upcoming paper.

Abstract. The resurrection principle (RP) asserts that, in each forcing extension, all true assertions with real parameters retain their forceability throughout subsequent forcing extensions. This property exhibits deep connections with set-theoretic geology, the modal logic of forcing, and inner model theory. I will discuss classical and more recent results on RP, as well as its natural refinements.

I shall explore Kripke categories—extensions of concrete categories that incorporate natural modal semantics, offering a fresh lens for the analysis of categories through modal logic. Central to my analysis will be a comprehensive examination of the archetypical category of sets, taking into account various naturally occurring classes of morphisms and elucidating their intrinsic propositional modal validities. Through this exploration, I hope to highlight the intriguing connections between category theory, model theory, and modal logic, opening doors for new thoughts and discussions in these fields.

If time permits, I shall sketch a proof of the failure of necessary -resurrection.

Abstract. Usuba proved that the mantle is a ground in the presence of an extendible cardinal. And by a recent result of Goldberg, this large cardinal hypothesis cannot be weakened. But my recent work (in progress) on resurrection principles suggests that, at heart, Usuba’s theorem is not about consistency strength. This is a project supervised by W. Hugh Woodin.

(Edited on 12 March to fix a typo.)

Abstract. One of the central incentives of the rise of category theory was to understand a mathematical structure in the context of a family of structures of a similar kind, allowing one to understand how these structures are interrelated. Nearly eight decades later, the modal model theory was introduced, with precisely that same intention in mind, albeit a completely different approach. I shall now provide a framework that unifies the two perspectives.

Let me illustrate the problem by means of an example. I am a human and shall remain as such for the rest of my life. But is it still true once I pass away? Admittedly, being human is something one cannot attribute to an inanimate object. There is a related and much more challenging question, however. Namely, am I still myself after I am gone? It is that latter question that I shall focus on.

For a logician, what is at stake is the truth value of the atomic assertion Of course, it is true; it is a tautology!—one might say. This position seems unsatisfactory and ill-founded, for it is solely based on our shared experience with syntax and semantics to date. Instead, I should like to propose a resolution adopted from my work on modal logic with actuality. Ultimately, I aim to convince the reader that the assertion is seldom true.

It is instructive to look at a corner case first. In a world with no individuals, the sentence is false, simply because there is no one to assert about. Therefore, the statement is true just in case the world cannot become uninhabited. On the other hand, is a necessary truth, which underscores (i) the importance of the scope of quantifiers and (ii) the contrast in how existential and universal quantifiers react to inanimate objects.

The empty world analysis suggests that the assertion is true of any individual whose ontological status is contingent. At heart, this assertion is equivalent to a potential failure of the existence of a witness in the domain of discourse. Indeed, suppose that is true. Then, in particular, there is a witness in the domain such that By the scope of the existential quantifier, we get that implies Conversely, suppose that Using the scope of again, we get a witness in the domain such that But is in the domain, so it is a self-witnessing witness, i.e., This, together with gives us Consequently, for any individual the assertion holds just in case may potentially cease to exist.

What is left is to explain why I contended that the assertion scarcely ever is true. Ostensibly, it was a frivolous claim intended to raise a few eyebrows. But here is my excuse: if you pick a random pair from the collection of all pairs of objects and sets of objects , what are the chances that ?

(Edited on March 12 2023: Two entries in the table on the last slide were wrong, now corrected.)