# On the logical structure of some maximality and well-foundedness principles equivalent to choice principles

Hugo Herbelin, Jad Koleilat

► To cite this version:

Hugo Herbelin, Jad Koleilat. On the logical structure of some maximality and well-foundedness principles equivalent to choice principles. 2023. hal-04572354

HAL Id: hal-04572354

https://inria.hal.science/hal-04572354

Preprint submitted on 15 May 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_1.png" /></figure>

HAL
open science

# On the logical structure of some maximality and well-foundedness principles equivalent to choice principles

Hugo Herbelin, Jad Koleilat

► To cite this version:

Hugo Herbelin, Jad Koleilat. On the logical structure of some maximality and well-foundedness principles equivalent to choice principles. 2023. hal-04572354

HAL Id: hal-04572354

https://inria.hal.science/hal-04572354v1

Preprint submitted on 15 May 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On the logical structure of some maximality and well-foundedness principles equivalent to choice principles

Hugo Herbelin

Université de Paris Cité, Inria, CNRS, IRIF

Jad Koleilat

Université Paris Cité

## Abstract

We study the logical structure of *Teichmüller-Tukey lemma*, a maximality principle equivalent to the axiom of choice and show that it corresponds to the generalisation to arbitrary cardinals of *update induction*, a well-foundedness principle from constructive mathematics classically equivalent to the axiom of dependent choice.

From there, we state general forms of maximality and well-foundedness principles equivalent to the axiom of choice, including a variant of Zorn's lemma. A comparison with the general class of choice and bar induction principles given by Brede and the first author is initiated.

**2012 ACM Subject Classification** Theory of computation → Proof theory

**Keywords and phrases** axiom of choice, Teichmüller-Tukey lemma, update induction, constructive reverse mathematics

Digital Object Identifier 10.4230/LIPIcs.FSCD.2024.23

# 1 Introduction

## 1.1 Context

The axiom of choice is independent of Zermelo-Fraenkel set theory and equivalent to many other formulations [3, 5, 6], the most famous ones being Zorn's lemma, a maximality statement, and Zermelo's theorem, a well-ordering thus also well-foundedness theorem, since well-foundedness and well-ordering are logically dual notions.

In the family of maximality theorems equivalent to the axiom of choice one statement happens to be particularly concise and general, it is Teichmüller-Tukey lemma, that states that every non-empty collection of *finite character*, that is, characterised only by its finite sets, has a maximal element with respect to inclusion.

The axiom of dependent choice is a strict consequence of the axiom of choice. In the context of constructive mathematics, various statements classically but non intuitionistically equivalent to the axiom of dependent choice are considered, such as bar induction, open induction [3], or, more recently, update induction [1], the last two relying on a notion of *open* predicate over functions of countable support expressing that the predicate depends only on finite approximations of the function.

In a first part of the paper, we reason intuitionistically and show that the notion of finite character, when specialised to countable sets, is dual to the notion of open predicate, or, alternatively, that the notion of open predicate, when generalised to arbitrary cardinals is dual to the notion of finite character. As a consequence, we establish that update induction and the specialisation of Teichmüller-Tukey lemma to countable sets are logically dual statements, or, alternatively, that Teichmüller-Tukey lemma and the generalisation of update induction to arbitrary cardinals are logically dual.

<figure><img src="image_2.png" /></figure>

© H. Herbelin, J. Koleilat;

licensed under Creative Commons License CC-BY 4.0

9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024).

Editor: Jakob Rehof; Article No. 23; pp. 23:1–23:16

<figure><img src="image_3.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
# On the logical structure of some maximality and well-foundedness principles equivalent to choice principles

Hugo Herbelin

Université de Paris Cité, Inria, CNRS, IRIF

Jad Koleilat

Université Paris Cité

## Abstract

We study the logical structure of *Teichmüller-Tukey lemma*, a maximality principle equivalent to the axiom of choice and show that it corresponds to the generalisation to arbitrary cardinals of *update induction*, a well-foundedness principle from constructive mathematics classically equivalent to the axiom of dependent choice.

From there, we state general forms of maximality and well-foundedness principles equivalent to the axiom of choice, including a variant of Zorn's lemma. A comparison with the general class of choice and bar induction principles given by Brede and the first author is initiated.

**2012 ACM Subject Classification** Theory of computation → Proof theory

**Keywords and phrases** axiom of choice, Teichmüller-Tukey lemma, update induction, constructive reverse mathematics

Digital Object Identifier 10.4230/LIPIcs.FSCD.2024.23

# 1 Introduction

## 1.1 Context

The axiom of choice is independent of Zermelo-Fraenkel set theory and equivalent to many other formulations [4, 5, 6], the most famous ones being Zorn's lemma, a maximality statement, and Zermelo's theorem, a well-ordering thus also well-foundedness theorem, since well-foundedness and well-ordering are logically dual notions.

In the family of maximality theorems equivalent to the axiom of choice one statement happens to be particularly concise and general, it is Teichmüller-Tukey lemma, that states that every non-empty collection of *finite character*, that is, characterised only by its finite sets, has a maximal element with respect to inclusion.

The axiom of dependent choice is a strict consequence of the axiom of choice. In the context of constructive mathematics, various statements classically but non intuitionistically equivalent to the axiom of dependent choice are considered, such as bar induction, open induction [3], or, more recently, update induction [1], the last two relying on a notion of *open* predicate over functions of countable support expressing that the predicate depends only on finite approximations of the function.

In a first part of the paper, we reason intuitionistically and show that the notion of finite character, when specialised to countable sets, is dual to the notion of open predicate, or, alternatively, that the notion of open predicate, when generalised to arbitrary cardinals is dual to the notion of finite character. As a consequence, we establish that update induction and the specialisation of Teichmüller-Tukey lemma to countable sets are logically dual statements, or, alternatively, that Teichmüller-Tukey lemma and the generalisation of update induction to arbitrary cardinals are logically dual.

<figure><img src="image_3.png" /></figure>

© H. Herbelin, J. Koleilat;

licensed under Creative Commons License CC-BY 4.0

9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024).

Editor: Jakob Rehof; Article No. 23; pp. 23:1–23:16

<figure><img src="image_4.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 23:2 On the logical structure of some maximality and well-foundedness principles

In a second part of the paper, we show how Teichmüller-Tukey lemma and Zorn's lemma can be seen as mutual instances the one of the other.

Finally, in a third part, we introduce a slight variant of Teichmüller-Tukey lemma referring to functions rather than sets and make some connections with the classification of choice and bar induction principles studied by Brede and the first author in [2].

The ideas of Section 2 have been developed during an undergraduate internship of the second author under the supervision of the first author in 2022, leading to the idea in Section 4.1 of introducing $∃MPCF$ by the second author. Section 3 contains extra investigations made in 2023 by the second author. Section 4.2 contains investigations made jointly in 2024 by the authors.

## 1.2 The logical system

In this section we describe the logical setting and give definitions that are used throughout the article. The results we prove do not depend greatly on its structure as they require only basic constructions, we shall make precise exactly was is necessary and what is left to the preferences of the reader.

We work in an intuitionistic higher order arithmetic equipped with inductive types like the type with one element (1, 0 : 1), the type of Boolean values (B, 0B, 1B : B), the type of natural numbers (N), the product type (A × B), or the coproduct type (A + B). In particular, we write B⊥ for the coproduct of B and of 1, identifying b : B with inl(b) : B⊥ and ⊥ with inr(0) where inl and inr are the two injections of the coproduct.

We write *Prop* for the type of propositions. For all types A, the type $P(A)$ denotes the type $A \to Prop$, we shall sometimes refer to it as “subsets of A”. We also use the type $N \to A_\perp$, shortly $A_\perp$, to represent the countable subsets of A, implicitly referring to the non-⊥ elements of the image of the function<fnref n="1" />.

We also require a type for lists: for all types A we denote by $A^*$ the type of lists of terms of type A defined as follows:

$$ \varepsilon : A^* \qquad \frac{u : A^* \quad a : A}{u @ a : A^*} $$

We inductively define $\star : A^* \to A^* \to A^*$, the concatenation of two lists:

$$ \frac{u : A^* \qquad \frac{u : A^* \quad v : A^* \quad a : A}{u \star (v @ a) := (u \star v) @ a}}{u \star \varepsilon := u} $$

We denote by $[a_1, \dots, a_n]$ the list $(\dots (\varepsilon@a_1)@\dots)@a_n)$, since $\star$ is associative we drop the parentheses. If $n \in N$ and $\alpha : A^N$, we write $\alpha|_n$ for the recursively defined list $[\alpha(0), \dots, \alpha(n-1)]$. We define $\in : A \to A^* \to Prop$ as: $a \in u := \exists v, w^{A^*}, v \star [a] \star w = u$.

The symbol $\in$ will be used as defined above and also as a notation for $P(a)$. To be more precise, for all types A, $P : P(A)$ and $a : A$ we will write $a \in P$ for $P(a)$ and $a \notin P$ for $P(a) \to \perp$. Continuing with the set-like notations, for $P, Q : P(A)$ we write $P \subseteq Q$ for $\forall a^A, a \in P \to a \in Q$. We require extensional equality for predicates: for all $P, Q : P(A)$, $P = Q \leftrightarrow P \subseteq Q \land Q \subseteq P^2$. The symbol $\subseteq$ will also be used for lists: for all $u, v : A^*$,

<footnote n="1">¹ For inhabited A, this is intuitionistically equivalent to considering $N \to A$.</footnote>

<footnote n="2">² Extensionality for predicates is assumed for convenience, it is not fundamentally needed</footnote>
## 23:2 On the logical structure of some maximality and well-foundedness principles

In a second part of the paper, we show how Teichmüller-Tukey lemma and Zorn's lemma can be seen as mutual instances the one of the other.

Finally, in a third part, we introduce a slight variant of Teichmüller-Tukey lemma referring to functions rather than sets and make some connections with the classification of choice and bar induction principles studied by Brede and the first author in [2].

The ideas of Section 2 have been developed during an undergraduate internship of the second author under the supervision of the first author in 2022, leading to the idea in Section 4.1 of introducing $∃MPCF$ by the second author. Section 3 contains extra investigations made in 2023 by the second author. Section 4.2 contains investigations made jointly in 2024 by the authors.

## 1.2 The logical system

In this section we describe the logical setting and give definitions that are used throughout the article. The results we prove do not depend greatly on its structure as they require only basic constructions, we shall make precise exactly was is necessary and what is left to the preferences of the reader.

We work in an intuitionistic higher order arithmetic equipped with inductive types like the type with one element (1, 0 : 1), the type of Boolean values (B, 0B, 1B : B), the type of natural numbers (N), the product type (A × B), or the coproduct type (A + B). In particular, we write B⊥ for the coproduct of B and of 1, identifying b : B with inl(b) : B⊥ and ⊥ with inr(0) where inl and inr are the two injections of the coproduct.

We write *Prop* for the type of propositions. For all types A, the type $P(A)$ denotes the type $A \to Prop$, we shall sometimes refer to it as “subsets of A”. We also use the type $N \to A_\perp$, shortly $A_\perp$, to represent the countable subsets of A, implicitly referring to the non-⊥ elements of the image of the function<fnref n="1" />.

We also require a type for lists: for all types A we denote by $A^*$ the type of lists of terms of type A defined as follows:

$$ \varepsilon : A^* \qquad \frac{u : A^* \quad a : A}{u @ a : A^*} $$

We inductively define $\star : A^* \to A^* \to A^*$, the concatenation of two lists:

$$ \frac{u : A^* \qquad \frac{u : A^* \quad v : A^* \quad a : A}{u \star (v @ a) := (u \star v) @ a}}{u \star \varepsilon := u} $$

We denote by $[a_1, \dots, a_n]$ the list $(\dots (\varepsilon@a_1)@\dots)@a_n)$, since $\star$ is associative we drop the parentheses. If $n \in N$ and $\alpha : A^N$, we write $\alpha|_n$ for the recursively defined list $[\alpha(0), \dots, \alpha(n-1)]$. We define $\in : A \to A^* \to Prop$ as: $a \in u := \exists v, w^{A^*}, v \star [a] \star w = u$.

The symbol $\in$ will be used as defined above and also as a notation for $P(a)$. To be more precise, for all types A, $P : P(A)$ and $a : A$ we will write $a \in P$ for $P(a)$ and $a \notin P$ for $P(a) \to \perp$. Continuing with the set-like notations, for $P, Q : P(A)$ we write $P \subseteq Q$ for $\forall a^A, a \in P \to a \in Q$. We require extensional equality for predicates: for all $P, Q : P(A)$, $P = Q \leftrightarrow P \subseteq Q \land Q \subseteq P^2$. The symbol $\subseteq$ will also be used for lists: for all $u, v : A^*$,

<footnote n="1">¹ For inhabited A, this is intuitionistically equivalent to considering $N \to A$.</footnote>

<footnote n="2">² Extensionality for predicates is assumed for convenience, it is not fundamentally needed</footnote>
$u \subseteq v := \forall a^A, a \in u \to a \in v$. Note that equipped with this relation, lists behave more like finite sets than lists. Nevertheless the list structure is not superfluous as will be shown later.

As a convention, we let the scope of quantifiers spans until the end of the sentence, so, for instance, $\forall n, P \to Q$ reads as $\forall n, (P \to Q)$ and similarly for $\exists$.

## 1.3 Closure operators and partial functions

Let us now define some closure operators and relations on subsets and lists:

**► Definition 1.** Let $A$ be a type, $u : A^*$, $\alpha : \mathcal{P}(A)$, $T : \mathcal{P}(A^*)$, $P : \mathcal{P}(\mathcal{P}(A))$

$$u \subset \alpha : \text{Prop} \qquad \langle T \rangle : \mathcal{P}(\mathcal{P}(A))$$

$$u \subset \alpha := \forall a^A, a \in u \to a \in \alpha \qquad \langle T \rangle := \lambda \alpha^{\mathcal{P}(A)} \forall u^{A^*}, u \subset \alpha \to u \in T$$

$$\langle T \rangle^\circ : \mathcal{P}(\mathcal{P}(A))$$

$$\langle T \rangle^\circ := \lambda \alpha^{\mathcal{P}(A)} \exists u^{A^*}, u \subset \alpha \wedge u \in T$$

$$\langle u \rangle : \mathcal{P}(A) \qquad \lfloor P \rfloor : \mathcal{P}(A^*)$$

$$\langle u \rangle := \lambda x^A. x \in u \qquad \lfloor P \rfloor := \lambda u^{A^*}. \langle u \rangle \in P$$

The symbol $\langle \rangle$ is the translation from “the list world” to “the predicate world”. More precisely, $\langle u \rangle$ is the canonical way to see a list as a predicate ($u \subset \alpha \leftrightarrow \langle u \rangle \subseteq \alpha$) and $\langle T \rangle$ is an extension of $T$ as a predicate on subsets, $\alpha : \mathcal{P}(A)$ is in $\langle T \rangle$ if and only if it can be arbitrarily approximated by lists of $T$. Dually, $\lfloor \rfloor$ is the translation from predicate to list, taking predicate of finite domain to all lists of elements in the domain. Note that $\langle T \rangle$ is downward closed, that is, $\alpha \subset \beta$ and $\beta \in \langle T \rangle$ implies $\alpha \in \langle T \rangle$. Note also that $\langle \lfloor P \rfloor \rangle$ is a downward closure operator, defining the largest downward closed subset of $P$. On its side, $\lfloor \langle T \rangle \rfloor$ builds the downward closure up to permutation and replication of the elements of the lists of $T$. Also, symmetrical properties applies to $\langle \rangle^\circ$ exchanging downward with upward and largest subset with smallest superset. Finally, notice that $\langle T \rangle$ may be empty, in fact $\langle T \rangle$ is inhabited if and only if $\varepsilon \in T$, and the same for $\langle T \rangle^\circ$.

**Examples:**

