arXiv subjects

Wojciech Aleksander Wołoszyn

Publications and source records attributed to Wojciech Aleksander Wołoszyn.

10 recordsLinked to original sources

arXiv2026

Vopěnka's Principle without Choice: Preservation under Symmetric Extensions

We give a detailed proof that every set-sized symmetric extension of a model of $\mathsf{ZF}+\mathsf{VP}$ again satisfies $\mathsf{ZF}+\mathsf{VP}$, where $\mathsf{VP}$ is formulated for arbitrary set-sized languages. For each standard $n\geq 1$, the same preservation theorem holds for $\mathsf{VP}(Π_n)$, with set parameters and arbitrary set-sized languages. We also prove that $\mathsf{ZF}+\mathsf{VP}$ and $\mathsf{ZFC}+\mathsf{VP}$ are equiconsistent, and that $\mathsf{ZF}+\mathsf{VP}$ proves the existence of a proper class of Löwenheim-Skolem cardinals. Relative to $\operatorname{Con}(\mathsf{ZF}+\mathsf{VP})$, the axiom $\mathsf{DC}$ is independent of $\mathsf{ZF}+\mathsf{VP}+\neg\mathsf{AC}$. The preservation theorem also yields Feferman-Lévy and full Solovay models satisfying $\mathsf{VP}$. We consider whether every countable model of $\mathsf{ZF}+\mathsf{VP}$ has a class-generic extension satisfying $\mathsf{ZFC}+\mathsf{VP}$.

math.LO↗

arXiv2026

Modal group theory: homomorphisms

I investigate modal group theory for arbitrary homomorphisms. Possibility is interpreted by the existence of a group homomorphism out of the given group, so the semantics is governed by the possibility of collapse: elements may be identified, parameters may be killed, and new relations may hold in the target. I show that the modal language nevertheless expresses cyclic subgroup membership, subgroup generation by a fixed finite tuple, cyclicity, finite generation by a fixed number of elements, and torsion. I use these definability results to interpret arithmetic, and prove that, as sets of Goedel numbers, the homomorphic modal theory of finitely presented groups is computably isomorphic to true arithmetic. I also analyze propositional modal validities: sentential validities are exactly S5, the trivial group has exact parameter-validities S5, and uniformly prime-indivisible groups have exact parameter-validities S4.2.

math.LO↗

arXiv2026

The modal theory of linear orders

I study the modal theory of linear orders under embeddings, monotone maps, condensations, and end-extensions. I prove modality elimination for embeddings and monotone maps, show that condensations make scatteredness modally definable, and compute exact propositional modal validities in the main cases.

math.LO↗

arXiv2026

Modal group theory

I introduce modal group theory, in which we study the category of all groups, considering embeddability as providing a notion of modal possibility. Using HNN extensions and Britton's lemma, I demonstrate that the modal language of groups is more expressive than the first-order language of groups. I interpret the theory of true arithmetic in modal group theory, and show that, as sets of Goedel numbers, it is computably isomorphic to the modal theory of finitely presented groups. I answer an open question of Berger, Block, and Loewe by showing that the formulaic propositional modal validities of groups under embeddings are precisely S4.2. I also analyze sentential validities and worlds validating S5.

math.LO↗

arXiv2026

The modal theory of the category of sets

We classify the propositional modal validities arising from the category of sets under its natural classes of morphisms. The resulting validities depend on the morphism class, the size of the world, and the permitted substitution instances. Our main technical tool is a modality-and-quantifier elimination theorem for the first-order modal language of equality, reducing formulas to finite Boolean combinations of partition conditions and exact cardinality assertions. This yields exact classifications for the main categories of sets, including the full subcategories of finite sets and of infinite sets. In particular, finite $n$-element worlds in the category of sets with parameters realize $\mathrm{Prepartition}_n$; finite $n$-element worlds in the category of sets and surjections realize $\mathrm{Grz.3J}_n$ at the sentential level; and in the infinite-only subcategories, sentential validities collapse to the trivial modal theory, while the formulaic validities for functions and surjections are exactly $\mathrm{Grz.2}$.

math.LO↗

arXiv2026

Grzegorczyk Logic Unlocked

