\(\dashv\) ALVARO PINTADO \(\vDash\)

I am a 3rd-year PhD student and Fontaine Fellow at the University of Pennsylvania (Penn).

My research interests are broadly in proof theory. I am currently interested in dilators, a higher type functorial notion of ordinal

\[ D:\mathbf{Ord}\rightarrow\mathbf{Ord} \]

introduced by J.-Y. Girard in the context of ordinal analysis.

My other research interests include circular proof theory.

Outside my research, I enjoy functional programming, and learning about type theory and programming language theory.


    Background
  • I founded, and now co-organize the Graduate Logic Seminar (GLoS) at Penn.
  • I completed my masters at Penn, where I was a Bridge to PhD Fellow and wrote my masters thesis under the supervision of Henry Towsner.
  • I got a BS in math at the University of Nevada Las Vegas (UNLV). While at UNLV, I also developed a strong interest in philosophy and sat in on numerous philosophy courses. I am interested broadly in the foundations of math and philosophical logic.

Papers

Expository Writing

''The development of mathematics toward greater precision has led, as is well known, to the formalization of large tracts of it, so that one can prove any theorem using nothing but a few mechanical rules. The most comprehensive formal systems that have been set up hitherto are the system of Principia Mathematica on the one hand and the Zermelo-Frankel axiom system of set theory (further developed by J. von Neumann) on the other. These two systems are so comprehensive that in them all methods of proof today used in mathematics are formalized, that is, reduced to a few axioms and rules of inference. One might therefore conjecture that these axioms an rules of inference are sufficient to decide any mathematical question that can at all be formally expressed in these systems. It will be shown below that this is not the case... ''

- K. Gödel (1931)