Consider $T : \mathcal{P}(\mathbb{B}^*)$, for simplicity let us use set-like notations when defining $T$. If $T := \{[1_{\mathbb{B}}, 0_{\mathbb{B}}], [1_{\mathbb{B}}], [0_{\mathbb{B}}], \epsilon\}$ then $\langle T \rangle$ will contain all subsets of $\mathbb{B}$. Now, if $T := \{[1_{\mathbb{B}}, 0_{\mathbb{B}}], [1_{\mathbb{B}}], [0_{\mathbb{B}}]\}$, $\langle T \rangle$ will be empty since for all $\alpha : \mathcal{P}(\mathbb{B})$, $\epsilon \subset \alpha$ but $\epsilon \notin T$. If $T := \{\epsilon, [1_{\mathbb{B}}], [1_{\mathbb{B}}, 0_{\mathbb{B}}]\}$ then $\langle T \rangle$ will contain only the empty subset and the singleton containing $1_{\mathbb{B}}$. Now consider $T' := \{\epsilon, [1_{\mathbb{B}}], [1_{\mathbb{B}}, 1_{\mathbb{B}}], [0_{\mathbb{B}}, 1_{\mathbb{B}}], [1_{\mathbb{B}}, 0_{\mathbb{B}}, 1_{\mathbb{B}}, 1_{\mathbb{B}}]\}$, notice that $\langle T \rangle = \langle T' \rangle$. The $\langle \rangle$ operation does not care for duplications or permutations.

For $T := \{\epsilon, [1_{\mathbb{B}}], [1_{\mathbb{B}}, 0_{\mathbb{B}}]\}$, $\lfloor \langle T \rangle \rfloor$ is $\{\epsilon, [1_{\mathbb{B}}], [1_{\mathbb{B}}, 1_{\mathbb{B}}], [1_{\mathbb{B}}, 1_{\mathbb{B}}, 1_{\mathbb{B}}], \dots\}$. Similarly, for $T := \{\epsilon, [1_{\mathbb{B}}], [0_{\mathbb{B}}], [1_{\mathbb{B}}, 0_{\mathbb{B}}]\}$, $\lfloor \langle T \rangle \rfloor$ is the set of all lists on $\mathbb{B}$.

The $\langle \rangle^\circ$ operator has the dual behaviour. Consider $T : \mathcal{P}(\mathbb{N}^*)$, $T := \{[1]\}$ then, $\langle T \rangle^\circ$ contains exactly all subsets of $\mathbb{N}$ containing 1. Similarly if $\epsilon \in T$, then $\langle T \rangle^\circ$ contains all subsets of $\mathbb{N}$. For $T := \{[1]\}$, $\lfloor \langle T \rangle^\circ \rfloor$ will contain every list on $\mathbb{N}$ that contains at least one 1.

We also give similar definitions relatively to countable subsets, abbreviating $(A_\perp)^*$ into $A_\perp^*$:
$u \subseteq v := \forall a^A, a \in u \to a \in v$. Note that equipped with this relation, lists behave more like finite sets than lists. Nevertheless the list structure is not superfluous as will be shown later.

As a convention, we let the scope of quantifiers spans until the end of the sentence, so, for instance, $\forall n, P \to Q$ reads as $\forall n, (P \to Q)$ and similarly for $\exists$.

## 1.3 Closure operators and partial functions

Let us now define some closure operators and relations on subsets and lists:

**► Definition 1.** Let $A$ be a type, $u : A^*$, $\alpha : \mathcal{P}(A)$, $T : \mathcal{P}(A^*)$, $P : \mathcal{P}(\mathcal{P}(A))$

$$u \subset \alpha : \text{Prop} \qquad \langle T \rangle : \mathcal{P}(\mathcal{P}(A))$$

$$u \subset \alpha := \forall a^A, a \in u \to a \in \alpha \qquad \langle T \rangle := \lambda \alpha^{\mathcal{P}(A)} \forall u^{A^*}, u \subset \alpha \to u \in T$$

$$\langle T \rangle^\circ : \mathcal{P}(\mathcal{P}(A))$$

$$\langle T \rangle^\circ := \lambda \alpha^{\mathcal{P}(A)} \exists u^{A^*}, u \subset \alpha \wedge u \in T$$

$$\langle u \rangle : \mathcal{P}(A) \qquad \lfloor P \rfloor : \mathcal{P}(A^*)$$

$$\langle u \rangle := \lambda x^A. x \in u \qquad \lfloor P \rfloor := \lambda u^{A^*}. \langle u \rangle \in P$$

The symbol $\langle \rangle$ is the translation from “the list world” to “the predicate world”. More precisely, $\langle u \rangle$ is the canonical way to see a list as a predicate ($u \subset \alpha \leftrightarrow \langle u \rangle \subseteq \alpha$) and $\langle T \rangle$ is an extension of $T$ as a predicate on subsets, $\alpha : \mathcal{P}(A)$ is in $\langle T \rangle$ if and only if it can be arbitrarily approximated by lists of $T$. Dually, $\lfloor \rfloor$ is the translation from predicate to list, taking predicate of finite domain to all lists of elements in the domain. Note that $\langle T \rangle$ is downward closed, that is, $\alpha \subset \beta$ and $\beta \in \langle T \rangle$ implies $\alpha \in \langle T \rangle$. Note also that $\langle \lfloor P \rfloor \rangle$ is a downward closure operator, defining the largest downward closed subset of $P$. On its side, $\lfloor \langle T \rangle \rfloor$ builds the downward closure up to permutation and replication of the elements of the lists of $T$. Also, symmetrical properties applies to $\langle \rangle^\circ$ exchanging downward with upward and largest subset with smallest superset. Finally, notice that $\langle T \rangle$ may be empty, in fact $\langle T \rangle$ is inhabited if and only if $\varepsilon \in T$, and the same for $\langle T \rangle^\circ$.

**Examples:**

Consider $T : \mathcal{P}(\mathbb{B}^*)$, for simplicity let us use set-like notations when defining $T$. If $T := \{[1_{\mathbb{B}}, 0_{\mathbb{B}}], [1_{\mathbb{B}}], [0_{\mathbb{B}}], \epsilon\}$ then $\langle T \rangle$ will contain all subsets of $\mathbb{B}$. Now, if $T := \{[1_{\mathbb{B}}, 0_{\mathbb{B}}], [1_{\mathbb{B}}], [0_{\mathbb{B}}]\}$, $\langle T \rangle$ will be empty since for all $\alpha : \mathcal{P}(\mathbb{B})$, $\epsilon \subset \alpha$ but $\epsilon \notin T$. If $T := \{\epsilon, [1_{\mathbb{B}}], [1_{\mathbb{B}}, 0_{\mathbb{B}}]\}$ then $\langle T \rangle$ will contain only the empty subset and the singleton containing $1_{\mathbb{B}}$. Now consider $T' := \{\epsilon, [1_{\mathbb{B}}], [1_{\mathbb{B}}, 1_{\mathbb{B}}], [0_{\mathbb{B}}, 1_{\mathbb{B}}], [1_{\mathbb{B}}, 0_{\mathbb{B}}, 1_{\mathbb{B}}, 1_{\mathbb{B}}]\}$, notice that $\langle T \rangle = \langle T' \rangle$. The $\langle \rangle$ operation does not care for duplications or permutations.

For $T := \{\epsilon, [1_{\mathbb{B}}], [1_{\mathbb{B}}, 0_{\mathbb{B}}]\}$, $\lfloor \langle T \rangle \rfloor$ is $\{\epsilon, [1_{\mathbb{B}}], [1_{\mathbb{B}}, 1_{\mathbb{B}}], [1_{\mathbb{B}}, 1_{\mathbb{B}}, 1_{\mathbb{B}}], \dots\}$. Similarly, for $T := \{\epsilon, [1_{\mathbb{B}}], [0_{\mathbb{B}}], [1_{\mathbb{B}}, 0_{\mathbb{B}}]\}$, $\lfloor \langle T \rangle \rfloor$ is the set of all lists on $\mathbb{B}$.

The $\langle \rangle^\circ$ operator has the dual behaviour. Consider $T : \mathcal{P}(\mathbb{N}^*)$, $T := \{[1]\}$ then, $\langle T \rangle^\circ$ contains exactly all subsets of $\mathbb{N}$ containing 1. Similarly if $\epsilon \in T$, then $\langle T \rangle^\circ$ contains all subsets of $\mathbb{N}$. For $T := \{[1]\}$, $\lfloor \langle T \rangle^\circ \rfloor$ will contain every list on $\mathbb{N}$ that contains at least one 1.

We also give similar definitions relatively to countable subsets, abbreviating $(A_\perp)^*$ into $A_\perp^*$:
23:4 On the logical structure of some maximality and well-foundedness principles

► **Definition 2.** Let A be a type, $u : A_{\perp}^{*}$, $\alpha : A_{\perp}^{\mathbb{N}}$ and $T : \mathcal{P}(A_{\perp}^{*})$

$$u \subset_{\mathbb{N}} \alpha : \mathrm{Prop} \qquad \langle T \rangle_{\mathbb{N}} : \mathcal{P}(A_{\perp}^{\mathbb{N}})$$

$$u \subset_{\mathbb{N}} \alpha := \exists n^{\mathbb{N}}, u = \alpha|_n \qquad \langle T \rangle_{\mathbb{N}} := \lambda\alpha^{A_{\perp}^{\mathbb{N}}}. \forall u^{A^{*}}, u \subset_{\mathbb{N}} \alpha \rightarrow u \in T$$

$$\langle T \rangle_{\mathbb{N}}^{\circ} : \mathcal{P}(A_{\perp}^{\mathbb{N}})$$

$$\langle T \rangle_{\mathbb{N}}^{\circ} := \lambda\alpha^{A_{\perp}^{\mathbb{N}}}. \exists u^{A^{*}}, u \subset_{\mathbb{N}} \alpha \wedge u \in T$$

We conclude this section defining two different notions of partial functions:

