{'fraction_non_alphanumeric': 0.014545454545454545, 'fraction_numerical': 0.0018181818181818182, 'mean_word_length': 5.116666666666666, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
The extended predicative Mahlo universe in explicit mathematics

The Mahlo universe has been introduced in order to obtain a predicatively justified proof theoretically strong extension of Martin-Löf Type Theory. The strength is of this theory is Kripke-Platek set theory extended by one recursively Mahlo ordinal and finitely many admissibles above it, and therefore it proves the extension of for instance the theory KPM. There have been many discussions in the proof theoretic community whether this theory is indeed predicatively justified. In this talk we present the extended predicative Mahlo universe ([2]) in the setting of explicit mathematics. This Mahlo universe is entirely built from below and can therefore be considered as predicatively justified. The ordinary Mahlo universe in explicit mathematics can easily be embedded into this theory and therefore it is likely to be slightly stronger than the Mahlo universe in type theory. We will introduce this theory and show how to adapt the model construction in [1] in order to obtain a model for the extended predicative Mahlo Universe.