Transfinite Fixed Points in Alpay Algebra as Ordinal Game Equilibria in Dependent Type Theory

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Alpay, Faruk, Kilictas, Bugra, Alpay, Taylan
Format: Preprint
Published: 2025
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866915409451548672
author Alpay, Faruk
Kilictas, Bugra
Alpay, Taylan
author_facet Alpay, Faruk
Kilictas, Bugra
Alpay, Taylan
contents This paper contributes to the Alpay Algebra by demonstrating that the stable outcome of a self referential process, obtained by iterating a transformation through all ordinal stages, is identical to the unique equilibrium of an unbounded revision dialogue between a system and its environment. The analysis initially elucidates how classical fixed point theorems guarantee such convergence in finite settings and subsequently extends the argument to the transfinite domain, relying upon well founded induction and principles of order theoretic continuity. Furthermore, the resulting transordinal fixed point operator is embedded into dependent type theory, a formalization which permits every step of the transfinite iteration and its limit to be verified within a modern proof assistant. This procedure yields a machine checked proof that the iterative dialogue necessarily stabilizes and that its limit is unique. The result provides a foundation for Alpay's philosophical claim of semantic convergence within the framework of constructive logic. By unifying concepts from fixed point theory, game semantics, ordinal analysis, and type theory, this research establishes a broadly accessible yet formally rigorous foundation for reasoning about infinite self referential systems and offers practical tools for certifying their convergence within computational environments.
format Preprint
id arxiv_https___arxiv_org_abs_2507_19245
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Transfinite Fixed Points in Alpay Algebra as Ordinal Game Equilibria in Dependent Type Theory
Alpay, Faruk
Kilictas, Bugra
Alpay, Taylan
Logic in Computer Science
Artificial Intelligence
68T27, 03B70, 68Q55
This paper contributes to the Alpay Algebra by demonstrating that the stable outcome of a self referential process, obtained by iterating a transformation through all ordinal stages, is identical to the unique equilibrium of an unbounded revision dialogue between a system and its environment. The analysis initially elucidates how classical fixed point theorems guarantee such convergence in finite settings and subsequently extends the argument to the transfinite domain, relying upon well founded induction and principles of order theoretic continuity. Furthermore, the resulting transordinal fixed point operator is embedded into dependent type theory, a formalization which permits every step of the transfinite iteration and its limit to be verified within a modern proof assistant. This procedure yields a machine checked proof that the iterative dialogue necessarily stabilizes and that its limit is unique. The result provides a foundation for Alpay's philosophical claim of semantic convergence within the framework of constructive logic. By unifying concepts from fixed point theory, game semantics, ordinal analysis, and type theory, this research establishes a broadly accessible yet formally rigorous foundation for reasoning about infinite self referential systems and offers practical tools for certifying their convergence within computational environments.
title Transfinite Fixed Points in Alpay Algebra as Ordinal Game Equilibria in Dependent Type Theory
topic Logic in Computer Science
Artificial Intelligence
68T27, 03B70, 68Q55
url https://arxiv.org/abs/2507.19245