► **Definition 3 (Relational partial function).** Let A, B be types, a relational partial function f from A to B is a relational functional relation of $\mathcal{P}(A \times B)$. Formally, a relational partial function from A to B is a term f : $\mathcal{P}(A \times B)$ such that $\forall a^A, \forall b, b^B, ((a, b) \in f \wedge (a, b') \in f) \rightarrow b = b'$. Its domain is defined by:

$$\mathrm{dom}(f) : \mathcal{P}(A)$$

$$\mathrm{dom}(f) := \lambda a^A. \exists b^B, (a, b) \in f$$

For all $a' : A$, we denote by $\mathrm{dom}(f) \cup a'$ the predicate $\lambda a^A. (\exists b^B, (a, b) \in f) \lor a = a'$.

► **Definition 4 (Decidable partial function).** Let A, B be types, a decidable partial function f from A to B is a total function f : A $\rightarrow$ B$_{⊥}$. Its domain and graph are defined by:

$$\mathrm{dom}(f) : \mathcal{P}(A) \qquad \mathcal{G}(f) : \mathcal{P}(A \times B)$$

$$\mathrm{dom}(f) := \lambda a^A. f(a) \neq \perp \qquad \mathcal{G}(f) := \lambda(a, b)^{A \times B}. f(a) = \mathrm{inl}(b)$$

For all $a' : A$, we denote by $\mathrm{dom}(f) \cup a'$ the predicate $\lambda a^A. f(a) \neq \perp \lor a = a'$.

**Notation:**

We write $f \in A \rightarrow_{\mathrm{p}} B$ to denote that $f$ is a relational partial function from $A$ to $B$ and $f : A \rightarrow B_{\perp}$ for the type of decidable partial functions from $A$ to $B$. We will also write $\Theta f^{A \rightarrow_{\mathrm{p}} B}, P$ for $\Theta f^{\mathcal{P}(A \times B)}, (f \in A \rightarrow_{\mathrm{p}} B) \rightarrow P$ for $\Theta \in \{\lambda, \forall, \exists\}$.

The difference between these two definitions is in the decidability of the domain: decidable partial functions have a decidable domain while it's not the case of relational partial functions. The graph operation $\mathcal{G}$ allows us to recover a relational partial function from a decidable partial function. One needs excluded middle to recover a decidable partial function from a relation partial function, hence decidable partial functions are stronger axiomatically. Notice that we used the same notation $\mathrm{dom}$ in both definitions. Since they both have the same semantic meaning and we will make clear whether we are using relation partial function or decidable partial function, it should not cause any confusion.

## 2 TTL and UI

In this section, we define Teichmüller-Tukey lemma and update induction and emphasise that they are logically dual, up to the difference that the former is relative to predicates over subsets of arbitrary cardinals while update induction is relative to predicates over countable subsets. Underneath, they rely on the dual notions of predicate of finite character and of open predicate.
23:4 On the logical structure of some maximality and well-foundedness principles

► **Definition 2.** Let A be a type, $u : A_{\perp}^{*}$, $\alpha : A_{\perp}^{\mathbb{N}}$ and $T : \mathcal{P}(A_{\perp}^{*})$

$$u \subset_{\mathbb{N}} \alpha : \mathrm{Prop} \qquad \langle T \rangle_{\mathbb{N}} : \mathcal{P}(A_{\perp}^{\mathbb{N}})$$

$$u \subset_{\mathbb{N}} \alpha := \exists n^{\mathbb{N}}, u = \alpha|_n \qquad \langle T \rangle_{\mathbb{N}} := \lambda \alpha^{A_{\perp}^{\mathbb{N}}}. \forall u^{A^{*}}, u \subset_{\mathbb{N}} \alpha \rightarrow u \in T$$

$$\langle T \rangle_{\mathbb{N}}^{\circ} : \mathcal{P}(A_{\perp}^{\mathbb{N}})$$

$$\langle T \rangle_{\mathbb{N}}^{\circ} := \lambda \alpha^{A_{\perp}^{\mathbb{N}}}. \exists u^{A^{*}}, u \subset_{\mathbb{N}} \alpha \wedge u \in T$$

We conclude this section defining two different notions of partial functions:

► **Definition 3 (Relational partial function).** Let A, B be types, a relational partial function f from A to B is a relational functional relation of $\mathcal{P}(A \times B)$. Formally, a relational partial function from A to B is a term f : $\mathcal{P}(A \times B)$ such that $\forall a^A, \forall b, b^B, ((a, b) \in f \wedge (a, b') \in f) \rightarrow b = b'$. Its domain is defined by:

$$\mathrm{dom}(f) : \mathcal{P}(A)$$

$$\mathrm{dom}(f) := \lambda a^A. \exists b^B, (a, b) \in f$$

For all $a' : A$, we denote by $\mathrm{dom}(f) \cup a'$ the predicate $\lambda a^A. (\exists b^B, (a, b) \in f) \lor a = a'$.

► **Definition 4 (Decidable partial function).** Let A, B be types, a decidable partial function f from A to B is a total function f : A $\rightarrow$ B$_{⊥}$. Its domain and graph are defined by:

$$\mathrm{dom}(f) : \mathcal{P}(A) \qquad \mathcal{G}(f) : \mathcal{P}(A \times B)$$

$$\mathrm{dom}(f) := \lambda a^A. f(a) \neq \perp \qquad \mathcal{G}(f) := \lambda (a, b)^{A \times B}. f(a) = \mathrm{inl}(b)$$

For all $a' : A$, we denote by $\mathrm{dom}(f) \cup a'$ the predicate $\lambda a^A. f(a) \neq \perp \lor a = a'$.

**Notation:**

We write $f \in A \rightarrow_{\mathrm{p}} B$ to denote that $f$ is a relational partial function from $A$ to $B$ and $f : A \rightarrow B_{\perp}$ for the type of decidable partial functions from $A$ to $B$. We will also write $\Theta f^{A \rightarrow_{\mathrm{p}} B}, P$ for $\Theta f^{\mathcal{P}(A \times B)}, (f \in A \rightarrow_{\mathrm{p}} B) \rightarrow P$ for $\Theta \in \{\lambda, \forall, \exists\}$.

The difference between these two definitions is in the decidability of the domain: decidable partial functions have a decidable domain while it's not the case of relational partial functions. The graph operation $\mathcal{G}$ allows us to recover a relational partial function from a decidable partial function. One needs excluded middle to recover a decidable partial function from a relation partial function, hence decidable partial functions are stronger axiomatically. Notice that we used the same notation $\mathrm{dom}$ in both definitions. Since they both have the same semantic meaning and we will make clear whether we are using relation partial function or decidable partial function, it should not cause any confusion.

## 2 TTL and UI

In this section, we define Teichmüller-Tukey lemma and update induction and emphasise that they are logically dual, up to the difference that the former is relative to predicates over subsets of arbitrary cardinals while update induction is relative to predicates over countable subsets. Underneath, they rely on the dual notions of predicate of finite character and of open predicate.
## 2.1 Predicates of finite character

A set is of finite character if all its information is contained in its finite elements. In our setting, a predicate $P: \mathcal{P}(\mathcal{P}(A))$ is of finite character if all its information is contained in a predicate over lists. There are two canonical ways to express this:

**► Definition 5 (Finite character).** Let $A$ be a type and $P: \mathcal{P}(\mathcal{P}(A))$. We propose two definitions of finite character:

$$P \in \mathbf{FC}_1 := \forall \alpha^{\mathcal{P}(A)}, \alpha \in P \leftrightarrow \forall u^{A^*}, u \subset \alpha \rightarrow u \in \lfloor P \rfloor$$

$$P \in \mathbf{FC}_2 := \exists T^{\mathcal{P}(A^*)}, \langle T \rangle = P$$

Rewriting $\mathbf{FC}_1$ using the terms just defined:

$$P \in \mathbf{FC}_1 := P = \langle \lfloor P \rfloor \rangle$$

$\mathbf{FC}_1$ and $\mathbf{FC}_2$ are, in essence, paraphrases of one another, thus there is no reason not to expect them to be equivalent. First we will need a lemma:

**► Lemma 6.** Let $A$ be a type and $T: \mathcal{P}(A^*)$ then $\langle T \rangle \in \mathbf{FC}_1$.

*Proof.* Let $\alpha: \mathcal{P}(A)$. Suppose $\alpha \in \langle T \rangle$, our goal is to show that $\alpha \in \langle \lfloor T \rfloor \rangle$. Let $u: A^*$ such that $u \subset \alpha$, we will show that $u \in \lfloor T \rfloor$. By definition $u \in \lfloor T \rfloor$ if and only if $\langle u \rangle \in \langle T \rangle$ if and only if every sublist of $u$ is in $T$. Since $\alpha$ can be arbitrarily approximated by terms of $T$ and $u \subset \alpha$, so can $u$. Hence, $u \in \lfloor T \rfloor$ thus, $\alpha \in \langle \lfloor T \rfloor \rangle$.

Suppose $\alpha \in \langle \lfloor T \rfloor \rangle$, then for all $u: A^*$ such that $u \subset \alpha$, $u \in \lfloor T \rfloor$ which we can rewrite as $\langle u \rangle \in \langle T \rangle$. We easily show that $\langle u \rangle \in \langle T \rangle \rightarrow u \in T$ thus $\alpha \in \langle T \rangle$. ◀

We have shown that $\langle T \rangle = \langle \lfloor T \rfloor \rangle$. This means that without loss of generality, we can require in $\mathbf{FC}_2$ that the witness $T$ be of the form $\lfloor T' \rfloor$ for some $T'$. This is a way to express that $T$ can be chosen to be minimal. In fact if we are given $P$ and $T$ such as in $\mathbf{FC}_2$, it may happen that $T$ contains a list $u$ that is not closed under $\subseteq$ (i.e., $v \subseteq u \nrightarrow v \in T$). Such an $u$ will be invisible when looking at $\langle T \rangle$, hence we can consider $u$ as a superfluous term. The $\lfloor \langle \cdot \rangle \rfloor$ operation allows us, without loss of generality, to remove those terms, thus making $T$ minimal.

**► Theorem 7.** $\mathbf{FC}_1 \leftrightarrow \mathbf{FC}_2$

*Proof.* Let $A$ be a type and $P: \mathcal{P}(\mathcal{P}(A))$. From left to right: suppose $P \in \mathbf{FC}_1$. $\lfloor P \rfloor$ is a witness of $P \in \mathbf{FC}_2$.

From right to left: suppose $P \in \mathbf{FC}_2$, let $T$ be the witness of $P \in \mathbf{FC}_2$. By lemma 6 $\langle \lfloor T \rfloor \rangle = \langle T \rangle$ and by hypothesis $P = \langle T \rangle$, we can rewrite the first equality as $\langle \lfloor P \rfloor \rangle = P$. ◀

Since $\mathbf{FC}_1$ and $\mathbf{FC}_2$ are equivalent, we will from now on write $\mathbf{FC}$ without the indices.

## 2.2 Open predicates

A notion of open predicates over functions of countable domain was defined in Coquand [3] and generalised by Berger [1]. Using the definitions of Section 1.3, a predicate over $\alpha: A^N$ is open in the sense of Berger if it has the form $\alpha \in \langle T \rangle_N \rightarrow \alpha \in \langle U \rangle_N^\circ$ for some $T, U: \mathcal{P}(A^*)$. In order to get a closer correspondence with the notion of finite character, we will however stick to Coquand's definition. Additionally, to get a closer correspondence with the case of open predicates used in update induction, we consider open predicates for functions to $A_\perp$.
## 2.1 Predicates of finite character

A set is of finite character if all its information is contained in its finite elements. In our setting, a predicate $P: \mathcal{P}(\mathcal{P}(A))$ is of finite character if all its information is contained in a predicate over lists. There are two canonical ways to express this:

**Definition 5 (Finite character).** Let $A$ be a type and $P: \mathcal{P}(\mathcal{P}(A))$. We propose two definitions of finite character:

$$P \in \mathbf{FC}_1 := \forall \alpha^{\mathcal{P}(A)}, \alpha \in P \leftrightarrow \forall u^{A^*}, u \subset \alpha \rightarrow u \in \lfloor P \rfloor$$

$$P \in \mathbf{FC}_2 := \exists T^{\mathcal{P}(A^*)}, \langle T \rangle = P$$

Rewriting $\mathbf{FC}_1$ using the terms just defined:

$$P \in \mathbf{FC}_1 := P = \langle \lfloor P \rfloor \rangle$$

$\mathbf{FC}_1$ and $\mathbf{FC}_2$ are, in essence, paraphrases of one another, thus there is no reason not to expect them to be equivalent. First we will need a lemma:

**Lemma 6.** Let $A$ be a type and $T: \mathcal{P}(A^*)$ then $\langle T \rangle \in \mathbf{FC}_1$.

*Proof.* Let $\alpha: \mathcal{P}(A)$. Suppose $\alpha \in \langle T \rangle$, our goal is to show that $\alpha \in \langle \lfloor T \rfloor \rangle$. Let $u: A^*$ such that $u \subset \alpha$, we will show that $u \in \lfloor T \rfloor$. By definition $u \in \lfloor T \rfloor$ if and only if $\langle u \rangle \in \langle T \rangle$ if and only if every sublist of $u$ is in $T$. Since $\alpha$ can be arbitrarily approximated by terms of $T$ and $u \subset \alpha$, so can $u$. Hence, $u \in \lfloor T \rfloor$ thus, $\alpha \in \langle \lfloor T \rfloor \rangle$.

Suppose $\alpha \in \langle \lfloor T \rfloor \rangle$, then for all $u: A^*$ such that $u \subset \alpha$, $u \in \lfloor T \rfloor$ which we can rewrite as $\langle u \rangle \in \langle T \rangle$. We easily show that $\langle u \rangle \in \langle T \rangle \rightarrow u \in T$ thus $\alpha \in \langle T \rangle$. $\quad$

We have shown that $\langle T \rangle = \langle \lfloor T \rfloor \rangle$. This means that without loss of generality, we can require in $\mathbf{FC}_2$ that the witness $T$ be of the form $\lfloor T' \rfloor$ for some $T'$. This is a way to express that $T$ can be chosen to be minimal. In fact if we are given $P$ and $T$ such as in $\mathbf{FC}_2$, it may happen that $T$ contains a list $u$ that is not closed under $\subseteq$ (i.e., $v \subseteq u \nrightarrow v \in T$). Such an $u$ will be invisible when looking at $\langle T \rangle$, hence we can consider $u$ as a superfluous term. The $\lfloor \langle \cdot \rangle \rfloor$ operation allows us, without loss of generality, to remove those terms, thus making $T$ minimal.

**Theorem 7.** $\mathbf{FC}_1 \leftrightarrow \mathbf{FC}_2$

*Proof.* Let $A$ be a type and $P: \mathcal{P}(\mathcal{P}(A))$. From left to right: suppose $P \in \mathbf{FC}_1$. $\lfloor P \rfloor$ is a witness of $P \in \mathbf{FC}_2$.

From right to left: suppose $P \in \mathbf{FC}_2$, let $T$ be the witness of $P \in \mathbf{FC}_2$. By lemma 6 $\langle \lfloor T \rfloor \rangle = \langle T \rangle$ and by hypothesis $P = \langle T \rangle$, we can rewrite the first equality as $\langle \lfloor P \rfloor \rangle = P$. $\quad$

Since $\mathbf{FC}_1$ and $\mathbf{FC}_2$ are equivalent, we will from now on write $\mathbf{FC}$ without the indices.

## 2.2 Open predicates

A notion of open predicates over functions of countable domain was defined in Coquand [3] and generalised by Berger [1]. Using the definitions of Section 1.3, a predicate over $\alpha: A^N$ is open in the sense of Berger if it has the form $\alpha \in \langle T \rangle_N \rightarrow \alpha \in \langle U \rangle_N^\circ$ for some $T, U: \mathcal{P}(A^*)$. In order to get a closer correspondence with the notion of finite character, we will however stick to Coquand's definition. Additionally, to get a closer correspondence with the case of open predicates used in update induction, we consider open predicates for functions to $A_\perp$.
23:6 On the logical structure of some maximality and well-foundedness principles

► **Definition 8** (Countably-open predicate, in Coquand's sense, with partiality). Let A be a type and P : $\mathcal{P}(A_{\perp}^{\mathbb{N}})$. We define:

$$P \in \mathbf{OPEN}_{\mathbb{N}} := \exists T^{\mathcal{P}(A_{\perp}^{*})}, \langle T \rangle_{\mathbb{N}}^{\circ} = P$$

The observations made on predicates of finite character apply to countably-open predicates, namely that $\langle T \rangle_{\mathbb{N}}^{\circ} = \langle \lfloor \langle T \rangle_{\mathbb{N}}^{\circ} \rfloor \rangle_{\mathbb{N}}^{\circ}$. Obviously, we can also move from $A_{\perp}^{\mathbb{N}}$ to $\mathcal{P}(A)$ and introduce a general notion of open predicates which again, will satisfy $\langle T \rangle^{\circ} = \langle \lfloor \langle T \rangle^{\circ} \rfloor \rangle^{\circ}$:

► **Definition 9** (Open predicate). Let A be a type and P : $\mathcal{P}(\mathcal{P}(A))$. We define:

$$P \in \mathbf{OPEN} := \exists T^{\mathcal{P}(A^*)}, \langle T \rangle^{\circ} = P$$

Conversely, we can define a notion of predicate of countably-finite character dual the notion of countably-open predicate:

► **Definition 10** (Predicate of countably-finite character). Let A be a type and P : $\mathcal{P}(A_{\perp}^{\mathbb{N}})$. We define:

$$P \in \mathbf{FC}_{\mathbb{N}} := \exists T^{\mathcal{P}(A_{\perp}^{*})}, \langle T \rangle_{\mathbb{N}}^{\circ} = P$$

This finally results in the following dualities:

<table><caption>Table 1 Predicates of finite character VS Open predicate</caption><thead><tr><th></th><th>Universal notion</th><th>Existential notion</th></tr></thead><tbody><tr><td>Arbitrary subsets</td><td>Finite character</td><td>Open</td></tr><tr><td>Countable subsets</td><td>Countably-finite character</td><td>Countably-open</td></tr></tbody></table>

2.3 Teichmüller-Tukey lemma and Update induction

Before defining Teichmüller-Tukey lemma we need a few definitions:

► **Definition 11.** Let A be a type, P : $\mathcal{P}(\mathcal{P}(A))$ and $\alpha, \beta : \mathcal{P}(A)$. We define:

$$\beta \prec \alpha : \mathrm{Prop}$$

$$\beta \prec \alpha := \exists a^A, a \notin \alpha \land \beta = (\lambda x^A. x \in \alpha \lor x = a)$$

$$\alpha \in \mathbf{Max}_{\prec}(P) : \mathrm{Prop}$$

$$\alpha \in \mathbf{Max}_{\prec}(P) := \alpha \in P \land \forall \beta^{\mathcal{P}(A)}, \beta \prec \alpha \rightarrow \beta \notin P$$

Thus, $\beta \prec \alpha$ stands for $\beta$ extends $\alpha$ (if $\beta$ is an update of $\alpha$) while $\mathbf{Max}_{\prec}(P)$ is the predicate of maximal elements of $(P, \succ)$ ($\succ$ is the reverse of $\prec$).

What we are interested in are predicates of finite character but Theorem 7 allows us to consider only predicates on lists since there is a correspondence between them. Hence, we will quantify or instantiate schemas on predicate on lists.

► **Definition 12** (Teichmüller-Tukey lemma). Let A be a type and T : $\mathcal{P}(A^*)$, we define the Teichmüller-Tukey lemma, $\mathbf{TTL}_{AT}$:

$$(\exists \alpha^{\mathcal{P}(A)}, \alpha \in \langle T \rangle) \rightarrow \exists \alpha^{\mathcal{P}(A)}, \alpha \in \mathbf{Max}_{\prec}(\langle T \rangle)$$
23:6 On the logical structure of some maximality and well-foundedness principles

► **Definition 8** (Countably-open predicate, in Coquand's sense, with partiality). Let A be a type and P : $\mathcal{P}(A_\perp)$. We define:

$$P \in \mathbf{OPEN}_N := \exists T^{\mathcal{P}(A_\perp)}, \langle T \rangle_\mathcal{N}^\circ = P$$

The observations made on predicates of finite character apply to countably-open predicates, namely that $\langle T \rangle_\mathcal{N}^\circ = \langle \lfloor \langle T \rangle_\mathcal{N}^\circ \rfloor \rangle_\mathcal{N}^\circ$. Obviously, we can also move from $A_\perp^N$ to $\mathcal{P}(A)$ and introduce a general notion of open predicates which again, will satisfy $\langle T \rangle_\mathcal{N}^\circ = \langle \lfloor \langle T \rangle_\mathcal{N}^\circ \rfloor \rangle_\mathcal{N}^\circ$:

► **Definition 9** (Open predicate). Let A be a type and P : $\mathcal{P}(\mathcal{P}(A))$. We define:

$$P \in \mathbf{OPEN} := \exists T^{\mathcal{P}(A^*)}, \langle T \rangle_\mathcal{N}^\circ = P$$

Conversely, we can define a notion of predicate of countably-finite character dual the notion of countably-open predicate:

► **Definition 10** (Predicate of countably-finite character). Let A be a type and P : $\mathcal{P}(A_\perp^N)$. We define:

$$P \in \mathbf{FC}_N := \exists T^{\mathcal{P}(A_\perp^*)}, \langle T \rangle_\mathcal{N} = P$$

This finally results in the following dualities:

<table><caption>Table 1 Predicates of finite character VS Open predicate</caption><thead><tr><th></th><th>Universal notion</th><th>Existential notion</th></tr></thead><tbody><tr><td>Arbitrary subsets</td><td>Finite character</td><td>Open</td></tr><tr><td>Countable subsets</td><td>Countably-finite character</td><td>Countably-open</td></tr></tbody></table>

2.3 Teichmüller-Tukey lemma and Update induction

Before defining Teichmüller-Tukey lemma we need a few definitions:

► **Definition 11.** Let A be a type, P : $\mathcal{P}(\mathcal{P}(A))$ and $\alpha, \beta : \mathcal{P}(A)$. We define:

$$\beta \prec \alpha : \mathrm{Prop}$$

$$\beta \prec \alpha := \exists a^A, a \notin \alpha \wedge \beta = (\lambda x^A. x \in \alpha \lor x = a)$$

$$\alpha \in \mathbf{Max}_<(P) : \mathrm{Prop}$$

$$\alpha \in \mathbf{Max}_<(P) := \alpha \in P \wedge \forall \beta^{\mathcal{P}(A)}, \beta \prec \alpha \rightarrow \beta \notin P$$

Thus, $\beta \prec \alpha$ stands for $\beta$ extends $\alpha$ (if $\beta$ is an update of $\alpha$) while $\mathbf{Max}_<(P)$ is the predicate of maximal elements of $(P, \succ)$ ($\succ$ is the reverse of $<$).

What we are interested in are predicates of finite character but Theorem 7 allows us to consider only predicates on lists since there is a correspondence between them. Hence, we will quantify or instantiate schemas on predicate on lists.

► **Definition 12** (Teichmüller-Tukey lemma). Let A be a type and T : $\mathcal{P}(A^*)$, we define the Teichmüller-Tukey lemma, $\mathbf{TTL}_{AT}$:

$$(\exists \alpha^{\mathcal{P}(A)}, \alpha \in \langle T \rangle) \rightarrow \exists \alpha^{\mathcal{P}(A)}, \alpha \in \mathbf{Max}_<(\langle T \rangle)$$
**Notations:**

TTL denotes the full schema: for all types A and all T : P(A*), ∃αP(A), α ∈ ⟨T⟩ → ∃αP(A), α ∈ Max_⟨⟨T⟩⟩.

TTL<sub>AT</sub> denotes the schema specialised in this A and this T.

TTL<sub>AT</sub> denotes the restriction of the full schema TTL to A and T of a particular shape. For example: TTL<sub>NT</sub> is the schema: for all T : P(N*), ∃αP(N), α ∈ ⟨T⟩ → ∃αP(N), α ∈ Max_⟨⟨T⟩⟩. Moreover, if C<sub>A</sub> denotes a particular collection of predicates over lists of A (A is a parameter), then TTL<sub>AC<sub>A</sub></sub> denotes the restrictions of the schema TTL to any A type and T : P(A*) that is in C<sub>A</sub>.

Following an earlier remark, we impose that the finite character predicate we are considering must be inhabited, without this TTL becomes trivially inconsistent. Having defined TTL we now show that we can recover an induction principle by using contraposition and Morgan's rules:

Unfolding some definitions, TTL<sub>AT</sub> is

$$(\exists \alpha^{P(A)}, \alpha \in \langle T \rangle) \rightarrow \exists \alpha^{P(A)}, \alpha \in \langle T \rangle \wedge (\forall \beta^{P(A)}, \beta \prec \alpha \rightarrow \beta \notin \langle T \rangle)$$

Contraposing and pushing some negations:

$$\forall \alpha^{P(A)}, [\neg(\alpha \in \langle T \rangle) \lor \neg\forall \beta^{P(A)}, \beta \prec \alpha \rightarrow \beta \notin \langle T \rangle] \rightarrow \forall \alpha^{P(A)}, \alpha \notin \langle T \rangle$$

We have a sub-formula of the form $\neg A \lor \neg B$, we have the choice of writing it as $A \rightarrow \neg B$ or $B \rightarrow \neg A$. The first choice leads to a principle we will call TTL<sub>AT</sub><sup>co</sup>:

$$\forall \alpha^{P(A)}, [\alpha \in \langle T \rangle \rightarrow \exists \beta^{P(A)}, \beta \prec \alpha \wedge \beta \in \langle T \rangle] \rightarrow \forall \alpha^{P(A)}, \alpha \notin \langle T \rangle$$

And the second choice leads to an induction principle:

$$\forall \alpha^{P(A)}, [(\forall \beta^{P(A)}, \beta \prec \alpha \rightarrow \beta \notin \langle T \rangle) \rightarrow \alpha \notin \langle T \rangle] \rightarrow \forall \alpha^{P(A)}, \alpha \notin \langle T \rangle$$

TTL<sup>co</sup> is intuitively an opposite formulation of TTL. The induction principle we obtain seems to express something different. We can push further the negations in order to obtain a positive formulation of it:

$$\forall \alpha^{P(A)}, [\neg(\forall \beta^{P(A)}, \beta \prec \alpha \rightarrow \beta \in \langle T \rangle^\circ) \rightarrow \alpha \in \langle T \rangle^\circ] \rightarrow \forall \alpha^{P(A)}, \alpha \in \langle T \rangle^\circ$$

And this can be seen as a generalisation of Berger's update induction [1] going from countably-open predicates to arbitrary open predicates.

To state update induction, we need to focus on partial functions from $\mathbb{N}$ to A which we equip with an order:

**► Definition 13.** Let A be a type, P : P(A<sub>⊥</sub><sup>N</sup>) and α, β : A<sub>⊥</sub><sup>N</sup>. We define:

$$\beta \prec_N \alpha : \text{Prop}$$

$$\beta \prec_N \alpha := \exists m^N, \exists a^A, \alpha(m) = \perp \land \beta(m) = a \land \forall n^N, n \neq m \rightarrow \alpha(n) = \beta(n)$$

Like TTL, update induction is originally defined on open predicates but since any open predicate comes from a predicate on lists, we can more primitively state it as follows:
**Notations:**

TTL denotes the full schema: for all types A and all T : P(A*), ∃αP(A), α ∈ ⟨T⟩ → ∃αP(A), α ∈ Max_⟨⟨T⟩⟩.

TTL<sub>AT</sub> denotes the schema specialised in this A and this T.

TTL<sub>AT</sub> denotes the restriction of the full schema TTL to A and T of a particular shape. For example: TTL<sub>NT</sub> is the schema: for all T : P(N*), ∃αP(N), α ∈ ⟨T⟩ → ∃αP(N), α ∈ Max_⟨⟨T⟩⟩. Moreover, if C<sub>A</sub> denotes a particular collection of predicates over lists of A (A is a parameter), then TTL<sub>AC<sub>A</sub></sub> denotes the restrictions of the schema TTL to any A type and T : P(A*) that is in C<sub>A</sub>.

Following an earlier remark, we impose that the finite character predicate we are considering must be inhabited, without this TTL becomes trivially inconsistent. Having defined TTL we now show that we can recover an induction principle by using contraposition and Morgan's rules:

Unfolding some definitions, TTL<sub>AT</sub> is

$$(\exists \alpha^{P(A)}, \alpha \in \langle T \rangle) \rightarrow (\exists \alpha^{P(A)}, \alpha \in \langle T \rangle \wedge (\forall \beta^{P(A)}, \beta \prec \alpha \rightarrow \beta \notin \langle T \rangle))$$

Contraposing and pushing some negations:

$$\forall \alpha^{P(A)}, [\neg(\alpha \in \langle T \rangle) \lor \neg\forall \beta^{P(A)}, \beta \prec \alpha \rightarrow \beta \notin \langle T \rangle] \rightarrow \forall \alpha^{P(A)}, \alpha \notin \langle T \rangle$$

We have a sub-formula of the form $\neg A \lor \neg B$, we have the choice of writing it as $A \rightarrow \neg B$ or $B \rightarrow \neg A$. The first choice leads to a principle we will call TTL<sub>AT</sub><sup>co</sup>:

$$\forall \alpha^{P(A)}, [\alpha \in \langle T \rangle \rightarrow (\exists \beta^{P(A)}, \beta \prec \alpha \wedge \beta \in \langle T \rangle)] \rightarrow \forall \alpha^{P(A)}, \alpha \notin \langle T \rangle$$

And the second choice leads to an induction principle:

$$\forall \alpha^{P(A)}, [(\forall \beta^{P(A)}, \beta \prec \alpha \rightarrow \beta \notin \langle T \rangle) \rightarrow \alpha \notin \langle T \rangle] \rightarrow \forall \alpha^{P(A)}, \alpha \notin \langle T \rangle$$

TTL<sup>co</sup> is intuitively an opposite formulation of TTL. The induction principle we obtain seems to express something different. We can push further the negations in order to obtain a positive formulation of it:

$$\forall \alpha^{P(A)}, [(\forall \beta^{P(A)}, \beta \prec \alpha \rightarrow \beta \in \langle T \rangle^{\circ}) \rightarrow \alpha \in \langle T \rangle^{\circ}] \rightarrow \forall \alpha^{P(A)}, \alpha \in \langle T \rangle^{\circ}$$

And this can be seen as a generalisation of Berger's update induction [1] going from countably-open predicates to arbitrary open predicates.

To state update induction, we need to focus on partial functions from $\mathbb{N}$ to A which we equip with an order:

**► Definition 13.** Let A be a type, P : P(A<sub>⊥</sub><sup>N</sup>) and α, β : A<sub>⊥</sub><sup>N</sup>. We define:

$$\beta \prec_N \alpha : \text{Prop}$$

$$\beta \prec_N \alpha := \exists m^{\mathbb{N}}, \exists a^A, \alpha(m) = \perp \land \beta(m) = a \land \forall n^{\mathbb{N}}, n \neq m \rightarrow \alpha(n) = \beta(n)$$

Like TTL, update induction is originally defined on open predicates but since any open predicate comes from a predicate on lists, we can more primitively state it as follows:
23:8 On the logical structure of some maximality and well-foundedness principles

**Definition 14 (Update induction).** Let A be a type and T : $\mathcal{P}(A^*_{\perp})$, we define Update induction, $\mathbf{UI}_{AT}$:

$$ \forall \alpha^{A^N_{\perp}}, [(\forall \beta^{A^N_{\perp}}, \beta \prec_N \alpha \rightarrow \beta \in \langle T \rangle^{\circ}_{\mathbb{N}}) \rightarrow \alpha \in \langle T \rangle^{\circ}_{\mathbb{N}}] \rightarrow \forall \alpha^{A^N_{\perp}}, \alpha \in \langle T \rangle^{\circ}_{\mathbb{N}} $$

Contrastingly, we now formally state the dual of TTL that we obtained above:

**Definition 15 (Generalised update induction).** Let A be a type and T : $\mathcal{P}(A^*)$, we define Generalised update induction, $\mathbf{GUI}_{AT}$:

$$ \forall \alpha^{\mathcal{P}(A)}, [(\forall \beta^{\mathcal{P}(A)}, \beta \prec \alpha \rightarrow \beta \in \langle T \rangle^{\circ}) \rightarrow \alpha \in \langle T \rangle^{\circ}] \rightarrow \forall \alpha^{\mathcal{P}(A)}, \alpha \in \langle T \rangle^{\circ} $$

Also, we introduce a countable version of TTL, logically dual to UI:

**Definition 16 (Countable Teichmüller-Tukey lemma).** Let A be a type and T : $\mathcal{P}(A^*_{\perp})$, we define the countable Teichmüller-Tukey lemma, $\mathbf{TTL}^N_{AT}$:

$$ (\exists \alpha^{A^N_{\perp}}, \alpha \in \langle T \rangle_{\mathbb{N}}) \rightarrow \exists \alpha^{A^N_{\perp}}, \alpha \in \mathbf{Max}_{<_{\mathbb{N}}} (\langle T \rangle_{\mathbb{N}}) $$

We thus obtain the following table:

<table><caption>**Table 2** Maximality principles VS Induction principles</caption><thead><tr><th></th><th>Finite character</th><th>Open</th></tr></thead><tbody><tr><td>Arbitrary subsets</td><td><b>TTL</b><sub>AT</sub></td><td><b>GUI</b><sub>AT</sub></td></tr><tr><td>Countable subsets</td><td><b>TTL</b><sup>N</sup><sub>AT</sub></td><td><b>UI</b><sub>AT</sub></td></tr></tbody></table>

In particular, since TTL is classically equivalent to the full axiom of choice, GUI is also classically equivalent to the full axiom of choice.

3 TTL and Zorn's lemma

In this section we analyse precisely the relationships of TTL with Zorn's lemma. We go further than showing their equivalence, we look at which part of TTL (as a schema) is necessary to prove Zorn's lemma and reciprocally. This equivalence result is also a proof that the version of Teichmüller-Tukey lemma we defined captures the full choice.

**Definition 17.** Let A be a type, < a strict order on A, a : A and E, F : $\mathcal{P}(A)$. Define:

$$ E \in \mathbf{Ch}(A) : \mathrm{Prop} $$

$$ E \in \mathbf{Ch}(A) := \forall a, b^A, a, b \in E \rightarrow (a < b \lor b < a \lor a = b) $$

$$ F \in \mathbf{SCh}(E) : \mathrm{Prop} $$

$$ F \in \mathbf{SCh}(E) : F \subseteq E \land F \in \mathbf{Ch}(A) $$

$$ E \in \mathbf{Ind}(A) : \mathrm{Prop} $$

$$ E \in \mathbf{Ind}(A) := (\forall F^{\mathcal{P}(A)}, F \in \mathbf{SCh}(E) \rightarrow \exists a^A, a \in E \land \forall b^A, b \in F \rightarrow b \le a) $$

$$ a \in \mathbf{Max}_{<}(E) : \mathrm{Prop} $$

$$ a \in \mathbf{Max}_{<}(E) := a \in E \land \forall b^A, a < b \rightarrow b \notin E $$
23:8 On the logical structure of some maximality and well-foundedness principles

**Definition 14 (Update induction).** Let A be a type and T : $\mathcal{P}(A^*_{\perp})$, we define Update induction, $\mathbf{UI}_{AT}$:

$$ \forall \alpha^{A^N_{\perp}}, [(\forall \beta^{A^N_{\perp}}, \beta \prec_N \alpha \rightarrow \beta \in \langle T \rangle^{\circ}_{\mathbb{N}}) \rightarrow \alpha \in \langle T \rangle^{\circ}_{\mathbb{N}}] \rightarrow \forall \alpha^{A^N_{\perp}}, \alpha \in \langle T \rangle^{\circ}_{\mathbb{N}} $$

Contrastingly, we now formally state the dual of TTL that we obtained above:

**Definition 15 (Generalised update induction).** Let A be a type and T : $\mathcal{P}(A^*)$, we define Generalised update induction, $\mathbf{GUI}_{AT}$:

$$ \forall \alpha^{\mathcal{P}(A)}, [(\forall \beta^{\mathcal{P}(A)}, \beta \prec \alpha \rightarrow \beta \in \langle T \rangle^{\circ}) \rightarrow \alpha \in \langle T \rangle^{\circ}] \rightarrow \forall \alpha^{\mathcal{P}(A)}, \alpha \in \langle T \rangle^{\circ} $$

Also, we introduce a countable version of TTL, logically dual to UI:

**Definition 16 (Countable Teichmüller-Tukey lemma).** Let A be a type and T : $\mathcal{P}(A^*_{\perp})$, we define the countable Teichmüller-Tukey lemma, $\mathbf{TTL}^N_{AT}$:

$$ (\exists \alpha^{A^N_{\perp}}, \alpha \in \langle T \rangle_{\mathbb{N}}) \rightarrow \exists \alpha^{A^N_{\perp}}, \alpha \in \mathbf{Max}_{<_{\mathbb{N}}} (\langle T \rangle_{\mathbb{N}}) $$

We thus obtain the following table:

<table><caption>Table 2 Maximality principles VS Induction principles</caption><thead><tr><th></th><th>Finite character</th><th>Open</th></tr></thead><tbody><tr><td>Arbitrary subsets</td><td><b>TTL</b><sub>AT</sub></td><td><b>GUI</b><sub>AT</sub></td></tr><tr><td>Countable subsets</td><td><b>TTL</b><sup>N</sup><sub>AT</sub></td><td><b>UI</b><sub>AT</sub></td></tr></tbody></table>

In particular, since TTL is classically equivalent to the full axiom of choice, GUI is also classically equivalent to the full axiom of choice.

3 TTL and Zorn's lemma

In this section we analyse precisely the relationships of TTL with Zorn's lemma. We go further than showing their equivalence, we look at which part of TTL (as a schema) is necessary to prove Zorn's lemma and reciprocally. This equivalence result is also a proof that the version of Teichmüller-Tukey lemma we defined captures the full choice.

**Definition 17.** Let A be a type, < a strict order on A, a : A and E, F : $\mathcal{P}(A)$. Define:

$$ E \in \mathbf{Ch}(A) : \mathrm{Prop} $$

$$ E \in \mathbf{Ch}(A) := \forall a, b^A, a, b \in E \rightarrow (a < b \lor b < a \lor a = b) $$

$$ F \in \mathbf{SCh}(E) : \mathrm{Prop} $$

$$ F \in \mathbf{SCh}(E) : F \subseteq E \land F \in \mathbf{Ch}(A) $$

$$ E \in \mathbf{Ind}(A) : \mathrm{Prop} $$

$$ E \in \mathbf{Ind}(A) := (\forall F^{\mathcal{P}(A)}, F \in \mathbf{SCh}(E) \rightarrow \exists a^A, a \in E \land \forall b^A, b \in F \rightarrow b \le a) $$

$$ a \in \mathbf{Max}_{<}(E) : \mathrm{Prop} $$

$$ a \in \mathbf{Max}_{<}(E) := a \in E \land \forall b^A, a < b \rightarrow b \notin E $$
Where $\leq$ is the reflexive closure of $<$.

Ch is the chain predicate, SCh is the subchain predicate, Ind is the inductive "subset" predicate and Max< is simply the maximal element predicate. We choose to express these definitions in terms of predicates over types rather than directly in terms of types, to avoid discussions on proof relevance and stay in a more general setting. If we were proof-irrelevant, instantiating our schemas on predicates over types would be identical to doing it directly on types which would simplify notations and yield the same results. We can now define concisely Zorn's lemma:

**Definition 18 (Zorn lemma).** Let A be a type, < a strict order on A, and E a predicate on A. Zorn<sub>A<sub>≤</sub>E</sub> is the following statement

$$E \in \mathbf{Ind} \rightarrow \exists a^A, a \in \mathbf{Max}_< (E)$$

**Theorem 19.** TTL ↔ Zorn

The following is an adaptation of a usual set-theoretic proof in our setting.

**Proof.** From left to right: fix A a type, < a strict order on A and E : P(A) such that E ∈ Ind(A). We first show that SCh(E) is of finite character:

Let F : P(A) such that $F \in SCh(E)$, we show $F \in \langle [SCh(E)] \rangle$: let $u : A^*$ such that $u \subset F$, $\langle u \rangle$ is thus a chain of E therefore $u \in [SCh(E)]$. Let $F : P(A)$ such that $F \in \langle [SCh(E)] \rangle$, by choosing lists of length 2 we can show that F is a subchain of E. Hence $SCh(E) \in FC$.

Using TTL<sub>A|[SCh(E)]</sub>, we get $G : P(A)$ such that $G \in \mathbf{Max}(SCh(E))$. G is a subchain of E, since E is inductive we get $g : A$ such that $g \in E$ and $\forall aA, a \in G \rightarrow a < g$. Suppose we have $h : A$ such that $g < h$ and $h \in E$. Let $G' := \lambda a^A.\exists \beta^P(A), \beta \in Q \land a \in \beta$. By construction, $\alpha$ is an upper bound of Q, let's show that it is indeed in $\langle T \rangle$. Since $\langle T \rangle$ is of finite character it suffices to show that for all $u : A^*$, $u \subset \alpha \rightarrow u \in T$. Let $u : A^*$ such that $u \subset \alpha$. Since u is a finite list, we can enumerate its elements $a_0, \dots, a_n$. For all $0 \le i \le n$, let $\beta_i : P(A)$ be such that $\beta_i \in \beta_i \in Q$. Since Q is chain, there exists $0 \le i_0 \le n$ such that for all $0 \le i \le n, \beta_i \subseteq \beta_{i_0}$. Thus, $u \subset \beta_{i_0}, \beta_{i_0} \in \langle T \rangle$ and so $u \in \langle T \rangle$. ◀

From right to left: let $T : P(A^*)$. $\subset$ is a strict order on P(P(A)). Since $\langle T \rangle$ is of finite character, a maximal element for $\subset$ is also a maximal element for $>$. Hence, what is left to show is that $\langle T \rangle$ is inductive and use Zorn<sub>P(A)⊂<T></sub> to produce a maximal term. Let $Q : P(P(A))$ such that $Q \in SCh(\langle T \rangle)$. Let $\alpha := \lambda a^A.\exists \beta^P(A), \beta \in Q \land a \in \beta$. By construction, $\alpha$ is an upper bound of Q, let's show that it is indeed in $\langle T \rangle$. Since $\langle T \rangle$ is of finite character it suffices to show that for all $u : A^*$, $u \subset \alpha \rightarrow u \in T$. Let $u : A^*$ such that $u \subset \alpha$. Since u is a finite list, we can enumerate its elements $a_0, \dots, a_n$. For all $0 \le i \le n$, let $\beta_i : P(A)$ be such that $\beta_i \in \beta_i \in Q$. Since Q is chain, there exists $0 \le i_0 \le n$ such that for all $0 \le i \le n, \beta_i \subseteq \beta_{i_0}$. Thus, $u \subset \beta_{i_0}, \beta_{i_0} \in \langle T \rangle$ and so $u \in \langle T \rangle$. ◀

Looking more closely at this proof we notice that we have proved a finer result than simply the equivalence. We have shown TTL<sub>A|[SCh(E)]</sub> → Zorn<sub>A<sub>≤</sub>E</sub> and Zorn<sub>P(A)⊂<T></sub> → TTL<sub>AT</sub>. We can express for a predicate over lists to be of the form $[SCh(E)]$ in a more syntactic way.

**Definition 20.** Let A be a type and T : P(A*), we say that T is a list of chains, if there exists T' such that:

- $\epsilon \in T'$

- $u \@ a \in T'$ and $[a] \star v \in T'$ if and only if $u \star [a] \star v \in T'$

- $u \star [a] \star v \in T'$ implies $u \star v \in T'$
Where $\leq$ is the reflexive closure of $<$.

Ch is the chain predicate, SCh is the subchain predicate, Ind is the inductive "subset" predicate and Max< is simply the maximal element predicate. We choose to express these definitions in terms of predicates over types rather than directly in terms of types, to avoid discussions on proof relevance and stay in a more general setting. If we were proof-irrelevant, instantiating our schemas on predicates over types would be identical to doing it directly on types which would simplify notations and yield the same results.
We can now define concisely Zorn's lemma:

**Definition 18 (Zorn lemma).** Let A be a type, < a strict order on A, and E a predicate on A. Zorn<sub>A<sub>≤</sub>E</sub> is the following statement

$$E \in \mathbf{Ind} \rightarrow \exists a^A, a \in \mathbf{Max}_< (E)$$

**Theorem 19.** TTL ↔ Zorn

The following is an adaptation of a usual set-theoretic proof in our setting.

**Proof.** From left to right: fix A a type, < a strict order on A and E : P(A) such that E ∈ Ind(A). We first show that SCh(E) is of finite character:

Let F : P(A) such that F ∈ SCh(E), we show F ∈ ⟨[SCh(E)]⟩: let u : A* such that u ⊂ F, ⟨u⟩ is thus a chain of E therefore u ∈ ⌊SCh(E)⌋. Let F : P(A) such that F ∈ ⟨[SCh(E)]⟩, by choosing lists of length 2 we can show that F is a subchain of E. Hence SCh(E) ∈ FC.

Using TTL<sub>A|[SCh(E)]</sub>, we get G : P(A) such that G ∈ Max(SCh(E)). G is a subchain of E, since E is inductive we get g : A such that g ∈ E and ∀aA, a ∈ G → a < g. Suppose we have h : A such that g < h and h ∈ E. Let G' := λaA.∃βP(A), β ∈ Q ∧ a ∈ β. By construction, α is an upper bound of Q, let's show that it is indeed in ⟨T⟩. Since ⟨T⟩ is of finite character it suffices to show that for all u : A*, u ⊂ α → u ∈ T. Let u : A* such that u ⊂ α. Since u is a finite list, we can enumerate its elements a₀, ..., aₙ. For all 0 ≤ i ≤ n, let βᵢ : P(A) be such that aᵢ ∈ βᵢ and βᵢ ∈ Q. Since Q is chain, there exists 0 ≤ i₀ ≤ n such that for all 0 ≤ i ≤ n, βᵢ ≤ βᵢ₀. Thus, u ⊂ βᵢ₀, βᵢ₀ ∈ ⟨T⟩ and so u ∈ ⟨T⟩. ◀

From right to left: let T : P(A*). ⊂ is a strict order on P(P(A)). Since ⟨T⟩ is of finite character, a maximal element for ⊂ is also a maximal element for $>$. Hence, what is left to show is that ⟨T⟩ is inductive and use Zorn<sub>P(A)⊂⟨T⟩</sub> to produce a maximal term. Let Q : P(P(A)) such that Q ∈ SCh(⟨T⟩). Let α := λaA.∃βP(A), β ∈ Q ∧ a ∈ β. By construction, α is an upper bound of Q, let's show that it is indeed in ⟨T⟩. Since ⟨T⟩ is of finite character it suffices to show that for all u : A*, u ⊂ α → u ∈ T. Let u : A* such that u ⊂ α. Since u is a finite list, we can enumerate its elements a₀, ..., aₙ. For all 0 ≤ i ≤ n, let βᵢ : P(A) be such that aᵢ ∈ βᵢ and βᵢ ∈ Q. Since Q is chain, there exists 0 ≤ i₀ ≤ n such that for all 0 ≤ i ≤ n, βᵢ ≤ βᵢ₀. Thus, u ⊂ βᵢ₀, βᵢ₀ ∈ ⟨T⟩ and so u ∈ ⟨T⟩. ◀

Looking more closely at this proof we notice that we have proved a finer result than simply the equivalence. We have shown TTL<sub>A|[SCh(E)]</sub> → Zorn<sub>A<sub>≤</sub>E</sub> and Zorn<sub>P(A)⊂⟨T⟩</sub> → TTL<sub>AT</sub>. We can express for a predicate over lists to be of the form ⌊SCh(E)⌋ in a more syntactic way.

**Definition 20.** Let A be a type and T : P(A*), we say that T is a list of chains, if there exists T' such that:

- $\epsilon \in T'$

- $u \@ a \in T'$ and $[a] \star v \in T'$ if and only if $u \star [a] \star v \in T'$

- $u \star [a] \star v \in T'$ implies $u \star v \in T'$
23:10 On the logical structure of some maximality and well-foundedness principles

if $a \neq b$ and $u \star [a] \star v \star [b] \star w \in T'$ then for all $u', v', w' : A^*$, $u' \star [b] \star v' \star [a] \star w' \notin T'$ and $T$ is the downward closure of $T'$ by $\subseteq$. We denote by $C_A$ the collection of lists of chains of $A$.

**Lemma 21.** Let $A$ be a type, < a strict order on $A$ and $E : \mathcal{P}(A)$, then there exists $T \in C_A$ such that $\mathbf{SCh}(E) = \langle T \rangle$. Reciprocally, let $A$ be a type, then for every $T \in C_A$ there exist a strict order < on $A$ and $E : \mathcal{P}(A)$ such that $\mathbf{SCh}(E) = \langle T \rangle$.

**Proof.** Proof of the first statement: we inductively define a $T' : \mathcal{P}(A^*)$.

$$ \frac{\varepsilon \in T'}{[a] \in T'} \qquad \frac{a \in E}{b \in E} \qquad \frac{a < b \quad u@a \in T'}{u@a@b \in T'} $$

We easily show that $T'$ satisfies the conditions of the above definition. Let $T$ be the downward closure of $T'$. Let $F \in \mathbf{SCh}(E)$ and $u : A^*$ such that $u \subset F$. Since $F$ is a chain we can construct a list $u'$ of all elements of $u$ such that $u'$ does not contain twice the same element and is ordered increasingly relative to $<$. $u'$ is thus in $T'$ hence $u$ is in $T$. Let $F \in \langle T \rangle$ and $a, b : A$ such that $a, b \in F$. By hypothesis the list $[a, b]$ is in $T$. There exists $u \in T'$ such that $[a, b] \subset u$. Hence $a, b \in \langle u \rangle$ which is a chain. In conclusion $F$ is a subchain of $E$.

Proof of the reciprocal: suppose given a type $A$ with decidable equality and $T \in C_A$. There exists a $T'$ satisfying the aforementioned conditions. Let $E := \lambda a^A. \exists u A^*, u \in T' \wedge a \in u$. We now must define an ordering on $A$. Define < a binary relation on $A$ such that $a < b := [a, b] \in T'$. Using last "axiom" of the definition of $T'$ we easily show that it is irreflexive. For transitivity notice that if $[a, b], [b, c] \in T'$ then $[a, b, c] \in T'$ then $[a, c] \in T'$. Thus, it is a strict ordering on $A$. Let $F \in \mathbf{SCh}(E)$ and $u : A^*$ such that $u \subset F$. We can assume that $u$ is sorted increasingly relatively to $<$. Using the same trick used for proving transitivity show that $u \in T$. Let $F \in \langle T \rangle$ and $a, b : A$ such that $a, b \in F$. By hypothesis the list $[a, b]$ is in $T$ therefore, $a < b$ which means that $F$ is indeed a chain. ◀

**Corollary 22.** $\overline{\text{TTL}}_{AC_A} \to \text{Zorn and } \overline{\text{Zorn}}_{P(A)\subset\langle T \rangle} \to \text{TTL}$. Hence we deduce the somewhat surprising results TTL $\leftrightarrow \overline{\text{TTL}}_{AC_A}$ and Zorn $\leftrightarrow \overline{\text{Zorn}}_{P(A)\subset\langle T \rangle}$.

Looking back at the path we took to arrive at this conclusion, the results are quite expected, but looking only at the definition of a list of chains it is quite surprising that restricting TTL this much does not change its power.

4 ∃MPCF

In this section we define a choice principle ∃MPCF which stands for “Exists a Maximal Partial Choice Function” and a weaker version ∃MPCF⁻. It is weaker in the sense that ∃MPCF implies ∃MPCF⁻ but the equivalence is true if we allow excluded middle. We show that ∃MPCF⁻ is equivalent in its general form to TTL and link ∃MPCF to the general class of dependent choice GDC, given by Brede and the first author in [2]. In particular, ∃MPCF and ∃MPCF⁻ can be seen as refinements of TTL whose strength is more explicitly controlled.
23:10 On the logical structure of some maximality and well-foundedness principles

if $a \neq b$ and $u \star [a] \star v \star [b] \star w \in T'$ then for all $u', v', w' : A^*$, $u' \star [b] \star v' \star [a] \star w' \notin T'$ and $T$ is the downward closure of $T'$ by $\subseteq$. We denote by $C_A$ the collection of lists of chains of $A$.

**Lemma 21.** Let $A$ be a type, < a strict order on $A$ and $E : \mathcal{P}(A)$, then there exists $T \in C_A$ such that $\mathbf{SCh}(E) = \langle T \rangle$. Reciprocally, let $A$ be a type, then for every $T \in C_A$ there exist a strict order < on $A$ and $E : \mathcal{P}(A)$ such that $\mathbf{SCh}(E) = \langle T \rangle$.

**Proof.** Proof of the first statement: we inductively define a $T' : \mathcal{P}(A^*)$.

$$ \varepsilon \in T' \qquad \frac{a \in E}{[a] \in T'} \qquad \frac{b \in E \quad a < b \quad u@a \in T'}{u@a@b \in T'} $$

We easily show that $T'$ satisfies the conditions of the above definition. Let $T$ be the downward closure of $T'$. Let $F \in \mathbf{SCh}(E)$ and $u : A^*$ such that $u \subset F$. Since $F$ is a chain we can construct a list $u'$ of all elements of $u$ such that $u'$ does not contain twice the same element and is ordered increasingly relative to $<$. $u'$ is thus in $T'$ hence $u$ is in $T$. Let $F \in \langle T \rangle$ and $a, b : A$ such that $a, b \in F$. By hypothesis the list $[a, b]$ is in $T$. There exists $u \in T'$ such that $[a, b] \subset u$. Hence $a, b \in \langle u \rangle$ which is a chain. In conclusion $F$ is a subchain of $E$.

Proof of the reciprocal: suppose given a type $A$ with decidable equality and $T \in C_A$. There exists a $T'$ satisfying the aforementioned conditions. Let $E := \lambda a^A. \exists u A^*, u \in T' \wedge a \in u$. We now must define an ordering on $A$. Define < a binary relation on $A$ such that $a < b := [a, b] \in T'$. Using last "axiom" of the definition of $T'$ we easily show that it is irreflexive. For transitivity notice that if $[a, b], [b, c] \in T'$ then $[a, b, c] \in T'$ then $[a, c] \in T'$. Thus, it is a strict ordering on $A$. Let $F \in \mathbf{SCh}(E)$ and $u : A^*$ such that $u \subset F$. We can assume that $u$ is sorted increasingly relatively to $<$. Using the same trick used for proving transitivity show that $u \in T$. Let $F \in \langle T \rangle$ and $a, b : A$ such that $a, b \in F$. By hypothesis the list $[a, b]$ is in $T$ therefore, $a < b$ which means that $F$ is indeed a chain. ◀

**Corollary 22.** $\overline{\text{TTL}}_{AC_A} \to \text{Zorn and } \overline{\text{Zorn}}_{\mathcal{P}(A)\subset\langle T \rangle} \to \text{TTL}$. Hence we deduce the somewhat surprising results TTL $\leftrightarrow \overline{\text{TTL}}_{AC_A}$ and Zorn $\leftrightarrow \overline{\text{Zorn}}_{\mathcal{P}(A)\subset\langle T \rangle}$.

Looking back at the path we took to arrive at this conclusion, the results are quite expected, but looking only at the definition of a list of chains it is quite surprising that restricting TTL this much does not change its power.

4 ∃MPCF

In this section we define a choice principle $∃MPCF$ which stands for “Exists a Maximal Partial Choice Function” and a weaker version $∃MPCF^-$. It is weaker in the sense that $∃MPCF$ implies $∃MPCF^-$ but the equivalence is true if we allow excluded middle. We show that $∃MPCF^-$ is equivalent in its general form to TTL and link $∃MPCF$ to the general class of dependent choice GDC, given by Brede and the first author in [2]. In particular, $∃MPCF$ and $∃MPCF^-$ can be seen as refinements of TTL whose strength is more explicitly controlled.
**Definition 23.** Let A, B be types, $f, g \in A \to_P B$ and $P: \mathcal{P}(\mathcal{P}(A \times B))$, define:

$g \prec f: \mathrm{Prop}$

$g \prec f: \exists a^A, a \notin \mathrm{dom}(f) \wedge (\mathrm{dom}(g) = \mathrm{dom}(f) \cup a) \wedge$

$$(\forall x^A, x \in \mathrm{dom}(f) \to \exists b^B, (x, b) \in f \wedge (x, b) \in g)$$

$f \in \mathrm{Max}_{\mathrm{rfp}}(P) : \mathrm{Prop}$

$f \in \mathrm{Max}_{\mathrm{rfp}}(P) := f \in P \wedge \forall g^{A \to_P B}, g \prec f \to g \notin P$

**Definition 24 (∃MPCF⁻).** Let A, B be types and T: $\mathcal{P}((A \times B)^*)$, $\exists \mathrm{MPCF}_{\overline{ABT}}$ is the statement:

$$(\exists \alpha^{\mathcal{P}(A \times B)}, \alpha \in \langle T \rangle) \to \exists f^{A \to_P B}, f \in \mathrm{Max}_{\mathrm{rfp}}(\langle T \rangle)$$

**Definition 25.** Let A, B be types, $f, g: A \to B_\perp$ and $P: \mathcal{P}(\mathcal{P}(A \times B))$, define:

$g \prec f: \mathrm{Prop}$

$g \prec f: \exists a^A, a \notin \mathrm{dom}(f) \wedge (\mathrm{dom}(g) = \mathrm{dom}(f) \cup a) \wedge$

$$(\forall x^A, x \in \mathrm{dom}(f) \to f(x) = g(x))$$

$f \in \mathrm{Max}_{\mathrm{dpf}}(P) : \mathrm{Prop}$

$f \in \mathrm{Max}_{\mathrm{dpf}}(P) := \mathcal{G}(f) \in P \wedge \forall g^{A \to B_\perp}, g \prec f \to \mathcal{G}(g) \notin P$

Since the intuitive meaning is the same we use the symbol ≺ for predicate, for relational partial functions and decidable partial function.

**Definition 26 (∃MPCF).** Let A, B be types and T: $\mathcal{P}((A \times B)^*)$, the theorem of existence of a maximal partial choice function $\exists \mathrm{MPCF}_{ABT}$ is the statement:

$$(\exists \alpha^{\mathcal{P}(A \times B)}, \alpha \in \langle T \rangle) \to \exists f^{A \to B_\perp}, f \in \mathrm{Max}_{\mathrm{dpf}}(\langle T \rangle)$$

The difference between $\exists \mathrm{MPCF}$ and $\exists \mathrm{MPCF}^{-}$ lies solely in the "kind" of partial function that is used. Hence, as per the above remark on the differences between relation partial function and decidable partial function, $\exists \mathrm{MPCF} \to \exists \mathrm{MPCF}^{-}$ and assuming excluded middle $\exists \mathrm{MPCF}^{-} \to \exists \mathrm{MPCF}$ which we denote by $\exists \mathrm{MPCF}^{-} \to_{cl} \exists \mathrm{MPCF}$.

## 4.1 ∃MPCF and TTL

Now that we have defined $\exists \mathrm{MPCF}^{-}$, we show that it is equivalent to TTL hence, $\exists \mathrm{MPCF} \to TTL$ and TTL $\to_{cl} \exists \mathrm{MPCF}$.

**Theorem 27.** Let A be a type, $T: \mathcal{P}(A^*)$ and $\pi^*T$ the operation that maps $T$ to $\lambda u^{(A \times 1)^*}$. $\pi(u) \in T$ where $\pi$ is the canonical projection of $(A \times 1)^*$ on $A^*$. Then, $\exists \mathrm{MPCF}_{\overline{A_1\pi^*T}} \to TTL_{AT}$. Let A, B be types and T: $\mathcal{P}((A \times B)^*)$ then, TTL$_{(A \times B)T} \to \exists \mathrm{MPCF}_{\overline{ABT}}$.

**Proof.** $\exists \mathrm{MPCF}_{\overline{A_1\pi^*T}} \to TTL_{AT}$: let A a type, $T: \mathcal{P}(A^*)$ and $\pi^*T := \lambda u^{(A \times 1)^*}$. $\pi(u) \in T$. From $\exists \mathrm{MPCF}_{\overline{A_1\pi^*T}}$ we obtain $f \in A \to_P 1$ such that $f \in \mathrm{Max}_{\mathrm{rfp}}(\langle \pi^*T \rangle)$. Define $\alpha := \mathrm{dom}(f)$ and let's show that $\alpha \in \mathrm{Max}(\langle T \rangle)$. By construction, $\alpha$ is in $\langle T \rangle$. Suppose $\beta: \mathcal{P}(A \times B)$ such that $\beta \prec \alpha$. We can construct a relational partial function $g: A \to_P 1$ such that $\beta = \mathrm{dom}(g)$. Since $g \prec f, g$ is not in $\langle U \rangle$ hence $\beta$ is not in $\langle T \rangle$.
**Definition 23.** Let A, B be types, $f, g \in A \to_P B$ and $P: \mathcal{P}(\mathcal{P}(A \times B))$, define:

$g \prec f: \mathrm{Prop}$

$g \prec f: \exists a^A, a \notin \mathrm{dom}(f) \wedge (\mathrm{dom}(g) = \mathrm{dom}(f) \cup a) \wedge$

$$(\forall x^A, x \in \mathrm{dom}(f) \to \exists b^B, (x, b) \in f \wedge (x, b) \in g)$$

$f \in \mathrm{Max}_{\mathrm{rfp}}(P) : \mathrm{Prop}$

$f \in \mathrm{Max}_{\mathrm{rfp}}(P) := f \in P \wedge \forall g^{A \to_P B}, g \prec f \to g \notin P$

**Definition 24 (∃MPCF⁻).** Let A, B be types and T: $\mathcal{P}((A \times B)^*)$, $∃MPCF_{\overline{ABT}}$ is the statement:

$$(\exists \alpha^{\mathcal{P}(A \times B)}, \alpha \in \langle T \rangle) \to \exists f^{A \to_P B}, f \in \mathrm{Max}_{\mathrm{rfp}}(\langle T \rangle)$$

**Definition 25.** Let A, B be types, $f, g: A \to B_\perp$ and $P: \mathcal{P}(\mathcal{P}(A \times B))$, define:

$g \prec f: \mathrm{Prop}$

$g \prec f: \exists a^A, a \notin \mathrm{dom}(f) \wedge (\mathrm{dom}(g) = \mathrm{dom}(f) \cup a) \wedge$

$$(\forall x^A, x \in \mathrm{dom}(f) \to f(x) = g(x))$$

$f \in \mathrm{Max}_{\mathrm{dpf}}(P) : \mathrm{Prop}$

$f \in \mathrm{Max}_{\mathrm{dpf}}(P) := \mathcal{G}(f) \in P \wedge \forall g^{A \to B_\perp}, g \prec f \to \mathcal{G}(g) \notin P$

Since the intuitive meaning is the same we use the symbol ≺ for predicate, for relational partial functions and decidable partial function.

**Definition 26 (∃MPCF).** Let A, B be types and T: $\mathcal{P}((A \times B)^*)$, the theorem of existence of a maximal partial choice function $∃MPCF_{ABT}$ is the statement:

$$(\exists \alpha^{\mathcal{P}(A \times B)}, \alpha \in \langle T \rangle) \to \exists f^{A \to B_\perp}, f \in \mathrm{Max}_{\mathrm{dpf}}(\langle T \rangle)$$

The difference between $∃MPCF$ and $∃MPCF⁻$ lies solely in the "kind" of partial function that is used. Hence, as per the above remark on the differences between relation partial function and decidable partial function, $∃MPCF \to ∃MPCF⁻$ and assuming excluded middle $∃MPCF⁻ \to ∃MPCF$ which we denote by $∃MPCF⁻ \to_{cl} ∃MPCF$.

## 4.1 ∃MPCF and TTL

Now that we have defined $∃MPCF⁻$, we show that it is equivalent to TTL hence, $∃MPCF \to TTL$ and $TTL \to_{cl} ∃MPCF$.

**Theorem 27.** Let A be a type, $T: \mathcal{P}(A^*)$ and $\pi^*T$ the operation that maps $T$ to $\lambda u^{(A \times 1)^*}$. $\pi(u) \in T$ where $\pi$ is the canonical projection of $(A \times 1)^*$ on $A^*$. Then, $∃MPCF_{\overline{A_1\pi^*T}} \to TTL_{AT}$. Let A, B be types and $T: \mathcal{P}((A \times B)^*)$ then, $TTL_{(A \times B)T} \to ∃MPCF_{ABT}$.

**Proof.** $∃MPCF_{\overline{A_1\pi^*T}} \to TTL_{AT}$: let A a type, $T: \mathcal{P}(A^*)$ and $\pi^*T := \lambda u^{(A \times 1)^*}$. $\pi(u) \in T$. From $∃MPCF_{\overline{A_1\pi^*T}}$ we obtain $f \in A \to_P 1$ such that $f \in \mathrm{Max}_{\mathrm{rfp}}(\langle \pi^*T \rangle)$. Define $\alpha := \mathrm{dom}(f)$ and let's show that $\alpha \in \mathrm{Max}(\langle T \rangle)$. By construction, $\alpha$ is in $\langle T \rangle$. Suppose $\beta: \mathcal{P}(A \times B)$ such that $\beta \prec \alpha$. We can construct a relational partial function $g: A \to_P 1$ such that $\beta = \mathrm{dom}(g)$. Since $g \prec f, g$ is not in $\langle U \rangle$ hence $\beta$ is not in $\langle T \rangle$.
23:12 On the logical structure of some maximality and well-foundedness principles

$TTL_{(A \times B)T} \to \exists MPCF_{ABT}^{-}$: let A, B types and T : $P((A \times B)^*)$. Define

$$
Q := \lambda u^{(A \times B)^*}. (\forall a^A, \forall b, b'^B, (a, b) \in u \wedge (a, b') \in u \to b = b' \wedge u \in T
$$

Notice that ⟨Q⟩ is not empty, since ⟨T⟩ is inhabited, ϵ ∈ T. From this, we deduce that ϵ ∈ Q
hence, the empty predicate is in ⟨Q⟩. We can now apply TTL<sub>(A×B)Q</sub> and get α such that
α ∈ Max⟨Q⟩. By construction α is a relational partial function. It follows that it's a
maximal relational partial function, thus proving ∃MPCF<sub>ABT</sub>. ◀

TTL can be seen as a projection of ∃MPCF. The fact that they are so tightly linked
is not surprising as “being a partial function” for a subset of A × B is a property of finite
character.

4.2 ∃MPCF and GDC

Introduced in [2], Generalised Dependent Choice (GDC<sub>ABT</sub>) is a common generalisation of
the axiom of dependent choice and of the Boolean prime ideal theorem. Parameterised by a
domain A, a codomain B and a predicate T : P((A × B)<sup>*</sup>), it yields dependent choice when
A is countable, the Boolean prime ideal theorem when B is two-valued, and the full axiom
of choice when T comes as the “alignment” of some relation (see below). To the difference
of ∃MPCF, GDC asserts the existence of a total choice function, but this to the extra
condition of a property of “approximability” of T by arbitrary long finite approximations.
To the difference of ∃MPCF whose strength is the one of the full axiom of choice, expecting
a total choice function makes GDC inconsistent in its full generality.

In this section we investigate how restricting ∃MPCF to countable A or two-valued B
impacts its strength to exactly the same extent as it restricts the strength of GDC. Two
such preliminary results are given, but first, let's translate GDC in our setting:

► **Definition 28 (A-B-approximable).** Let A, B be types and T : $\mathcal{P}((A \times B)^*)$. For all $X : \mathcal{P}((A \times B)^*)$ define

$$
\phi(X) := \lambda u^{(A \times B)^*} . (u \in [\langle T \rangle] \wedge \forall a^A, \neg(\exists b^B, (a, b) \in u) \to \exists b^B, u \in X)
$$

The A-B-approximation of T denoted $T_{ABap}$ is the greatest fixed point of $\phi$. We say that $T$
is A-B-approximable if $\varepsilon \in T_{ABap}$.

► **Definition 29 (A-B-choice function).** Let A, B be types and T : P((A × B)<sup>*</sup>). T has an A-B-choice function if:

$$
\exists f^{A \to B}, \forall u^{(A \times B)^*}, u \subset \mathcal{G}(f) \to u \in T
$$

► **Definition 30 (GDC).** Let A, B be types and T : P((A × B)<sup>*</sup>), GDC<sub>ABT</sub> is the statement: if T is A-B-approximable then T has an A-B-choice function.

► **Theorem 31.** $\overline{\text{GDC}}_{\text{NBT}} \to_{\text{cl}} \overline{\text{∃MPCF}}_{\text{NBT}}$

**Proof.** Let B be a type and T : P((N × B)<sup>*</sup>). In order to use **GDC**, T must be N-B-approximable but the T we are given might not be. Thus, we are going to construct T<sub>⊥</sub> : P((N × B<sub>⊥</sub>)<sup>*</sup>) that is N-B<sub>⊥</sub>-approximable and use **GDC** to obtain a function that we will prove maximal.
$TTL_{(A \times B)T} \to \exists MPCF_{ABT}^{-}$: let A, B types and T : $\mathcal{P}((A \times B)^*)$. Define

$$Q := \lambda u^{(A \times B)^*}. (\forall a^A, \forall b, b'^B, (a, b) \in u \wedge (a, b') \in u \to b = b' \wedge u \in T)$$

Notice that $\langle Q \rangle$ is not empty, since $\langle T \rangle$ is inhabited, $\epsilon \in T$. From this, we deduce that $\epsilon \in Q$ hence, the empty predicate is in $\langle Q \rangle$. We can now apply $TTL_{(A \times B)Q}$ and get $\alpha$ such that $\alpha \in \text{Max}(\langle Q \rangle)$. By construction $\alpha$ is a relational partial function. It follows that it's a maximal relational partial function, thus proving $\exists MPCF_{ABT}^{-}$. ◀

$TTL$ can be seen as a projection of $\exists MPCF$. The fact that they are so tightly linked is not surprising as “being a partial function” for a subset of $A \times B$ is a property of finite character.

## 4.2 $\exists MPCF$ and GDC

Introduced in [2], Generalised Dependent Choice ($GDC_{ABT}$) is a common generalisation of the axiom of dependent choice and of the Boolean prime ideal theorem. Parameterised by a domain A, a codomain B and a predicate T : $\mathcal{P}((A \times B)^*)$, it yields dependent choice when A is countable, the Boolean prime ideal theorem when B is two-valued, and the full axiom of choice when T comes as the “alignment” of some relation (see below). To the difference of $\exists MPCF$, $GDC$ asserts the existence of a total choice function, but this to the extra condition of a property of “approximability” of T by arbitrary long finite approximations. To the difference of $\exists MPCF$ whose strength is the one of the full axiom of choice, expecting a total choice function makes $GDC$ inconsistent in its full generality.

In this section we investigate how restricting $\exists MPCF$ to countable A or two-valued B impacts its strength to exactly the same extent as it restricts the strength of $GDC$. Two such preliminary results are given, but first, let's translate $GDC$ in our setting:

**Definition 28 (A-B-approximable).** Let A, B be types and T : $\mathcal{P}((A \times B)^*)$. For all X : $\mathcal{P}((A \times B)^*)$ define

$$\phi(X) := \lambda u^{(A \times B)^*}. (u \in \langle T \rangle \wedge \forall a^A, \neg(\exists b^B, (a, b) \in u) \to \exists b^B, u \in X)$$

The A-B-approximation of T denoted $T_{ABap}$ is the greatest fixed point of $\phi$. We say that T is A-B-approximable if $\epsilon \in T_{ABap}$.

**Definition 29 (A-B-choice function).** Let A, B be types and T : $\mathcal{P}((A \times B)^*)$. T has an A-B-choice function if:

$$\exists f^{A \to B}, \forall u^{(A \times B)^*}, u \subset \mathcal{G}(f) \to u \in T$$

**Definition 30 (GDC).** Let A, B be types and T : $\mathcal{P}((A \times B)^*)$, $GDC_{ABT}$ is the statement: if T is A-B-approximable then T has an A-B-choice function.

**Theorem 31.** $\overline{GDC_{NBT}} \to_{cl} \exists MPCF_{NBT}$

*Proof.* Let B be a type and T : $\mathcal{P}((\mathbb{N} \times B)^*)$. In order to use $GDC$, T must be $\mathbb{N}$-B-approximable but the T we are given might not be. Thus, we are going to construct $T_{\perp} : \mathcal{P}((\mathbb{N} \times B_{\perp})^*)$ that is $\mathbb{N}$-B$_{\perp}$-approximable and use $GDC$ to obtain a function that we will prove maximal.
For all $u : \mathcal{P}((A \times B_\perp)^*)$ define $\bar{u}$ inductively:

$$ \overline{\varepsilon} := \varepsilon \qquad \frac{a : A \quad b : B}{u@(a, b)} := \bar{u}@\overline{(a, b)} \qquad \frac{a : A}{u@(a, \perp)} := \bar{u} $$

By induction define $T_\perp^n : \mathcal{P}((\mathbb{N} \times B_\perp)^*)$:

- $T_\perp^0 := \lambda u (\mathbb{N} \times B_\perp)^* . u = \varepsilon$

- Let $T_\perp^{n+1}$ be defined inductively

$$ \frac{u \in T_n \quad b : B \quad \bar{u}@\overline{(n+1, b)} \in T}{u@(n+1, b) \in T_\perp^{n+1}} \qquad \frac{u \in T_n \quad \forall b^B, \bar{u}@\overline{(n+1, b)} \notin T}{u@(n+1, \perp) \in T_\perp^{n+1}} $$

Now define $T_\perp$ as the $\subseteq$-downward closure of the union of the $T_\perp^n$. We must show that $T_\perp$ is $\mathbb{N}-B_\perp$-approximable. By definition $T_\perp = \lfloor \langle T_\perp \rangle \rfloor$. Let $n : \mathbb{N}$, $v : (\mathbb{N} \times B_\perp)^*$ such that $v \in T_\perp$ and $\neg (\exists c^{B_\perp}, (n, c) \in v)$. By definition, there exists $m : \mathbb{N}$ and $u \in T_\perp^m$ such that $v \subseteq u$. If $n \le m$ then there exists $c : B_\perp$ such that $(n, c) \in u$, thus $v@(n, c) \subseteq u$ and $v@(n, c) \in T_\perp$. If $n > m$ then there exists $u' \in T_\perp^m$ such that $u' \subseteq u$. It is in the proof of this statement that we need excluded middle to show that we always satisfy the hypothesis of one of the induction steps. Hence, $v \subseteq u'$ and we now repeat the same argument. $T_\perp$ satisfies $\phi$ and contains $\varepsilon$, thus we can apply $\mathbf{GDC}_{\mathbb{N}B_\perp T_\perp}$ and get $f : \mathbb{N} \to B_\perp$ a choice function.

What is left to show is that $f$ is a maximal partial function. Let $n : \mathbb{N}$ such that $n \notin \text{dom}(f)$ and let $g : \mathbb{N} \to B_\perp$ extending $f$ with $\text{dom}(g) = \text{dom}(f) \cup n$. Let us write $f_{<n}$ for the list $[(0, f(0)), \dots, (n-1, f(n-1))]$. $f_{<n} \in T_\perp^n$ and since $f_{<n+1}$ is of the form $f_{<n}@(n, \perp)$ by case analysis we deduce that $\forall b^B, \overline{f_{<n}@(n, b)} \notin T$. If $\mathcal{G}(g) \in \langle T_\perp \rangle$ then $g_{<n+1} = f_{<n}@\overline{(n, g(n))}$ with $g(n) : B$. $\overline{f_{<n}@(n, g(n))}$ is thus in $T$, contradiction. Hence, $f$ is maximal. $\blacksquare$

Let's write DC for the axiom of dependent choice. We have:

► **Corollary 32.** Since $\overline{\mathbf{GDC}_{\mathbb{N}B_\perp}}$ is equivalent to DC [2] we deduce: $\overline{\mathbf{DC}} \to_{\text{cl}} \overline{\mathbf{TTL}}_{(\mathbb{N} \times B)T}$

► **Theorem 33.** For A a type with decidable equality, $\exists \overline{\mathbf{MPCF}}_{ABT} \to \overline{\mathbf{GDC}}_{ABT}$

**Proof.** Let A be a type and $T : \mathcal{P}((A \times \mathbb{B})^*)$ A-B-approximable. Define $U := \lfloor \langle T_{ABap} \rangle \rfloor$, the A-B-approximable hypothesis guarantees that $\langle U \rangle$ is inhabited. Using $\exists \overline{\mathbf{MPCF}}_{ABU}$ we get $f : A \to \mathbb{B}_\perp$ a maximal partial choice function. We show that $f$ must be total, that is that it is impossible that it takes the value $\perp$. Indeed assume $f(a) = \perp$ for some $a : A$ and consider $g : A \to \mathbb{B}_\perp$ that extends $f$ with $g_0(a) = 0_\mathbb{B}$. We have $g \prec f$, thus $\mathcal{G}(g) \notin \langle U \rangle$. Then, there exists $u : (A \times \mathbb{B})^*$ such that $u \subset \mathcal{G}(g)$ and $u \notin U$. Using the decidability of equality in A, we can find $u'$ such that $u = u'@(a, 0_\mathbb{B})$ where $u' \subset \mathcal{G}(f)$. Symmetrically, by considering the extension $g$ of $f$ obtained by setting $g(a) = 1_\mathbb{B}$, there exists $v' \subset \mathcal{G}(f)$ such that $v'@(a, 1_\mathbb{B}) \notin U$. Since $u' \star v' \subset \mathcal{G}(f)$, $u' \star v' \in U$. There must be $b : \mathbb{B}$ such that $(u' \star v')@(a, b) \in U$. But in both cases ($b = 0_\mathbb{B}$ or $1_\mathbb{B}$) there is a sublist $(u'@(a, 0_\mathbb{B})$ or $v'@(a, 1_\mathbb{B}))$ that is not in $U$, contradiction. Hence, $f$ is total. $\blacksquare$

The following definition, taken from [2], describes how to turn a relation on A and B as a predicate over $(A \times \mathbb{B})^*$ that filters approximations.

► **Definition 34 (Positive alignment).** Let A and B be types and R a relation on A and B. The positive alignment $R_\perp$ of R is the predicate on $(A \times B)^*$ defined by:

$$ R_\perp := \lambda u. \forall (a, b) \in u, R(a, b) $$
For all $u : \mathcal{P}((A \times B_{\perp})^*)$ define $\bar{u}$ inductively:

$$ \bar{\varepsilon} := \varepsilon \qquad \frac{a : A \quad b : B}{u@(a, b)} := \bar{u}@ (a, b) \qquad \frac{a : A}{u@(a, \perp)} := \bar{u} $$

By induction define $T_{\perp}^n : \mathcal{P}((\mathbb{N} \times B_{\perp})^*)$:

- $T_{\perp}^0 := \lambda u (\mathbb{N} \times B_{\perp})^*$. $u = \varepsilon$

- Let $T_{\perp}^{n+1}$ be defined inductively

$$ \frac{u \in T_n \quad b : B \quad \bar{u}@ (n+1, b) \in T}{u@(n+1, b) \in T_{\perp}^{n+1}} \qquad \frac{u \in T_n \quad \forall b^B, \bar{u}@ (n+1, b) \notin T}{u@(n+1, \perp) \in T_{\perp}^{n+1}} $$

Now define $T_{\perp}$ as the $\subseteq$-downward closure of the union of the $T_{\perp}^n$. We must show that $T_{\perp}$ is $\mathbb{N}-B_{\perp}$-approximable. By definition $T_{\perp} = \lfloor \langle T_{\perp} \rangle \rfloor$. Let $n : \mathbb{N}$, $v : (\mathbb{N} \times B_{\perp})^*$ such that $v \in T_{\perp}$ and $\neg (\exists c^{B_{\perp}}, (n, c) \in v)$. By definition, there exists $m : \mathbb{N}$ and $u \in T_{\perp}^m$ such that $v \subseteq u$. If $n \le m$ then there exists $c : B_{\perp}$ such that $(n, c) \in u$, thus $v@(n, c) \subseteq u$ and $v@(n, c) \in T_{\perp}$. If $n > m$ then there exists $u' \in T_{\perp}^n$ such that $u' \subseteq u'$. It is in the proof of this statement that we need excluded middle to show that we always satisfy the hypothesis of one of the induction steps. Hence, $v \subseteq u'$ and we now repeat the same argument. $T_{\perp}$ satisfies $\phi$ and contains $\varepsilon$, thus we can apply $\mathbf{GDC}_{\mathbb{N}B_{\perp}T_{\perp}}$ and get $f : \mathbb{N} \to B_{\perp}$ a choice function.

What is left to show is that $f$ is a maximal partial function. Let $n : \mathbb{N}$ such that $n \notin \text{dom}(f)$ and let $g : \mathbb{N} \to B_{\perp}$ extending $f$ with $\text{dom}(g) = \text{dom}(f) \cup n$. Let us write $f_{<n}$ for the list $[(0, f(0)), \dots, (n-1, f(n-1))]$. $f_{<n} \in T_{\perp}^n$ and since $f_{<n+1}$ is of the form $f_{<n}@(n, \perp)$ by case analysis we deduce that $\forall b^B, \bar{f}_{<n}@ (n, b) \notin T$. If $\mathcal{G}(g) \in \langle T_{\perp} \rangle$ then $g_{<n+1} = f_{<n}@ (n, g(n))$ with $g(n) : B$. $\bar{f}_{<n}@ (n, g(n))$ is thus in $T$, contradiction. Hence, $f$ is maximal. $\blacksquare$

Let's write DC for the axiom of dependent choice. We have:

- **Corollary 32.** Since $\overline{\mathbf{GDC}_{\mathbb{N}B_{\perp}}}$ is equivalent to DC [2] we deduce: $\overline{\text{DC} \to \text{TTL}_{(\mathbb{N} \times B)T}}$

- **Theorem 33.** For A a type with decidable equality, $\exists \overline{\mathbf{MPCF}_{ABT}} \to \overline{\mathbf{GDC}_{ABT}}$

**Proof.** Let A be a type and $T : \mathcal{P}((A \times \mathbb{B})^*)$ A-B-approximable. Define $U := \lfloor \langle T_{ABap} \rangle \rfloor$, the A-B-approximable hypothesis guarantees that $\langle U \rangle$ is inhabited. Using $\exists \overline{\mathbf{MPCF}_{ABU}}$ we get $f : A \to \mathbb{B}_{\perp}$ a maximal partial choice function. We show that $f$ must be total, that is that it is impossible that it takes the value $\perp$. Indeed assume $f(a) = \perp$ for some $a : A$ and consider $g : A \to \mathbb{B}_{\perp}$ that extends $f$ with $g_0(a) = 0_{\mathbb{B}}$. We have $g \prec f$, thus $\mathcal{G}(g) \notin \langle U \rangle$. Then, there exists $u : (A \times \mathbb{B})^*$ such that $u \subset \mathcal{G}(g)$ and $u \notin U$. Using the decidability of equality in A, we can find $u'$ such that $u = u'@(a, 0_{\mathbb{B}})$ where $u' \subset \mathcal{G}(f)$. Symmetrically, by considering the extension $g$ of $f$ obtained by setting $g(a) = 1_{\mathbb{B}}$, there exists $v' \subset \mathcal{G}(f)$ such that $v'@(a, 1_{\mathbb{B}}) \notin U$. Since $u' \star v' \subset \mathcal{G}(f)$, $u' \star v' \in U$. There must be $b : \mathbb{B}$ such that $(u' \star v')@(a, b) \in U$. But in both cases ($b = 0_{\mathbb{B}}$ or $1_{\mathbb{B}}$) there is a sublist $(u'@(a, 0_{\mathbb{B}})$ or $v'@(a, 1_{\mathbb{B}})$) that is not in $U$, contradiction. Hence, $f$ is total. $\blacksquare$

The following definition, taken from [2], describes how to turn a relation on A and B as a predicate over $(A \times \mathbb{B})^*$ that filters approximations.

- **Definition 34 (Positive alignment).** Let A and B be types and R a relation on A and B. The positive alignment $R_{\perp}$ of R is the predicate on $(A \times B)^*$ defined by:

$$ R_{\perp} := \lambda u. \forall (a, b) \in u, R(a, b) $$
23:14 On the logical structure of some maximality and well-foundedness principles

Positive alignments can be characterised by the following property.

**Definition 35 (Downward prime).** Let A and B be types. We say that $T: \mathcal{P}((A \times B)^*)$ is downward prime when $u \in T$ and $v \in T$ implies $u \star v \in T$. We denote by $\mathbf{D}_{AB}$ the collection of downward prime $T: \mathcal{P}((A \times B)^*)$.

**Theorem 36.** If $R$ is a relation on $A$ and $B$, its positive alignment is downward prime. Conversely, if $T$ is downward prime, it is the positive alignment of the relation $|T|$ defined by

$$|T|(a, b) := [(a, b)] \in T$$

**Proof.** This is because $u \star v \in R_\top$, that is $\forall (a, b) \in u \star v, R(a, b)$ is equivalent to $(\forall (a, b) \in u, R(a, b)) \wedge (\forall (a, b) \in v, R(a, b))$, that is to $u \in R_\top \wedge v \in R_\top$, and, conversely, because $u \in |T|_\top$, that is $\forall (a, b) \in u, [(a, b)] \in T$, is equivalent, by induction on $u$, using downward primality at each step, to $u \in T$. ◀

Based on the equivalence between $\mathbf{AC}_{ABR}$ and $\mathbf{GDC}_{ABR_\top}$ in [2, Thm 7], we obtain:

**Corollary 37.** $\mathbf{GDC}_{ABT}$ for $T$ downward prime characterises the full axiom of choice $\mathbf{AC}_{ABR}$, that is $\forall x^A, \exists y^B, R(a, b) \rightarrow \exists f^{A \rightarrow B}, \forall x^A, R(a, f(a))$.

We now show that $\mathbf{GDC}_{ABT}$ is also equivalent to $\exists \mathbf{MPCF}_{ABT}$ for $T$ downward prime.

**Theorem 38.** For $T: \mathcal{P}((A \times B)^*)$ downward prime for $A$ with decidable equality, $\exists \mathbf{MPCF}_{ABT} \rightarrow \mathbf{GDC}_{ABT}$.

**Proof.** Since $T$ is $A$-$B$-approximable, it contains $\varepsilon$, so that $\langle T \rangle$ is non-empty. Thus, by $\exists \mathbf{MPCF}_{ABT}$, we get $f: A \rightarrow B_\perp$ a maximal partial choice function. We show that $f$ must be total. Indeed, assume $a: A$ such that $f(a) = \perp$. By $A$-$B$-approximability, we can obtain a $b$ such that $[(a, b)] \in [\langle T \rangle]$. Let's now consider the function $g: A \rightarrow B_\perp$ defined by setting $g(a') = b$ if $a = a'$ and $g(a') = f(a')$ otherwise. We have $g \prec f$, thus $\mathcal{G}(g) \notin \langle T \rangle$. But this contradicts that we can also prove that any $u \subset \mathcal{G}(g)$ is in $T$, that is $\mathcal{G}(g) \in \langle T \rangle$. Indeed, by decidability of equality on $A$, either $u$ has an element of the form $(a, b')$ or not. In the second case, $u \subset \mathcal{G}(f)$ and thus $u \in T$. In the first case, $u$ has the form $u' \star (a, b') \star u''$ with $u' \in \mathcal{G}(f)$ and $u'' \in \mathcal{G}(f)$, thus $u' \in T$ and $u'' \in T$. Since $u \subset \mathcal{G}(g)$, we also have $b' = g(a) = b$. Then, by downward primality, we get $u' \star [(a, b)] \star u'' \in T$. ◀

**Theorem 39.** For $T: \mathcal{P}((A \times B)^*)$ downward prime, $\overline{\mathbf{GDC}_{ABD_{AB}}} \rightarrow \overline{\exists \mathbf{MPCF}_{ABD_{AB}}}$.

**Proof.** There are two ways to embed a partial function from $A$ to $B$ into a total function: either restrict $A$ to the domain of the function, or extend $B$ into $B_\perp$, as in Theorem 31. We give a proof using the first approach.

Let $A'$ be the subset of $A$ such that $\exists b^B, [(a, b)] \in T$. We show coinductively that if $A'$ is infinite, the restriction of $T$ on $A'$ is $A'$-$B$-approximable. First, we do have $\varepsilon \in T$ because $\langle T \rangle$ is non empty. Then, assume $u \in T$ and $a: A'$ such that $\neg(\exists b^B, (a, b) \in u)$ (which is possible since $A'$ is supposed infinite). Since $a$ is in $A'$, there is $b$ such that $[(a, b)] \in T$, and by downward primality, $u \star (a, b) \in T$, hence $A'$-$B$-approximable by coinduction.

Thus, there is a total function $f: A' \rightarrow B$ such that $\mathcal{G}(f) \in \langle T \rangle$, which induces a partial function $f'$ from $A \rightarrow_B B_\perp$. It remains to show that $f'$ is maximal. Let $a \notin \text{dom}(f)$, that is such that $\forall b^B, \neg[(a, b)] \in T$. Then, there is obviously no extension of $f'$ on $a$ that would be in $\langle T \rangle$.

It remains to treat the case of $A'$ finite, which can be obtained by (artificially) reasoning on the disjoint sum of $A'$ and $\mathbb{N}$, and setting $T[(n, p)] := (n = p)$ on $\mathbb{N}$. ◀
23:14 On the logical structure of some maximality and well-foundedness principles

Positive alignments can be characterised by the following property.

**Definition 35 (Downward prime).** Let A and B be types. We say that $T: \mathcal{P}((A \times B)^*)$ is downward prime when $u \in T$ and $v \in T$ implies $u \star v \in T$. We denote by $\mathbf{D}_{AB}$ the collection of downward prime $T: \mathcal{P}((A \times B)^*)$.

**Theorem 36.** If $R$ is a relation on $A$ and $B$, its positive alignment is downward prime. Conversely, if $T$ is downward prime, it is the positive alignment of the relation $|T|$ defined by

$$|T|(a, b) := [(a, b)] \in T$$

**Proof.** This is because $u \star v \in R_\top$, that is $\forall (a, b) \in u \star v, R(a, b)$ is equivalent to $(\forall (a, b) \in u, R(a, b)) \wedge (\forall (a, b) \in v, R(a, b))$, that is to $u \in R_\top \wedge v \in R_\top$, and, conversely, because $u \in |T|_\top$, that is $\forall (a, b) \in u, [(a, b)] \in T$, is equivalent, by induction on $u$, using downward primality at each step, to $u \in T$. ◀

Based on the equivalence between $\mathbf{AC}_{ABR}$ and $\mathbf{GDC}_{ABR_\top}$ in [2, Thm 7], we obtain:

**Corollary 37.** $\mathbf{GDC}_{ABT}$ for $T$ downward prime characterises the full axiom of choice $\mathbf{AC}_{ABR}$, that is $\forall x^A, \exists y^B, R(a, b) \rightarrow \exists f^{A \rightarrow B}, \forall x^A, R(a, f(a))$.

We now show that $\mathbf{GDC}_{ABT}$ is also equivalent to $\exists \mathbf{MPCF}_{ABT}$ for $T$ downward prime.

**Theorem 38.** For $T: \mathcal{P}((A \times B)^*)$ downward prime for $A$ with decidable equality, $\exists \mathbf{MPCF}_{ABT} \rightarrow \mathbf{GDC}_{ABT}$.

**Proof.** Since $T$ is $A$-$B$-approximable, it contains $\varepsilon$, so that $\langle T \rangle$ is non-empty. Thus, by $\exists \mathbf{MPCF}_{ABT}$, we get $f: A \rightarrow B_\perp$ a maximal partial choice function. We show that $f$ must be total. Indeed, assume $a: A$ such that $f(a) = \perp$. By $A$-$B$-approximability, we can obtain a $b$ such that $[(a, b)] \in \langle T \rangle$. Let's now consider the function $g: A \rightarrow B_\perp$ defined by setting $g(a') = b$ if $a = a'$ and $g(a') = f(a')$ otherwise. We have $g \prec f$, thus $\mathcal{G}(g) \notin \langle T \rangle$. But this contradicts that we can also prove that any $u \subset \mathcal{G}(g)$ is in $T$, that is $\mathcal{G}(g) \in \langle T \rangle$. Indeed, by decidability of equality on $A$, either $u$ has an element of the form $(a, b')$ or not. In the second case, $u \subset \mathcal{G}(f)$ and thus $u \in T$. In the first case, $u$ has the form $u' \star (a, b') \star u''$ with $u' \in \mathcal{G}(f)$ and $u'' \in \mathcal{G}(f)$, thus $u' \in T$ and $u'' \in T$. Since $u \subset \mathcal{G}(g)$, we also have $b' = g(a) = b$. Then, by downward primality, we get $u' \star [(a, b)] \star u'' \in T$. ◀

