Proofs Beyond the Transfinite

Juan P. Aguilera (ORCID: 0000-0002-2768-6714)

Disciplines

Mathematics (100%)

Keywords

  • Ordinal Analysis,
  • Bachmann-Howard Ordinal,
  • Proof-Theoretic Ordinal,
  • Kripke-platek set theory,
  • Reverse Mathematics
Abstract

In 1931, Austrian mathematician Kurt Gödel first showed that some mathematical problems are formally unsolvable. This means that there exist mathematical questions for which mathematics cannot provide any answers. Proof Theory is the branch of mathematical logic which studies unsolvable problems, mathematical theories, and the existence of proofs. Since Gödels work, the field has evolved rapidly. Ordinal Analysis uses methods related to infinitary proofs and transfinite numbers to study whether mathematical problems have answers, classify theories, and understand the structure of possible mathematical proofs. However, its scope is limited to a certain particular kind of mathematical problems. The goal of this project is to extend Ordinal Analysis to more general classes of problems in order to develop new tools to study mathematical theories and determine which mathematical questions have answers and which do not.
Research institution(s)

Research Output

  • 14 Citations
  • 28 Publications
  • 9 Disseminations
  • 4 Scientific Awards
  • 2 Fundings
Publications
  • 2025
    Title Binary Choice Games and Arithmetical Comprehension
    DOI 10.48550/arxiv.2510.12612
    Type Preprint
    Author Aguilera J
    Link Publication
  • 2025
    Title Large cardinals beyond HOD
    DOI 10.48550/arxiv.2509.10254
    Type Preprint
    Author Aguilera J
    Link Publication
  • 2025
    Title The Provably Total Set-Recursive Functions of KPl
    DOI 10.48550/arxiv.2510.14399
    Type Preprint
    Author Aguilera J
    Link Publication
  • 2025
    Title ON WINNING STRATEGIES FOR $F_\sigma $ GAMES
    DOI 10.1017/jsl.2024.77
    Type Journal Article
    Author Aguilera J
    Journal The Journal of Symbolic Logic
  • 2025
    Title The metamathematics of separated determinacy
    DOI 10.1007/s00222-025-01322-3
    Type Journal Article
    Author Aguilera J
    Journal Inventiones mathematicae
    Pages 313-457
    Link Publication
  • 2025
    Title Constructive Quantum Logics
    DOI 10.48550/arxiv.2503.15292
    Type Preprint
    Author Aguilera J
  • 2025
    Title Gödel–Dummett linear temporal logic
    DOI 10.1016/j.artint.2024.104236
    Type Journal Article
    Author Aguilera J
    Journal Artificial Intelligence
    Pages 104236
    Link Publication
  • 2025
    Title Large cardinals, structural reflection, and the HOD Conjecture
    DOI 10.48550/arxiv.2411.11568
    Type Preprint
    Author Aguilera J
  • 2025
    Title The logic of correct models
    DOI 10.1142/s0219061325500047
    Type Journal Article
    Author Aguilera J
    Journal Journal of Mathematical Logic
    Pages 2550004
  • 2026
    Title Large infinities and definable sets.
    DOI 10.1073/pnas.2528175123
    Type Journal Article
    Author Aguilera Jp
    Journal Proceedings of the National Academy of Sciences of the United States of America
  • 2026
    Title Reflection properties of ordinals in generic extensions
    DOI 10.1016/j.apal.2026.103765
    Type Journal Article
    Author Aguilera J
    Journal Annals of Pure and Applied Logic
  • 2026
    Title Induction on dilators and Bachmann-Howard fixed points
    DOI 10.1016/j.apal.2026.103740
    Type Journal Article
    Author Aguilera J
    Journal Annals of Pure and Applied Logic
  • 2026
    Title Constructive quantum logics
    DOI 10.1098/rspa.2025.0628
    Type Journal Article
    Author Aguilera J
    Journal Proceedings of the Royal Society A Mathematical Physical and Engineering Science
  • 2026
    Title Determinacy on the edge of second-order arithmetic, I
    DOI 10.1112/jlms.70456
    Type Journal Article
    Author Aguilera J
    Journal Journal of the London Mathematical Society
  • 2026
    Title The Reverse Mathematics of Analytic Measurability
    DOI 10.48550/arxiv.2603.22503
    Type Preprint
    Author Aguilera J
    Link Publication
  • 2024
    Title Functorial Fast-Growing Hierarchies
    DOI 10.1017/fms.2023.128
    Type Journal Article
    Author Aguilera J
    Journal Forum of Mathematics, Sigma
    Link Publication
  • 2024
    Title The Logic of Correct Models
    DOI 10.48550/arxiv.2402.15382
    Type Preprint
    Author Aguilera J
  • 2024
    Title Collapsing Constructive and Intuitionistic Modal Logics
    DOI 10.48550/arxiv.2408.16428
    Type Preprint
    Author Pacheco L
    Link Publication
  • 2024
    Title On some subtheories of strong dependent choice
    DOI 10.48550/arxiv.2411.17415
    Type Preprint
    Author Aguilera J
  • 2024
    Title The Limits of Determinacy in Higher-Order Arithmetic
    DOI 10.48550/arxiv.2411.04786
    Type Preprint
    Author Aguilera J
  • 2024
    Title Induction on Dilators and Bachmann-Howard Fixed Points
    DOI 10.48550/arxiv.2412.13051
    Type Preprint
    Author Aguilera J
  • 2024
    Title Monotone versus non-monotone projective operators
    DOI 10.1112/blms.13194
    Type Journal Article
    Author Aguilera J
    Journal Bulletin of the London Mathematical Society
    Pages 256-264
    Link Publication
  • 2024
    Title THE COMPACTNESS OF GÖDEL LOGIC
    DOI 10.1017/jsl.2024.87
    Type Journal Article
    Author Aguilera J
    Journal The Journal of Symbolic Logic
    Pages 626-635
  • 2024
    Title A Proof of Grilliot's Theorem
    DOI 10.36045/j.bbms.221123a
    Type Journal Article
    Author Aguilera J
    Journal Bulletin of the Belgian Mathematical Society - Simon Stevin
  • 2024
    Title A ONE-PAGE PROOF OF A THEOREM OF BELEZNAY
    DOI 10.1017/bsl.2024.39
    Type Journal Article
    Author Aguilera J
    Journal The Bulletin of Symbolic Logic
    Pages 536-537
  • 2024
    Title Higher-Order Feedback Computation
    DOI 10.1007/978-3-031-64309-5_24
    Type Book Chapter
    Author Aguilera J
    Publisher Springer Nature
    Pages 298-310
  • 2024
    Title Fundamental Logic Is Decidable
    DOI 10.1145/3665328
    Type Journal Article
    Author Aguilera J
    Journal ACM Transactions on Computational Logic
    Pages 1-14
    Link Publication
  • 2025
    Title Intuitionistic Gödel-Löb without Sharps
    DOI 10.1145/3748649
    Type Journal Article
    Author Aguilera J
    Journal ACM Transactions on Computational Logic
    Pages 1-14