The article offers a fresh perspective on Grzegorczyk logic Grz, introducing a simplified axiomatization and extending the analysis to its natural modal extensions, Grz.2 and Grz.3. I develop a control statement theory for these logics, utilizing concepts such as buttons, switches, and ratchets. Through this framework, I establish that Grz.2 is characterized by finite Boolean algebras.

math.LO↗

arXiv2023

Flexible remote attestation of pre-SNP SEV VMs using SGX enclaves

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 \emph{trusted guest owner}, implemented as an SGX enclave, to deploy, attest, and provision a 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 \emph{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.

cs.CR↗

arXiv2021

Guardian: symbolic validation of orderliness in SGX enclaves

Modern processors can offer hardware primitives that allow a process to run in isolation. These primitives implement a trusted execution environment (TEE) in which a program can run such that the integrity and confidentiality of its execution are guaranteed. Intel's Software Guard eXtensions (SGX) is an example of such primitives and its isolated processes are called \emph{enclaves}. These guarantees, however, can be easily thwarted if the enclave has not been properly designed. Its interface with the untrusted software stack is arguably the largest attack surface that adversaries can exploit; unintended interactions with untrusted code can expose the enclave to memory corruption attacks, for instance. In this paper, we propose a notion of an \emph{orderly} enclave which splits its behaviour into several execution phases each of which imposes a set of restrictions on accesses to untrusted memory, phase transitions and registers sanitisation. A violation to these restrictions indicates an undesired behaviour which could be harnessed to perpetrate attacks against the enclave. We also introduce \Analyser{}: a tool that uses symbolic execution to carry out the validation of an enclave against our notion of an orderly enclave; in this process, it also looks for some typical memory-corruption vulnerabilities. We discuss how our approach can prevent and flag enclave vulnerabilities that have been identified in the literature. Moreover, we have evaluated how our approach fares in the analysis of some practical enclaves. \Analyser{} was able to identify real vulnerabilities on these enclaves which have been acknowledged and fixed by their maintainers.

cs.CR↗

arXiv2020

Modal model theory

We introduce the subject of modal model theory, where one studies a mathematical structure within a class of similar structures under an extension concept that gives rise to mathematically natural notions of possibility and necessity. A statement $φ$ is possible in a structure (written $\Diamondφ$) if $φ$ is true in some extension of that structure, and $φ$ is necessary (written $\Boxφ$) if it is true in all extensions of the structure. A principal case for us will be the class Mod(T) of all models of a given theory T---all graphs, all groups, all fields, or what have you---considered under the substructure relation. In this article, we aim to develop the resulting modal model theory. The class of all graphs is a particularly insightful case illustrating the remarkable power of the modal vocabulary, for the modal language of graph theory can express connectedness, $k$-colorability, finiteness, countability, size continuum, size $\aleph_1$, $\aleph_2$, $\aleph_ω$, $\beth_ω$, first $\beth$-fixed point, first $\beth$-hyper-fixed-point and much more. A graph obeys the maximality principle $\Diamond\Boxφ(a)\toφ(a)$ with parameters if and only if it satisfies the theory of the countable random graph, and it satisfies the maximality principle for sentences if and only if it is universal for finite graphs.

math.LO↗

arXiv2020

Differentiability of continuous functions in terms of Haar-smallness

One of the classical results concerning differentiability of continuous functions states that the set $\mathcal{SD}$ of somewhere differentiable functions (i.e., functions which are differentiable at some point) is Haar-null in the space $C[0,1]$. By a recent result of Banakh et al., a set is Haar-null provided that there is a Borel hull $B\supseteq A$ and a continuous map $f\colon \{0,1\}^\mathbb{N}\to C[0,1]$ such that $f^{-1}[B+h]$ is Lebesgue's null for all $h\in C[0,1]$. We prove that $\mathcal{SD}$ is not Haar-countable (i.e., does not satisfy the above property with "Lebesgue's null" replaced by "countable", or, equivalently, for each copy $C$ of $\{0,1\}^\mathbb{N}$ there is an $h\in C[0,1]$ such that $\mathcal{SD}\cap (C+h)$ is uncountable. Moreover, we use the above notions in further studies of differentiability of continuous functions. Namely, we consider functions differentiable on a set of positive Lebesgue's measure and functions differentiable almost everywhere with respect to Lebesgue's measure. Furthermore, we study multidimensional case, i.e., differentiability of continuous functions defined on $[0,1]^k$. Finally, we pose an open question concerning Takagi's function.

math.FA↗