**Theorem 39.** For $T: \mathcal{P}((A \times B)^*)$ downward prime, $\overline{\mathbf{GDC}_{ABD_{AB}}} \rightarrow \overline{\exists \mathbf{MPCF}_{ABD_{AB}}}$.

**Proof.** There are two ways to embed a partial function from $A$ to $B$ into a total function: either restrict $A$ to the domain of the function, or extend $B$ into $B_\perp$, as in Theorem 31. We give a proof using the first approach.

Let $A'$ be the subset of $A$ such that $\exists b^B, [(a, b)] \in T$. We show coinductively that if $A'$ is infinite, the restriction of $T$ on $A'$ is $A'$-$B$-approximable. First, we do have $\varepsilon \in T$ because $\langle T \rangle$ is non empty. Then, assume $u \in T$ and $a: A'$ such that $\neg(\exists b^B, (a, b) \in u)$ (which is possible since $A'$ is supposed infinite). Since $a$ is in $A'$, there is $b$ such that $[(a, b)] \in T$, and by downward primality, $u \star (a, b) \in T$, hence $A'$-$B$-approximable by coinduction.

Thus, there is a total function $f: A' \rightarrow B$ such that $\mathcal{G}(f) \in \langle T \rangle$, which induces a partial function $f'$ from $A \rightarrow_B B_\perp$. It remains to show that $f'$ is maximal. Let $a \notin \text{dom}(f)$, that is such that $\forall b^B, \neg[(a, b)] \in T$. Then, there is obviously no extension of $f'$ on $a$ that would be in $\langle T \rangle$.