Disseminations
  • 2026 Link
    Title TU Wien press release PNAS
    Type A magazine, newsletter or online publication
    Link Link
  • 2025 Link
    Title Popular Mechanics article
    Type A press release, press conference or response to a media enquiry/interview
    Link Link
  • 2025 Link
    Title Interview for Science et vie
    Type A press release, press conference or response to a media enquiry/interview
    Link Link
  • 2025 Link
    Title Article at Der Standard
    Type A press release, press conference or response to a media enquiry/interview
    Link Link
  • 2025 Link
    Title LC Press
    Type A magazine, newsletter or online publication
    Link Link
  • 2024 Link
    Title New Scientist article
    Type A press release, press conference or response to a media enquiry/interview
    Link Link
  • 2025 Link
    Title ESI Program
    Type Participation in an activity, workshop or similar
    Link Link
  • 2025 Link
    Title Quanta magazine
    Type A press release, press conference or response to a media enquiry/interview
    Link Link
  • 2025 Link
    Title IFLScience interview
    Type A press release, press conference or response to a media enquiry/interview
    Link Link
Scientific Awards
  • 2026
    Title Wallenberg Visiting Professorship
    Type Research prize
    Level of Recognition Continental/International
  • 2025
    Title Medal of the Austrian Mathematical Society
    Type Medal
    Level of Recognition National (any country)
  • 2025
    Title CNRL Award 2025
    Type Research prize
    Level of Recognition National (any country)
  • 2025
    Title 2025 Franco Montagna Award
    Type Research prize
    Level of Recognition National (any country)
Fundings
  • 2026
    Title Uncovering the Axioms of Mathematics
    Type Research grant (including intramural programme)
    DOI 10.55776/efp2661725
    Start of Funding 2026
    Funder Austrian Science Fund (FWF)
  • 2026
    Title Aspects of Undecidability
    Type Research grant (including intramural programme)
    Start of Funding 2026
    Funder Wallenberg Foundations