2020/06/22 by Anton Freund, Freund, Anton
Computer Science · Earth and Planetary Sciences · Engineering · #03B30 #03D65 #03F15 #03F35 #Computability, Logic, AI Algorithms #FOS: Mathematics #Hydraulic Fracturing and Reservoir Analysis #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Reservoir Engineering and Simulation Methods #Seismic Imaging and Inversion Techniques
paper · pdf · doi:10.48550/arxiv.2006.12111
openalex publication_date 2020/06/22 · openalex created_date 2024/04/11 · openalex updated_date 2026/07/28
In previous work, the author has shown that Π11-induction along \mathbb N is equivalent to a suitable formalization of the statement that every normal function on the ordinals has a fixed point. More precisely, this was proved for a representation of normal functions in terms of J.-Y. Girard's dilators, which are particularly uniform transformations of well orders. The present paper works on the next type level and considers uniform transformations of dilators, which are called 2-ptykes. We show that Π12-induction along \mathbb N is equivalent to the existence of fixed points for all 2-ptykes that satisfy a certain normality condition. Beyond this specific result, the paper paves the way for the analysis of further Π14-statements in terms of well ordering principles.