It remains to treat the case of $A'$ finite, which can be obtained by (artificially) reasoning on the disjoint sum of $A'$ and $\mathbb{N}$, and setting $T[(n, p)] := (n = p)$ on $\mathbb{N}$. ◀
# 5 Conclusion

While Brede and the first author [2] investigated the general form of a variety of choice and bar induction principles seen as contrapositive principles, this paper initiated the investigation of a general form of maximality and well-foundedness principles equivalent to the axiom of choice. One of the surprise was that, up to logical duality, two principles such as Teichmüller-Tukey lemma and Berger's update induction were actually of the very same nature. By seeing all these principles as schemes, we could also investigate how to express Zorn's lemma and Teichmüller-Tukey lemma as mutual instances the one of the other. Finally, by starting investigating how maximality, when applied to functions, relates to totality in the presence of either a countable domain or a finite codomain, we initiated a bridge between maximality and well-foundedness principles and the general family of choice and bar induction principles from [2].

The investigation could be continued in at least five directions:

- In the articulation between TTL and $∃MPCF$: assuming an alternative definition of TTL, say TTL$^+$, where $P(A)$ is represented as a characteristic function from A to $B$, that is, equivalently, as a function from A to $1_⊥$, one would get the following identifications:

$$ \begin{aligned} TTL_{AT}^{+} &= ∃MPCF_{A1π*T} & TTL_{(A×B)T}^{+} &= ∃MPCF_{ABT} \\ TTL_{AT} &= ∃MPCF_{A1π*T}^{-} & TTL_{(A×B)T} &= ∃MPCF_{ABT}^{-} \end{aligned} $$

