Partizan Games in Isabelle/HOLZF

Steven Obua

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

Partizan Games (PGs) were invented by John H. Conway and are described in his book On Numbers and Games. We formalize PGs in Higher Order Logic extended with ZF axioms (HOLZF) using Isabelle, a mechanical proof assistant. We show that PGs can be defined as the unique fixpoint of a function that arises naturally from Conway’s original definition. While the construction of PGs in HOLZF relies heavily on the ZF axioms, operations on PGs are defined on a game type that hides its set theoretic origins. A polymorphic type of sets that are not bigger than ZF sets facilitates this. We formalize the induction principle that Conway uses throughout his proofs about games, and prove its correctness. For these purposes we examine how the notions of well-foundedness in HOL and ZF are related in HOLZF. Finally, games (modulo equality) are added to Isabelle’s numeric types by showing that they are an instance of the axiomatic type class of partially ordered abelian groups.
Original languageEnglish
Title of host publicationTheoretical Aspects of Computing - ICTAC 2006
Subtitle of host publicationThird International Colloquium, Tunis, Tunisia, November 20-24, 2006. Proceedings
EditorsKamel Barkaoui, Ana Cavalcanti, Antonio Cerone
Place of PublicationBerlin, Heidelberg
PublisherSpringer Berlin Heidelberg
Pages272-286
Number of pages15
ISBN (Electronic)978-3-540-48816-3
ISBN (Print)978-3-540-48815-6
DOIs
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume4281
ISSN (Print)0302-9743

Cite this