This thesis explores two novel algebraic applications of Internal Set Theory (IST). We propose an explicitly topological formalism of structural approximation of groups, generalizing previous work by Gordon and Zilber. Using the new formalism, we prove that every profinite group admits a finite approximation in the sense of Zilber. Our main result states that wellbehaved actions of the approximating group on a compact manifold give rise to similarly wellbehaved actions of periodic subgroups of the approximated group on the same manifold. The theorem generalizes earlier results on discrete circle actions, and gives partial nonapproximability results for SO(3). Motivated by the extraction of computational bounds from proofs in a ``pure'' fragment of IST (Sanders), we devise a ``pure'' presentation of sheaves over topological spaces in the style of Robinson and prove it equivalent to the usual definition over standard objects. We introduce a nonstandard extension of MartinLÃ¶f Type Theory with a hierarchy of universes for external propositions along with an external standardness predicate, allowing us to computerverify our main result using the Agda proof assistant.
Date of Award  31 Dec 2019 

Original language  English 

Awarding Institution   The University of Manchester


Supervisor  Alexandre Borovik (Supervisor) & Gareth Jones (Supervisor) 

 group actions
 sheaves
 type theory
 nonstandard analysis
 internal set theory
 group theory
Development of Group Theory in the Language of Internal Set Theory
Kocsis, Z. (Author). 31 Dec 2019
Student thesis: Phd