- In the articulation between a sequential definition of countably-finite character and countably-open predicate, as in TTL$^N_{BT}$ and UI$_{BT}$, and a non-sequential definition, as in $∃MPCF_{NBT}$ and $∃MPCF_{NBT}^{-}$, similar to the connection between $DC_{BT}^{prod.}$ and GDC$_{NBT}$ in [2].

- In the relation between $∃MPCF_{ABT}$ and $∃MPCF_{ABT}^{-}$ on one side and GDC$_{ABT}$ on the other side, verifying that the correspondences between $∃MPCF_{NBT}$ and GDC$_{NBT}$, and between $∃MPCF_{ABT}$ and GDC$_{ABT}$ hold, at least classically, in both directions, the same way as they do in the case T downward prime.

- In the articulation between TTL and GUI, formulating statements dual to $∃MPCF$ and $∃MPCF$- and connecting them to the dual of GDC, that is GBI [2], analysing the role of classical reasoning and decidability of the equality on the domain in the correspondences.

- In the relation between TTL, $∃MPCF$, $∃MPCF$- and other maximality principles than Zorn's lemma, also studying other well-foundedness principles than UI.

In particular, an advantage of $∃MPCF$ and $∃MPCF$- over GDC is that their more general form is classically equivalent to the axiom of choice while the most general form of GDC is inconsistent.

# References

1. Ulrich Berger. A computational interpretation of open induction. In *Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science*, LICS '04, page 326, USA, 2004. IEEE Computer Society.

2. Nuria Brede and Hugo Herbelin. On the logical structure of choice and bar induction principles. *36th Annual Symposium on Logic in Computer Science*, 2021.

3. Thierry Coquand. Constructive topology and combinatorics. In J. Paul Myers and Michael J. O'Donnell, editors, *Constructivity in Computer Science*, pages 159–164, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg.

4. Horst Herrlich. *Axiom of Choice*. Lecture Notes in Mathematics. Springer, 2006.
# 5 Conclusion

While Brede and the first author [2] investigated the general form of a variety of choice and bar induction principles seen as contrapositive principles, this paper initiated the investigation of a general form of maximality and well-foundedness principles equivalent to the axiom of choice. One of the surprise was that, up to logical duality, two principles such as Teichmüller-Tukey lemma and Berger's update induction were actually of the very same nature. By seeing all these principles as schemes, we could also investigate how to express Zorn's lemma and Teichmüller-Tukey lemma as mutual instances the one of the other. Finally, by starting investigating how maximality, when applied to functions, relates to totality in the presence of either a countable domain or a finite codomain, we initiated a bridge between maximality and well-foundedness principles and the general family of choice and bar induction principles from [2].

The investigation could be continued in at least five directions:

- In the articulation between TTL and $∃MPCF$: assuming an alternative definition of TTL, say TTL$^+$, where $P(A)$ is represented as a characteristic function from A to $B$, that is, equivalently, as a function from A to $1_⊥$, one would get the following identifications:

$$ \begin{aligned} \text{TTL}_{AT}^{+} &= \exists \text{MPCF}_{A1\pi^*T} \qquad \text{TTL}_{(A \times B)T}^{+} = \exists \text{MPCF}_{ABT} \\ \text{TTL}_{AT} &= \exists \text{MPCF}_{A1\pi^*T}^{-} \qquad \text{TTL}_{(A \times B)T} = \exists \text{MPCF}_{ABT}^{-} \end{aligned} $$

- In the articulation between a sequential definition of countably-finite character and countably-open predicate, as in TTL$^N_{BT}$ and UI$_{BT}$, and a non-sequential definition, as in $∃MPCF_{NBT}$ and $∃MPCF_{NBT}^{-}$, similar to the connection between $DC_{BT}^{prod.}$ and GDC$_{NBT}$ in [2].

- In the relation between $∃MPCF_{ABT}$ and $∃MPCF_{ABT}^{-}$ on one side and GDC$_{ABT}$ on the other side, verifying that the correspondences between $∃MPCF_{NBT}$ and GDC$_{NBT}$, and between $∃MPCF_{ABT}$ and GDC$_{ABT}$ hold, at least classically, in both directions, the same way as they do in the case T downward prime.

- In the articulation between TTL and GUI, formulating statements dual to $∃MPCF$ and $∃MPCF$- and connecting them to the dual of GDC, that is GBI [2], analysing the role of classical reasoning and decidability of the equality on the domain in the correspondences.

- In the relation between TTL, $∃MPCF$, $∃MPCF$- and other maximality principles than Zorn's lemma, also studying other well-foundedness principles than UI.

In particular, an advantage of $∃MPCF$ and $∃MPCF$- over GDC is that their more general form is classically equivalent to the axiom of choice while the most general form of GDC is inconsistent.

# References

1. Ulrich Berger. A computational interpretation of open induction. In *Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science*, LICS '04, page 326, USA, 2004. IEEE Computer Society.

2. Nuria Brede and Hugo Herbelin. On the logical structure of choice and bar induction principles. In *36th Annual Symposium on Logic in Computer Science*, 2021.

3. Thierry Coquand. Constructive topology and combinatorics. In J. Paul Myers and Michael J. O'Donnell, editors, *Constructivity in Computer Science*, pages 159-164, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg.

4. Horst Herrlich. *Axiom of Choice*. Lecture Notes in Mathematics. Springer, 2006.
23:16 On the logical structure of some maximality and well-foundedness principles

5 Thomas J. Jech. *The Axiom of Choice*. Dover Books on Mathematics Series. Courier corporation, 1973.

6 Herman Rubin and Jean E. Rubin. *Equivalents of the Axiom of Choice*. North-Holland Publishing Company, 1970.
23:16 On the logical structure of some maximality and well-foundedness principles

5 Thomas J. Jech. *The Axiom of Choice*. Dover Books on Mathematics Series. Courier corporation, 1973.

6 Herman Rubin and Jean E. Rubin. *Equivalents of the Axiom of Choice*. North-Holland Publishing Company, 1970.