The Category of Node-and-Choice Forms, with Subcategories for Choice-Sequence Forms and Choice-Set Forms

TL;DR

This paper develops a categorical framework for extensive-form games, establishing isomorphisms between different game styles and simplifying existing equivalences, with practical benefits for analyzing game forms.

Contribution

It introduces the category of node-and-choice forms and subcategories, proving isomorphic enclosures that unify and simplify prior style equivalences in game theory.

Findings

Shows that node-and-choice forms are isomorphic to choice-sequence forms.

Demonstrates that choice-sequence forms with no-absentmindedness are isomorphic to choice-set forms.

Provides practical tools for deriving and applying style equivalences in extensive-form games.

Abstract

The literature specifies extensive-form games in many styles, and eventually I hope to formally translate games across those styles. Toward that end, this paper defines $\mathbf{NCF}$, the category of node-and-choice forms. The category's objects are extensive forms in essentially any style, and the category's isomorphisms are made to accord with the literature's small handful of ad hoc style equivalences. Further, this paper develops two full subcategories: $\mathbf{CsqF}$ for forms whose nodes are choice-sequences, and $\mathbf{CsetF}$ for forms whose nodes are choice-sets. I show that $\mathbf{NCF}$ is "isomorphically enclosed" in $\mathbf{CsqF}$ in the sense that each $\mathbf{NCF}$ form is isomorphic to a $\mathbf{CsqF}$ form. Similarly, I show that $\mathbf{CsqF_{\tilde a}}$ is isomorphically enclosed in $\mathbf{CsetF}$ in the sense that each $\mathbf{CsqF}$ form with no-absentmindedness is isomorphic to a $\mathbf{CsetF}$ form. The converses are found to be almost immediate, and the resulting equivalences unify and simplify two ad hoc style equivalences in Kline and Luckraz 2016 and Streufert 2019. Aside from the larger agenda, this paper already makes three practical contributions. Style equivalences are made easier to derive by [1] a natural concept of isomorphic invariance and [2] the composability of isomorphic enclosures. In addition, [3] some new consequences of equivalence are systematically deduced.

Equations

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[P1]}&\text{there is a correspondence}⋅F{:}T⇉C⋅\text{and a}⋅t^{o}∈T\\ &\text{such that}⋅⊗⋅\text{is a bijection from}⋅F\mspace{1.0mu}^{\mathsf{gr}}⋅\text{onto}⋅T⧷⎨t^{o}⎬,\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[P2]}&(T,p)⋅\text{is a functioned tree where}⋅p{:}T⧷⎨t^{o}⎬\textrightarrow F^{-1}(C)\\ &\text{is defined}⋅\text{by}⋅p\mspace{1.0mu}^{\mathsf{gr}}=⎨(t^{\sharp},t)∈T^{2}|(∃c∈C)(t,c,t^{\sharp})∈⊗\mspace{1.0mu}^{\mathsf{gr}}⎬,⋅\text{and}\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[P3]}&{\mathcal{H}}⋅\text{partitions}⋅F^{-1}(C)\\ &\text{where}⋅{\mathcal{H}}⋅⊆⋅{\mathcal{P}}(T)⋅\text{is defined by}⋅{\mathcal{H}}=⎨F^{-1}(c)|c∈C⎬.\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[F1]}&(T,C,⊗)⋅\text{is a preform where}⋅C=∪_{i∈I}C_{i},\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[F2]}&(∀i∈I,j∈I⧷⎨i⎬)⋅C_{i}∩C_{j}=∅,⋅\text{and}\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[F3]}&(∀t∈T)(∃i∈I)⋅F(t)⋅⊆⋅C_{i}.\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[PM1]}&τ{:}T\textrightarrow T′,\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[PM2]}&δ{:}C\textrightarrow C′,⋅\text{and}\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[PM3]}&⎨\,(τ(t),δ(c),τ(t^{\sharp}))\,|\,(t,c,t^{\sharp})∈⊗\mspace{1.0mu}^{\mathsf{gr}}\,⎬⋅⊆⋅⊗′\mspace{1.0mu}^{\mathsf{gr}}.\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[FM1]}&[Π,Π′,τ,δ]⋅\text{is a preform morphism where}\\ &Π=(T,C,⊗),⋅C=∪_{i∈I}C_{i},⋅Π′=(T′,C′,⊗′),⋅\text{and}⋅C′=∪_{i′∈I′}C′_{i′},\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[FM2]}&ι{:}I\textrightarrow I′,⋅\text{and}\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[FM3]}&(∀i∈I)⋅δ(C_{i})⋅⊆⋅C′_{ι(i)}.\end{array}$$

$${\beta }^{\mathsf{src}}=[\Phi ,\Phi \prime ,\iota ,\tau ,\delta {]}^{\mathsf{src}}=\Phi ,$$

$${\beta }^{\mathsf{trg}}=[\Phi ,\Phi \prime ,\iota ,\tau ,\delta {]}^{\mathsf{trg}}=\Phi \prime ,$$

$${\mathsf{id}}_{\Phi }={\mathsf{id}}_{(I,T,(C_i{)}_{i\in I},\otimes )}=[\Phi ,\Phi ,{\mathsf{id}}_I,{\mathsf{id}}_T,{\mathsf{id}}_{{\cup }_{i\in I}{C}_i}],\cdot \text{and}$$

$$\beta \prime ○\beta =[\Phi \prime ,\Phi ″,\iota \prime ,\tau \prime ,\delta \prime ]○[\Phi ,\Phi \prime ,\iota ,\tau ,\delta ]=[\Phi ,\Phi ″,\iota \prime ○\iota ,\tau \prime ○\tau ,\delta \prime ○\delta ],$$

$${\mathsf{P}}_0\cdot :\cdot (I,T,(C_i{)}_{i\in I},\otimes )\cdot \mapsto (T,{\cup }_{i\in I}{C}_i,\otimes )\cdot \text{and}$$

$${\mathsf{P}}_1\cdot :\cdot [\Phi ,\Phi \prime ,\iota ,\tau ,\delta ]\cdot \mapsto \cdot [{\mathsf{P}}_0(\Phi ),{\mathsf{P}}_0(\Phi \prime ),\tau ,\delta ].$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[Csq1]}&T⋅\text{is a collection of (finite) sequences which contains}⋅⎨⎬,\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[Csq2]}&(∀\,(t,c,t^{\sharp})\,∈\,⊗\mspace{1.0mu}^{\mathsf{gr}})⋅t{\oplus}(c)=t^{\sharp}.\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[Cset1]}&T⋅\text{is a collection of finite sets which contains}⋅⎨⎬⋅\text{and}\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[Cset2]}&(∀(t,c,t^{\sharp})∈⊗\mspace{1.0mu}^{\mathsf{gr}})⋅t∪⎨c⎬=t^{\sharp}.\end{array}$$

$$\tau (F^{-1}(c))=$$

$$=$$

$$\subseteq$$

$$=$$

$$\subseteq$$

$$=$$

$$\tau (F^{-1}(c))=$$

$$=$$

$${\beta }^{-1}=[{\Phi }^{\ast },{\Phi }^{\ast \ast },{\iota }^{\ast },{\tau }^{\ast },{\delta }^{\ast }]=[\Phi \prime ,\Phi ,{\iota }^{-1},{\tau }^{-1},{\delta }^{-1}],$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[FM1$′$]}&[Π′,Π,τ^{-1},δ^{-1}]⋅\text{is a preform morphism},\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[FM2$′$]}&ι^{-1}{:}I′\textrightarrow I,\text{and}\end{array}$$

$$\displaystyle\begin{array}[]{lc}\rule{21.52771pt}{0.0pt}&\rule{340.13782pt}{0.0pt}\\[-12.91663pt] \text{[FM3$′$]}&(∀i′∈I′)⋅δ^{-1}(C′_{i′})⋅⊆⋅C_{ι^{-1}(i′)}.\end{array}$$

$${\beta }^{\ast }○\beta =[\Phi \prime ,\Phi ,{\iota }^{-1},{\tau }^{-1},{\delta }^{-1}]○[\Phi ,\Phi \prime ,\iota ,\tau ,\delta ]={\mathsf{id}}_{\Phi }\cdot \cdot \text{and}$$

$$\beta ○{\beta }^{\ast }=[\Phi ,\Phi \prime ,\iota ,\tau ,\delta ]○[\Phi \prime ,\Phi ,{\iota }^{-1},{\tau }^{-1},{\delta }^{-1}]={\mathsf{id}}_{\Phi \prime }.$$

$$\tau (X_i)=\cup ⎨\cdot \tau (F^{-1}(c))\cdot |\cdot c\in C_i\cdot ⎬$$

$$=\cup ⎨\cdot (F\prime {)}^{-1}(\delta (c))\cdot |\cdot c\in C_i\cdot ⎬$$

$$=\cup ⎨\cdot (F\prime {)}^{-1}(c\prime )\cdot |\cdot c\prime \in C{\prime }_{\iota (i)}\cdot ⎬=X{\prime }_{\iota (i)}.$$

$${\mathsf{P}}_1(\beta \prime ○\beta )=$$

$$=$$

Full text

Further, this paper develops two full subcategories: $\mathbf{CsqF}$ for forms whose nodes are choice-sequences, and $\mathbf{CsetF}$ for forms whose nodes are choice-sets. I show that $\mathbf{NCF}$ is “isomorphically enclosed” in $\mathbf{CsqF}$ in the sense that each $\mathbf{NCF}$ form is isomorphic to a $\mathbf{CsqF}$ form. Similarly, I show that $\mathbf{CsqF_{\tilde{a}}}$ is isomorphically enclosed in $\mathbf{CsetF}$ in the sense that each $\mathbf{CsqF}$ form with no-absentmindedness is isomorphic to a $\mathbf{CsetF}$ form. The converses are found to be almost immediate, and the resulting equivalences unify and simplify two ad hoc style equivalences in Kline and Luckraz 2016 and Streufert 2019.

Aside from the larger agenda, this paper already makes three practical contributions. Style equivalences are made easier to derive by [1] a natural concept of isomorphic invariance and [2] the composability of isomorphic enclosures. In addition, [3] some new consequences of equivalence are systematically deduced.

I thank Deanna Walker for many valuable suggestions.

Peter A. Streufert

Economics Department

Western University

1. Introduction

1.1.

Specification styles

To set the stage, this subsection recalls that there are many styles in which to specify an extensive-form game. All styles must specify [a] nodes, which are variously called “histories”, “vertices”, or “states”; and [b] choices, which are variously called “actions”, “alternatives”, “labels”, or “programs”. The following paragraphs arrange the styles into five broad groups according to how the styles specify nodes and choices.

[1] Some styles specify nodes and choices abstractly without restriction. Classic examples from economics include the style of Kuhn 1953 and the style of Selten 1975. Examples from computer science and/or logic include the style of Shoham and Leyton-Brown 2009, page 125; the “labeled transition system” style111Note 10 more precisely links “labeled transition systems” with “node-and-choice forms”. in Blackburn, de Rijke, and Venema 2002, page 3; and the “epistemic process graph” style of van Benthem 2014, page 70. A final example is the “node-and-choice” style of this paper (see Figure 1.1). Because each of these styles specifies nodes and choices abstractly without restriction, each can be roughly understood to encompass all other styles as special cases.222Accordingly, this paper’s “node-and-choice” style essentially encompasses all other extensive-form styles. Several aspects of this claim should be clarified. [1] An extensive-form game specifies a tree. This feature excludes recursively specified stochastic games such as those of Mertens 2002. [2] A node-and-choice form is assumed to be discrete in the sense that every node has a finite number of predecessors. This assumption excludes non-discrete extensive-form games such as those of Dockner, Jørgensen, Long, and Sorger 2000, and Alós-Ferrer and Ritzberger 2016. [3] A node-and-choice form assumes that information sets do not share alternatives. This assumption is insubstantial in the sense of note 21 below. [4] A node-and-choice form assumes that exactly one player moves at each information set. Accordingly, simultaneous moves by several players are specified by several information sets, as in Osborne and Rubinstein, 1994, page 202.

[2] Other styles specify nodes as sequences of choices. A popular example in economics is the style of Osborne and Rubinstein 1994, page 200. Examples from logic include the “logical game” style of Hodges 2013, Section 2, and the “epistemic forest model” style of van Benthem 2014, page 130. Examples from computer science include the “protocol” style of Parikh and Ramanujam 1985, the “history-based multi-agent structure” style of Pacuit 2007, and the “sequence-form representation” style of Shoham and Leyton-Brown 2009, page 129. A final example is the “choice-sequence” style of this paper (see Figure 1.2(a)). [3] Other styles specify nodes as sets of choices. Examples include the “choice-set” style of Streufert 2019 (henceforth “SE”), and also the “choice-set” style of this paper (see Figure 1.2(b)).

There are still other possibilities. [4] Some styles specify choices as sets of nodes, as in the “simple” style of Alós-Ferrer and Ritzberger 2016, Section 6.3 (see Figure 1.3(a)). [5] Other styles express both nodes and choices as sets of outcomes, as in the style of von Neumann and Morgenstern 1944, Section 10. and the style of Alós-Ferrer and Ritzberger 2016, Section 6.2 (see Figure 1.3(b)). Possibilities [1]–[5] are arranged in a spectrum by SE (Streufert 2019), Figure 2. Further, SE Section 7 explains how each possibility has its own advantages and disadvantages.

1.2.

General motivation

It is difficult to formally compare the different styles. Indeed, the first such results have only recently appeared in Alós-Ferrer and Ritzberger 2016 Section 6.3, in Kline and Luckraz 2016, and in SE (whose Figure 2 provides an overview of all these results). These contributions show, by ad hoc constructions, that the five styles in the above figures are of roughly equal generality. To be somewhat more precise, these papers argue that one style is at least as general as another style, by showing that each game333To be meticulous, these papers concern forms rather than games. In other words, they stop before specifying player preferences. in the first style can be reasonably mapped to a game in the second style. Then two styles are regarded as equivalent if such an argument can be made in both directions. Notice that each such argument hinges upon an ad hoc mapping linking games in one style to games in another style. Lacking is a way to compare styles that is based on a systematic way of comparing games. I hope to provide that systematization in a fashion that is compatible with the prior style equivalences.

Further, I have a larger agenda in mind. Suppose that two styles have been compared and found to be equivalent. Then I hope to do more than merely translate each game in one style to an equivalent game in the other style. I hope to translate properties, defined for games, from one style to the other. I hope to translate equilibrium concepts from one style to the other. And ultimately, I hope to translate theorems from one style to the other. In other words, I hope to formally translate game theory from one style to another.

Such an overarching theory promises to deliver large conceptual benefits. Foremost among the benefits is the synthesis of results and questions from the many disciplines and subdisciplines which are currently studying some version of game theory. There is much to be gained because there is so much diversity. Further, I believe that, fundamentally, we should make the focus of our thinking an equivalence class of games, rather than an individual game. Such an equivalence class will typically contain games in many styles. If we can easily translate across those styles, the essence of the equivalence class can emerge.444Although it lies outside my current expertise, there appears to be a further conceptual benefit, namely, that categorical translations between games may allow for syntactic translations between the logical languages that are interpreted in those games. This would accord with the correspondence theory of van Benthem 2001, and Conradie, Ghilardi, and Palmigiano 2014.

Formal translation is a daunting task. Fortunately, category theory promises to be a powerful and natural tool. In order to gain access to this tool, my intermediate-range objective has been to construct a category [a] whose objects are extensive-form games in any style, and [b] whose isomorphisms accord with the handful of style equivalences already in the literature. My first step was Streufert 2018 (henceforth “SP”). That paper defined $\mathbf{NCP}$, which is the category of node-and-choice “preforms”, where a preform is a rooted tree with choices and information sets. My second step is the present paper. Here I define $\mathbf{NCF}$, which is the category of node-and-choice “forms”, where a form augments a preform with players. Later, a third paper will augment $\mathbf{NCF}$ forms with preferences in order to define extensive-form games.

Elsewhere there is little categorical work on game theory. Lapitsky 1999 and Jiménez 2014 define categories of simultaneous-move games. Machover and Terrington 2014 defines a category of simple voting games. Vannucci 2007 defines categories of various games, but in its category of extensive-form games, every morphism merely maps a game to itself. Finally, Hedges 2017 develops morphisms for open games, which resemble extensive-form games but which do not appear to accommodate players with different information.555In addition, there have been categories developed for some relatively specialized games within the theoretical computer-science literature. Examples include, for example, Abramsky, Jagadeesan, and Malacaria 2000, Hyland and Ong 2000, and McCusker 2000.

1.3.

Categorical Investments

As explained two paragraphs ago, this paper constructs a category of forms [a] whose objects are forms in any style, and [b] whose isomorphisms accord with the style equivalences already in the literature. Goals [a] and [b] are discussed in the next two paragraphs.

Section 2 introduces $\mathbf{NCF}$, which is the category of node-and-choice forms, in which both nodes and choices are specified abstractly without restriction. Thereby goal [a] is achieved. Further, one special kind of node-and-choice form is a choice-sequence form, in which nodes are choice-sequences. Correspondingly, Section 3 introduces $\mathbf{CsqF}$, which is the full $\mathbf{NCF}$ subcategory for choice-sequence forms. Similarly, another special kind of node-and-choice form is a choice-set form, in which nodes are choice-sets. Correspondingly, Section 4 introduces $\mathbf{CsetF}$, which is the full $\mathbf{NCF}$ subcategory for choice-set forms. Finally, consider again the five styles in Section 1.1. $\mathbf{NCF}$ itself corresponds to style [1], $\mathbf{CsqF}$ corresponds to style [2], and $\mathbf{CsetF}$ corresponds to style [3]. Left for future research are style [4] with its node-set choices, and style [5] with its outcome-set nodes and outcome-set choices. These two additional styles will correspond to two additional subcategories of $\mathbf{NCF}$, as suggested in Section 5.2’s discussion of future research.

To achieve goal [b], Section 2 defines $\mathbf{NCF}$’s morphisms in such a way that the category’s isomorphisms accord with the style equivalences in the literature. Since this paper does not build subcategories for the node-set and outcome-set styles, only two of the literature’s style equivalences remain: [i] Kline and Luckraz 2016 Theorems 1 and 2, which are essentially an equivalence between node-and-choice forms and choice-sequence forms, and [ii] SE Theorems 3.1 and 3.2, which are essentially an equivalence between (no-absentminded) choice-sequence forms and choice-set forms. As discussed earlier, each of these two equivalences is a matching pair of results, in which each result states that each form in one style can be reasonably mapped to a form in the other style. Section 3.2 proposes to strengthen each such result by requiring that each form in one style is $\mathbf{NCF}$ isomorphic to a form in the other style. This new kind of result is called an “isomorphic enclosure”, and a matching pair of isomorphic enclosures is called an “isomorphic equivalence”. Equivalence [i] accords with Corollary 3.3(b), which states that $\mathbf{NCF}$ and $\mathbf{CsqF}$ are isomorphically equivalent. Similarly, equivalence [ii] accords with Corollary 4.3(b), which states that $\mathbf{CsqF_{\tilde{a}}}$ and $\mathbf{CsetF}$ are isomorphically equivalent. The paragraphs after these two corollaries provide historical context, more details, and more senses in which the two corollaries accord with literature’s equivalences [i] and [ii].

Other results show that $\mathbf{NCF}$ is pleasant in other ways. Theorem 2.3 shows that $\mathbf{NCF}$ is a well-defined category. Theorem 2.4 shows that an $\mathbf{NCF}$ isomorphism can be characterized by bijections for nodes, choices, and players. Theorem 2.7 shows that there is a forgetful functor from $\mathbf{NCF}$ to $\mathbf{NCP}$, which is SP’s category of node-and-choice preforms. In addition, various results in Sections 2.1–2.3 show that the category interacts naturally with game-theoretic concepts like the assignment of information sets to players. Also, Section 2.4 shows that the properties of no-absentmindedness and perfect-information are invariant to $\mathbf{NCF}$ isomorphisms. Finally, the paragraph after Corollary 3.5 shows how the negation of isomorphic enclosure formalizes the notion that a property is truly “restrictive” and “substantial” as opposed to merely “notational”.

1.4.

Categorical Dividends

Section 1.3 above argues that $\mathbf{NCF}$ systematizes prior style equivalences and that it is a pleasant category in a variety of other ways. Also, Sections 1.2 and 5.2 argue that $\mathbf{NCF}$ promises to be of practical importance in the larger agenda of translating game theory across styles. Further, the following three paragraphs identify three practical ways that $\mathbf{NCF}$ directly contributes to game theory.

First, isomorphic invariance is a natural and powerful concept. For example, two elementary propositions in Section 3.3 use isomorphic invariance to find [1] general circumstances in which one subcategory is strictly isomorphically enclosed by another and [2] general circumstances in which an isomorphic enclosure can be restricted to smaller subcategories. The latter proposition is used by Corollary 3.7(b) to easily construct an isomorphic enclosure for the proof highlighted in the next paragraph. Further, both propositions are used by Section 4.3 to easily derive new results about perfect-information.

Second, isomorphic enclosures can be composed (note 19). Such compositions can make it much easier to derive other isomorphic enclosures. For example, the proof of Corollary 4.3(b)’s reverse direction is just six lines long, and the third paragraph following the corollary’s proof explains how this simple argument replaces six difficult pages in SE’s proof of its Theorem 3.2. Thus the isomorphic equivalence of Corollary 4.3(b) is much easier to prove than the corresponding ad hoc equivalence of SE Theorems 3.1 and 3.2 (this was called equivalence [ii] in Section 1.3).

Third, isomorphic enclosures have consequences for form derivatives, and Section 5.1 deduces them simultaneously for all isomorphic enclosures. More specifically, each isomorphic enclosure is defined via isomorphisms, and Proposition 2.6 implies that each such isomorphism has consequences not only for form components (such as nodes, choices, and players) but also for form derivatives (such as the precedence relation among nodes, and each player’s collection of information sets). In contrast, the literature’s ad hoc style equivalences concern only form components.

1.5.

Organization

Section 2 develops $\mathbf{NCF}$, the category of node-and-choice forms. Less generally, Section 3 develops the subcategory $\mathbf{CsqF}$ for choice-sequence forms, and Section 4 develops the subcategory $\mathbf{CsetF}$ for choice-set forms. Sections 3.2 and 3.3 use the context of $\mathbf{CsqF}$ to introduce the general concept of isomorphic enclosure, and to introduce general propositions about isomorphic invariance. Further, Section 5.1 uses parts of Sections 3 and 4 to illustrate some general consequences of isomorphic enclosure. Finally, Section 5.2 discusses future research.

Although many proofs appear within the text, twelve lengthy proofs and their associated lemmas are relegated to the appendices. Appendix A concerns $\mathbf{NCF}$, Appendix B concerns $\mathbf{CsqF}$, and Appendix C concerns $\mathbf{CsetF}$.

2. The Category of Node-and-Choice Forms

2.1.

Objects

Let $T$ be a set of elements $t$ called nodes. As in SP Section 2.1 (where “SP” abbreviates Streufert 2018), a pair $(T,p)$ is a functioned tree iff there are $t^{o}⋅∈⋅T$ and $X⋅⊆⋅T$ such that [T1] $p$ is a nonempty function from $T⧷⎨t^{o}⎬$ onto $X$ and [T2] $(∀t∈T⧷⎨t^{o}⎬)(∃m∈{{\mathbb{N}}_{1}})$ $p^{m}(t)=t^{o}$.666I adopt the conventions that ${{\mathbb{N}}_{0}}$ is $⎨0,1,2,...⎬$, that ${{\mathbb{N}}_{1}}$ is $⎨1,2,...⎬$, and that, for any function $f$, $f^{0}$ is the identity function. Call $p$ the (immediate) predecessor function.

A functioned tree (uniquely) determines many entities beyond $T$ and $p$. First, it determines its root node $t^{o}$ and its set $X$ of decision nodes. Second, it determines its stage function $k{:}T\textrightarrow{{\mathbb{N}}_{0}}$ by [a] $k(t^{o})=0$ and [b] $(∀t∈T⧷⎨t^{o}⎬)$ $p^{k(t)}(t)=t^{o}$. Further, it determines its (strict) precedence relation $≺$ on $T$ by $(∀t^{1}∈T,t^{2}∈T)$ $t^{1}⋅≺⋅t^{2}$ iff $(∃m∈{{\mathbb{N}}_{1}})$ $t^{1}=p^{m}(t^{2})$. Relatedly, it determines its weak precedence relation $≼$ on $T$ by $(∀t^{1}∈T,t^{2}∈T)$ $t^{1}⋅≼⋅t^{2}$ iff $(∃m∈{{\mathbb{N}}_{0}})$ $t^{1}=p^{m}(t^{2})$. Finally, it determines the set ${\mathcal{Z}}$ of maximal chains in $(T,≼)$. This can be split into the set $\mathcal{Z}_{\mathsf{ft}}$ of finite maximal chains and the (possibly empty) set $\mathcal{Z}_{\mathsf{inft}}$ of infinite maximal chains. These derived entities and their basic properties are developed in SP Sections 2.1 and 2.2.

Let $C$ be a set of elements $c$ called choices. A triple $Π=(T,C,⊗)$ is a (node-and-choice) preform (SP Section 3.1) iff

[TABLE]

Call $⊗$ the node-and-choice operator,101010A preform’s node-and-choice operator $⊗$ can be regarded as a special kind of labeled transition system (e.g. Blackburn, de Rijke, and Venema 2001, page 3; van Benthem 2014, page 36). More precisely, a labeled transition system is a pair $(S,(R_{a})_{a∈A})$ consisting of [1] a set $S$ of states $s$ and [2] a collection of binary relations $R_{a}$, each defined over $S$, which is indexed by a set $A$ of labels $a$. A preform’s node-and-choice operator $⊗⋅⊆⋅T×C×T$ determines a labeled transition system $(S,(R_{a})_{a∈A})$ by setting $S=T$, setting $A=C$, and setting each $R_{c}=⎨(t,t^{\sharp})|(t,c,t^{\sharp})∈⊗⎬$. Conversely, a labeled transition system $(S,(R_{a})_{a∈A})$ determines a node-and-choice operator $⊗⋅⊆⋅T×C×T$ by setting $T=S$, setting $C=A$, and setting $⊗=⎨(s,a,s′)|(s,s′)∈R_{a}⎬$. [P2] restricts this construction by requiring that $⎨(s′,s)|(∃a∈A)(s,s′)∈R_{a}⎬$ is a functioned tree, and [P3] further restricts the construction by requiring that the labels $a⋅∈⋅A$ serve to specify information sets (these two restrictions concern [1] and [3] in note 2). and let $t⊗c$ denote its value at $(t,c)⋅∈⋅F\mspace{1.0mu}^{\mathsf{gr}}$. Call $F$ the feasibility correspondence, call $t^{o}$ the root node, call $p$ the immediate-predecessor function, and call ${\mathcal{H}}$ the collection of information sets. In addition, let $X$ equal $F^{-1}(C)$ (inconsequentially, SP uses $F^{-1}(C)$ rather than $X$). Call $X$ the decision-node set.111111SP Lemma C.1(b,c) implies that a preform’s $t^{o}$ and $X$ coincide with the underlying tree’s $t^{o}$ and $X$. Hence the symbols $t^{o}$ and $X$ are unambiguous.

A node-and-choice preform $Π$ (uniquely) determines many entities. First, it determines its components $T$, $C$, and $⊗$. Second, it determines its $F$, $t^{o}$, $p$, ${\mathcal{H}}$, and $X$, as discussed in the previous paragraph. Third, [P2] determines the functioned tree $(T,p)$, which in turn determines $k$, $≺$, $≼$, $\mathcal{Z}_{\mathsf{ft}}$, and $\mathcal{Z}_{\mathsf{inft}}$, as discussed in the second-previous paragraph. Finally, define the preform’s previous-choice function $q{:}T⧷⎨t^{o}⎬\textrightarrow C$ by $q\mspace{1.0mu}^{\mathsf{gr}}=⎨(t^{\sharp},c)∈T×C|(∃t∈T)(t,c,t^{\sharp})∈⊗\mspace{1.0mu}^{\mathsf{gr}}⎬$. All these entities and their basic properties are developed in SP Sections 3.1 and 3.2. Among the basic properties is the convenient fact that $(p,q)=⊗^{-1}$. Further properties appear in SP Lemmas A.1, C.1, and C.2, and also in Lemma A.1 here.

Let $I$ be a set of elements $i$ called players. A quadruple $Φ=(I,T,(C_{i})_{i∈I},⊗)$ is a (node-and-choice) form iff

[TABLE]

Each $C_{i}$ is the set of choices that are assigned to player $i$. The definitions in this paragraph are new to this paper (and an earlier version, Streufert 2016).

A node-and-choice form $Φ$ (uniquely) determines many entities. First, it determines its components $I$, $T$, $(C_{i})_{i∈I}$, and $⊗$. Second, [F1] determines $C$ and the preform $(T,C,⊗)$, which in turn determines $F$, $t^{o}$, $p$, $q$, ${\mathcal{H}}$, $X$, $k$, $≺$, $≼$, $\mathcal{Z}_{\mathsf{ft}}$, and $\mathcal{Z}_{\mathsf{inft}}$, as discussed in the second-previous paragraph. In addition, define $(X_{i})_{i∈I}$ at each $i$ by $X_{i}=∪_{c∈C_{i}}F^{-1}(c)$. $X_{i}$ is the set of decision nodes that are assigned to player $i$. Further, define $({\mathcal{H}}_{i})_{i∈I}$ at each $i$ by ${\mathcal{H}}_{i}=⎨F^{-1}(c)|c∈C_{i}⎬$. ${\mathcal{H}}_{i}$ is the collection of information sets that are assigned to player $i$.

Proposition 2.1**.**

Suppose $(I,T,(C_{i})_{i},⊗)$ is a node-and-choice form with its $X$, ${\mathcal{H}}$, $(X_{i})_{i∈I}$, and $({\mathcal{H}}_{i})_{i∈I}$. Then the following hold.

• (a)

$∪_{i∈I}X_{i}=X$* and $(∀i∈I,j∈I⧷⎨i⎬)⋅X_{i}∩X_{j}=∅$.*

• (b)

$(∀i∈I)⋅{\mathcal{H}}_{i}$* partitions $X_{i}$.*

• (c)

$∪_{i∈I}{\mathcal{H}}_{i}={\mathcal{H}}$* and $(∀i∈I,j∈I⧷⎨i⎬)⋅{\mathcal{H}}_{i}∩{\mathcal{H}}_{j}=∅$. (Proof A.3.)*

Here are two minor remarks. [1] A preform can be understood as a one-player form. Specifically, $(T,C,⊗)$ is a preform iff $(⎨1⎬,T,(C),⊗)$ is a form, where $(C_{i})_{i}=(C)$ is taken to mean $C_{1}=C$. [2] A player $i$ in a form is said to be vacuous iff $C_{i}=∅$. A vacuous player $i$ necessarily has $X_{i}=∅$ and ${\mathcal{H}}_{i}=∅$. Vacuous players can be convenient. For example, one can posit the existence of a chance player, and yet create a game without chance nodes by letting the chance player be vacuous.

2.2.

Morphisms

A (node-and-choice) preform morphism (SP Section 3.3) is a quadruple $α=[Π,Π′,τ,δ]$ such that $Π=(T,C,⊗)$ and $Π′=(T′,C′,⊗′)$ are preforms,

[TABLE]

SP Propositions 3.3 and 3.4 give two characterizations of preform morphisms which feel more category-theoretic. A (node-and-choice) form morphism is a quintuple $β=[Φ,Φ′,ι,τ,δ]$ s.t. $Φ=(I,T,(C_{i})_{i∈I},⊗)$ and $Φ′=(I′,T′,(C′_{i′})_{i′∈I′},⊗′)$ are forms,

[TABLE]

The first paragraph of Proposition 2.2 rearranges the definition of a morphism. Meanwhile, the second and third paragraphs concern the many derivatives which can be constructed, via Section 2.1, from the source and target forms. Parts (k) and (m) are new, while the remainder are obtained by combining [FM1] with various SP results for preforms and trees.

Proposition 2.2**.**

Suppose $Φ=(I,T,(C_{i})_{i∈I},⊗)$ and $Φ′=(I′,T′,(C′_{i′})_{i′∈I′},⊗′)$ are forms. Let $C=∪_{i∈I}C_{i}$ and $C′=∪_{i′∈I′}C′_{i′}$. Then $[Φ,Φ′,ι,τ,δ]$ is a morphism iff the following hold.

• (a)

$ι\,{:}\,I\,\textrightarrow\,I′$* .*

• (b)

$τ\,{:}\,T\,\textrightarrow\,T′$* .*

• (c)

$δ\,{:}\,C\,\textrightarrow\,C′$* .*

• (d)

$(∀i∈I)⋅δ(C_{i})⋅⊆⋅C′_{ι(i)}$.

• (e)

$⎨\,(τ(t),δ(c),τ(t^{\sharp}))\,|\,(t,c,t^{\sharp})∈⊗\mspace{1.0mu}^{\mathsf{gr}}\,⎬⋅⊆⋅⊗′\mspace{1.0mu}^{\mathsf{gr}}$.

Further, suppose $[Φ,Φ′,ι,τ,δ]$ is a morphism. Let $Π=(T,C,⊗)$ and $Π′=(T′,C′,⊗′)$. Also, derive $F$, $t^{o}$, $p$, $q$, $X$, $(X_{i})_{i∈I}$, ${\mathcal{H}}$, and $({\mathcal{H}}_{i})_{i∈I}$ from $Π$ and $Φ$. Also, derive $F′$, $t^{\prime o}$, $p′$, $q′$, $X′$, $(X′_{i′})_{i′∈I′}$, ${\mathcal{H}}′$, and $({\mathcal{H}}′_{i′})_{i′∈I′}$ from $Π′$ and $Φ′$. Then the following hold.

• (f)

$⎨\,(τ(t),δ(c))\,|\,(t,c)∈F\mspace{1.0mu}^{\mathsf{gr}}\,⎬⋅⊆⋅F′\mspace{1.0mu}^{\mathsf{gr}}$.

• (g)

$t^{\prime o}⋅≼′⋅τ(t^{o})$.

• (h)

$⎨\,(τ(t^{\sharp}),τ(t))\,|\,(t^{\sharp},t)∈p\mspace{1.0mu}^{\mathsf{gr}}\,⎬⋅⊆⋅p′\mspace{1.0mu}^{\mathsf{gr}}$.

• (i)

$⎨\,(τ(t^{\sharp}),δ(c))\,|\,(t^{\sharp},c)∈q\mspace{1.0mu}^{\mathsf{gr}}\,⎬⋅⊆⋅q′\mspace{1.0mu}^{\mathsf{gr}}$.

• (j)

$τ(X)⋅⊆⋅X′$.

• (k)

$(∀i∈I)⋅τ(X_{i})⋅⊆⋅X′_{ι(i)}$.

• (l)

$(∀H∈{\mathcal{H}})(∃H′∈{\mathcal{H}}′)⋅τ(H)⋅⊆⋅H′$.

• (m)

$(∀i∈I,H∈{\mathcal{H}}_{i})(∃H′∈{\mathcal{H}}′_{ι(i)})⋅τ(H)⋅⊆⋅H′$.

Finally, derive $k$, $≺$, $≼$, $\mathcal{Z}_{\mathsf{ft}}$, and $\mathcal{Z}_{\mathsf{inft}}$ from $(T,p)$. Also, derive $k′$, $≺′$, $≼′$, $\mathcal{Z}_{\mathsf{ft}}′$, and $\mathcal{Z}_{\mathsf{inft}}′$ from $(T′,p′)$. Then the following hold.

• (n)

$(∀t∈T)⋅k′(τ(t))=k(t)+k′(τ(t^{o}))$.

• (o)

$⎨\,(τ(t^{1}),τ(t^{2}))\,|\,(t^{1},t^{2})∈≺\mspace{1.0mu}^{\mathsf{gr}}\,⎬⋅⊆⋅≺′\mspace{1.0mu}^{\mathsf{gr}}$.

• (p)

$⎨\,(τ(t^{1}),τ(t^{2}))\,|\,(t^{1},t^{2})∈≼\mspace{1.0mu}^{\mathsf{gr}}\,⎬⋅⊆⋅≼′\mspace{1.0mu}^{\mathsf{gr}}$.

• (q)

$(∀Z∈\mathcal{Z}_{\mathsf{ft}})(∃Z′∈\mathcal{Z}_{\mathsf{ft}}′∪\mathcal{Z}_{\mathsf{inft}}′)⋅τ(Z)⋅⊆⋅Z′$.

• (r)

$(∀Z∈\mathcal{Z}_{\mathsf{inft}})(∃Z′∈\mathcal{Z}_{\mathsf{inft}}′)⋅τ(Z)⋅⊆⋅Z′$. (Proof A.4.)

2.3.

The category $\mathbf{NCF}$

This paragraph and Theorem 2.3 define the category $\mathbf{NCF}$, which is called the category of node-and-choice forms. Let an object be a (node-and-choice) form $Φ=(I,T,(C_{i})_{i∈I},⊗)$. Let an arrow be a (node-and-choice) form morphism $β=[Φ,Φ′,ι,τ,δ]$. Let source, target, identity, and composition be

[TABLE]

where $\mathsf{id}_{I}$, $\mathsf{id}_{T}$, and $\mathsf{id}_{∪_{i∈I}C_{i}}$ are identities in $\mathbf{Set}$.

Theorem 2.3**.**

$\mathbf{NCF}$* is a category. (Proof A.5.)*

Theorem 2.4**.**

Suppose $β=[Φ,Φ′,ι,τ,δ]$ is a morphism. Then (a) $β$ is an isomorphism iff $ι$, $τ$, and $δ$ are bijections. Further (b) if $β$ is an isomorphism, then $β^{-1}=[Φ′,Φ,ι^{-1},τ^{-1},δ^{-1}]$. (Proof A.7.)

Corollary 2.5**.**

Suppose $[Φ,Φ′,ι,τ,δ]$ is a morphism. Let $Π$ be the preform in $Φ$, and let $Π′$ be the preform in $Φ′$. Then $[Φ,Φ′,ι,τ,δ]$ is an isomorphism iff [1] $[Π,Π′,τ,δ]$ is a preform isomorphism and [2] $ι$ is a bijection. (Proof here.)

Proof*.*

Note $[Π,Π′,τ,δ]$ is a preform morphism by [FM1] for $[Φ,Φ′,ι,τ,δ]$. Thus SP Theorem 3.7(a) shows that [1] is equivalent to the bijectivity of $τ$ and $δ$. Therefore [1] and [2] together are equivalent to the bijectivity of $ι$, $τ$, and $δ$. By Theorem 2.4(a), this is equivalent to $[Φ,Φ′,ι,τ,δ]$ being an isomorphism. $\Box$

Proposition 2.6 organizes some121212The proposition’s list of consequences is far from exhaustive. For example, in the notation of the proposition’s second paragraph, Lemma A.2(b) deduces that $(∀c∈C)$ $τ(F^{-1}(c))=(F′)^{-1}(δ(c))$. of the consequences of a form isomorphism. The proposition’s first paragraph concerns form components, while the second and third paragraphs concern form derivatives. Consequences (a)–(c) repeat the forward direction of Theorem 2.4(a). Consequences (d), (k), and (m) are new, while the remainder are obtained by combining the forward direction of Corollary 2.5 with SP results about preforms and trees. The entire proposition is comparable to Proposition 2.2 for morphisms, and Section 5.1 will discuss how the proposition contributes directly to game theory.

To address a minor technical issue, note that many of the proposition’s consequences are formulated by restricting functions. In each case, the codomain of the restriction is defined so that the restriction is surjective. Some other minor technical issues are discussed in notes 8, 13, and 14.

Proposition 2.6**.**

Suppose $[Φ,Φ′,ι,τ,δ]$ is an isomorphism, where $Φ=(I,T,$ $(C_{i})_{i∈I},⊗)$ and $Φ′=(I′,T′,(C′_{i′})_{i′∈I′},⊗′)$. Let $C=∪_{i∈I}C_{i}$ and $C′=∪_{i′∈I′}C′_{i′}$. Then the following hold.

• (a)

$ι$* is a bijection from $I$ onto $I′$.*

• (b)

$τ$* is a bijection from $T$ onto $T′$.*

• (c)

$δ$* is a bijection from $C$ onto $C′$.*

• (d)

$(∀i∈I)⋅δ|_{C_{i}}$* is a bijection from $C_{i}$ onto $C′_{ι(i)}$.131313To be clear, parts (d), (k), and (m) do hold when there is a vacuous player $i$. In this case, $C_{i}$ is empty, and thus, $δ|_{C_{i}}$, $C′_{ι(i)}$, $X_{i}$, $τ|_{X_{i}}$, $X′_{ι(i)}$, ${\mathcal{H}}_{i}$, $τ|_{{\mathcal{H}}_{i}}$, and ${\mathcal{H}}′_{ι(i)}$ are all empty as well.*

• (e)

$(τ,δ,τ)|_{⊗\mspace{1.0mu}^{\mathsf{gr}}}$* is a bijection from $⊗\mspace{1.0mu}^{\mathsf{gr}}$ onto $⊗′\mspace{1.0mu}^{\mathsf{gr}}$.*

Further, let $Π=(T,C,⊗)$ and $Π′=(T′,C′,⊗′)$. Also, derive $F$, $t^{o}$, $p$, $q$, $X$, $(X_{i})_{i∈I}$, ${\mathcal{H}}$, and $({\mathcal{H}}_{i})_{i∈I}$ from $Π$ and $Φ$. Also, derive $F′$, $t^{\prime o}$, $p′$, $q′$, $X′$, $(X′_{i′})_{i′∈I′}$, ${\mathcal{H}}′$, and $({\mathcal{H}}′_{i′})_{i′∈I′}$ from $Π′$ and $Φ′$. Then the following hold.

• (f)

$(τ,δ)|_{F\mspace{1.0mu}^{\mathsf{gr}}}$* is a bijection from $F\mspace{1.0mu}^{\mathsf{gr}}$ onto $F′\mspace{1.0mu}^{\mathsf{gr}}$.*

• (g)

$τ(t^{o})=t^{\prime o}$.

• (h)

$(τ,τ)|_{p\mspace{1.0mu}^{\mathsf{gr}}}$* is a bijection from $p\mspace{1.0mu}^{\mathsf{gr}}$ onto $p′\mspace{1.0mu}^{\mathsf{gr}}$.*

• (i)

$(τ,δ)|_{q\mspace{1.0mu}^{\mathsf{gr}}}$* is a bijection from $q\mspace{1.0mu}^{\mathsf{gr}}$ onto $q′\mspace{1.0mu}^{\mathsf{gr}}$.*

• (j)

$τ|_{X}$* is a bijection from $X$ onto $X′$.*

• (k)

$(∀i∈I)⋅τ|_{X_{i}}$* is a bijection from $X_{i}$ onto $X′_{ι(i)}$.*${}^{\text{\ref{8190}}}$**

• (l)

$τ|_{{\mathcal{H}}}$* is a bijection from ${\mathcal{H}}$ onto ${\mathcal{H}}′$.141414In parts (l), (m), (q), and (r), $τ$ is understood to be the function ${\mathcal{P}}(T)⋅∋⋅S⋅\mapsto⋅⎨τ(t)|t∈S⎬⋅∈⋅{\mathcal{P}}(T′)$. For example, if $H⋅∈⋅{\mathcal{H}}$, then $τ(H)=⎨τ(t)|t∈H⎬$. Similarly, if $Z⋅∈⋅\mathcal{Z}_{\mathsf{ft}}∪\mathcal{Z}_{\mathsf{inft}}$, then $τ(Z)=⎨τ(t)|t∈Z⎬$.*

• (m)

$(∀i∈I)⋅τ|_{{\mathcal{H}}_{i}}$* is a bijection from ${\mathcal{H}}_{i}$ onto ${\mathcal{H}}′_{ι(i)}$.*${}^{\text{\ref{8190}}}$,${}^{\text{\ref{8158}}}$**

Finally, derive $k$, $≺$, $≼$, $\mathcal{Z}_{\mathsf{ft}}$, and $\mathcal{Z}_{\mathsf{inft}}$ from $(T,p)$. Also, derive $k′$, $≺′$, $≼′$, $\mathcal{Z}_{\mathsf{ft}}′$, $\mathcal{Z}_{\mathsf{inft}}′$ from $(T′,p′)$. Then the following hold.

• (n)

$(∀t∈T)⋅k′(τ(t))=k(t)$.

• (o)

$(τ,τ)|_{≺\mspace{1.0mu}^{\mathsf{gr}}}$* is a bijection from $≺\mspace{1.0mu}^{\mathsf{gr}}$ onto $≺′\mspace{1.0mu}^{\mathsf{gr}}$.*

• (p)

$(τ,τ)|_{≼\mspace{1.0mu}^{\mathsf{gr}}}$* is a bijection from $≼\mspace{1.0mu}^{\mathsf{gr}}$ onto $≼′\mspace{1.0mu}^{\mathsf{gr}}$.*

• (q)

$τ|_{\mathcal{Z}_{\mathsf{ft}}}$* is a bijection from $\mathcal{Z}_{\mathsf{ft}}$ onto $\mathcal{Z}_{\mathsf{ft}}′$.*${}^{\text{\ref{8158}}}$**

• (r)

$τ|_{\mathcal{Z}_{\mathsf{inft}}}$* is a bijection from $\mathcal{Z}_{\mathsf{inft}}$ onto $\mathcal{Z}_{\mathsf{inft}}′$.${}^{\text{\ref{8158}}}$ (Proof A.9.)*

As already noted, the definition of a form incorporates a preform, and the definition of a form morphism incorporates a preform morphism. Correspondingly, Theorem 2.7 shows there is a “forgetful” functor $\mathsf{P}$ from $\mathbf{NCF}$ to $\mathbf{NCP}$. Incidentally, SP Theorem 3.9 shows there is a similar functor $\mathsf{F}$ from $\mathbf{NCP}$ to $\mathbf{Tree}$. Hence $\mathsf{F}○\mathsf{P}$ is a functor from $\mathbf{NCF}$ to $\mathbf{Tree}$.

Theorem 2.7**.**

Define $\mathsf{P}$ from $\mathbf{NCF}$ to $\mathbf{NCP}$ by

[TABLE]

Then $\mathsf{P}$ is a well-defined functor. (Proof A.10.)

2.4.

No-absentmindedness and perfect-information

Consider an arbitrary category $\mathbf{Z}$, and a property which is defined for the objects of $\mathbf{Z}$. The property is said to be isomorphically invariant iff, for each object, the object satisfies the property iff all of its isomorphs satisfy the property. This section explores two isomorphically invariant properties: [1] no-absentmindedness and [2] perfect-information. Both properties restrict information sets.

No-absentmindedness is a standard property which is widely regarded as being very weak (see, for example, Alós-Ferrer and Ritzberger 2016 Section 4.2.3). To define this property in $\mathbf{NCP}$, consider an $\mathbf{NCP}$ preform with its $≺$ and ${\mathcal{H}}$. Then the preform is said to have no-absentmindedness iff $(∄H∈{\mathcal{H}},t^{A}∈H,t^{B}∈H)⋅t^{A}⋅≺⋅t^{B}$.151515Piccione and Rubinstein 1997 Figure 1 provides an example of absentmindedness. A corresponding $\mathbf{NCP}$ preform $Π=(T,C,⊗)$ can be defined by $T=⎨⎨⎬,({\mathsf{a}}),({\mathsf{b}}),({\mathsf{a}},{\mathsf{a}}),({\mathsf{a}},{\mathsf{b}})⎬$, $C=⎨{\mathsf{a}},{\mathsf{b}}⎬$, and $⊗=⎨(⎨⎬,{\mathsf{a}},({\mathsf{a}})),$ $(⎨⎬,{\mathsf{b}},({\mathsf{b}}))$, $(({\mathsf{a}}),{\mathsf{a}},({\mathsf{a}},{\mathsf{a}}))$, $(({\mathsf{a}}),{\mathsf{b}},({\mathsf{a}},{\mathsf{b}})⎬$. No-absentmindedness fails because ${\mathcal{H}}$ contains $H=⎨⎨⎬,({\mathsf{a}})⎬$ and $⎨⎬⋅≺⋅({\mathsf{a}})$. A corresponding $\mathbf{NCF}$ form $Φ=(I,T,(C_{i})_{i},⊗)$ can be defined by setting $T$ and $⊗$ as above, setting $I=⎨\mathsf{1}⎬$, and setting $C_{\mathsf{1}}=⎨{\mathsf{a}},{\mathsf{b}}⎬$. The existence of this example is used in the proof of Corollary 3.5. Further, consider an $\mathbf{NCF}$ form with its preform. Then the form is said to have no-absentmindedness iff its preform has no-absentmindedness.

Proposition 2.8**.**

(ao) If $[Π,Π′,τ,δ]$ is an $\mathbf{NCP}$ morphism and $Π′$ has no-absentmindedness, then $Π$ has no-absentmindedness. (a) No-absentmindedness is isomorphically invariant in $\mathbf{NCP}$. (bo) If $[Φ,Φ′,ι,τ,δ]$ is an $\mathbf{NCF}$ morphism and $Φ′$ has no-absentmindedness, then $Φ$ has no-absentmindedness. (b) No-absentmindedness is isomorphically invariant in $\mathbf{NCF}$. (Proof A.11.)

Let $\mathbf{NCP_{\tilde{a}}}$ be the full subcategory of $\mathbf{NCP}$ whose objects are preforms with no-absentmindedness. (I am endeavouring to use subscripts for isomorphically invariant properties.) Similarly, let $\mathbf{NCF_{\tilde{a}}}$ be the full subcategory of $\mathbf{NCF}$ whose objects are forms with no-absentmindedness. No-absentmindedness will appear again in Section 3.3.

Perfect-information is another standard property. It is restrictive, and at the same time, there are many interesting games which satisfy it (see, for example, Osborne and Rubinstein 1994 Part II). As in SP Section 3.5, an $\mathbf{NCP}$ preform, with its collection ${\mathcal{H}}$ of information sets $H$, is said to have perfect-information iff $(∀H∈{\mathcal{H}})$ $|H|=1$. Perfect-information is strictly stronger than no-absentmindedness.161616To see that perfect-information implies no-absentmindedness, assume no-absentmindedness is violated. Then there is $H⋅∈⋅{\mathcal{H}}$, $t^{A}⋅∈⋅H$, and $t^{B}⋅∈⋅H$ such that $t^{A}⋅≺⋅t^{B}$. Thus $t^{A}⋅≠⋅t^{B}$. So $|H|>1$ and perfect-information is violated.,171717 A simple example of a form which satisfies no-absentmindedness but not perfect-information is a form corresponding to a two-person simultaneous-move game. Specifically, define the $\mathbf{NCP}$ preform $Π=(T,C,⊗)$ by $T=⎨⎨⎬,({\mathsf{a}}),({\mathsf{b}}),({\mathsf{a}},{\mathsf{c}}),({\mathsf{a}},{\mathsf{d}}),({\mathsf{b}},{\mathsf{c}}),({\mathsf{b}},{\mathsf{d}})⎬$, $C=⎨{\mathsf{a}},{\mathsf{b}},{\mathsf{c}},{\mathsf{d}}⎬$, and $⊗=⎨(⎨⎬,{\mathsf{a}},({\mathsf{a}})),$ $(⎨⎬,{\mathsf{b}},({\mathsf{b}}))$, $(({\mathsf{a}}),{\mathsf{c}},({\mathsf{a}},{\mathsf{c}}))$, $(({\mathsf{a}}),{\mathsf{d}},({\mathsf{a}},{\mathsf{d}}))$, $(({\mathsf{b}}),{\mathsf{c}},({\mathsf{b}},{\mathsf{c}}))$, $(({\mathsf{b}}),{\mathsf{d}},({\mathsf{b}},{\mathsf{d}}))⎬$. Note that ${\mathcal{H}}$ consists of $H=⎨⎨⎬⎬$ and $H′=⎨({\mathsf{a}}),({\mathsf{b}})⎬$. No-absentmindedness holds because [i] $H$ is a singleton and [ii] neither $({\mathsf{a}})⋅≺⋅({\mathsf{b}})$ nor $({\mathsf{a}})⋅≻⋅({\mathsf{b}})$. Perfect-information fails because $|H′|⋅≠⋅1$. A corresponding $\mathbf{NCF}$ form $Φ=(I,T,(C_{i})_{i},⊗)$ can be defined by setting $T$ and $⊗$ as above, setting $I=⎨\mathsf{1},\mathsf{2}⎬$, and setting $C_{\mathsf{1}}=⎨{\mathsf{a}},{\mathsf{b}}⎬$ and $C_{\mathsf{2}}=⎨{\mathsf{c}},{\mathsf{d}}⎬$. The existence of this example is used in the proof of Corollary 4.4. [A slightly more complicated example with the same combination of properties can be obtained from any of the five figures in Section 1.1.] Further, an $\mathbf{NCF}$ form is said to have perfect-information iff the form’s preform has perfect-information. (In spite of Proposition 2.9, the existence of a morphism does not lead to any logical relationship between the source’s perfect-information and the target’s perfect-information.)

Proposition 2.9**.**

(a) Perfect-information is isomorphically invariant in $\mathbf{NCP}$. (b) Perfect-information is isomorphically invariant in $\mathbf{NCF}$. (Proof A.12.)

Let $\mathbf{NCP_{p}}$ be the full subcategory of $\mathbf{NCP}$ whose objects are preforms with perfect-information. (The subscript $\mathbf{{}_{{\tilde{a}}p}}$ would be equivalent to the subscript p, because no-absentmindedness is implied by perfect-information, as shown in note 16.) Further, let $\mathbf{NCF_{p}}$ be the full subcategory of $\mathbf{NCF}$ whose objects are forms with perfect-information. Perfect-information will appear again in Section 4.3.

3. The Subcategory of Choice-Sequence Forms

3.1.

Objects

Let a (finite) sequence be a function from $⎨1,2,...\,m⎬$ for some nonnegative integer $m$ (to be clear, the empty sequence181818The empty sequence is the empty set. Further, $⎨⎬$ and $∅$ are alternative notations for the empty set. I use $⎨⎬$ for a root node, and use $∅$ for all other purposes. with empty domain is admitted by $m=0$). I will regard a sequence as a set of ordered pairs. For example, $t^{*}=⎨(1,{\mathsf{g}}),$ $(2,{\mathsf{f}}),$ $(3,{\mathsf{f}})⎬$ is a sequence with domain $⎨1,2,3⎬$. An alternative notation for the same entity is $t^{*}=(\mathsf{g,f,f})$. Yet another is $t^{*}=(t^{*}_{n})^{3}_{n=1}$ where $t^{*}_{1}={\mathsf{g}}$ and $t^{*}_{2}=t^{*}_{3}={\mathsf{f}}$.

Let the length of a sequence $t$ be $|t|$. For instance, the length of the example sequence is $|t^{*}|$ $=$ $|⎨(1,{\mathsf{g}}),(2,{\mathsf{f}}),(3,{\mathsf{f}})⎬|$ $=3$, which is consistent with the observation that $(2,{\mathsf{f}})$ $≠$ $(3,{\mathsf{f}})$. Note that the length of the empty sequence $⎨⎬$ is $|⎨⎬|=0$. Next, let the range of a sequence $t$ be $R(t)=⎨\,t_{n}\,|\,n∈⎨1,2,...\,|t|⎬\,⎬$. For instance, the range of the example sequence is $R(t^{*})=⎨\,t^{*}_{n}\,|\,n∈⎨1,2,3⎬\,⎬=⎨{\mathsf{g}},{\mathsf{f}},{\mathsf{f}}⎬=⎨{\mathsf{g}},{\mathsf{f}}⎬$. Note that the range of the empty sequence $⎨⎬$ is $R(⎨⎬)=∅$.

Let the concatenation $t±s$ of two sequences $t$ and $s$ be $⎨(1,t_{1}),$ $...$ $(|t|,t_{|t|}),$ $(|t|{+}1,s_{1}),$ $...$ $(|t|{+}|s|,s_{|s|})⎬$. Thus the concatenation of a sequence $t=(t_{1},t_{2},...\,t_{|t|})$ with a one-element sequence $(c)$ is $t±(c)=(t_{1},t_{2},...\,t_{|t|},c)$. Next, for any sequence $t$ and any $ℓ⋅∈⋅⎨0,1,2,...\,|t|⎬$, let ${}_{1}t_{ℓ}$ denote the initial segment $(t_{1},t_{2},...\,t_{ℓ})$. Thus for any sequence $t$, ${}_{1}t_{0}=⎨⎬$.

A choice-sequence $\mathbf{NCP}$ preform is an $\mathbf{NCP}$ preform $(T,C,⊗)$ such that

[TABLE]

Let $\mathbf{CsqP}$ be the full subcategory of $\mathbf{NCP}$ whose objects are choice-sequence preforms. Proposition 3.1 lists some of the special properties of $\mathbf{CsqP}$ preforms. Incidentally, property (h) and assumption [Csq1] together imply that each node in a $\mathbf{CsqP}$ preform is actually a choice sequence, as the terminology suggests.

Proposition 3.1**.**

Suppose $(T,C,⊗)$ is a $\mathbf{CsqP}$ preform. Derive its $F$, $t^{o}$, $p$, $q$, $k$, $≺$, and $≼$. Then the following hold.

• (a)

$t^{o}=⎨⎬$.

• (b)

$(∀t^{\sharp}∈T⧷⎨⎨⎬⎬)⋅p(t^{\sharp})={{}_{1}t^{\sharp}_{|t^{\sharp}|-1}}\,\text{and}⋅q(t^{\sharp})=t^{\sharp}_{|t^{\sharp}|}$.

• (c)

$⊗\mspace{1.0mu}^{\mathsf{gr}}=⎨⋅(t,c,t^{\sharp})∈T×C×T⋅|⋅t±(c){=}t^{\sharp}⋅⎬$.

• (d)

$F\mspace{1.0mu}^{\mathsf{gr}}=⎨⋅(t,c)∈T×C⋅|⋅t±(c)∈T⋅⎬$.

• (e)

$(∀t∈T,m∈⎨0,1,...\,|t|⎬)⋅p^{m}(t)={{}_{1}t_{|t|-m}}$.

• (f)

$(∀t∈T)$* $k(t)=|t|$.*

• (g)

$(∀t∈T)⋅t=(q○p^{|t|-ℓ}(t))^{|t|}_{ℓ=1}$.

• (h)

$C=∪_{t∈T}R(t)$.

• (i)

$(∀t^{A}∈T,t^{B}∈T)$* $t^{A}⋅≺⋅t^{B}$ iff $(|t^{A}|\,{<}\,|t^{B}|⋅\text{and}⋅t^{A}\,{=}\,{{}_{1}t^{B}_{|t^{A}|}})$.*

• (j)

$(∀t^{A}∈T,t^{B}∈T)$* $t^{A}⋅≼⋅t^{B}$ iff $(|t^{A}|\,≤\,|t^{B}|⋅\text{and}⋅t^{A}\,{=}\,{{}_{1}t^{B}_{|t^{A}|}})$. (Proof B.1.)*

Finally, let a choice-sequence $\mathbf{NCF}$ form be an $\mathbf{NCF}$ form whose preform is a $\mathbf{CsqP}$ preform. Then let $\mathbf{CsqF}$ be the full subcategory of $\mathbf{NCF}$ whose objects are choice-sequence $\mathbf{NCF}$ forms.

3.2.

Isomorphic Enclosure

Consider two full subcategories $\mathbf{A}$ and $\mathbf{B}$ of some overarching category $\mathbf{Z}$. Say that $\mathbf{A}$ is isomorphically enclosed in $\mathbf{B}$ (in symbols, $\mathbf{A}$ ̣\textrightarrow $\mathbf{B}$) iff every object of $\mathbf{A}$ is isomorphic to an object of $\mathbf{B}$. Note that $\mathbf{A}$ ̣\textrightarrow $\mathbf{B}$ concerns not only the subcategories $\mathbf{A}$ and $\mathbf{B}$ but also, implicitly, the overarching category $\mathbf{Z}$ within which isomorphisms are defined. Further note that isomorphic enclosures can be composed in the sense that $\mathbf{A}$ ̣\textrightarrow $\mathbf{B}$ and $\mathbf{B}$ ̣\textrightarrow $\mathbf{C}$ imply $\mathbf{A}$ ̣\textrightarrow $\mathbf{C}$.191919To prove composability, recall $\mathbf{A}$ ̣\textrightarrow $\mathbf{B}$ means that [a] each $\mathbf{A}$ form is isomorphic to a $\mathbf{B}$ form. Similarly, $\mathbf{B}$ ̣\textrightarrow $\mathbf{C}$ means that [b] each $\mathbf{B}$ form is isomorphic to a $\mathbf{C}$ form. [a] and [b] imply that each $\mathbf{A}$ form is isomorphic to a $\mathbf{C}$ form, and this is what is meant by $\mathbf{A}$ ̣\textrightarrow $\mathbf{C}$. Finally, let \text{\mathbf{A}}⋅{\text{\@text@daccent{⟷}}}⋅\text{\mathbf{B}} mean that both \text{\mathbf{A}}⋅{\text{\@text@daccent{→}}}⋅\text{\mathbf{B}} and \text{\mathbf{A}}⋅{\text{\@text@daccent{←}}}⋅\text{\mathbf{B}} hold. Call ̣⟷ isomorphic equivalence. Isomorphic equivalence implies the standard categorical concept of equivalence in MacLane 1998 page 18.

Theorem 3.2**.**

(a) $\mathbf{NCP}$ ̣\textrightarrow $\mathbf{CsqP}$. In particular, suppose $Π=(T,C,⊗)$ is an $\mathbf{NCP}$ preform with its $p$, $q$, and $k$. Define $\bar{T}=⎨\,(q○p^{k(t)-ℓ}(t))^{k(t)}_{ℓ=1}\,|\,t∈T\,⎬$, define $\bar{τ}{:}T\textrightarrow\bar{T}$ by $\bar{τ}(t)=(q○p^{k(t)-ℓ}(t))^{k(t)}_{ℓ=1}$, and define $\bar{⊗}$ by surjectivity and $\bar{⊗}\mspace{1.0mu}^{\mathsf{gr}}=⎨\,(\bar{τ}(t),c,\bar{τ}(t^{\sharp}))\,|\,(t,c,t^{\sharp})∈⊗\mspace{1.0mu}^{\mathsf{gr}}\,⎬$. Then $\bar{Π}=(\bar{T},C,\bar{⊗})$ is an $\mathbf{CsqP}$ preform, $\bar{τ}$ is a bijection, and $[Π,\bar{Π},\bar{τ},\mathsf{id}_{C}]$ is an $\mathbf{NCP}$ isomorphism. (b) $\mathbf{NCF}$ ̣\textrightarrow $\mathbf{CsqF}$. In particular, suppose $Φ=(I,T,(C_{i})_{i∈I},⊗)$ is an $\mathbf{NCF}$ form. Define $\bar{T}$, $\bar{τ}$, and $\bar{⊗}$ as in part (a). Then $\bar{Φ}=(I,\bar{T},(C_{i})_{i∈I},\bar{⊗})$ is a $\mathbf{CsqF}$ form and $[Φ,\bar{Φ},\mathsf{id}_{I},\bar{τ},\mathsf{id}_{∪_{i∈I}C_{i}}]$ is an $\mathbf{NCF}$ isomorphism. (Proof B.3.)202020Theorems 3.2 and 4.2 draw upon Lemmas A.14 and A.15. These nontrivial lemmas show how to construct isomorphisms in $\mathbf{NCP}$ and $\mathbf{NCF}$ from bijections for nodes, choices, and players. These lemmas appear to have application beyond this paper.

Corollary 3.3**.**

(a) $\mathbf{NCP}$ ̣⟷ $\mathbf{CsqP}$. (b) $\mathbf{NCF}$ ̣⟷ $\mathbf{CsqF}$. (Proof here.)

Proof*.*

(a). $\mathbf{NCP}$ ̣\textrightarrow $\mathbf{CsqP}$ by Theorem 3.2(a). Conversely, each $\mathbf{CsqP}$ preform is an $\mathbf{NCP}$ preform by definition. (b). This is very similar to (a). Change “preform” to “form”, $\mathbf{P}$ to $\mathbf{F}$, and (a) to (b). $\Box$

This equivalence has a long history. In the more distant past, it was informally understood that game trees could be specified in terms of either [i] a collection of nodes and a collection of edges or [ii] a collection of sequences. Harris 1985 page 617 provides an example of this informal understanding. Specification style [i] uses the nomenclature of graph theory (e.g., Tutte 1984), and style-[i] trees were the basis on which Kuhn 1953 and Selten 1975 built game forms. Later, style-[ii] trees became the basis on which Osborne and Rubinstein 1994 built game forms.

Kline and Luckraz 2016212121The terms “choice”, “action”, and “alternative” are fundamentally synonymous. However, the literature tends to use “choice” when it is assumed that information sets do not share alternatives, and conversely, to use “action” when the assumption is relaxed. The assumption itself is insubstantial in the sense that one can always introduce more alternatives until each information set has its own alternatives (see SE Section 5.2, first paragraph, for more discussion). This paper makes the assumption for notational convenience, and correspondingly, uses “choice” (see SP Proposition 3.2(16b) and the paragraphs beforehand). In contrast, KL16 relaxes the assumption and uses “action”. (henceforth “KL16”) develop this equivalence by a pair of theorems. In recognition of the above authors, they call style-[i] forms “KS forms” and call style-[ii] forms “OR forms”. Then, one of their theorems (their Theorem 2) shows that a KS form can be derived from each OR form, while the other theorem (their Theorem 1) shows that each KS form can be mapped to an OR form.222222SE Theorems 3.2 and 3.1 adapt and slightly extend KL16 Theorems 2 and 1. These two theorems are depicted by the two arrows in Figure 3.1(a). The arrows are dashed to convey that the equivalence is ad hoc.

Corollary 3.3(b) develops the equivalence further. Specification-[i] forms are written as $\mathbf{NCF}$ forms, and specification-[ii] forms are written as $\mathbf{CsqF}$ forms. Corollary 3.3(b) is then a pair of results: one half (the very easy half) shows that an $\mathbf{NCF}$ form is isomorphic to each $\mathbf{CsqF}$ form, while the other half (Theorem 3.2) shows that each $\mathbf{NCF}$ form is isomorphic to a $\mathbf{CsqF}$ form. Thus the corollary’s isomorphic equivalence strengthens the KL16 equivalence by introducing isomorphisms.

There are further senses in which the corollary’s isomorphic equivalence accords with the KL16 equivalence. In the backward direction, KL16 Theorem 2 is appealing because the nodes in the constructed KS form are identical to the sequences in the given OR form. This is possible because KS nodes admit OR sequences as special cases. Nonetheless KL16 Theorem 2 is nontrivial because KS forms do not admit OR forms as special cases. Here the analogous result is cleaner: $\mathbf{NCF}$ forms have been defined so that $\mathbf{NCF}$ forms admit $\mathbf{CsqF}$ forms as special cases. In the forward direction, KL16 Theorem 1 is made appealing by KL16 Lemma 2, which shows that there is a bijection $α$ from the “vertex histories” in the given KS form to the nodes in the constructed OR form. That bijection is closely related to Theorem 3.2’s bijection $\bar{τ}$, which maps from the nodes of the given $\mathbf{NCF}$ form to the nodes in the constructed $\mathbf{CsqF}$ form.

3.3.

More about No-absentmindedness

3.3.1. Proposition 3.4 describes a general situation in which one subcategory strictly isomorphically encloses another. In the proposition, $w$ and $s$ are two properties defined for the objects of $\mathbf{Z}$. Further, $w⋅{⇐}\mspace{0.0mu}{\not\mspace{-5.0mu}{⇒}}⋅s$ means that $w$ is strictly weaker than $s$. In other words, $w⋅{⇐}\mspace{0.0mu}{\not\mspace{-5.0mu}{⇒}}⋅s$ means that [a] each object of $\mathbf{Z}$ satisfies $w$ if it satisfies $s$, and [b] there is an object of $\mathbf{Z}$ that satisfies $w$ but not $s$. Corollary 3.5 applies Proposition 3.4 to the nonvacuous property of no-absentmindedness.

Proposition 3.4**.**

Suppose $w$ and $s$ are properties defined for the objects of $\mathbf{Z}$, and that $s$ is isomorphically invariant. Let $\mathbf{Z_{w}}$ be the full subcategory of $\mathbf{Z}$ whose objects satisfy $w$, and let $\mathbf{Z_{s}}$ be the full subcategory of $\mathbf{Z}$ whose objects satisfy $s$. Then $w⋅{⇐}\mspace{0.0mu}{\not\mspace{-5.0mu}{⇒}}⋅s$ implies $\mathbf{Z_{w}}$ {\text{\@text@daccent{←}}}\mspace{0.0mu}{{\not\mspace{-5.0mu}{\text{\@text@daccent{→}}}}} $\mathbf{Z_{s}}$. (Proof here.)

Proof*.*

Suppose $w⋅{⇐}\mspace{0.0mu}{\not\mspace{-5.0mu}{⇒}}⋅s$. To see $\mathbf{Z_{w}}$ ̣\textleftarrow $\mathbf{Z_{s}}$, take an object of $\mathbf{Z_{s}}$. Since $w⋅⇐⋅s$, the object is also an object of $\mathbf{Z_{w}}$. Thus (trivially) the object is isomorphic to an object of $\mathbf{Z_{w}}$. To see $\mathbf{Z_{w}}$ {{\not\mspace{-5.0mu}{\text{\@text@daccent{→}}}}} $\mathbf{Z_{s}}$, note the assumption $w⋅{⇐}\mspace{0.0mu}{\not\mspace{-5.0mu}{⇒}}⋅s$ implies that there is an object of $\mathbf{Z}$ that satisfies $w$ and violates $s$. Thus there is an object of $\mathbf{Z_{w}}$ that violates $s$. Thus since $s$ is isomorphically invariant, this object does not have an isomorph that satisfies $s$. Thus the object does not have an isomorph in $\mathbf{Z_{s}}$. $\Box$

Corollary 3.5**.**

(a) $\mathbf{NCP}$ {\text{\@text@daccent{←}}}\mspace{0.0mu}{{\not\mspace{-5.0mu}{\text{\@text@daccent{→}}}}} $\mathbf{NCP_{\tilde{a}}}$. (b) $\mathbf{NCF}$ {\text{\@text@daccent{←}}}\mspace{0.0mu}{{\not\mspace{-5.0mu}{\text{\@text@daccent{→}}}}} $\mathbf{NCF_{\tilde{a}}}$. (Proof here.)

Proof*.*

(a). Consider Proposition 3.4 at $\mathbf{Z}$ equal to $\mathbf{NCP}$, when $w$ is the vacuous property satisfied by all objects of $\mathbf{NCP}$, and $s$ is the property of no-absentmindedness. No-absentmindedness is invariant by Proposition 2.8(a). Further the vacuous property is strictly weaker than no-absentmindedness because there exists an absentminded preform (recall note 15). Thus Proposition 3.4 implies that $\mathbf{NCP_{w}}$ = $\mathbf{NCP}$ strictly isomorphically encloses $\mathbf{NCP_{s}}$ = $\mathbf{NCP_{\tilde{a}}}$. (b). This is very similar to (a). Change “preform” to “form”, $\mathbf{P}$ to $\mathbf{F}$, and (a) to (b). $\Box$

To better interpret Corollary 3.5, recall Theorem 3.2(b) which states $\mathbf{NCF}$ ̣\textrightarrow $\mathbf{CsqF}$. Formally, this means each $\mathbf{NCF}$ form is isomorphic to a $\mathbf{CsqF}$ form. This can be interpreted to mean that the property of having choice-sequence nodes is not “restrictive”. In contrast, Corollary 3.5(b) implies $\mathbf{NCF}$ \not\mspace{-5.0mu}{\text{\@text@daccent{→}}} $\mathbf{NCF_{\tilde{a}}}$. Formally, this means there is at least one $\mathbf{NCF}$ form (such as the one in note 15) that is not isomorphic to an $\mathbf{NCF_{\tilde{a}}}$ form. This can be interpreted to mean that the property of no-absentmindedness is “restrictive”. Informally, the first result states that choice-sequence-ness is “purely notational”. In contrast, the second result states that no-absentmindedness is “substantial”, “significant”, and “real”, and that it “limits the range of decision processes and social interactions that can be modelled”. The categorical concept of isomorphic enclosure (̣\textrightarrow) serves to formalize and to standardize these important terms. Note that both an isomorphic enclosure, and the negation of an isomorphic enclosure, are meaningful.

3.3.2. Next, Proposition 3.6 shows that an isomorphic enclosure can be restricted by any isomorphically invariant property. Corollary 3.7 uses this result to restrict Corollary 3.3 by no-absentmindedness. Corollary 3.7 will in turn be used in the remarkably quick proof of Corollary 4.3.

Proposition 3.6**.**

Suppose that $\mathbf{A}$ and $\mathbf{B}$ are full subcategories of $\mathbf{Z}$, and that $w$ is an isomorphically invariant property defined for the objects of $\mathbf{Z}$. Let $\mathbf{A_{w}}$ be the full subcategory of $\mathbf{A}$ whose objects satisfy $w$, and let $\mathbf{B_{w}}$ be the full subcategory of $\mathbf{B}$ whose objects satisfy $w$. Then $\mathbf{A}$ ̣\textrightarrow $\mathbf{B}$ implies $\mathbf{A_{w}}$ ̣\textrightarrow $\mathbf{B_{w}}$. (Proof here.)

Proof*.*

Suppose $\mathbf{A}$ ̣\textrightarrow $\mathbf{B}$. To show $\mathbf{A_{w}}$ ̣\textrightarrow $\mathbf{B_{w}}$, take an object of $\mathbf{A_{w}}$. Then [1] the object is an object of $\mathbf{A}$ and [2] the object satisfies $w$. By [1] and $\mathbf{A}$ ̣\textrightarrow $\mathbf{B}$, the object has an isomorph in $\mathbf{B}$. By [2] and the isomorphic invariance of $w$, the isomorph satisfies $w$. The conclusions of the previous two sentences imply that the isomorph is in $\mathbf{B_{w}}$. $\Box$

Corollary 3.7**.**

(a) $\mathbf{NCP_{\tilde{a}}}$ ̣⟷ $\mathbf{CsqP_{\tilde{a}}}$. (b) $\mathbf{NCF_{\tilde{a}}}$ ̣⟷ $\mathbf{CsqF_{\tilde{a}}}$. (Proof here.)

Proof*.*

(a) follows from Corollary 3.3(a), Proposition 3.6, and Proposition 2.8(a). (b) is very similar to (a). Just change (a) to (b). $\Box$

3.3.3. Finally, Corollary 3.8 could be proved by mimicking the proof of Corollary 3.5, in which case Proposition 3.4 would be employed once for part (a) at $\mathbf{Z}$ = $\mathbf{CsqP}$, and again for part (b) at $\mathbf{Z}$ = $\mathbf{CsqF}$. Instead, Corollary 3.8 is proved by composing isomorphic enclosures (note 19), and the proof of the corollary’s part (b) is illustrated by Figure 3.2. Both proof techniques are straightforward, and a more interesting example of composition will soon appear in the proof of Corollary 4.3.

Corollary 3.8**.**

(a) $\mathbf{CsqP}$ {\text{\@text@daccent{←}}}\mspace{0.0mu}{{\not\mspace{-5.0mu}{\text{\@text@daccent{→}}}}} $\mathbf{CsqP_{\tilde{a}}}$. (b) $\mathbf{CsqF}$ {\text{\@text@daccent{←}}}\mspace{0.0mu}{{\not\mspace{-5.0mu}{\text{\@text@daccent{→}}}}} $\mathbf{CsqF_{\tilde{a}}}$. (Proof here.)

Proof*.*

(a). This is very similar to (b). Change $\mathbf{F}$ to $\mathbf{P}$, and (b) to (a). (b). To see $\mathbf{CsqF}$ ̣\textleftarrow $\mathbf{CsqF_{\tilde{a}}}$, note that $\mathbf{CsqF}$ ̣\textleftarrow $\mathbf{NCF}$ ̣\textleftarrow $\mathbf{NCF_{\tilde{a}}}$ ̣\textleftarrow $\mathbf{CsqF_{\tilde{a}}}$ by, respectively, Corollary 3.3(b), Corollary 3.5(b), and Corollary 3.7(b). To see $\mathbf{CsqF}$ {\not\mspace{-5.0mu}{\text{\@text@daccent{→}}}} $\mathbf{CsqF_{\tilde{a}}}$, suppose it were. Then $\mathbf{NCF}$ ̣\textrightarrow $\mathbf{CsqF}$ ̣\textrightarrow $\mathbf{CsqF_{\tilde{a}}}$ ̣\textrightarrow $\mathbf{NCF_{\tilde{a}}}$ by, respectively, Corollary 3.3(b), the supposition of the previous sentence, and Corollary 3.7(b). This contradicts Corollary 3.5(b), which states that $\mathbf{NCF}$ {\not\mspace{-5.0mu}{\text{\@text@daccent{→}}}} $\mathbf{NCF_{\tilde{a}}}$. $\Box$

4. The Subcategory of Choice-Set Forms

4.1.

Objects

Let a choice-set $\mathbf{NCP}$ preform be an $\mathbf{NCP}$ preform $(T,C,⊗)$ such that

[TABLE]

Then let $\mathbf{CsetP}$ be the full subcategory of $\mathbf{NCP}$ whose objects are choice-set $\mathbf{NCP}$ preforms. Proposition 4.1 lists some of the special properties of $\mathbf{CsetP}$ preforms.232323Almost every $\mathbf{CsetP}$ property in Proposition 4.1 has a $\mathbf{CsqP}$ analog in Proposition 3.1. The properties are merely presented in different orders because they are proved in different orders. The exceptions are that properties (g)–(i) have no $\mathbf{CsqP}$ analogs in Proposition 3.1. Incidentally, property (f) and assumption [Cset1] together imply that each node in a $\mathbf{CsetP}$ preform is actually a choice set, in accord with the terminology. More significantly, property (g) shows that every $\mathbf{CsetP}$ preform has no-absentmindedness. In this sense the combination of [Cset1] and [Cset2] is restrictive.

Proposition 4.1**.**

Suppose $(T,C,⊗)$ is a $\mathbf{CsetP}$ preform with its $F$, $t^{o}$, $p$, $q$, $k$, $≺$, $≼$, and ${\mathcal{H}}$. Then the following hold.

• (a)

$t^{o}=⎨⎬$.

• (b)

$(∀t^{\sharp}∈T⧷⎨⎨⎬⎬)$* $q(t^{\sharp})⋅∉⋅p(t^{\sharp})$ and $p(t^{\sharp})∪⎨q(t^{\sharp})⎬=t^{\sharp}$.*

• (c)

$(∀t∈T)$* $k(t)=|t|$.*

• (d)

$(∀t∈T,m∈⎨0,1,...\,|t|⎬)$* $p^{m}(t)\,⊆\,t$ and $t⧷p^{m}(t)$ $=$ $⎨\,q○p^{n}(t)\,|\,\!$ $m{>}n≥0\,⎬$.*

• (e)

$(∀t∈T)⋅t=⎨\,q○p^{n}(t)\,|\,|t|{>}n≥0\,⎬$.

• (f)

$C=∪T$.

• (g)

$(T,C,⊗)$* has no-absentmindedness.*

• (h)

$(∀t∈T,H∈{\mathcal{H}})$* $|t∩F(H)|⋅≤⋅1$.*

• (i)

$(∀t^{A}∈T,t^{B}∈T)$* $t^{A}⋅⊆⋅t^{B}$ implies $t^{A}=p^{|t^{B}|-|t^{A}|}(t^{B})$.*

• (j)

$(∀t^{A}∈T,t^{B}∈T)⋅t^{A}⋅≺⋅t^{B}$* iff $t^{A}⋅⊊⋅t^{B}$.*

• (k)

$(∀t^{A}∈T,t^{B}∈T)⋅t^{A}⋅≼⋅t^{B}$* iff $t^{A}⋅⊆⋅t^{B}$.*

• (l)

$⊗\mspace{1.0mu}^{\mathsf{gr}}=⎨⋅(t,c,t^{\sharp})∈T×C×T⋅|⋅c∉t,⋅t∪⎨c⎬{=}t^{\sharp}⋅⎬$*.*242424Lemma C.1 shows the following are equivalent: [a] $c∉t$ and $t∪⎨c⎬{=}t^{\sharp}$. [b] $t≠t^{\sharp}$ and $t∪⎨c⎬{=}t^{\sharp}$. [c] $t≠t^{\sharp}$ and $t{=}t^{\sharp}⧷⎨c⎬$. [d] $t⊆t^{\sharp}$ and $⎨c⎬{=}t^{\sharp}⧷t$.

• (m)

$F\mspace{1.0mu}^{\mathsf{gr}}=⎨⋅(t,c)∈T×C⋅|⋅c∉t,⋅t∪⎨c⎬∈T⋅⎬$. (Proof C.2.)

Finally, let a choice-set $\mathbf{NCF}$ form be an $\mathbf{NCF}$ form whose preform is a $\mathbf{CsetP}$ preform. Then let $\mathbf{CsetF}$ be the full subcategory of $\mathbf{NCF}$ whose objects are choice-set $\mathbf{NCF}$ forms.

4.2.

Isomorphic Enclosure

Theorem 4.2**.**

(a) $\mathbf{CsqP_{\tilde{a}}}$ ̣\textrightarrow $\mathbf{CsetP}$. In particular, suppose $\bar{Π}=(\bar{T},\bar{C},\bar{⊗})$ is a $\mathbf{CsqP_{\tilde{a}}}$ preform. Define $T=R(\bar{T})$, and define $⊗$ by surjectivity and $⊗\mspace{1.0mu}^{\mathsf{gr}}=⎨\,(R(\bar{t}),\bar{c},R(\bar{t}^{\sharp}))\,|\,(\bar{t},\bar{c},\bar{t}^{\sharp})∈\bar{⊗}\mspace{1.0mu}^{\mathsf{gr}}\,⎬$. Then $Π=(T,\bar{C},⊗)$ is a $\mathbf{CsetP}$ preform, $R|_{\bar{T}}$ is a bijection, and $[\bar{Π},Π,R|_{\bar{T}},\mathsf{id}_{\bar{C}}]$ is an $\mathbf{NCP}$ isomorphism. (b) $\mathbf{CsqF_{\tilde{a}}}$ ̣\textrightarrow $\mathbf{CsetF}$. In particular, suppose $\bar{Φ}=({\bar{I}},\bar{T},(\bar{C}_{\bar{i}})_{{\bar{i}}∈{\bar{I}}},\bar{⊗})$ is a $\mathbf{CsqF_{\tilde{a}}}$ form. Define $T$ and $⊗$ as in part (a). Then $Φ=({\bar{I}},T,(\bar{C}_{\bar{i}})_{{\bar{i}}∈{\bar{I}}},⊗)$ is a $\mathbf{CsetF}$ form and $[\bar{Φ},Φ,\mathsf{id}_{\bar{I}},R|_{\bar{T}},\mathsf{id}_{∪_{{\bar{i}}∈{\bar{I}}}\bar{C}_{\bar{i}}}]$ is an $\mathbf{NCF}$ isomorphism. (Proof C.3.)

Corollary 4.3**.**

(a) $\mathbf{CsqP_{\tilde{a}}}$ ̣⟷ $\mathbf{CsetP}$. (b) $\mathbf{CsqF_{\tilde{a}}}$ ̣⟷ $\mathbf{CsetF}$. (Proof here.)

Proof*.*

(a). This is very similar to (b). Change “form” to “preform”, $\mathbf{F}$ to $\mathbf{P}$, (b) to (a), and the last phrase to “because it has no-absentmindedness by Proposition 4.1(g)”.

(b). Theorem 4.2(b) shows $\mathbf{CsqF_{\tilde{a}}}$ ̣\textrightarrow $\mathbf{CsetF}$. Thus it remains to show $\mathbf{CsqF_{\tilde{a}}}$ ̣\textleftarrow $\mathbf{CsetF}$. Since isomorphic enclosures can be composed, it suffices to show [1] $\mathbf{CsetF}$ ̣\textrightarrow $\mathbf{NCF_{\tilde{a}}}$ and [2] $\mathbf{NCF_{\tilde{a}}}$ ̣\textrightarrow $\mathbf{CsqF_{\tilde{a}}}$. [2] is the forward direction of Corollary 3.7(b). [1] holds simply because any $\mathbf{CsetF}$ form is a $\mathbf{NCF_{\tilde{a}}}$ form. To see this, take a $\mathbf{CsetF}$ form. It is an $\mathbf{NCF}$ form by construction. It has no-absentmindedness because its preform has no-absentmindedness by Proposition 4.1(g). $\Box$

Corollary 4.3(b) is analogous to an ad hoc style equivalence in SE. There, a pair of results argues that no-absentminded OR forms (“OR$\bar{\text{a}}$ forms” in this subsection) are equivalent to SE-choice-set forms (“SEcs forms” in this subsection). One of the results (SE Theorem 3.2) shows that an OR$\bar{\text{a}}$ form can be reasonably derived from each SEcs form, and the other result (SE Theorem 3.1) shows that each OR$\bar{\text{a}}$ form can be reasonably mapped to an SEcs form. These two theorems are depicted by the two dashed arrows in Figure 4.1(a).

Corollary 4.3(b) strengthens this equivalence. $\mathbf{CsqF_{\tilde{a}}}$ forms are like OR$\bar{\text{a}}$ forms in that both specify nodes as choice-sequences, and $\mathbf{CsetF}$ forms are like SEcs forms in that both specify nodes as choice-sets. Then, Corollary 4.3(b)’s isomorphic equivalence is a matching pair of results: one half (labelled “easy” in Figure 4.1(b)) shows that a $\mathbf{CsqF_{\tilde{a}}}$ form is isomorphic to each $\mathbf{CsetF}$ form, while the other half (Theorem 4.2) shows that each $\mathbf{CsqF_{\tilde{a}}}$ form is isomorphic to a $\mathbf{CsetF}$ form. Thus Corollary 4.3(b) strengthens the SE equivalence by introducing isomorphisms.252525There is also another sense in which Corollary 4.3(b) accords with the SE equivalence. The forward half of the corollary is Theorem 4.2, and that theorem transforms choice-sequence nodes to choice-set nodes via the bijection $R|_{\bar{T}}$. That same bijection is used in SE Theorem 3.1.

Corollary 4.3(b)’s proof highlights how useful it is to compose isomorphic enclosures. In particular, consider the reverse direction of Corollary 4.3(b), which is $\mathbf{CsqF_{\tilde{a}}}$ ̣\textleftarrow $\mathbf{CsetF}$ in Figure 4.1(b), and compare it with SE Theorem 3.2, which is OR$\bar{\text{a}}$ $\dashleftarrow$ SEcs in Figure 4.1(a). The lemmas and proof for SE Theorem 3.2 span six difficult pages. In contrast, the reverse direction of Corollary 4.3(b) is proved in six lines by composing an easily-proved enclosure ($\mathbf{CsetF}$ ̣\textrightarrow $\mathbf{NCF_{\tilde{a}}}$ in part [1] of proof) with a previously-proved enclosure ($\mathbf{NCF_{\tilde{a}}}$ ̣\textrightarrow $\mathbf{CsqF_{\tilde{a}}}$ from the forward half of Corollary 3.7(b)). Figure 4.1(b) shows this composition as the curved arrow followed by the forward direction of Corollary 3.7(b).

4.3.

More about Perfect-Information

Corollaries 4.4 and 4.5 are additional applications of Section 3.3’s general propositions using isomorphic invariance.

Corollary 4.4**.**

(a) $\mathbf{NCP_{\tilde{a}}}$ {\text{\@text@daccent{←}}}\mspace{0.0mu}{{\not\mspace{-5.0mu}{\text{\@text@daccent{→}}}}} $\mathbf{NCP_{p}}$. (b) $\mathbf{NCF_{\tilde{a}}}$ {\text{\@text@daccent{←}}}\mspace{0.0mu}{{\not\mspace{-5.0mu}{\text{\@text@daccent{→}}}}} $\mathbf{NCF_{p}}$. (Proof here.)

Proof*.*

(a). Consider Proposition 3.4 at $\mathbf{Z}$ equal to $\mathbf{NCP}$, when $w$ is the property of no-absentmindedness ${\tilde{a}}$, and $s$ is the property of perfect-information $p$. Perfect-information is isomorphically invariant by Proposition 2.9(a). Further no-absentmindedness is strictly weaker than perfect-information by notes 16 and 17. Thus Proposition 3.4 implies that $\mathbf{NCP_{\tilde{a}}}$ strictly isomorphically encloses $\mathbf{NCP_{p}}$. (b). This is very similar to (a). Change $\mathbf{P}$ to $\mathbf{F}$, and (a) to (b). $\Box$

Corollary 4.5**.**

(a) $\mathbf{NCP_{p}}$ ̣⟷ $\mathbf{CsqP_{p}}$ ̣⟷ $\mathbf{CsetP_{p}}$. (b) $\mathbf{NCF_{p}}$ ̣⟷ $\mathbf{CsqF_{p}}$ ̣⟷ $\mathbf{CsetF_{p}}$. (Proof here.)

Proof*.*

(a). Corollary 3.7(a) and Corollary 4.3(a) imply $\mathbf{NCP_{\tilde{a}}}$ ̣⟷ $\mathbf{CsqP_{\tilde{a}}}$ ̣⟷ $\mathbf{CsetP}$. Thus, Propositions 3.6 and 2.9(a) imply that $\mathbf{NCP_{{\tilde{a}}p}}$ ̣⟷ $\mathbf{CsqP_{{\tilde{a}}p}}$ ̣⟷ $\mathbf{CsetP_{p}}$, where $\mathbf{NCP_{{\tilde{a}}p}}$ is the full subcategory of $\mathbf{NCP}$ consisting of those objects that satisfy both no-absentmindedness and perfect-information, and where similarly $\mathbf{CsqP_{{\tilde{a}}p}}$ is the full subcategory of $\mathbf{CsqP}$ consisting of those objects that satisfy both no-absentmindedness and perfect-information. Since no-absentmindedness is weaker than perfect-information (note 16), $\mathbf{NCP_{{\tilde{a}}p}}$ = $\mathbf{NCP_{p}}$ and $\mathbf{CsqP_{{\tilde{a}}p}}$ = $\mathbf{CsqP_{p}}$. (b). This is very similar to (a). Change $\mathbf{P}$ to $\mathbf{F}$, and (a) to (b). $\Box$

Incidentally, since isomorphic equivalence implies categorical equivalence, Corollary 4.5(a) implies $\mathbf{NCP_{p}}$, $\mathbf{CsqP_{p}}$, and $\mathbf{CsetP_{p}}$ are categorically equivalent. Further, SP Theorem 3.13 and Corollary 3.14 show that $\mathbf{NCP_{p}}$, $\mathbf{Tree}$, and $\mathbf{Grph_{ca}}$ are categorically equivalent, where $\mathbf{Tree}$ is the category of functioned trees which SP uses in its development of $\mathbf{NCP}$, and where $\mathbf{Grph_{ca}}$ is the full subcategory of $\mathbf{Grph}$ whose objects are converging arborescences. Thus, $\mathbf{NCP_{p}}$, $\mathbf{CsqP_{p}}$, $\mathbf{CsetP_{p}}$, $\mathbf{Tree}$, and $\mathbf{Grph_{ca}}$ are categorically equivalent.

Figure 4.2’s arrow diagram illustrates most of the isomorphic-enclosure results from Sections 3.2 and following. In addition, the diagram has some unlabelled arrows. They are derived by composing arrows as in the proof of Corollary 3.8. Many diagonal arrows could be similarly derived.

5. Further Remarks

5.1.

Deducing consequences from an isomorphic enclosure

Consider this paper’s first isomorphic enclosure. Theorem 3.2 shows that each $\mathbf{NCF}$ form $Φ$ is isomorphic to a $\mathbf{CsqF}$ form $\bar{Φ}$ by means of an isomorphism which transforms nodes via the bijection $\bar{τ}$. Proposition 2.6 deduces many consequences from such an isomorphism. For example, its part (o) implies that $(∀t^{1}∈T,t^{2}∈T)$ $t^{1}⋅≺⋅t^{2}$ iff $\bar{τ}(t^{1})⋅\bar{≺}⋅\bar{τ}(t^{2})$, where $T$ is the node set of $Φ$, $≺$ is derived from $Φ$, and $\bar{≺}$ is derived from $\bar{Φ}$. Although such consequences about form derivatives like $≺$ and $\bar{≺}$ are tantalizingly natural, the consequences about form derivatives in Proposition 2.6(f)–(r) take about 10 pages to prove. That work is important because such consequences are fundamental to drawing more conclusions from the isomorphic enclosure of $\mathbf{NCF}$ in $\mathbf{CsqF}$.

As Section 3.2 explained, the isomorphic enclosure of $\mathbf{NCF}$ in $\mathbf{CsqF}$ is analogous to KL16 Theorem 1. No consequences about form derivatives have been deduced from that ad hoc theorem, and an analog of Proposition 2.6(f)–(r) would likely require about 10 pages to prove. Moreover, like KL16 Theorem 1, no consequences about form derivatives have been deduced from KL16 Theorem 2 or from SE Theorems 3.1 and 3.2. Each of these ad hoc theorems has its own formulation, so deriving analogs of Proposition 2.6(f)–(r) for the three of them would likely require another $3×10=30$ pages.

In contrast, Proposition 2.6(f)–(r) applies not only to the isomorphic enclosure of $\mathbf{NCF}$ in $\mathbf{CsqF}$. It applies to any isomorphic enclosure. Thus it applies to all the arrows in Figure 4.2, as well as to all isomorphic enclosures in the future.

5.2.

Future research

As discussed in Section 1.2, this paper is part of a larger agenda to translate game theory across specification styles. In this larger context, isomorphic enclosures can be seen as a way to translate form components from one style to another, and on the basis of these isomorphic enclosures, Proposition 2.6(f)–(r) (discussed just above) can be seen as a way of translating form derivatives from one style to another.

The  5. Further Remarksresults of this paper wait to be expanded in three orthogonal directions.

[1] There is more to translate beyond forms and their derivatives. This would include properties that forms might satisfy, and theorems that might relate these properties to one another. (This paper makes some limited progress in this direction by exploring the isomorphically invariant properties of no-absentmindedness and perfect-information, and by identifying some special properties of $\mathbf{CsqF}$ forms and $\mathbf{CsetF}$ forms via Propositions 3.1 and 4.1.) Expanding in this direction would correspond to expanding the three substantive sections of this paper.

[2] This paper concerns only three styles: $\mathbf{NCF}$, $\mathbf{CsqF}$, and $\mathbf{CsetF}$. There are other styles to explore, including the two neglected styles mentioned at the start of this paper, namely, the “node-set” style of Alós-Ferrer and Ritzberger 2016 Section 6.3, and the “outcome-set” style of von Neumann and Morgenstern 1944 and Alós-Ferrer and Ritzberger 2016 Section 6.2. Expanding in this direction will require defining new $\mathbf{NCF}$ subcategories for “node-set” forms and “outcome-set” forms, and will correspond to adding, to the present paper, two new sections for the two new subcategories.

[3] This paper concerns only forms, which need to be augmented with preferences in order to define games. At the higher level of games, many more issues emerge. To return to [1], there is more to translate, including equilibrium concepts and the theorems which might relate one equilibrium concept to another. To return to [2], there will be more than five styles because there are alternative ways to specify preferences over the same form. Expanding in this third direction will require building a new category for games that incorporates this paper’s category for forms.

Appendix A $\mathbf{NCF}$

Lemma A.1**.**

Suppose $(T,C,⊗)$ is an $\mathbf{NCP}$ preform with its $F$, $t^{o}$, $p$, $q$, and ${\mathcal{H}}$. Then the following hold.

• (a)

$|T|⋅≥⋅2$, $|C|⋅≥⋅1$, $|⊗\mspace{1.0mu}^{\mathsf{gr}}|⋅≥⋅1$.

• (b)

$(∀H∈{\mathcal{H}},c∈C)$* $c⋅∈⋅F(H)$ iff $F^{-1}(c)=H$.*

• (c)

$(∀H∈{\mathcal{H}},t^{\sharp}∈T⧷⎨t^{o}⎬)$* $q(t^{\sharp})⋅∈⋅F(H)$ iff $p(t^{\sharp})⋅∈⋅H$.*

Proof*.*

(a). In the paragraph after SP equation (1), remark [ii] shows that $(∄t∈T)$ $p(t)=t$. Thus, since $p$ is nonempty by [T1], there are distinct $t^{1}⋅∈⋅T$ and $t^{2}⋅∈⋅T$ such that $t^{1}=p(t^{2})$. Thus, by the definition of $p$ in [P2], there is $c⋅∈⋅C$ such that $(t^{1},c,t^{2})⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$.

(b). (Forward direction). Suppose

$[$a$]$ $c⋅∈⋅C$,

(2) $H⋅∈⋅{\mathcal{H}}$, and

(3) $c⋅∈⋅F(H)$. 3 implies there is

(4) $t⋅∈⋅H$ such that

(5) $c⋅∈⋅F(t)$. 5 implies

(6) $t⋅∈⋅F^{-1}(c)$. Meanwhile, $[$a$]$ and [P3] imply

(7) $F^{-1}(c)⋅∈⋅{\mathcal{H}}$. Since ${\mathcal{H}}$ is a partition by [P3], 2 and 7 imply $H$ and $F^{-1}(c)$ are elements of the same partition. Hence 4 and 6 imply $H=F^{-1}(c)$.

(Reverse direction). Suppose $c⋅∈⋅C$,

$[$a$]$ $H⋅∈⋅{\mathcal{H}}$, and

(2) $F^{-1}(c)=H$. Since $H$ belongs to a partition by $[$a$]$ and [P3], there is

(3) $t⋅∈⋅H$. 3 and 2 implies $t⋅∈⋅F^{-1}(c)$, which implies $c⋅∈⋅F(t)$. This and 3 imply $c⋅∈⋅F(H)$.

(c). (Forward direction). Suppose $H⋅∈⋅{\mathcal{H}}$,

$[$a$]$ $t^{\sharp}⋅∈⋅T⧷⎨t^{o}⎬$ and

(2) $q(t^{\sharp})⋅∈⋅F(H)$. 2 and the forward direction of part (b) imply

(3) $F^{-1}(q(t^{\sharp}))=H$. Meanwhile, $[$a$]$ and SP Proposition 3.1(b) imply $p(t^{\sharp})⊗q(t^{\sharp})=t^{\sharp}$. This and [P1] imply $(p(t^{\sharp}),q(t^{\sharp}))⋅∈⋅F\mspace{1.0mu}^{\mathsf{gr}}$. This implies $p(t^{\sharp})⋅∈⋅F^{-1}(q(t^{\sharp}))$, which equals $H$ by 3.

(Reverse direction). Suppose $H⋅∈⋅{\mathcal{H}}$,

$[$a$]$ $t^{\sharp}⋅∈⋅T⧷⎨t^{o}⎬$ and

(2) $p(t^{\sharp})⋅∈⋅H$. $[$a$]$ and SP Proposition 3.1(b) imply $p(t^{\sharp})⊗q(t^{\sharp})=t^{\sharp}$. This and [P1] imply $(p(t^{\sharp}),q(t^{\sharp}))$ $∈⋅F\mspace{1.0mu}^{\mathsf{gr}}$. This implies $q(t^{\sharp})⋅∈⋅F(p(t^{\sharp}))$. This and 2 imply $q(t^{\sharp})⋅∈⋅F(H)$. $\Box$

Lemma A.2**.**

262626This lemma excerpts parts of proofs from SP. In particular, the proof of part (a) rearranges part of SP Proof C.12’s argument for SP Proposition 3.5, and the proof of the part (b) rearranges part of the argument for SP Lemma C.17(e).

Suppose $α=[Π,Π′,τ,δ]$ is a preform morphism, where $Π=(T,C,⊗)$ determines $F$ and where $Π′=(T′,C′,⊗′)$ determines $F′$. Then the following hold. (a) $(∀c∈C)⋅τ(F^{-1}(c))⋅⊆⋅(F′)^{-1}(δ(c))$. (b) Suppose $α$ is an isomorphism. Then $(∀c∈C)⋅τ(F^{-1}(c))=(F′)^{-1}(δ(c))$.

Proof*.*

(a). Take $c$. I argue

[TABLE]

The first inclusion holds by (18a) of SP Lemma C.6. The second inclusion holds because $τ(T)⋅⊆⋅T′$ by [PM1]. The equalities are rearrangements.

(b). Take $c$. I argue

[TABLE]

The third equality holds by SP Proposition 3.8(c). The fifth holds because $τ$ is a bijection by SP Theorem 3.7 (second sentence). The remaining equalities are rearrangements. $\Box$

Proof A.3** (for Proposition 2.1).**

(a). First I show

$[$1$]$ $∪_{i∈I}X_{i}=X$ by arguing, in steps, that $∪_{i∈I}X_{i}$ by the definition of $(X_{i})_{i∈I}$ equals $∪_{i∈I}(∪_{c∈C_{i}}F^{-1}(c))$; which by rearrangement equals $∪_{c∈∪_{i∈I}C_{i}}F^{-1}(c)$; which by the definition of $C$ equals $∪_{c∈C}F^{-1}(c)$; which by definition equals $F^{-1}(C)$; which by definition (in Section 2.1) equals $X$. Thus it remains to show that $(∀i∈I,j∈I⧷⎨i⎬)$ $X_{i}∩X_{j}=∅$. Toward that end, suppose there are $i^{1}⋅∈⋅I$ and $i^{2}⋅∈⋅I$ such that

(2) $i^{1}⋅≠⋅i^{2}$ and $X_{i^{1}}∩X_{i^{2}}⋅≠⋅∅$. This nonemptiness and $[$1$]$ imply there is

(3) $t⋅∈⋅X$ such that

(4) $t⋅∈⋅X_{i^{1}}∩X_{i^{2}}$. 3 and [F3] imply there is $i^{*}⋅∈⋅I$ such that

(5) $F(t)⋅⊆⋅C_{i^{*}}$. 4 implies $t⋅∈⋅X_{i^{1}}$, which by the definition of $X_{i^{1}}$ implies there is [61] $c^{1}⋅∈⋅C_{i^{1}}$ such that $t⋅∈⋅F^{-1}(c^{1})$. The previous set membership is equivalent to [71] $c^{1}⋅∈⋅F(t)$. [71] and 5 imply $c^{1}⋅∈⋅C_{i^{*}}$, and thus [61] and [F2] imply [81] $i^{1}=i^{*}$. Similarly, 4 implies $t⋅∈⋅X_{i^{2}}$, which by the definition of $X_{i^{2}}$ implies there is [62] $c^{2}⋅∈⋅C_{i^{2}}$ such that $t⋅∈⋅F^{-1}(c^{2})$. The previous set membership is equivalent to [72] $c^{2}⋅∈⋅F(t)$. [72] and 5 imply $c^{2}⋅∈⋅C_{i^{*}}$, and thus [62] and [F2] imply [82] $i^{2}=i^{*}$. [81] and [82] imply $i^{1}=i^{2}$, which contradicts 2.

(b). Take $i$. First I show

$[$1$]$ ${\mathcal{H}}_{i}⋅⊆⋅{\mathcal{H}}$. I do this by arguing, in steps, that ${\mathcal{H}}_{i}$ by definition equals $⎨F^{-1}(c)|c∈C_{i}⎬$; which by the definition of $C$ is a subset of $⎨F^{-1}(c)|c∈C⎬$; which by definition (in [P3]) equals ${\mathcal{H}}$. Since ${\mathcal{H}}$ is a partition by [P3], $[$1$]$ implies that the elements of ${\mathcal{H}}_{i}$ are nonempty and disjoint. Thus it remains to show that $∪{\mathcal{H}}_{i}=X_{i}$. I argue, in steps, that $∪{\mathcal{H}}_{i}$ by the definition of ${\mathcal{H}}_{i}$ equals $∪⎨F^{-1}(c)|c∈C_{i}⎬$; which by the definition of $X_{i}$ equals $X_{i}$.

(c). First I show $∪_{i∈I}{\mathcal{H}}_{i}={\mathcal{H}}$. I do this by arguing, in steps, that $∪_{i∈I}{\mathcal{H}}_{i}$ by the definition of $({\mathcal{H}}_{i})_{i∈I}$ equals $∪_{i∈I}⎨F^{-1}(c)|c∈C_{i}⎬$; which by rearrangement equals $⎨F^{-1}(c)|c∈∪_{i∈I}C_{i}⎬$; which by the definition of $C$ equals $⎨F^{-1}(c)|c∈C⎬$; which by definition (in [P3]) equals ${\mathcal{H}}$. Thus it remains to show $(∀i∈I,j∈I⧷⎨i⎬)⋅{\mathcal{H}}_{i}∩{\mathcal{H}}_{j}⋅≠⋅∅$. Toward that end, suppose $i^{1}⋅∈⋅I$ and $i^{2}⋅∈⋅I$ satisfy

$[$1$]$ $i^{1}⋅≠⋅i^{2}$ and ${\mathcal{H}}_{i^{1}}∩{\mathcal{H}}_{i^{2}}⋅≠⋅∅$. This nonemptiness implies there is $H⋅∈⋅{\mathcal{H}}_{i^{1}}∩{\mathcal{H}}_{i^{2}}$. $H⋅∈⋅{\mathcal{H}}_{i^{1}}$ and part (b) implies $H$ is a nonempty subset of $X_{i^{1}}$. Similarly, $H⋅∈⋅{\mathcal{H}}_{i^{2}}$ and part (b) implies $H$ is a nonempty subset of $X_{i^{2}}$. The previous two sentences imply $X_{i^{1}}∩X_{x^{2}}⋅≠⋅∅$. Hence part (a) implies $i^{1}=i^{2}$, which contradicts $[$1$]$. $\Box$

Proof A.4** (for Proposition 2.2).**

The next two paragraphs prove the first paragraph of the proposition. In particular, the next two paragraphs show that $[Φ,Φ′,ι,τ,δ]$ is a morphism iff (a)–(e) hold.

Forward Direction. Assume $[Φ,Φ′,ι,τ,δ]$ is a morphism. Then [FM1] implies $[(T,C,⊗),(T′,C′,⊗′),τ,δ]$ is a preform morphism, so [PM1] implies (b), [PM2] implies (c), and [PM3] implies (e). Further, [FM2] implies (a), and [FM3] implies (d).

Reverse Direction. Assume (a)–(e). Since $Φ$ and $Φ′$ are forms by assumption, it suffices to show [FM1]–[FM3]. [FM3] holds by (d). [FM2] holds by (a). For [FM1], note that $Π$ and $Π′$ are preforms by [F1] and the assumption that $Φ$ and $Φ′$ are forms. Thus it suffices to show [PM1]–[PM3]. [PM1] holds by (b), [PM2] holds by (c), and [PM3] holds by (e).

Henceforth assume that $[Φ,Φ′,ι,τ,δ]$ is a morphism. The remaining two paragraphs of the proposition follow from Claims 1, 2, 4, and 5 below.

• Claim 1:

(k) holds. Take $i$. I argue, in steps, that $τ(X_{i})$ by definition equals $τ(∪_{c∈C_{i}}F^{-1}(c))$, which by rearrangement equals $∪⎨\,τ(F^{-1}(c))\,|$ $c∈C_{i}\,⎬$, which by Lemma A.2(a) is included in $∪⎨\,(F′)^{-1}(δ(c))\,|\,c∈C_{i}\,⎬$, which by rearrangement is $∪⎨\,(F′)^{-1}(c′)\,|\,c′∈δ(C_{i})\,⎬$, which by [FM3] is included in $∪⎨\,(F′)^{-1}(c′)\,|\,c′∈C′_{ι(i)}\,⎬$, which by definition is $X′_{ι(i)}$.

• Claim 2:

(m) holds. Take $i$ and $H⋅∈⋅{\mathcal{H}}_{i}$. By the definition of ${\mathcal{H}}_{i}$, there exists

$[$1$]$ $c⋅∈⋅C_{i}$ such that

(2) $H=F^{-1}(c)$. Let

(3) $H′=(F′)^{-1}(δ(c))$. $[$1$]$ and [FM3] imply $δ(c)⋅∈⋅C′_{ι(i)}$. Thus the definition of ${\mathcal{H}}′_{ι(i)}$ implies $(F′)^{-1}(δ(c))⋅∈⋅{\mathcal{H}}′_{ι(i)}$. This and 3 imply $H′⋅∈⋅{\mathcal{H}}′_{ι(i)}$. Thus it remains to show that $τ(H)⋅⊆⋅H′$. I argue, in steps, that $τ(H)$ by 2 equals $τ(F^{-1}(c))$, which by Lemma A.2(a) is included in $(F′)^{-1}(δ(c))$, which by 3 equals $H′$.

• Claim 3:

(a) $[Π,Π,τ,δ]$ is an $\mathbf{NCP}$ morphism. (b) $[(T,p),(T′,p′),τ]$ is a $\mathbf{Tree}$ morphism. (a) follows from [FM1]. For (b), note that (a) and SP Theorem 3.9 imply that $\mathsf{F_{1}}([Π,Π′,τ,δ])$ is a $\mathbf{Tree}$ morphism. By that theorem’s definition of $\mathsf{F}$, $\mathsf{F_{1}}([Π,Π′,τ,δ])=[\mathsf{F_{0}}(Π),\mathsf{F_{0}}(Π′),τ]=[(T,p),(T′,p′),τ]$.

• Claim 4:

(f), (h), (i), (j), and (l) hold. Because of Claim 3(a), these parts follow from various results in SP. In particular, (f) follows from SP Lemma C.6(18a). (h) follows from SP Lemma C.9(20a). (i) follows from SP Lemma C.9(20b). (j) follows from SP Proposition 3.4(22a) since Section 2.1 defines $X$ equal to $F^{-1}(C)$ and thus $X′$ equal to $(F′)^{-1}(C′)$. (l) follows from SP Proposition 3.5.

• Claim 5:

(g) and (n)–(r) hold. Because of Claim 3(b), these parts of the proposition follow from various parts of SP Proposition 2.4. In particular, (g) follows from SP Proposition 2.4(a). (n)–(p) follow from SP Proposition 2.4(c)–(e). (q) follows from SP Proposition 2.4(h). (r) follows from SP Proposition 2.4(g).

$\Box$

Proof A.5** (for Theorem 2.3).**

The next two paragraphs draw upon SP Theorem 3.6, which showed that $\mathbf{NCP}$ is a well-defined category.

This paragraph shows that, for each form $Φ$, $\mathsf{id}_{Φ}$ is a form morphism. Toward this end, take a form $Φ=[I,T,(C_{i})_{i∈I},⊗]$. By [F1], let $Π=(T,∪_{i∈I}C_{i},⊗)$ be its $\mathbf{NCP}$ preform. It must be shown that $\mathsf{id}_{Φ}=[Φ,Φ,\mathsf{id}_{T},\mathsf{id}_{I},\mathsf{id}_{∪_{i∈I}C_{i}}]$ satisfies [FM1]–[FM3]. [FM1] holds because $[Π,Π,\mathsf{id}_{T},\mathsf{id}_{∪_{i∈I}C_{i}}]$ is an $\mathbf{NCP}$ identity, and hence, an $\mathbf{NCP}$ morphism. [FM2] holds because $\mathsf{id}_{I}{:}I\textrightarrow I$. [FM3] holds because $(∀j∈I)$ $\mathsf{id}_{∪_{i∈I}C_{i}}(C_{j})=C_{j}=C_{\mathsf{id}_{I}(j)}$.

This paragraph shows that, for any two form morphisms $β$ and $β′$, $β′○β$ is a form morphism. Toward this end, take form morphisms $β=[Φ,Φ′,ι,τ,δ]$ and $β′=[Φ′,Φ″,ι′,τ′,δ′]$, where $Φ=(I,T,(C_{i})_{i∈I},⊗)$, $Φ′=(I′,T′,(C′_{i′})_{i′∈I′},⊗′)$, and $Φ″=(I″,T″,(C″_{i″})_{i″∈I″},⊗″)$. By [F1], let $Π$, $Π′$, and $Π″$ be the NCP preforms underlying $Φ$, $Φ′$, and $Φ″$. It must be shown that $β′○β=[Φ,Φ″,τ′○ι,τ′○ι,δ′○δ]$ satisfies [FM1]–[FM3]. For [FM1], it must be shown that the quadruple $[Π,Π″,τ′○τ,δ′○δ]$ is an $\mathbf{NCP}$ morphism. This holds because [a] the quadruple equals $[Π′,Π″,τ′,δ′]○$ $[Π,Π′,τ,δ]$ in $\mathbf{NCP}$, and because [b] $[Π,Π′,τ,δ]$ and $[Π′,Π″,τ′,δ′]$ are $\mathbf{NCP}$ morphisms by [FM1] for $β$ and $β′$. For [FM2], it must be shown that $ι′○ι{:}I\textrightarrow I″$. This holds because $ι{:}I\textrightarrow I′$ by [FM2] for $β$, and because $ι′{:}I′\textrightarrow I″$ by [FM2] for $β′$. For [FM3], it must be shown that $(∀i∈I)$ $(δ′○δ)(C_{i})⋅⊆⋅C″_{ι′○ι(i)}$. To prove this, take $i$. I argue $δ′(δ(C_{i}))$ $⊆$ $δ′(C′_{ι(i)})$ $⊆$ $C″_{ι′○ι(i)}$, where the first inclusion holds because $δ(C_{i})⋅⊆⋅C′_{ι(i)}$ by [FM3] for $β$, applied at $i$, and where the second inclusion holds by [FM3] for $β′$, applied at $i′=ι(i)$.

The previous two paragraphs have established the well-definition of identity and composition. The unit and associative laws are immediate. Thus $\mathbf{NCF}$ is a category (e.g. Mac Lane 1998, page 10). $\Box$

Lemma A.6**.**

*Suppose $[Φ,Φ′,ι,τ,δ]$ is a morphism, where $Φ=(I,T,(C_{i})_{i∈I},⊗)$ and $Φ′=(I′,T′,(C′_{i′})_{i′∈I′},⊗′)$. Further suppose that $ι$ and $δ$ are bijections. Then the following hold.

(a) $(∀i∈I)⋅δ|_{C_{i}}$ is a bijection from $C_{i}$ onto $C′_{ι(i)}$.

(b) $(∀i′∈I′)⋅δ^{-1}|_{C′_{i′}}$ is a bijection from $C′_{i′}$ onto $C_{ι^{-1}(i′)}$.*

Proof*.*

Define $C=∪_{i∈I}C_{i}$ and $C′=∪_{i′∈I′}C′_{i′}$. The lemma follows from Claims 3 and 4.

• Claim 1:

$δ$ is a bijection from $∪_{i∈I}C_{i}$ onto $∪_{i′∈I′}C′_{i′}$. [FM1] implies [PM2], which implies $δ$ is a function from $C$ to $C′$. Thus the definitions of $C$ and $C′$ imply $δ$ is a function from $∪_{i∈I}C_{i}$ to $∪_{i′∈I′}C′_{i′}$. $δ$ is a bijection by assumption.

• Claim 2:

$(∀i∈I)⋅δ(C_{i})=C′_{ι(i)}$. Take $i$. [FM3] implies $δ(C_{i})⋅⊆⋅C′_{ι(i)}$. Thus it remains to show that $C′_{ι(i)}⧷δ(C_{i})=∅$. Toward that end, suppose contrariwise there is $c′$ such that

$[$a$]$ $c′⋅∈⋅C′_{ι(i)}$ and

(2) $c′⋅∉⋅δ(C_{i})$. $[$a$]$ and Claim 1 implies that $δ^{-1}(c′)$ is a well-defined element of $∪_{k∈I}C_{k}$. Thus there is $j⋅∈⋅I$ such that $δ^{-1}(c′)⋅∈⋅C_{j}$. This implies

(3) $c′⋅∈⋅δ(C_{j})$. 3 and 2 imply

(4) $i⋅≠⋅j$. Also, 3 and [FM3] imply $c′⋅∈⋅C′_{ι(j)}$. This and $[$a$]$ imply

(5) $c′⋅∈⋅C′_{ι(i)}∩C′_{ι(j)}$. Meanwhile, 4 and the bijectivity of $ι$ imply

(6) $ι(i)⋅≠⋅ι(j)$. 5 and 6 contradict [F2] for $Φ′$.

• Claim 3:

(a) holds. This follows from the bijectivity of $δ$ and Claim 2.

• Claim 4:

(b) holds. Since $ι$ is bijective, it suffices to prove that $(∀i∈I)$ $δ^{-1}|_{C′_{ι(i)}}$ is a bijection from $C′_{ι(i)}$ onto $C_{i}$. By Claim 2, this is equivalent to proving that $(∀i∈I)$ $δ^{-1}|_{δ(C_{i})}$ is a bijection from $δ(C_{i})$ onto $C_{i}$. This follows from part (a).

$\Box$

Proof A.7** (for Theorem 2.4).**

Let the components of $Φ$ be $(I,T,(C_{i})_{i∈I},⊗)$, define $C=∪_{i}C_{i}$, let the components of $Φ′$ be $(I′,T′,(C′_{i′})_{i′∈I′},⊗′)$, and define $C′=∪_{i′}C′_{i′}$.

The forward half of (a) and all of (b). Suppose that $β$ is an isomorphism (Awodey 2010, page 12, Definition 1.3). Recall that $β=[Φ,Φ′,ι,τ,δ]$ and let $β^{-1}=[Φ^{*},Φ^{**},ι^{*},τ^{*},δ^{*}]$. Then

⋅

$[$1$]$

$[Φ^{*},Φ^{**},ι^{*},τ^{*},δ^{*}]○[Φ,Φ′,ι,τ,δ]=\mathsf{id}_{Φ}=[Φ,Φ,\mathsf{id}_{I},\mathsf{id}_{T},\mathsf{id}_{C}]$ and

(2)

$[Φ,Φ′,ι,τ,δ]○[Φ^{*},Φ^{**},ι^{*},τ^{*},δ^{*}]=\mathsf{id}_{Φ′}=[Φ′,Φ′,\mathsf{id}_{I′},\mathsf{id}_{T′},\mathsf{id}_{C′}]$,

⋅

where the first equality in both lines holds by the definition of $β^{-1}$, and the second equality in both lines holds by the definition of $\mathsf{id}$. The well definition of $○$ in $[$1$]$ implies

$[$a$]$

$Φ^{*}=Φ′$. Analogously, the well definition of $○$ in 2 implies

(2) $Φ^{**}=Φ$. The third component of $[$1$]$ implies $ι^{*}○ι=\mathsf{id}_{I}$, and the third component of 2 implies $ι○ι^{*}=\mathsf{id}_{I′}$. Thus $ι$ is a bijection from $I$ onto $I′$ and

(3) $ι^{*}=ι^{-1}$. Similarly, the fourth components of $[$1$]$ and 2 imply $τ$ is a bijection from $T$ onto $T′$ and

(4) $τ^{*}=τ^{-1}$. Similarly again, the fifth components of $[$1$]$ and 2 imply $δ$ is a bijection from $C$ onto $C′$ and

(5) $δ^{*}=δ^{-1}$. To conclude, the previous three sentences have shown that $ι$, $τ$, and $δ$ are bijections. Further,

[TABLE]

where the first equality follows from the definition of $β^{-1}$, and where the second equality follows from $[$a$]$–5.

The reverse half of (a). Suppose that $ι$, $τ$, and $δ$ are bijections. Define $β^{*}=[Φ′,Φ,ι^{-1},τ^{-1},δ^{-1}]$. Derive $Π$ from $Φ$ and $Π′$ from $Φ′$. The remainder of this paragraph will show that $β^{*}$ is a form morphism by showing that it satisfies

[TABLE]

To see [FM1$′$], first note that $[Π,Π′,τ,δ]$ is a preform morphism by [FM1] for $β$. Thus the bijectivity of $τ$ and $δ$, together with SP Theorem 3.7(a), imply that $[Π′,Π,τ^{-1},δ^{-1}]$ is an $\mathbf{NCP}$ isomorphism. Hence a fortiori, it is a preform morphism. To see [FM2$′$], first note that $ι{:}I\textrightarrow I′$ by [FM2] for $β$. Thus the bijectivity of $ι$ implies that $ι^{-1}{:}I′\textrightarrow I$. Finally, to see [FM3$′$], consider Lemma A.6. The lemma’s assumptions are met because the theorem assumes that $β=[Φ,Φ′,ι,τ,δ]$ is a morphism and because the start of this paragraph assumes that $ι$ and $δ$ are bijections. Thus the lemma’s part (b) implies that $(∀i′∈I′)$ $δ^{-1}(C′_{i′})=C_{ι^{-1}(i′)}$.

To conclude, $β^{*}$ is a form morphism by the previous paragraph. Further,

[TABLE]

Hence $β$ is an isomorphism (and incidentally, $β^{-1}=β^{*}$). $\Box$

Lemma A.8**.**

Suppose $[Φ,Φ′,ι,τ,δ]$ is a morphism, where $Φ=$ $(I,T,(C_{i})_{i∈I},⊗)$ determines $({\mathcal{H}}_{i})_{i∈I}$, and where $Φ′=(I′,T′,(C′_{i′})_{i′∈I′},⊗′)$ determines $({\mathcal{H}}′_{i′})_{i′∈I′}$. Further suppose that $[Π,Π′,τ,δ]$ is an isomorphism, where $Π=(T,C,⊗)$, $C=∪_{i∈I}C_{i}$, $Π′=(T′,C′,⊗′)$, and $C′=∪_{i′∈I′}C′_{i′}$. Then $(∀i∈I,H∈{\mathcal{H}}_{i})⋅τ(H)⋅∈⋅{\mathcal{H}}′_{ι(i)}$.

Proof*.*

Derive $F$ from $Π$, and $F′$ from $Π′$. Since $[Π,Π′,τ,δ]$ is an isomorphism, Lemma A.2(b) implies

$[$1$]$ $(∀c∈C)$ $τ(F^{-1}(c))=(F′)^{-1}(δ(c))$.

Now take $i$ and $H⋅∈⋅{\mathcal{H}}_{i}$. Then there is

(2) $c^{*}⋅∈⋅C_{i}$ such that

(3) $H=F^{-1}(c^{*})$. First I show

(4) $δ(c^{*})⋅∈⋅C′_{ι(i)}$ by arguing, in steps, that $δ(c^{*})$ by 2 belongs to $δ(C_{i})$, which by [FM3] is included in $C′_{ι(i)}$. Finally, I argue, in steps, that $τ(H)$ by 3 equals $τ(F^{-1}(c^{*}))$, which by $[$1$]$ equals $(F′)^{-1}(δ(c^{*}))$, which by 4 belongs to ${\mathcal{H}}′_{ι(i)}$. $\Box$

Proof A.9** (for Proposition 2.6).**

The proposition follows from Claims 1–4 and 6–7.

• Claim 1:

(a)–(c) hold. The forward direction of Theorem 2.4(a) implies that $ι$, $τ$, and $δ$ are bijections.

• Claim 2:

(d) holds. This follows from Lemma A.6(a).

• Claim 3:

(k) holds. Take $i$. Since $τ$ is a bijection by Claim 1 (part (b)), it suffices to argue that

[TABLE]

The first equality holds by the definition of $X_{i}$ and a rearrangement. The second equality follows from Lemma A.2(b) because $[Π,Π′,τ,δ]$ is an isomorphism by Corollary 2.5. The third equality holds by Claim 2 (part (d)). The fourth equality holds by the definition of $X′_{ι(i)}$.

• Claim 4:

(m) holds. Take $i$. Since $[Π,Π′,τ,δ]$ is an isomorphism by Corollary 2.5, Lemma A.8 implies that $τ|_{{\mathcal{H}}_{i}}$ is a well-defined function from ${\mathcal{H}}_{i}$ into ${\mathcal{H}}′_{ι(i)}$. It is injective because $τ$ is injective by Claim 1 (part (b)). To show that it is surjective, take $H′⋅∈⋅{\mathcal{H}}_{ι(i)}$. Since $[Φ′,Φ,ι^{-1},τ^{-1},δ^{-1}]$ is an isomorphism by Theorem 2.4(b), $[Π′,Π,τ^{-1},δ^{-1}]$ is an isomorphism by Corollary 2.5. Thus Lemma A.8 can be applied to $[Φ′,Φ,τ^{-1},ι^{-1},δ^{-1}]$. Therefore $H′⋅∈⋅{\mathcal{H}}_{ι(i)}$ implies $τ^{-1}(H′)⋅∈⋅{\mathcal{H}}_{ι^{-1}○ι(i)}$. Hence $τ^{-1}(H′)⋅∈⋅{\mathcal{H}}_{i}$. This implies that $τ(τ^{-1}(H′))=H′$ is in the range of $τ|_{{\mathcal{H}}_{i}}$.

• Claim 5:

(a). $[Π,Π′,τ,δ]$ is an $\mathbf{NCP}$ isomorphism, where $Π=(T,C,⊗)$ and $Π=(T′,C′,⊗′)$. (b) $[(T,p),(T′,p′),τ]$ is a $\mathbf{Tree}$ isomorphism. (a) holds by Corollary 2.5. For (b), note that (a) and SP Theorem 3.9 imply $\mathsf{F_{1}}([Π,Π′,τ,δ])$ is a $\mathbf{Tree}$ isomorphism. By that theorem’s definition of $\mathsf{F}$, $\mathsf{F_{1}}([Π,Π′,τ,δ])=[\mathsf{F_{0}}(Π),\mathsf{F_{0}}(Π′),τ]=[(T,p),(T′,p′),τ]$.

• Claim 6:

(e), (f), (i), (j), and (l) hold. These hold by Claim 5(a) and the parts of SP Proposition 3.8. In particular, (e) holds by SP Proposition 3.8(b). (f) holds by SP Proposition 3.8(c). (i) holds by SP Proposition 3.8(d). (j) holds by SP Proposition 3.8(a) since Section 2.1 defines $X$ as $F^{-1}(C)$ and thus $X′$ as $(F′)^{-1}(C′)$. (l) holds by SP Proposition 3.8(e).

• Claim 7:

(g), (h), and (n)–(r) hold. These hold by Claim 5(b) and various parts of SP Proposition 2.7. In particular, (g) holds by SP Proposition 2.7(c). (h) holds by SP Proposition 2.7(e). (n) holds by SP Proposition 2.7(d). (o)–(r) hold by SP Proposition 2.7(f)–(i).

$\Box$

Proof A.10** (for Theorem 2.7).**

By [F1], $\mathsf{P_{0}}$ maps any form into a preform. By [FM1], $\mathsf{P_{1}}$ maps any form morphism into a preform morphism. Thus it suffices to show that $\mathsf{P}$ preserves source, target, identity, and composition (Mac Lane 1998 page 13). This is done in the following four claims.

• Claim 1:

$\mathsf{P_{1}}(β)^{\mathsf{src}}=\mathsf{P_{0}}(β^{\mathsf{src}})$. Take $β=[Φ,Φ′,ι,τ,δ]$. Then I argue, in steps, that $\mathsf{P_{1}}(β)^{\mathsf{src}}$ by the definition of $β$ is equal to $\mathsf{P_{1}}([Φ,Φ′,ι,τ,δ])^{\mathsf{src}}$, which by the definition of $\mathsf{P_{1}}$ is equal to $[\mathsf{P_{0}}(Φ),\mathsf{P_{0}}(Φ′),τ,δ]^{\mathsf{src}}$, which by the definition of $\mathsf{src}$ in $\mathbf{NCP}$ is equal to $\mathsf{P_{0}}(Φ)$, which by the definition of $\mathsf{src}$ in $\mathbf{NCF}$ is equal to $\mathsf{P_{0}}([Φ,Φ′,ι,τ,δ]^{\mathsf{src}})$, which by the definition of $β$ is equal to $\mathsf{P_{0}}(β^{\mathsf{src}})$.

• Claim 2:

$\mathsf{P_{1}}(β)^{\mathsf{trg}}=\mathsf{P_{0}}(β^{\mathsf{trg}})$. This is very similar to Claim 1. Simply change $\mathsf{src}$ to $\mathsf{trg}$.

• Claim 3:

$\mathsf{P_{1}}(\mathsf{id}_{Φ})=\mathsf{id}_{\mathsf{P_{0}}(Φ)}$. Take $Φ=(I,T,(C_{i})_{i∈I},⊗)$ and let $C=∪_{i}C_{i}$. First I show [a] $\mathsf{P_{0}}(Φ)=(T,C,⊗)$ by arguing, in steps, that $\mathsf{P_{0}}(Φ)$ by the definition of $Φ$ is $\mathsf{P_{0}}(I,T,(C_{i})_{i∈I},⊗)$, which by the definition of $\mathsf{P_{0}}$ is $(T,∪_{i∈I}C_{i},⊗)$, which by the definition of $C$ is $(T,C,⊗)$. Then I argue, in steps, that $\mathsf{P_{1}}(\mathsf{id}_{Φ})$ by the definition of $\mathsf{id}$ in $\mathbf{NCF}$ is equal to $\mathsf{P_{1}}([Φ,Φ,\mathsf{id}_{I},\mathsf{id}_{T},\mathsf{id}_{C}])$, which by the definition of $\mathsf{P_{1}}$ is equal to $[\mathsf{P_{0}}(Φ),\mathsf{P_{0}}(Φ),\mathsf{id}_{T},\mathsf{id}_{C}]$, which by [a] is equal to $[(T,C,⊗),(T,C,⊗),\mathsf{id}_{T},\mathsf{id}_{C}]$, which by the definition of $\mathsf{id}$ in $\mathbf{NCP}$ is equal to $\mathsf{id}_{(T,C,⊗)}$, which by [a] is equal to $\mathsf{id}_{\mathsf{P_{0}}(Φ)}$.

• Claim 4:

$\mathsf{P_{1}}(β′○β)=\mathsf{P_{1}}(β′)○\mathsf{P_{1}}(β)$. Take $β=[Φ,Φ′,ι,τ,δ]$ and $β′=[Φ′,Φ″,$ $ι′,τ′,δ′]$. First I note that, since $\mathsf{P_{1}}$ is well-defined by the first paragraph, $\mathsf{P_{1}}([Φ,Φ′,$ $ι,τ,δ])=[\mathsf{P_{0}}(Φ),\mathsf{P_{0}}(Φ′),τ,δ]$ and $\mathsf{P_{1}}([Φ′,Φ″,ι′,τ′,δ′])=[\mathsf{P_{0}}(Φ′),\mathsf{P_{0}}(Φ″),τ′,δ′]$ are preform morphisms. Then I argue that

[TABLE]

where the first equality holds by the definitions of $β$ and $β′$, the second by the definition of $○$ in $\mathbf{NCF}$, the third by the definition of $\mathsf{P_{1}}$, the fourth by the previous sentence and by the definition of $○$ in $\mathbf{NCP}$, the fifth by the definition of $\mathsf{P_{1}}$, and the sixth by the definitions of $β$ and $β′$.

$\Box$

Proof A.11** (for Proposition 2.8).**

(a${}^{\text{o}}$). Suppose $[Π,Π′,τ,δ]$ is a preform morphism, with $Π=(T,C,⊗)$ determining $≺$ and ${\mathcal{H}}$, and with $Π′=(T′,C′,⊗′)$ determining $≺′$ and ${\mathcal{H}}′$. It suffices to show that the absentmindedness of $Π$ implies the absentmindedness of $Π′$. Toward that end, suppose $Π$ has absentmindedness. Then there are

$[$1$]$ $H⋅∈⋅{\mathcal{H}}$,

(2) $t^{A}⋅∈⋅H$, and

(3) $t^{B}⋅∈⋅H$ such that

(4) $t^{A}⋅≺⋅t^{B}$. $[$1$]$ and SP Proposition 3.5 imply there exists

(5) $H′⋅∈⋅{\mathcal{H}}′$ such that

(6) $τ(H)⋅⊆⋅H′$. 2 implies $τ(t^{A})⋅∈⋅τ(H)$ and thus 6 implies

(7) $τ(t^{A})⋅∈⋅H′$. Similarly, 3 implies $τ(t^{B})⋅∈⋅τ(H)$ and thus 6 implies

(8) $τ(t^{B})⋅∈⋅H′$. In addition, 4 and SP Proposition 2.4(d) (via SP Corollary 3.10) imply

(9) $τ(t^{A})⋅≺′⋅τ(t^{B})$. 5, 7, 8, and 9 imply $Π′$ has absentmindedness.

(a). Suppose $Π$ and $Π′$ are isomorphic. Then (a fortiori) there is a morphism to $Π$ from $Π′$ and also a morphism from $Π$ to $Π′$. By part (a${}^{\text{o}}$) and the first morphism, the no-absentmindedness of $Π$ implies the no-absentmindedness of $Π′$. Similarly, by part (a${}^{\text{o}}$) and the second morphism, the no-absentmindedness of $Π$ is implied by the no-absentmindedness of $Π′$.

(b${}^{\text{o}}$). This follows from part (a${}^{\text{o}}$) and the definition of no-absentmindedness for forms.

(b). This follows from part (b${}^{\text{o}}$) just as part (a) follows from part (a${}^{\text{o}}$). $\Box$

Proof A.12** (for Proposition 2.9).**

Claim 1. If $[Π,Π′,τ,δ]$ is an isomorphism and $Π′$ has perfect-information, then $Π$ has perfect-information. Suppose $[Π,Π′,τ,δ]$ is an isomorphism, with $Π=(T,C,⊗)$ determining ${\mathcal{H}}$ and $Π′=(T′,C′,⊗)$ determining ${\mathcal{H}}′$. Further suppose $Π$ does not have perfect-information. It suffices to show that $Π′$ does not have perfect-information. Because $Π$ does not have perfect-information, there are $t^{1}⋅∈⋅T$, $t^{2}⋅∈⋅T$, and

$[$a$]$ $H⋅∈⋅{\mathcal{H}}$ such that

(2) $t^{1}⋅≠⋅t^{2}$ and

(3) $⎨t^{1},t^{2}⎬⋅⊆⋅H$. SP Proposition 3.8(e) implies $τ|_{\mathcal{H}}$ is a bijection from ${\mathcal{H}}$ onto ${\mathcal{H}}′$. Hence $[$a$]$ implies

(4) $τ(H)⋅∈⋅{\mathcal{H}}′$. Further, SP Theorem 3.7 implies that $τ$ is a bijection from $T$ onto $T′$. Hence 2 implies

(5) $τ(t^{1})⋅≠⋅τ(t^{2})$. Yet further, 3 implies

(6) $⎨τ(t^{1}),τ(t^{2})⎬⋅⊆⋅τ(H)$. 4, 5, and 6 imply that $Π′$ does not have perfect-information.

(a). This follows from Claim 1.

(b). This follows from part (a) and the definition of perfect-information for forms. $\Box$

Lemma A.13**.**

Suppose that $(T,p)$ is a functioned tree and that $τ{:}T\textrightarrow T′$ is a bijection. Define the function $p′$ by surjectivity and $p′\mspace{1.0mu}^{\mathsf{gr}}=⎨\,(τ(t^{\sharp}),τ(t))\,|\,(t^{\sharp},t)∈p\mspace{1.0mu}^{\mathsf{gr}}\,⎬.$ Then $(T′,p′)$ is a functioned tree.

Proof*.*

Since $(T,p)$ is a functioned tree, there exist $t^{o}⋅∈⋅T$ and $X⋅⊆⋅T$ to satisfy [T1]–[T2]. Define $t^{\prime o}=τ(t^{o})$ and $X′=τ(X)$. It suffices to show

[TABLE]

These two statements are shown by Claims 6 and 8.

• Claim 1:

$τ|_{T⧷⎨t^{o}⎬}{:}T⧷⎨t^{o}⎬\textrightarrow T′⧷⎨t^{\prime o}⎬$ is a bijection. This follows from the bijectivity of $τ$ and the definition of $t^{\prime o}$.

• Claim 2:

$τ|_{X}{:}X\textrightarrow X′$ is a bijection. This follows from the bijectivity of $τ$ and the definition of $X′$.

• Claim 3:

$τ|_{X}○p○(τ|_{T⧷⎨t^{o}⎬})^{-1}$ is a nonempty function from $T′⧷⎨t^{\prime o}⎬$ onto $X′$. The claim follows from composition. In particular, $(τ|_{T⧷⎨t^{o}⎬})^{-1}{:}T′⧷⎨t^{\prime o}⎬\textrightarrow T⧷⎨t^{o}⎬$ is a bijection by Claim 1, $p{:}T⧷⎨t^{o}⎬\textrightarrow X$ is nonempty and surjective by [T1], and $τ|_{X}{:}X\textrightarrow X′$ is a bijection by Claim 2. These bijections appear on the bottom, left, and top of Figure A.1.

• Claim 4:

$p′\mspace{1.0mu}^{\mathsf{gr}}=(τ|_{X}○p○(τ|_{T⧷⎨t^{o}⎬})^{-1})\mspace{1.0mu}^{\mathsf{gr}}$. I argue

[TABLE]

The first equality holds by the lemma’s definition of $p′\mspace{1.0mu}^{\mathsf{gr}}$. The second holds since the domain of $p$ is $T⧷⎨t^{o}⎬$ by [T1]. The third is a rearrangement. The fourth holds by Claim 1. The fifth and sixth are rearrangements. The last holds because the domain of $(τ|_{T⧷⎨t^{\prime o}⎬})^{-1}$ is $T′⧷⎨t^{\prime o}⎬$ by Claim 1.

• Claim 5:

$p′=τ|_{X}○p○(τ|_{t⧷⎨t^{o}⎬})^{-1}$, that is, Figure A.1 commutes. This follows from Claim 4 because [a] $p′$ is surjective by assumption and [b] $τ|_{X}○p○(τ|_{t⧷⎨t^{o}⎬})^{-1}$ is surjective by Claim 3.

• Claim 6:

[T1 $′$] holds. This follows from Claims 3 and 5.

• Claim 7:

$(∀t∈T⧷⎨t^{o}⎬)(∃m≥1)⋅t^{o}=p\mspace{2.0mu}○[(τ|_{T⧷⎨t^{o}⎬})^{-1}○τ|_{X}○p]^{m-1}(t)$. Take $t\,≠\,t^{o}$. By [T2] there exists $m⋅≥⋅1$ such that $t^{o}=p^{m}(t)$. On the one hand, suppose $m=1$. Then the claim holds by the definition of $m$. On the other hand, suppose $m⋅≥⋅2$. Then proving the claim requires several steps. First, I show

[TABLE]

Take any such $n$. Since $τ$ is bijective, it suffices to show that the composition $(τ|_{T⧷⎨t^{o}⎬})^{-1}○τ|_{X}○p^{n}(t)$ is well-defined. In other words, it suffices to show [i] that $p^{n}(t)⋅∈⋅X$ and [ii] that $τ|_{X}○p^{n}(t)$ is in the domain of $(τ|_{T⧷⎨t^{o}⎬})^{-1}$. [i] holds because the codomain of $p$ is $X$ by [T1]. To see [ii], note that $t^{o}=p^{m}(t)$ and $m{-}1\,≥\,n\,≥\,1$ imply that $p^{n}(t)$ is in the domain of $p$. Thus, since the domain of $p$ is $T⧷⎨t^{o}⎬$ by [T1], we have $p^{n}(t)⋅∈⋅T⧷⎨t^{o}⎬$. Hence the definition of $t^{\prime o}$ and the bijectivity of $τ$ imply $τ|_{X}○p^{n}(t)⋅∈⋅T′⧷⎨t^{\prime o}⎬$. This and Claim 1 imply [ii]. Second, I argue

[TABLE]

This holds because the right-hand side of (b) is a rearrangement of the right-hand side of (a). Third, I argue

[TABLE]

where the first equality holds by (b) at $n{=}m{-}1$, the second by (b) at $n{=}m{-}2$, …, and the last by (b) at $n{=}1$. Finally, I argue the claim holds because

[TABLE]

where the first equality holds by the definition of $m$, the second is a rearrangement, and the third holds by (c).

• Claim 8:

[T2$\,′$] holds. Take $t′⋅∈⋅T′⧷⎨t^{\prime o}⎬$. Then Claim 1 implies $(τ|_{T⧷⎨t^{o}⎬})^{-1}(t′)$ $∈$ $T⧷⎨t^{o}⎬$. Thus by Claim 7, there exists $m⋅≥⋅1$ such that

[TABLE]

I now argue

[TABLE]

The first equation holds by the definition of $t^{\prime o}$ and the fact that $t^{o}⋅∈⋅X$ in any functioned tree (by remark [iv] in the paragraph following SP equation (1)). The second equation holds by the definition of $m$, the third is a rearrangement, and the fourth holds by Claim 5.

$\Box$

Lemma A.14**.**

Suppose $Π=(T,C,⊗)$ is an $\mathbf{NCP}$ preform. Also suppose $τ{:}T\textrightarrow T′$ and $δ{:}C\textrightarrow C′$ are bijections. Define $⊗′$ by surjectivity and $⊗′\mspace{1.0mu}^{\mathsf{gr}}=$ $⎨\,(τ(t),δ(c),τ(t^{\sharp})\,|\,$ $\!(t,c,t^{\sharp})∈⊗\mspace{1.0mu}^{\mathsf{gr}}\,⎬$. Also define $Π′=(T′,C′,⊗′)$. Then (a) $Π′$ is an $\mathbf{NCP}$ preform and (b) $[Π,Π′,τ,δ]$ is an $\mathbf{NCP}$ isomorphism.

Proof*.*

(a). By [P1] there exist $F{:}T⇉C$ and $t^{o}⋅∈⋅T$ such that $⊗$ is a bijection from $F\mspace{1.0mu}^{\mathsf{gr}}$ onto $T⧷⎨t^{o}⎬$. Define $F′{:}T′⇉C′$ by $F′\mspace{1.0mu}^{\mathsf{gr}}=$ $⎨(τ(t),δ(c))|(t,c)∈F\mspace{1.0mu}^{\mathsf{gr}}⎬$. Also define $t^{\prime o}=τ(t^{o})$. It suffices to show that

[TABLE]

This is done by Claims 6, 7, and 9.

• Claim 1:

$(τ,δ)|_{F\mspace{1.0mu}^{\mathsf{gr}}}{:}F\mspace{1.0mu}^{\mathsf{gr}}\textrightarrow F′\mspace{1.0mu}^{\mathsf{gr}}$ is a bijection. This follows from the bijectivity of $τ$, the bijectivity of $δ$, and the definition of $F′$.

• Claim 2:

$τ|_{τ⧷⎨t^{o}⎬}{:}T⧷⎨t^{o}⎬\textrightarrow T′⧷⎨t^{\prime o}⎬$ is a bijection. This follows from the bijectivity of $τ$ and the definition of $t^{\prime o}$.

• Claim 3:

$τ|_{τ⧷⎨t^{o}⎬}○⊗○[(τ,δ)|_{F\mspace{1.0mu}^{\mathsf{gr}}}]^{-1}$ is a bijection from $F′\mspace{1.0mu}^{\mathsf{gr}}$ onto $T′⧷⎨t^{\prime o}⎬$. The claim follows from composition. In particular, $((τ,δ)|_{F\mspace{1.0mu}^{\mathsf{gr}}})^{-1}{:}F′\mspace{1.0mu}^{\mathsf{gr}}\textrightarrow F\mspace{1.0mu}^{\mathsf{gr}}$ is a bijection by Claim 1, $⊗{:}F\mspace{1.0mu}^{\mathsf{gr}}\textrightarrow T⧷⎨t^{o}⎬$ is a bijection by the definitions of $F$ and $t^{o}$, and $τ_{T⧷⎨t^{o}⎬}{:}T⧷⎨t^{o}⎬\textrightarrow T′⧷⎨t^{\prime o}⎬$ is a bijection by Claim 2. These three functions appear on the top, left, and bottom of Figure A.2.

• Claim 4:

$⊗′\mspace{1.0mu}^{\mathsf{gr}}=(τ|_{T⧷⎨t^{o}⎬}○⊗○[(τ,δ)|_{F\mspace{1.0mu}^{\mathsf{gr}}}]^{-1})\mspace{1.0mu}^{\mathsf{gr}}$. I argue

[TABLE]

The first equality holds by the lemma’s definition of $⊗′$. The second holds by the definition of $F$, and the third by the definition of $t^{o}$. The fourth holds by Claim 1. The fifth and sixth are rearrangements. The seventh holds by Claim 1.

• Claim 5:

$⊗′=τ|_{T⧷⎨t^{o}⎬}○⊗○[(τ,δ)|_{F\mspace{1.0mu}^{\mathsf{gr}}}]^{-1}$, that is, Figure A.2 commutes. This follows from Claim 4 because [a] $⊗′$ is surjective by definition and [b] $τ|_{T⧷⎨t^{o}⎬}$ is surjective by Claim 2.

• Claim 6:

[P1 $′$] holds. This follows from Claims 3 and 5.

• Claim 7:

[P2 $′$] holds. Define $p$ by [P2]. [P2] implies that

$[$a$]$ $(T,p)$ is a functioned tree. Define $p′$ by [P2$′$]. Claim 6 and SP Lemma C.1(a) implies

(2) $p′$ is well-defined and

(3) $p′$ is surjective. Because of 2, it suffices to show that $(T′,p′)$ is a functioned tree.

Toward that end, consider Lemma A.13. Lemma A.13’s assumptions are met by $[$a$]$ and the injectivity of $τ$. Thus Lemma A.13 implies that $(T′,p^{\star})$ is a functioned tree, where the function $p^{\star}$ is defined by

(4) $p^{\star}$ being surjective and

(5) $p^{\star}\mspace{1.0mu}^{\mathsf{gr}}=⎨\,(τ(t^{\sharp}),τ(t))\,|\,(t^{\sharp},t)∈p\mspace{1.0mu}^{\mathsf{gr}}\,⎬$. Thus it suffices to show that $p′=p^{\star}$.

Toward that end, note 3 and 4 imply that both $p′$ and $p^{\star}$ are surjective. Thus it suffices to show $p′\mspace{1.0mu}^{\mathsf{gr}}=p^{\star}\mspace{1.0mu}^{\mathsf{gr}}$. I argue

[TABLE]

The first equality holds by the definition of $p′$ two paragraphs ago, and the second equality holds by the definition of $⊗′$ in the lemma statement. The $⊆$ direction of the third equality holds simply because the variable $c′$ does not appear in the right-hand side. The $⊇$ direction follows from $⊗\mspace{1.0mu}^{\mathsf{gr}}⋅⊆⋅T×C×T$ and $δ{:}C\textrightarrow C′$. The fourth equality holds because the codomain of $τ$ is $T′$. The fifth equality follows from the definition of $p$ two paragraphs ago, and the sixth equality follows from 5.

• Claim 8:

$(∀c′∈C′)⋅(F′)^{-1}(c′)=τ(F^{-1}(δ^{-1}(c′)))$. Take $c′⋅∈⋅C′$. I argue, in seven steps, that $(F′)^{-1}(c′)$ by definition is $⎨t′∈T′|c′∈F′(t′)⎬$, which by rearrangement is $⎨t′∈T′|(t′,c′)∈F′\mspace{1.0mu}^{\mathsf{gr}}⎬$, which, by the definition of $F′$, the bijectivity of $τ$, and the bijectivity of $δ$, is $⎨t′∈T′|(τ^{-1}(t′),δ^{-1}(c′))∈F\mspace{1.0mu}^{\mathsf{gr}}⎬$, which by the bijectivity of $τ$ is $⎨t′|(∃t∈T)\,t′{=}τ(t),\,(τ^{-1}(t′),δ^{-1}(c′))∈F\mspace{1.0mu}^{\mathsf{gr}}⎬$, which by rearrangement is $⎨τ(t)|(∃t∈T)(τ^{-1}○τ(t),δ^{-1}(c′))∈F\mspace{1.0mu}^{\mathsf{gr}}⎬$, which by rearrangement is $τ(⎨t∈T|(t,δ^{-1}(c′))∈F\mspace{1.0mu}^{\mathsf{gr}}⎬$, which by rearrangement is $τ(F^{-1}(δ^{-1}(c′)))$.

• Claim 9:

[P3 $′$] holds. It must be shown that

[TABLE]

To show [a], take $c′$. By the bijectivity of $δ$, $δ^{-1}(c′)⋅∈⋅C$. Thus by [P3], $F^{-1}(δ^{-1}(c′))$ $≠$ $∅$. Thus $τ(F^{-1}(δ^{-1}(c′)))⋅≠⋅∅$. Thus by Claim 8, $(F′)^{-1}(c′)⋅≠⋅∅$. To show [b], suppose that [b] were false. Then there would be $c^{\prime A}$ and $c^{\prime B}$ such that $(F′)^{-1}(c^{\prime A})$ and $(F′)^{-1}(c^{\prime B})$ intersect and are unequal. Hence by Claim 8, $τ(F^{-1}(δ^{-1}(c^{\prime A})))$ and $τ(F^{-1}(δ^{-1}(c^{\prime A})))$ intersect and are unequal. Hence by the bijectivity of $τ$, $F^{-1}(δ^{-1}(c^{\prime A}))$ and $F^{-1}(δ^{-1}(c^{\prime B}))$ intersect and are unequal. This contradicts [P3] because both $δ^{-1}(c^{\prime A})$ and $δ^{-1}(c^{\prime B})$ belong to $C$ by the bijectivity of $δ$. Finally, [c] holds by definition (recall the last sentence of note 7).

(b). This paragraph shows that $[Π,Π′,τ,δ]$ is a morphism. $Π$ is a preform by assumption and $Π′$ is a preform by part (a). [PM1] and [PM2] hold by assumption (a fortiori). [PM3] holds with equality by the definition of $⊗′$.

Finally, SP Theorem 3.7 implies that $[Π,Π′,τ,δ]$ is an isomorphism because [a] it is a morphism by the previous paragraph and [b] $τ$ and $δ$ are bijective by assumption. $\Box$

Lemma A.15**.**

Suppose $Φ=(I,T,(C_{i})_{i∈I},⊗)$ is an $\mathbf{NCF}$ form. Also suppose $ι{:}I\textrightarrow I′$, $τ{:}T\textrightarrow T′$, and $δ{:}∪_{i∈I}C_{i}\textrightarrow C′$ are bijections. Define $⊗′$ by surjectivity and $⊗′\mspace{1.0mu}^{\mathsf{gr}}=⎨(τ(t),δ(c),τ(t^{\sharp})|(t,c,t^{\sharp})∈⊗\mspace{1.0mu}^{\mathsf{gr}}⎬$. Also define $(C′_{i′})_{i′∈I′}$ at each $i′$ by $C′_{i′}=δ(C_{ι^{-1}(i′)})$. Also define $Φ′=(I′,T′,(C′_{i′})_{i′∈I′},⊗′)$. Then (a) $Φ′$ is an $\mathbf{NCF}$ form and (b) $[Φ,Φ′,ι,τ,δ]$ is an $\mathbf{NCF}$ isomorphism.

Proof*.*

Define $C=∪_{i∈I}C_{i}$. Define $Π=(T,C,⊗)$. Define $Π′=(T′,C′,⊗′)$.

• Claim 1:

(a) $Π′$ is an $\mathbf{NCP}$ preform and (b) $[Π,Π′,τ,δ]$ is an $\mathbf{NCP}$ isomorphism. Consider Lemma A.14. The assumptions of Lemma A.14 are met because [i] $Π$ is an $\mathbf{NCP}$ preform by [F1], [ii] $τ{:}T\textrightarrow T′$ is a bijection by assumption, and [iii] $δ{:}C\textrightarrow C′$ is a bijection because $C=∪_{i∈I}C_{i}$ by definition and $δ{:}∪_{i∈I}C_{i}\textrightarrow C′$ is a bijection by assumption. Further, Lemma A.14’s definitions of $⊗′$ and $Π′$ coincide with the present definitions of $⊗′$ and $Π′$. Thus Lemma A.14 implies this claim’s two conclusions.

• Claim 2:

$C′=∪_{i′∈I′}C′_{i′}$. I argue, in four steps, that $C′$ by the bijectivity of $δ$ equals $δ(∪_{i∈I}C_{i})$, which by rearrangement equals $∪_{i∈I}δ(C_{i})$, which by the bijectivity of $ι$ equals $∪_{i′∈I′}δ(C_{ι^{-1}(i′)})$, which by the definition of $(C′_{i′})_{i′∈I′}$ equals $∪_{i′∈I′}C′_{i′}$.

• Claim 3:

$Φ′$ satisfies [F1]. It must be shown that $(T′,C^{\star},⊗′)$ is a preform where $C^{\star}$ is defined as $∪_{i′∈I′}C′_{i′}$. Claim 2 implies that $C^{\star}=C′$. Hence $Π′=(T′,C^{\star},⊗′)$. Hence Claim 1(a) implies that $(T′,C^{\star},⊗′)$ is a preform.

• Claim 4:

$Φ′$ satisfies [F2]. Take $i′⋅∈⋅I′$ and $j′⋅∈⋅I′⧷⎨i′⎬$. The bijectivity of $ι$ implies $ι^{-1}(i′)⋅∈⋅I$ and $ι^{-1}(j′)⋅∈⋅I⧷⎨ι^{-1}(i′)⎬$. Thus [F2] for $Φ$ implies $C_{ι^{-1}(i′)}\,∩\,C_{ι^{-1}(j′)}=∅$. Hence the bijectivity of $δ$ implies $δ(C_{ι^{-1}(i′)})\,∩\,δ(C_{ι^{-1}(j′)})=∅$. Hence the definition of $(C′_{i′})_{i′∈I′}$ implies $C′_{i′}∩C′_{j′}=∅$.

• Claim 5:

$Φ′$ satisfies [F3]. Take $t′⋅∈⋅T′$. The bijectivity of $τ$ implies $τ^{-1}(t′)⋅∈⋅T$. Hence [F3] for $Φ$ implies there is $i⋅∈⋅I$ such that $F(τ^{-1}(t′))⋅⊆⋅C_{i}$. Hence the bijectivity of $ι$ implies there is $i′⋅∈⋅I′$ such that

$[$a$]$ $F(τ^{-1}(t′))⋅⊆⋅C_{ι^{-1}(i′)}$. Also, I show

(2) $F(τ^{-1}(t′))=δ^{-1}(F′(t′))$ by arguing, in steps, that $F(τ^{-1}(t′))$ by rearrangement equals $⎨c∈C|(τ^{-1}(t′),c)∈F\mspace{1.0mu}^{\mathsf{gr}}⎬$, which by Claim 1(b) and SP Proposition 3.8(c) equals $⎨c∈C|(t′,δ(c))∈F′\mspace{1.0mu}^{\mathsf{gr}}⎬$, which by the bijectivity of $δ$ equals $⎨c|(∃c′∈C′)$ $c{=}δ^{-1}(c′),\,(t′,δ(c))∈F′\mspace{1.0mu}^{\mathsf{gr}}⎬$, which by rearrangement equals $⎨δ^{-1}(c′)|(∃c′∈C′)$ $(t′,c′)∈F′\mspace{1.0mu}^{\mathsf{gr}}⎬$, which by rearrangement equals $δ^{-1}(⎨c′∈C′|(t′,c′)∈F′\mspace{1.0mu}^{\mathsf{gr}}⎬)$, which by rearrangement equals $δ^{-1}(F′(t′))$. $[$a$]$ and 2 imply $δ^{-1}(F′(t′))⋅⊆⋅C_{ι^{-1}(i′)}$. Hence the bijectivity of $δ$ implies $F′(t′)⋅⊆⋅δ(C_{ι^{-1}(i′)})$. Hence the definition of $C′_{i′}$ implies $F′(t′)⋅⊆⋅C′_{i′}$.

• Claim 6:

$Φ′$ is an $\mathbf{NCF}$ form. This follows from Claims 3–5.

• Claim 7:

$[Φ,Φ′,ι,τ,δ]$ is an $\mathbf{NCF}$ morphism. $Φ$ is an $\mathbf{NCF}$ form by assumption, and $Φ′$ is an $\mathbf{NCF}$ form by Claim 6. [FM1] holds because $[Π,Π′,τ,δ]$ is an $\mathbf{NCP}$ morphism a fortiori by Claim 1(b). [FM2] holds by assumption. For [FM3], take $i⋅∈⋅I$. I argue, in two steps, that $δ(C_{i})$ by the bijectivity of $ι$ equals $δ(C_{ι^{-1}○ι(i)})$, which by definition of $C′_{ι(i)}$ equals $C′_{ι(i)}$.

• Claim 8:

$[Φ,Φ′,ι,τ,δ]$ is an $\mathbf{NCF}$ isomorphism. This follows from the reverse direction of Corollary 2.5 because [a] $[Φ,Φ′,ι,τ,δ]$ is an $\mathbf{NCF}$ morphism by Claim 7, [b] $[Π,Π′,τ,δ]$ is an $\mathbf{NCP}$ isomorphism by Claim 1(b), and [c] $ι$ is a bijection by assumption.

Conclusion. The lemma’s conclusions follow from Claims 6 and 8. $\Box$

Appendix B $\mathbf{CsqF}$

Proof B.1** (for Proposition 3.1).**

The  Appendix B. $\mathbf{CsqF}$proposition follows from Claims 1–8 and 13–14.

• Claim 1:

(a) holds. Suppose [a] $t^{o}⋅≠⋅⎨⎬$. [Csq1] states [b] $⎨⎬⋅∈⋅T$. [a] and [b] imply $⎨⎬⋅∈⋅T⧷⎨t^{o}⎬$. Thus by [P1], there are $t⋅∈⋅T$ and $c⋅∈⋅C$ such that $(t,c,⎨⎬)⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$. Thus by [Csq2], $p(⎨⎬)±(c)$ $=⎨⎬$. This is impossible because the left-hand sequence has positive length and the right-hand sequence has zero length.

• Claim 2:

(b) holds. Take $t^{\sharp}⋅∈⋅T⧷⎨⎨⎬⎬$. Claim 1 (a) implies $t^{\sharp}⋅∈⋅T⧷⎨t^{o}⎬$. Thus the reverse direction of SP Proposition 3.1(a) implies $(p(t^{\sharp}),q(t^{\sharp}),t^{\sharp})$ $∈$ $⊗$. Thus [Csq2] implies $p(t^{\sharp})±(q(t^{\sharp}))=t^{\sharp}$. Thus $p(t^{\sharp})={{}_{1}t^{\sharp}_{|t^{\sharp}|-1}}$ and $q(t^{\sharp})=t^{\sharp}_{|t^{\sharp}|}$.

• Claim 3:

(c) holds. Assume $(t,c,t^{\sharp})⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$. Then [P1] yields $(t,c,t^{\sharp})⋅∈⋅T×C×T$, and [Csq2] yields $t±(c)=t^{\sharp}$. Conversely, suppose

$[$1$]$ $(t,c,t^{\sharp})⋅∈⋅T×C×T$ and

(2) $t±(c)=t^{\sharp}$. 2 implies

(3) $t={{}_{1}t^{\sharp}_{|t^{\sharp}|-1}}$ and

(4) $c=t^{\sharp}_{|t^{\sharp}|}$. Further, 4 implies $t^{\sharp}⋅≠⋅⎨⎬$. This and $[$1$]$ implies

(5) $t^{\sharp}⋅∈⋅T⧷⎨⎨⎬⎬$. 5 and Claim 2 (b) imply

(6) $p(t^{\sharp})={{}_{1}t^{\sharp}_{|t^{\sharp}|-1}}$ and

(7) $q(t^{\sharp})=t^{\sharp}_{|t^{\sharp}|}$. 3 and 6 imply

(8) $t=p(t^{\sharp})$. 4 and 7 imply

(9) $c=q(t^{\sharp})$. Further, 5 and Claim 1 (a) imply $t^{\sharp}⋅≠⋅t^{o}$, and thus SP Proposition 3.1(a) implies

(10) $(p(t^{\sharp}),q(t^{\sharp}),t^{\sharp})⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$. 8–10 imply $(t,c,t^{\sharp})⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$.

• Claim 4:

(d) holds. By [P1], $F⋅⊆⋅T×C$. Thus it suffices to show $(∀t∈T,c∈C)$ $(t,c)⋅∈⋅F\mspace{1.0mu}^{\mathsf{gr}}$ iff $t±c⋅∈⋅T$. Suppose $(t,c)⋅∈⋅F\mspace{1.0mu}^{\mathsf{gr}}$. Then [P1] implies there is

$[$1$]$ $t^{\sharp}⋅∈⋅T$ such that

(2) $(t,c,t^{\sharp})⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$. 2 and Claim 3 (c) imply $t±(c)=t^{\sharp}$. This and $[$1$]$ imply $t±(c)⋅∈⋅T$. Conversely, suppose $t±(c)⋅∈⋅T$. There there is $t^{\sharp}⋅∈⋅T$ such that $t±(c)=t^{\sharp}$. Thus Claim 3 (c) implies $(t,c,t^{\sharp})⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$. This and [P1] imply $(t,c)⋅∈⋅F\mspace{1.0mu}^{\mathsf{gr}}$.

• Claim 5:

(e) holds. Take $t⋅∈⋅T$. I will use induction on $m⋅∈⋅⎨0,1,...\,|t|⎬$. For the initial step, assume $m=0$. Then $p^{0}(t)=t={{}_{1}t_{|t|}}={{}_{1}t_{|t|-0}}={{}_{1}t_{|t|-m}}$ by inspection. For the inductive step, assume $m>0$. Note $m⋅≤⋅|t|$ implies $|t|{-}m⋅≥⋅0$, which implies $|t|{-}(m{-}1)>0$, which implies

$[$1$]$ ${}_{1}t_{|t|-(m-1)}⋅≠⋅⎨⎬$. I then argue, in steps, that $p^{m}(t)$ by $m>0$ equals $p(p^{m-1}(t))$, which by the inductive hypothesis equals $p(_{1}t_{|t|-(m-1)})$, which by $[$1$]$ and Claim 2 (b) at $t^{\sharp}={{}_{1}t_{|t|-(m-1)}}$ equals ${}_{1}t_{|t|-(m-1)-1}$, which by rearrangement equals ${}_{1}t_{|t|-m}$.

• Claim 6:

(f) holds. Take $t⋅∈⋅T$. I show $p^{|t|}(t)=t^{0}$ by arguing, in steps, that $p^{|t|}(t)$ by Claim 5 (e) at $m=|t|$ equals ${}_{1}t_{|t|-|t|}$, which equals ${}_{1}t_{0}$, which equals $⎨⎬$, which by Claim 1 (a) equals $t^{o}$. This and the definition of $k$ imply $k(t)=|t|$.

• Claim 7:

(g) holds. Take $t⋅∈⋅T$. By inspection, the result is equivalent to $(∀ℓ∈⎨1,2,...\,|t|⎬)$ $t_{ℓ}=q○p^{|t|-ℓ}(t)$. On the one hand, take $t=⎨⎬$. Then $|t|=0$ so the result is vacuously true. On the other hand, take $t⋅≠⋅⎨⎬$. Then take

$[$1$]$ $ℓ⋅∈⋅⎨1,2,...\,|t|⎬$. First I show

(2) $p^{|t|-ℓ}(t)={{}_{1}t_{ℓ}}$ by arguing, in steps, that $p^{|t|-ℓ}(t)$ by Claim 5 (e) at $m=|t|{-}ℓ$ equals ${}_{1}t_{|t|-(|t|-ℓ)}$, which by rearrangement equals ${}_{1}t_{ℓ}$. Then I argue, in steps, that $q○p^{|t|-ℓ}(t)$ by 2 equals $q(_{1}t_{ℓ})$, which by $[$1$]$ and Claim 2 (b) equals $t_{ℓ}$.

• Claim 8:

(h) holds. Suppose $c⋅∈⋅C$. This and [P3] imply $F^{-1}(c)⋅≠⋅∅$. Thus there is $t^{\star}⋅∈⋅T$ such that $(t^{\star},c)⋅∈⋅F\mspace{1.0mu}^{\mathsf{gr}}$. This and Claim 4 (d) imply $t^{*}±(c)⋅∈⋅T$. Thus $c⋅∈⋅R(t^{*}±(c))⋅⊆⋅∪⎨R(t)|t∈T⎬$. Conversely, suppose $b⋅∈⋅∪⎨R(t)|t∈T⎬$. There there is

$[$1$]$ $t^{*}⋅∈⋅T$ such that

(2) $b⋅∈⋅R(t^{*})$. $[$1$]$ and Claim 7 (g) imply that $t^{*}=(q○p^{|t^{*}|-ℓ}(t^{*}))^{|t^{*}|}_{ℓ=1}$. This and 2 imply there is $ℓ^{*}⋅∈⋅⎨1,2,...\,|t^{*}|⎬$ such that $b=q○p^{|t^{*}|-ℓ^{*}}(t^{*})$. This implies $b⋅∈⋅C$ since the codomain of $q$ is $C$ by the definition of $q$.

• Claim 9:

$(∀t^{A}∈T,t^{B}∈T)$ $(|t^{A}|\,{<}\,|t^{B}|⋅\text{and}⋅t^{A}\,{=}\,{{}_{1}t^{B}_{|t^{A}|}})$ iff $t^{A}⋅⊊⋅t^{B}$. Take $t^{A}⋅∈⋅T$ and $t^{B}⋅∈⋅T$. First, suppose

$[$1$]$ $|t^{A}|<|t^{B}|$ and

(2) $t^{A}={{}_{1}t^{B}_{|t^{A}|}}$. $[$1$]$ and the definition of ${}_{1}t^{B}_{|t^{A}|}$ imply

(3) ${}_{1}t^{B}_{|t^{A}|}⋅⊊⋅t^{B}$. 2 and 3 imply $t^{A}⋅⊊⋅t^{B}$. Conversely, suppose

(4) $t^{A}⋅⊊⋅t^{B}$. [Csq1] implies

(5) $t^{A}=⎨(1,t^{A}_{1}),(2,t^{A}_{2}),...\,(|t^{A}|,t^{A}_{|t^{A}|})⎬$ and

(6) $t^{B}=⎨(1,t^{B}_{1}),(2,t^{B}_{2}),...\,(|t^{B}|,t^{B}_{|t^{B}|})⎬$. By inspection, 4–6 imply $|t^{A}|<|t^{B}|$ and $t^{A}={{}_{1}t^{B}_{|t^{A}|}}$.

• Claim 10:

$(∀t^{A}∈T,t^{B}∈T)$ $(|t^{A}|\,≤\,|t^{B}|⋅\text{and}⋅t^{A}\,{=}\,{{}_{1}t^{B}_{|t^{A}|}})$ iff $t^{A}⋅⊆⋅t^{B}$.272727Claim 10 says that one sequence is an initial segment of another sequence iff the former is a restriction of the latter. This may appear implausible. For example, $⎨(\mathsf{2},{\mathsf{f}})⎬$ is not an initial sequence of $t^{*}=$ $⎨(1,{\mathsf{g}}),(2,{\mathsf{f}}),(3,{\mathsf{f}})⎬$ even though $⎨(\mathsf{2},{\mathsf{f}})⎬$ is a restriction of $t^{*}$. This is consistent with Claim 10, because $⎨(2,{\mathsf{f}})⎬$ is not a sequence and thus not an element of $T$ by [Csq1]. In the proof of Claim 7719o, change $<$ to $≤$, and $⊊$ to $⊆$.

• Claim 11:

$(∀t^{A}∈T,t^{B}∈T)⋅t^{A}⋅≺⋅t^{B}$ iff $t^{A}⋅⊊⋅t^{B}$. Take $t^{A}⋅∈⋅T$ and $t^{B}⋅∈⋅T$. First, suppose $t^{A}⋅≺⋅t^{B}$. This and the definition of $≺$ imply there is

$[$1$]$ $m⋅∈⋅⎨1,2,...\,k(t^{B})⎬$ such that

(2) $t^{A}=p^{m}(t^{B})$. $[$1$]$ and Claim 6 (f) imply

(3) $m⋅∈⋅⎨1,2,...\,|t^{B}|⎬$. Finally, I argue, in steps, that $t^{A}$ by 2 equals $p^{m}(t^{B})$, which by 3 and Claim 5 (e) equals ${{}_{1}t^{B}_{|t^{B}|-m}}$, which by 3 is a strict subset of ${}_{1}t^{B}_{|t^{B}|}$, which by inspection equals $t^{B}$.

Conversely, suppose $t^{A}⋅⊊⋅t^{B}$. This and Claim 7719o imply

$[$1$]$ $|t^{A}|<|t^{B}|$ and

(2) $t^{A}={{}_{1}t^{B}_{|t^{A}|}}$. For convenience, let

(3) $m=|t^{B}|{-}|t^{A}|$. Note $[$1$]$ and $|t^{A}|⋅≥⋅0$ imply

(4) $m⋅∈⋅⎨1,2,...\,|t^{B}|⎬$. I now show

(5) $t^{A}=p^{m}(t^{B})$ by arguing, in steps, that $t^{A}$ by 2 equals ${}_{1}t^{B}_{|t^{A}|}$, which by 3 equals ${}_{1}t^{B}_{|t^{B}|-m}$, which by 4 and Claim 5 (e) at $t=t^{B}$ equals $p^{m}(t^{B})$. Finally, 5, 4, and the definition of $≺$ imply $t^{A}⋅≺⋅t^{B}$.

• Claim 12:

$(∀t^{A}∈T,t^{B}∈T)⋅t^{A}⋅≼⋅t^{B}$ iff $t^{A}⋅⊆⋅t^{B}$. Take $t^{A}⋅∈⋅T$ and $t^{B}⋅∈⋅T$. First, suppose $t^{A}⋅≼⋅t^{B}$. Then by the definition of $≼$, either $t^{A}⋅≺⋅t^{B}$ or $t^{A}=t^{B}$. In the first case, Claim 7724o implies $t^{A}⋅⊊⋅t^{B}$. Thus $t^{A}⋅⊆⋅t^{B}$ in both cases. Conversely, suppose $t^{A}⋅⊆⋅t^{B}$. Then either $t^{A}⋅⊊⋅t^{B}$ or $t^{A}=t^{B}$. In the first case, Claim 11 implies $t^{A}⋅≺⋅t^{B}$. Thus the definition of $≼$ implies $t^{A}⋅≼⋅t^{B}$ in both cases.

• Claim 13:

(i) holds. Combine Claims 9 and 11.

• Claim 14:

(j) holds. Combine Claims 10 and 12.

$\Box$

Lemma B.2**.**

Suppose $(T,C,⊗)$ is a node-and-choice preform with its $t^{o}$, $p$, and $q$. Let $\bar{T}=⎨\,(q○p^{k(t)-ℓ}(t))^{k(t)}_{ℓ=1}\,|\,t∈T\,⎬$. Then

[TABLE]

is a well-defined bijection. Its inverse is

[TABLE]

(to be clear, T⋅∋⋅t^{o}⋅\text{\reflectbox{\mapsto}}⋅⎨⎬⋅∈⋅\bar{T}).

Proof*.*

Let $α$ be the function from $T$ to $\bar{T}$, and conversely, let $β$ be the function to $T$ from $\bar{T}$.

This paragraph shows that $β○α$ is the identity function on $T$. The composition is well-defined because [1] the domain of $β$ is $\bar{T}$ and [2] the range of $α$ is $\bar{T}$ by the definition of $\bar{T}$. Thus it suffices to show $(∀t∈T)⋅β○α(t)=t$. Toward that end, take $t⋅∈⋅T$. First, suppose $k(t)=0$. I argue, in steps, that $β○α(t)$ by the definition of $α$ equals $β(⎨⎬)$, which by the definition of $β$ equals $t^{o}$, which by $k(t)=0$ equals $t$. Second, suppose $k(t)=1$. I argue, in steps, that $β○α(t)$ by the definition of $α$ equals $β[(q(t))]$, which by the definition of $β$ equals $t^{o}⊗q(t)$, which by $k(t)=1$ equals $p(t)⊗q(t)$, which by SP Proposition 3.1(b) equals $t$. Third and finally, suppose $k(t)⋅≥⋅2$. I will argue

[TABLE]

The first equality holds by the definition of $α$, the second by the definition of $β$, and the third by the definition of $k$. The fourth and fifth equalities hold by a rearrangement and SP Proposition 3.1(b). The sixth equality holds by $k(t){-}2$ similar applications of SP Proposition 3.1(b), and the final equality holds by a final application of SP Proposition 3.1(b).

This paragraph shows that $α○β$ is the identity function on $\bar{T}$. The composition is well-defined because [a] the domain of $α$ is $T$ and [b] each value of $β$ is a value of $⊗$ and the codomain of $⊗$ is a subset of $T$. Thus it suffices to show $(∀\bar{t}∈\bar{T})⋅α○β(\bar{t})=\bar{t}$. Toward that end, take $\bar{t}$. First, suppose $\bar{t}=⎨⎬$. I argue, in steps, that $α○β(⎨⎬)$ by the definition of $β$ equals $α(t^{o})$, which by the definition of $α$ equals $⎨⎬$. Second, suppose $\bar{t}⋅≠⋅⎨⎬$. Then it suffices to show that $(∀\bar{t}∈\bar{T})$ $(∀ℓ∈⎨1,2,...|\bar{t}|⎬)$ $(α○β(\bar{t}))_{ℓ}=\bar{t}_{ℓ}$. Toward this end, take $\bar{t}$ and $ℓ$. [i] First assume $ℓ<|\bar{t}|$. I will argue

[TABLE]

The first equality holds by the definition of $α$. The second equality holds because $k(β(\bar{t}))=|\bar{t}|$ by inspecting the definitions of $k$ and $β$. The third holds by the definition of $β$. The fourth holds by the definition of $p$. The fifth holds by $|t|{-}ℓ{-}1$ similar applications of the definition of $p$. The sixth is a rearrangement. The seventh holds by the definition of $q$. [ii] Second assume $ℓ=|\bar{t}|$. Then I will argue

[TABLE]

The first equality holds by the definition of $α$ and $ℓ=|\bar{t}|$. The second equality holds because $k(β(\bar{t}))=|\bar{t}|$ by inspecting the definitions of $k$ and $β$. The third is trivial. The fourth holds by the definitions of $q$ and $β$. $\Box$

Proof B.3** (for Theorem 3.2).**

(a). Lemma B.2 implies $\bar{τ}{:}T\textrightarrow\bar{T}$ is a bijection. Thus the assumptions of Lemma A.14 are met at $T′=\bar{T}$, $C′=C$, and $δ=\mathsf{id}_{C}$. Further, the definition of $\bar{⊗}$ here coincides with the definition of $⊗′$ in Lemma A.14. Therefore Lemma A.14 implies that $(\bar{T},C,\bar{⊗})$ is an $\mathbf{NCP}$ preform, and that $[(T,C,⊗),(\bar{T},C,\bar{⊗}),\bar{τ},\mathsf{id}_{C}]$ is an $\mathbf{NCP}$ isomorphism. Thus [Csq1] and [Csq2] remain to be shown.

For [Csq1], note that the definition of $\bar{T}$ implies that $\bar{T}$ is a collection of finite sequences. Further, since $t^{o}⋅∈⋅T$ by [P1], the definition of $\bar{T}$ implies that $(q○p^{k(t^{o})-ℓ}(t^{o}))^{k(t^{o})}_{ℓ=1}⋅∈⋅\bar{T}$. Thus, since $k(t^{o})=0$ by the definition of $k$, $(q○p^{0-ℓ}(t^{o}))^{0}_{ℓ=1}⋅∈⋅\bar{T}$. Thus $⎨⎬⋅∈⋅\bar{T}$.

For [Csq2], take $(\bar{t},c,\bar{t}^{\sharp})⋅∈⋅\bar{⊗}$. Then by the definition of $\bar{⊗}$, there are $t⋅∈⋅T$ and $t^{\sharp}⋅∈⋅T$ such that

$[$a$]$ $\bar{τ}(t)=\bar{t}$,

(2) $\bar{τ}(t^{\sharp})=\bar{t}^{\sharp}$, and

(3) $(t,c,t^{\sharp})⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$. $[$a$]$, 2, and the definition of $\bar{τ}$ imply

(4) $\bar{t}=(q○p^{k(t)-ℓ}(t))^{k(t)}_{ℓ=1}$ and

(5) $\bar{t}^{\sharp}=(q○p^{k(t^{\sharp})-ℓ}(t^{\sharp}))^{k(t^{\sharp})}_{ℓ=1}$. Also 3 and SP Proposition 3.1(b) imply

(6) $t=p(t^{\sharp})$ and

(7) $c=q(t^{\sharp})$. 6 and the definition of $k$ imply

(8) $k(t)=k(t^{\sharp}){-}1$. Finally, I argue, in steps, that $\bar{t}±(c)$ by 4 equals $(q○p^{k(t)-ℓ}(t))^{k(t)}_{ℓ=1}±(c)$, which by 6–8 equals $(q○p^{k(t^{\sharp})-1-ℓ}○p(t^{\sharp}))^{k(t^{\sharp})-1}_{ℓ=1}±(q(t^{\sharp}))$, which by rearrangement equals $(q○p^{k(t^{\sharp})-ℓ}(t^{\sharp}))^{k(t^{\sharp})-1}_{ℓ=1}±(q(t^{\sharp}))$, which by rearrangement equals $(q○p^{k(t^{\sharp})-ℓ}(p(t^{\sharp}))^{k(t^{\sharp})}_{ℓ=1}$, which by 5 equals $\bar{t}^{\sharp}$.

(b). By assumption, $(I,T,(C_{i})_{i∈I},⊗)$ is an $\mathbf{NCF}$ form. Thus [F1] implies $(T,∪_{i∈I}C_{i},⊗)$ is an $\mathbf{NCP}$ preform. Further, part (b) defines $\bar{T}$, $\bar{τ}$, and $\bar{⊗}$ as part (a) did. Thus part (a) implies

$[$1$]$ $(\bar{T},∪_{i∈I}C_{i},\bar{⊗})$ is a $\mathbf{CsqP}$ preform.

Meanwhile, Lemma B.2 implies $\bar{τ}{:}T\textrightarrow\bar{T}$ is a bijection. Thus the assumptions of Lemma A.15 are met at $I′=I$, $ι=\mathsf{id}_{I}$, $T′=\bar{T}$, $C′=∪_{i∈I}C_{i}$, and $δ=\mathsf{id}_{∪_{i∈I}C_{i}}$. Further, the definition of $\bar{⊗}$ here coincides with the definition of $⊗′$ in Lemma A.15. Also, the transparent definitions of $ι$ and $δ$ here, and the definition of $(C′_{i′})_{i′∈I′}$ in Lemma A.15, imply that $(C′_{i′})_{i′∈I′}=(C_{i})_{i∈I}$. Hence Lemma A.15 implies that

$[$1$]$ $(I,\bar{T},(C_{i})_{i∈I},\bar{⊗})$ is an $\mathbf{NCF}$ form, and

(2) $[(I,T,(C_{i})_{i∈I},⊗),$ $\!(I,\bar{T},(C_{i})_{i∈I},\bar{⊗}),$ $\!\mathsf{id}_{I},\bar{τ},$ $\!\mathsf{id}_{∪_{i∈I}C_{i}}]$ is an $\mathbf{NCF}$ isomorphism.

$[$1$]$ and $[$1$]$ imply that $(I,\bar{T},(C_{i})_{i∈I},\bar{⊗})$ is a $\mathbf{CsqF}$ form. This and 2 are part (b)’s conclusions. $\Box$

Lemma B.4**.**

Suppose $(T,C,⊗)$ is a $\mathbf{CsqP}$ preform. Then the following are equivalent.

• (a)

$(T,C,⊗)$* has no absentmindedness.*

• (b)

$(∄H∈{\mathcal{H}},t∈H,ℓ{<}|t|)⋅_{1}t_{ℓ}⋅∈⋅H$.

• (c)

$(∀t∈T,H∈{\mathcal{H}})⋅|⎨\,ℓ\,{:}\,1≤ℓ≤|t|,\,t_{ℓ}∈F(H)\,⎬|⋅≤⋅1$.282828The “ : ” replaces “$\,|\,$” for clarity.

• (d)

$(∀t∈T)⋅|R(t)|=|t|$.

• (e)

$R|_{T}$* is injective.*

Proof*.*

The lemma follows from Claims 5–7.

• Claim 1:

Not (a) $⇒$ not (b). Assume absentmindedness. Then there are

$[$a$]$ $H⋅∈⋅{\mathcal{H}}$,

(2) $t⋅∈⋅H$, and

(3) $s⋅∈⋅H$ such that

(4) $s⋅≺⋅t$. 4 and Proposition 3.1(i) imply

(5) $|s|<|t|$ and

(6) $s={{}_{1}t_{|s|}}$. 6 and 3 imply

(7) ${{}_{1}t_{|s|}}⋅∈⋅H$. $[$a$]$, 2, 5, and 7 show property (b) is violated at $ℓ=|s|$.

• Claim 2:

Not (b) $⇒$ not (c). Assume not (b). Then there is $H⋅∈⋅{\mathcal{H}}$,

$[$a$]$ $t⋅∈⋅H$, and

(2) $ℓ<|t|$ such that

(3) ${}_{1}t_{ℓ}⋅∈⋅H$. 2 implies $t_{ℓ+1}$ is well-defined; thus the definition of $F$ implies $t_{ℓ+1}⋅∈⋅F({{}_{1}t_{ℓ}})$; and thus 3 implies

(4) $t_{ℓ+1}⋅∈⋅F(H)$. 4 and $[$a$]$ imply $t_{ℓ+1}⋅∈⋅F(t)$; and thus $t^{*}=t±(t_{ℓ+1})$ is a member of $T$. Finally, I argue, in steps, that $|⎨ℓ′{:}1≤ℓ′≤|t^{*}|,t^{*}_{ℓ′}∈F(H)⎬|$ by 4 is at least $|⎨ℓ′{:}1≤ℓ′≤|t^{*}|,t^{*}_{ℓ′}{=}t_{ℓ+1}⎬|$, which by the construction of $t^{*}$ is at least $|⎨ℓ{+}1,|t|{+}1⎬|$, which by 2 is 2.

• Claim 3:

Not (c) $⇒$ not (d). Assume not (c). There there are $t⋅∈⋅T$ and $H⋅∈⋅{\mathcal{H}}$ such that $|⎨ℓ{:}1≤ℓ≤|t|,t_{ℓ}∈F(H)⎬|⋅≥⋅2$. Hence there are $ℓ$ and $ℓ′$ such that

$[$a$]$ $ℓ<ℓ′$,

(2) $t_{ℓ}⋅∈⋅F(H)$, and

(3) $t_{ℓ′}⋅∈⋅F(H)$. I argue in three steps that 3 by Proposition 3.1(b) implies $q({{}_{1}t_{ℓ′}})⋅∈⋅F(H)$, which by Proposition A.1(c) implies $p({{}_{1}t_{ℓ′}})⋅∈⋅H$, which by Proposition 3.1(b) implies

(4) ${}_{1}t_{ℓ′-1}⋅∈⋅H$. 2 and 4 imply $t_{ℓ}⋅∈⋅F(_{1}t_{t′-1})$. Thus $t^{*}={{}_{1}t_{ℓ′-1}}±(t_{ℓ})$ is a member of $T$. Further, $[$a$]$ implies $t^{*}_{ℓ}$ is well-defined and equal to $t_{ℓ}$. Thus $t^{*}_{ℓ}=t^{*}_{ℓ′}$. This and $[$a$]$ again imply $|R(t^{*})|<|t^{*}|$.

• Claim 4:

Not (d) $⇒$ not (a). Assume not (d). There there is $t⋅∈⋅T$ such that $|R(t)|⋅≠⋅|t|$. Since $|R(t)|>|t|$ is inconceivable, $|R(t)|<|t|$. Thus there are $ℓ$ and $ℓ′$ in $⎨1,2,...\,|t|⎬$ such that

$[$a$]$ $ℓ<ℓ′$ and

(2) $t_{ℓ}=t_{ℓ′}$. The definition of $F$ implies

(3) ${{}_{1}t_{ℓ-1}}⋅∈⋅F^{-1}(t_{ℓ})$ and

(4) ${{}_{1}t_{ℓ′-1}}⋅∈⋅F^{-1}(t_{ℓ′})$. 2 and 4 imply

(5) ${{}_{1}t_{ℓ′-1}}⋅∈⋅F^{-1}(t_{ℓ})$. [P3] implies

(6) $F^{-1}(t_{ℓ})⋅∈⋅{\mathcal{H}}$. Finally, $[$a$]$ implies $ℓ{-}1<ℓ′{-}1$; thus Proposition 3.1(i) implies

(7) ${{}_{1}t_{ℓ-1}}⋅≺⋅{{}_{1}t_{ℓ′-1}}$. 6, 3, 5, and 7 imply absentmindedness.

• Claim 5:

(a), (b), (c), and (d) are equivalent. This follows from Claims 1–4.

• Claim 6:

Not (d) $⇒$ not (e). Assume not (d). Then there is $t⋅∈⋅T$ such that $|R(t)|⋅≠⋅|t|$. Thus since $|R(t)|>|t|$ is inconceivable, $|R(t)|<|t|$. Thus there are $ℓ$ and $ℓ′$ in $⎨1,2,...\,|t|⎬$ such that

$[$a$]$ $ℓ<ℓ′$ and

(2) $t_{ℓ}=t_{ℓ′}$. $[$a$]$ and 2 imply $R({{}_{1}t_{ℓ′-1}})=R({{}_{1}t_{ℓ′}})$. Thus $R|_{T}$ is not injective.

• Claim 7:

Not (e) $⇒$ not (d). Assume not (e). Then $R|_{T}$ is not injective. Then there are $s$ and $t$ in $T$ such that

$[$a$]$ $s⋅≠⋅t$ and

(2) $R(s)=R(t)$.

On the one hand, suppose there is not an $ℓ$ in $⎨1,2,...\,\text{min}⎨|s|,|t|⎬⎬$ such that $s_{ℓ}⋅≠⋅t_{ℓ}$. Then

(3) ${}_{1}s_{\text{max}⎨|s|,|t|⎬}={{}_{1}t_{\text{max}⎨|s|,|t|⎬}}$. Thus $[$a$]$ implies $|s|⋅≠⋅|t|$. Hence $|s|<|t|$ or $|t|<|s|$. Without loss of generality assume

(4) $|s|<|t|$. Hence 3 implies

(5) $s={{}_{1}t_{|s|}}$. 4 implies $t_{|s|+1}$ exists. Thus 2 implies $s⋅≠⋅⎨⎬$ and there is

(6) $ℓ⋅∈⋅⎨1,2,...\,|s|⎬$ such that

(7) $s_{ℓ}=t_{|s|+1}$. But 5 implies $s_{ℓ}=t_{ℓ}$, and thus 7 implies $t_{ℓ}=t_{|s|+1}$. This and 6 imply $|R(t)|<|t|$. In other words, property (d) is violated.

On the other hand, suppose there is an $ℓ$ in $⎨1,2,...\,\text{min}⎨|s|,|t|⎬⎬$ such that $s_{ℓ}⋅≠⋅t_{ℓ}$. Let $j$ be the smallest such $ℓ$. Then

(8) ${}_{1}s_{j-1}={{}_{1}t_{j-1}}$ and

(9) $s_{j}⋅≠⋅t_{j}$. The definition of $F$ implies $s_{j}⋅∈⋅F({{}_{1}s_{j-1}})$ and $t_{j}⋅∈⋅F({{}_{1}t_{j-1}})$, and thus, 8 implies

(10) $⎨s_{j},t_{j}⎬⋅⊆⋅F({{}_{1}s_{j-1}})$. A fortiori 10 and [P3] imply there is $H⋅∈⋅{\mathcal{H}}$ such that ${{}_{1}s_{j-1}}⋅∈⋅H$. Hence 10 also implies

(11) $⎨s_{j},t_{j}⎬⋅⊆⋅F(H)$. Further, 2 and 9 imply there is $j^{*}⋅∈⋅⎨1,2,...\,|s|⎬$ such that

(12) $j^{*}⋅≠⋅j$ and

(13) $s_{j^{*}}=t_{j}$. 13 and 11 imply

(14) $⎨s_{j},s_{j^{*}}⎬⋅⊆⋅F(H)$. Finally, I argue that $|⎨\,ℓ\,{:}\,1≤ℓ≤|s|,s_{ℓ}∈F(H)\,⎬|$ is at least as great as $|⎨j,j^{*}⎬|$ by 14, which is 2 by 12. Thus the proposition’s property (c) is violated. So Claim 5((c)$⟺$(d)) implies property (d) is violated.

$\Box$

Appendix C $\mathbf{CsetF}$

Lemma C.1**.**

Suppose $C$ is a set, $t\,⊆\,C$, $c\,∈\,C$, and $t^{\sharp}\,⊆\,C$. Then the following are equivalent. (a) $c\,∉\,t$ and $t∪⎨c⎬\,{=}\,t^{\sharp}$. (b) $t\,≠\,t^{\sharp}$ and $t∪⎨c⎬\,{=}\,t^{\sharp}$. (c) $t\,≠\,t^{\sharp}$ and $t\,{=}\,t^{\sharp}⧷⎨c⎬$. (d) $t\,⊆\,t^{\sharp}$ and $⎨c⎬\,{=}\,t^{\sharp}⧷t$.

Proof*.*

(a)$⟺$(b). It suffices to show that if $t∪⎨c⎬=t^{\sharp}$, then $c⋅∉⋅t$ and $t⋅≠⋅t^{\sharp}$ are equivalent. Toward that end, assume $t∪⎨c⎬=t^{\sharp}$. Then both directions of the equivalence hold by inspection.

(b)$⟺$(c). It suffices to show that if $t⋅≠⋅t^{\sharp}$, then $t∪⎨c⎬=t^{\sharp}$ and $t=t^{\sharp}⧷⎨c⎬$ are equivalent. Toward that end, assume

$[$1$]$ $t⋅≠⋅t^{\sharp}$. For the forward direction, assume

(2) $t∪⎨c⎬=t^{\sharp}$. $[$1$]$, 2 imply

(3) $c⋅∉⋅t$. 2 implies $(t∪⎨c⎬)⧷⎨c⎬=t^{\sharp}⧷⎨c⎬$, and 3 implies the left-hand side is $t$. For the reverse direction, assume

(4) $t=t^{\sharp}⧷⎨c⎬$. $[$1$]$ and 4 imply

(5) $c⋅∈⋅t^{\sharp}$. 4 implies $t∪⎨c⎬=(t^{\sharp}⧷⎨c⎬)∪⎨c⎬$, and 5 implies the right-hand side is $t^{\sharp}$.

(a)$⟺$(d). Assume (a). That is, assume

$[$a$]$ $c⋅∉⋅t$ and

(2) $t∪⎨c⎬=t^{\sharp}$. 2 implies $t⋅⊆⋅t^{\sharp}$. Further, 2 implies $(t∪⎨c⎬)⧷t=t^{\sharp}⧷t$, and $[$a$]$ implies that the left-hand side is $⎨c⎬$. Conversely, assume (d). That is, assume

(3) $t⋅⊆⋅t^{\sharp}$ and

(4) $⎨c⎬=t^{\sharp}⧷t$. 4 implies $c⋅∉⋅t$. Further, 4 implies $t∪⎨c⎬=t∪(t^{\sharp}⧷t)$, and 3 implies the right-hand side is $t^{\sharp}$. $\Box$

Proof C.2** (for Proposition 4.1).**

The proposition if proved by Claims 1, 3, 5, 6, 9, 10, 11, 12, 14, 15, 16, 18, and 19.

• Claim 1:

(a) holds. Suppose [a] $t^{o}⋅≠⋅⎨⎬$. [Cset1] states [b] $⎨⎬⋅∈⋅T$. [a] and [b] imply $⎨⎬⋅∈⋅T⧷⎨t^{o}⎬$. Thus by [P1], there is $t⋅∈⋅T$ and $c⋅∈⋅C$ such that $(t,c,⎨⎬)⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$. Thus by [Cset2], $t∪⎨c⎬$ $=⎨⎬$. This implies $c⋅∈⋅⎨⎬$, which is impossible.

• Claim 2:

$⊗⋅⊆⋅⎨\,(t,c,t^{\sharp})∈T×C×T\,|\,c∉t,\,t∪⎨c⎬{=}t^{\sharp}\,⎬$. Take $(t,c,t^{\sharp})⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$. [P1] yields

$[$a$]$ $(t,c,t^{\sharp})⋅∈⋅T×C×T$. [P2] yields

(2) $t=p(t^{\sharp})$. Remark [ii] in the paragraph following SP equation (1) yields

(3) $p(t^{\sharp})⋅≠⋅t^{\sharp}$. 2 and 3 imply

(4) $t⋅≠⋅t^{\sharp}$. [Cset2] yields

(5) $t∪⎨c⎬{=}t^{\sharp}$. 4 and 5 yield

(6) $c⋅∉⋅t$. $[$a$]$, 6, and 5 are the desired results.

• Claim 3:

(b) holds. Take $t^{\sharp}⋅∈⋅T⧷⎨⎨⎬⎬$. Claim 1 (a) implies that $t^{\sharp}⋅∈⋅T⧷⎨t^{o}⎬$. Thus SP Proposition 3.1(a) implies that $(p(t^{\sharp}),q(t^{\sharp}),t^{\sharp})$ $∈$ $⊗$. Thus Claim 2 implies that $q(t^{\sharp})⋅∉⋅p(t^{\sharp})$ and $p(t^{\sharp})∪⎨q(t^{\sharp})⎬=t^{\sharp}$.

• Claim 4:

$(∀t∈T,∀m∈⎨0,1,2,...\,k(t)⎬)$ $|p^{m}(t)|=|t|\,{-}\,m$. Note by inspection, that Claim 3 (b) implies

$[$a$]$ $(∀t^{\sharp}∈T⧷⎨⎨⎬⎬)$ $|p(t^{\sharp})|=|t^{\sharp}|{-}1$. To prove the present claim, take $t⋅∈⋅T$. I will show $(∀m∈⎨0,1,2,...\,k(t)⎬)$ $|p^{m}(t)|=|t|\,{-}\,m$ by induction. For the initial step ($m{=}0$), $|p^{0}(t)|=|t|=|t|{-}0=|t|{-}m$ by inspection. For the inductive step ($m≥1$), I first note that by assumption $m⋅≤⋅k(t)$, which trivially implies $m{-}1<k(t)$, which by the definition of $k$ implies $p^{m-1}(t)⋅≠⋅t^{o}$, which by Claim 1 (a) implies

(2) $p^{m-1}(t)⋅≠⋅⎨⎬$. I then argue, in steps, that $|p^{m}(t)|$ by rearrangement equals $|p○p^{m-1}(t)|$, which by 2 and $[$a$]$ at $t^{\sharp}=p^{m-1}(t)$ equals $|p^{m-1}(t)|-1$, which by the inductive hypothesis equals $(|t|{-}(m{-}1))-1$, which by rearrangement equals $|t|-m$.

• Claim 5:

(c) holds. Take $t⋅∈⋅T$. Note [a] $|p^{k(t)}(t)|=|t|\,{-}\,k(t)$ by Claim 4 at $m\,{=}\,k(t)$. Also note [b] $|p^{k(t)}(t)|=|t^{o}|=|⎨⎬|=0$ by the definition of $k(t)$ and by Claim 1 (a). [a] and [b] imply $|t|\,{-}\,k(t)=0$. Hence $|t|=k(t)$.

• Claim 6:

(d) holds. Take $t⋅∈⋅T$. I will use induction on $m⋅∈⋅⎨0,1,...\,|t|⎬$. For the initial step ($m{=}0$), $p^{m}(t)=p^{0}(t)=t$ and $t⧷p^{m}(t)=t⧷p^{0}(t)=t⧷t=⎨⎬=⎨\,q○p^{n}(t)\,|\,0{>}n≥0\,⎬=⎨\,q○p^{n}(t)\,|\,m{>}n≥0\,⎬$. For the inductive step ($m≥1$), note $m⋅≤⋅|t|$ by assumption; which implies $m{-}1<|t|$; which implies $m{-}1<k(t)$ by Claim 5 (c); which implies $p^{m-1}(t)⋅≠⋅t^{o}$ by the definition of $k$; which implies $p^{m-1}(t)⋅≠⋅⎨⎬$ by Claim 1 (a). Hence, Claim 3 (b) at $t^{\sharp}=p^{m-1}(t)$ implies $q○p^{m-1}(t)⋅∉⋅p○p^{m-1}(t)$ and $p○p^{m-1}(t)∪⎨q○p^{m-1}(t)⎬=p^{m-1}(t)$. By Lemma C.1(a)$⟺$(d), this is equivalent to $p○p^{m-1}(t)⋅⊆⋅p^{m-1}(t)$ and $p^{m-1}(t)⧷p○p^{m-1}(t)=⎨q○p^{m-1}(t)⎬$. By a small rearrangement, this is equivalent to

(3) $p^{m}(t)⋅⊆⋅p^{m-1}(t)$ and

(4) $p^{m-1}(t)⧷p^{m}(t)$ $=$ $⎨q○p^{m-1}(t)⎬$. Meanwhile, the inductive hypothesis is

(5) $p^{m-1}(t)⋅⊆⋅t$ and

(6) $t⧷p^{m-1}(t)$ $=$ $⎨\,q○p^{n}(t)\,|\,m{-}1{>}n≥0\,⎬$. 3 and 5 imply

(7) $p^{m}(t)⋅⊆⋅t$. 3 and 5 also imply

(8) $t⧷p^{m}(t)$ $=$ $(t⧷p^{m-1}(t))⋅∪⋅(p^{m-1}(t)⧷p^{m}(t))$. 8, 6, and 4 imply

(9) $t⧷p^{m}(t)$ $=$ $⎨\,q○p^{n}(t)\,|\,m{-}1{>}n≥0\,⎬$ $∪$ $⎨q○p^{m-1}(t)⎬$. The right-hand side of 9 is equal to $⎨\,q○p^{n}(t)\,|\,m{-}1≥n≥0\,⎬$, which is equal to $⎨\,q○p^{n}(t)\,|\,m{>}n≥0\,⎬$. Hence 9 is equivalent to

(10) $t⧷p^{m}(t)$ $=$ $⎨\,q○p^{n}(t)\,|\,m{>}n≥0\,⎬$. 7 and 10 are the desired results.

• Claim 7:

$(∀t^{A}∈T,t^{B}∈T)$ $t^{A}⋅≺⋅t^{B}$ $⇒$ $t^{A}⋅⊊⋅t^{B}$. Suppose $t^{A}⋅≺⋅t^{B}$. Then the definitions of $≺$ and $k$ imply there is

$[$a$]$ $m⋅∈⋅⎨1,2,...\,k(t^{B})⎬$ such that

(2) $t^{A}=p^{m}(t^{B})$. $[$a$]$ and Claim 5 (c) imply $m⋅∈⋅⎨1,2,...\,|t^{B}|⎬$. Thus Claim 6 (d) at $t=t^{B}$ implies

(3) $p^{m}(t^{B})⋅⊆⋅t^{B}$ and

(4) $t^{B}⧷p^{m}(t^{B})=⎨\,q○p^{n}(t^{B})\,|\,m{>}n≥0\,⎬$. Since $m⋅≥⋅1$ by $[$a$]$, $⎨\,q○p^{n}(t^{B})\,|\,m{>}n≥0\,⎬$ is nonempty. Thus 3 and 4 imply $p^{m}(t^{B})⋅⊊⋅t^{B}$. Thus 2 implies $t^{A}⋅⊊⋅t^{B}$.

• Claim 8:

$(∀t^{A}∈T,t^{B}∈T)$ $t^{A}⋅≼⋅t^{B}$ $⇒$ $t^{A}⋅⊆⋅t^{B}$. Suppose $t^{A}⋅≼⋅t^{B}$. Then the definition of $≼$ implies $t^{A}⋅≺⋅t^{B}$ or $t^{A}=t^{B}$. The first implies $t^{A}⋅⊆⋅t^{B}$ by Claim 7. The second implies $t^{A}⋅⊆⋅t^{B}$ trivially.

• Claim 9:

(e) holds. Take $t⋅∈⋅T$. I argue, in steps, that $t$ trivially equals $t⧷⎨⎬$, which by Claim 1 (a) equals $t⧷t^{o}$, which by the definition of $k$ equals $t⧷p^{k(t)}(t)$, which by Claim 5 (c) equals $t⧷p^{|t|}(t)$, which by Claim 6 (d) at $m=|t|$ equals $⎨\,q○p^{n}(t)\,|\,|t|{>}n≥0\,⎬$

• Claim 10:

(f) holds. Forward direction. Take $c⋅∈⋅C$. By [P3], $F^{-1}(c)$ is a member of a partition, and thus, it is nonempty. Take $t^{*}⋅∈⋅F^{-1}(c)$. By [P1], $t^{*}⊗c⋅∈⋅T$. Thus by [Cset2], $t^{*}∪⎨c⎬⋅∈⋅T$. Thus $c$ belongs to an element of $T$. Reverse direction. Take any $t$. [Cset1] implies that $t$ is a set. Take $b⋅∈⋅t$. By Claim 9 (e), there is $n$ such that $b=q○p^{n}(t)$. Thus, since the codomain of $q$ is $C$, $b⋅∈⋅C$.

• Claim 11:

(g) holds. Suppose there were $H⋅∈⋅{\mathcal{H}}$,

$[$a$]$ $t^{A}⋅∈⋅H$, and

(2) $t^{B}⋅∈⋅H$ such that

(3) $t^{A}⋅≺⋅t^{B}$. 3 and the definition of $≺$ imply there is

(4) $m>1$ such that

(5) $t^{A}=p^{m}(t^{B})$. 4 and 5 imply $t^{A}=p○p^{m-1}(t^{B})$. Thus [P2]’s definition of $p$ implies there is $c⋅∈⋅C$ such that

(6) $(t^{A},c,p^{m-1}(t^{B}))⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$. Thus the definition of $F$ implies $c⋅∈⋅F(t^{A})$. This, $[$a$]$, 2, and SP Proposition 3.2(16a) imply $c⋅∈⋅F(t^{B})$. Thus the definition of $F$ implies there is $t^{\star}⋅∈⋅T$ such that $(t^{B},c,t^{\star})⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$. This and Claim 2 implies

(7) $c⋅∉⋅t^{B}$. But, 6 and Claim 2 imply

(8) $c⋅∈⋅p^{m-1}(t^{B})$. And, the definition of $≼$ implies $p^{m-1}(t^{B})⋅≼⋅t^{B}$, and thus Claim 8 implies

(9) $p^{m-1}(t^{B})⋅⊆⋅t^{B}$. 8 and 9 imply $c⋅∈⋅t^{B}$, which contradicts 7.

• Claim 12:

(h) holds. Suppose $|t∩F(H)|⋅≥⋅2$. Then by Claim 9 (e), there exist distinct $m′$ and $m$ such that $⎨⋅q○p^{m′}(t),⋅q○p^{m}(t)⋅⎬$ $⊆$ $F(H)$. Thus by Lemma A.1(c),

$[$a$]$ $⎨⋅p^{m′+1}(t),⋅p^{m+1}(t)⋅⎬$ $⊆⋅H$. Without loss of generality assume $m′>m$. Then $p^{m′+1}(t)=p^{m′-m}○p^{m+1}(t)$. Hence

(2) $p^{m′+1}(t)⋅≺⋅p^{m+1}(t)$ by the definition of $≺$. $[$a$]$ and 2 show there is absentmindedness, which contradicts Claim 11 (g).

• Claim 13:

$(∀t^{A}∈T,t^{B}∈T)$ $t^{A}⋅⊊⋅t^{B}$ implies $(∀m∈⎨0,1,...\,|t^{A}|⎬)$ $p^{m}(t^{A})$ $=$ $p^{m+|t^{B}|-|t^{A}|}(t^{B})$. Suppose

$[$1$]$ $t^{A}⋅⊊⋅t^{B}$. I will use induction on $m$.

For the initial step, assume

(2) $m=|t^{A}|$. I argue, in steps, that $p^{m}(t^{A})$ by 2 equals $p^{|t^{A}|}(t^{A})$, which by Claim 5 (c) equals $p^{k(t^{A})}(t^{A})$, which by the definition of $k$ equals $t^{o}$, which by the definition of $k$ again equals $p^{k(t^{B})}(t^{B})$, which by Claim 5 (c) again equals $p^{|t^{B}|}(t^{B})$, which by manipulation equals $p^{|t^{A}|+|t^{B}|-|t^{A}|}(t^{B})$, which by 2 again equals $p^{m+|t^{B}|-|t^{A}|}(t^{B})$.

For the inductive step, assume

(3) $m<|t^{A}|$. (The next two sentences concern $p^{m}(t^{A})$ alone.) 3 and Claim 5 (c) imply $m<k(t^{A})$, which by the definition of $k$ implies $p^{m}(t^{A})⋅≠⋅t^{o}$. This and SP Proposition 3.1(a) at $t^{\sharp}=p^{m}(t^{A})$ yield

(4)

$p^{m+1}(t^{A})⋅⊗⋅q○p^{m}(t^{A})=p^{m}(t^{A})$.

(The next three sentences concern $p^{m+|t^{B}|-|t^{A}|}(t^{B})$ alone.) 3 and manipulation imply $m{+}|t^{B}|{-}|t^{A}|<|t^{A}|{+}|t^{B}|{-}|t^{A}|=|t^{B}|$, which by Claim 5 (c) implies $m{+}|t^{B}|{-}|t^{A}|<k(t^{B})$, which by the definition of $k$ implies $p^{m{+}|t^{B}|{-}|t^{A}|}(t^{B})⋅≠⋅t^{o}$. This and SP Proposition 3.1(a) at $t^{\sharp}=p^{m{+}|t^{B}|{-}|t^{A}|}(t^{B})$ yield

(5)

$p^{m+1+|t^{B}|-|t^{A}|}(t^{B})⋅⊗⋅q○p^{m+|t^{B}|-|t^{A}|}(t^{B})=p^{m+|t^{B}|-|t^{A}|}(t^{B})$.

Since the inductive hypothesis is $p^{m+1}(t^{A})=p^{m+1+|t^{B}|-|t^{A}|}(t^{B})$, 5 yields

(6)

$p^{m+1}(t^{A})⋅⊗⋅q○p^{m+|t^{B}|-|t^{A}|}(t^{B})=p^{m+|t^{B}|-|t^{A}|}(t^{B})$.

4, 6, and the definition of $F$ yield

(7) $⎨⋅q○p^{m}(t^{A}),⋅q○p^{m+|t^{B}|-|t^{A}|}(t^{B})⋅⎬$ $⊆$ $F(p^{m+1}(t^{A}))$. Also, Claim 9 (e) and $[$1$]$ yield

(8) $q○p^{m}(t^{A})⋅∈⋅t^{A}⋅⊆⋅t^{B}$. Also, Claim 9 (e) yields

(9) $q○p^{m+|t^{B}|-|t^{A}|}(t^{B})⋅∈⋅t^{B}$. 7, 8, 9, and Claim 12 (h) imply

(10) $q○p^{m}(t^{A})=q○p^{m+|t^{B}|-|t^{A}|}(t^{B})$.

Finally, I argue, in steps, that $p^{m}(t^{A})$ by 4 equals $p^{m+1}(t^{A})⊗q○p^{m}(t^{A})$, which by 10 equals $p^{m+1}(t^{A})$ $⊗$ $q○p^{m+|t^{B}|-|t^{A}|}(t^{B})$, which by 6 equals $p^{m+|t^{B}|-|t^{A}|}(t^{B})$.

• Claim 14:

(i) holds. This follows from Claim 13 at $m=0$.

• Claim 15:

(j) holds. Because of Claim 7, it suffices to show the reverse direction. Toward that end, suppose

$[$1$]$ $t^{A}⋅⊊⋅t^{B}$. $[$1$]$ and Claim 14 (i) imply $t^{A}=p^{|t^{B}|-|t^{A}|}(t^{B})$. Further, $[$1$]$ and [Cset1] imply $|t^{B}|{-}|t^{A}|>0$. The last two sentences and the definition of $≺$ imply $t^{A}⋅≺⋅t^{B}$.

• Claim 16:

(k) holds. Because of Claim 8, it suffices to show the reverse direction. Toward that end, suppose $t^{A}⋅⊆⋅t^{B}$. Then either $t^{A}⋅⊊⋅t^{B}$ or $t^{A}=t^{B}$. In the first case, Claim 15 (j) implies $t^{A}⋅≼⋅t^{B}$. In the second case, $t^{A}⋅≼⋅t^{B}$ holds trivially by the definition of $≼$.

• Claim 17:

$(∀t∈T,c∈C,t^{\sharp}∈T)$ ($c\,∉\,t$ and $t∪⎨c⎬\,{=}\,t^{\sharp}$) $⇒$ $(t,c)\,{=}\,(p(t^{\sharp}),q(t^{\sharp}))$. Suppose

$[$a$]$ $c⋅∉⋅t$ and

(2) $t∪⎨c⎬=t^{\sharp}$. $[$a$]$ and 2 imply

(3) $t⋅⊊⋅t^{\sharp}$ and

(4) $|t^{\sharp}|{-}|t|=1$. 3 and Claim 14 (i) at $(t^{A},t^{B})=(t,t^{\sharp})$ imply $t=p^{|t^{\sharp}|-|t|}(t^{\sharp})$. This and 4 imply

(5) $t=p(t^{\sharp})$. Further, 3 implies

(6) $t^{\sharp}⋅≠⋅⎨⎬$. I then argue, in steps, that $⎨c⎬$ by $[$a$]$–2 equals $t^{\sharp}⧷t$, which by 5 equals $t^{\sharp}⧷p(t^{\sharp})$, which by 6 and Claim 3 (b) equals $⎨q(t^{\sharp})⎬$. Thus

(7) $c=q(t^{\sharp})$. 5 and 7 are the required results.

• Claim 18:

(l) holds. By Claim 2, it suffices to show the reverse direction. Toward that end, suppose [a] $c⋅∉⋅t$ and [b] $t∪⎨c⎬=t^{\sharp}$. [b] implies $t^{\sharp}⋅≠⋅⎨⎬$. Thus Claim 1 (a) implies $t^{\sharp}⋅≠⋅t^{o}$. Thus SP Proposition 3.1(a) implies [c] $p(t^{\sharp})⊗q(t^{\sharp})=t^{\sharp}$. Also, [a], [b], and Claim 17 imply [d] $(t,c)=(p(t^{\sharp}),q(t^{\sharp}))$. [c] and [d] imply $t⊗c=t^{\sharp}$.

• Claim 19:

(m) holds. I argue, in three steps, that $(t,c)⋅∈⋅F\mspace{1.0mu}^{\mathsf{gr}}$ by [P1] is equivalent to [a] $(t,c)∈T×C$ and [b] $(∃t^{\sharp}∈T)\,(t,c,t^{\sharp})∈⊗\mspace{1.0mu}^{\mathsf{gr}}$, which by Claim 18 (l) is equivalent to [a] and [b$′$] $(∃t^{\sharp}∈T)\,c\,∉\,t$ and $t∪⎨c⎬\,{=}\,t^{\sharp}$, which by rearrangement is equivalent to [a] and [b$″$] $c\,∉\,t$ and $t∪⎨c⎬\,∈\,T$.

$\Box$

Proof C.3** (for Theorem 4.2).**

(a). Lemma B.4[(a)$⇒$(e)] implies $R|_{\bar{T}}{:}\bar{T}\textrightarrow T$ is a bijection. Thus the assumptions of Lemma A.14 are met at [1] its $(T,C,⊗)$ equal to $(\bar{T},\bar{C},\bar{⊗})$ here, [2] its $τ{:}T\textrightarrow T′$ equal to $R|_{\bar{T}}{:}\bar{T}\textrightarrow T$ here, and [3] its $δ{:}C\textrightarrow C′$ equal to $\mathsf{id}_{\bar{C}}{:}\bar{C}\textrightarrow\bar{C}$ here. Further, the definition of $⊗′$ in the lemma coincides with the definition of $⊗$ here. Therefore the lemma implies that $(T,\bar{C},⊗)$ is an $\mathbf{NCP}$ preform, and that $[(\bar{T},\bar{C},\bar{⊗}),(T,\bar{C},⊗),R|_{\bar{T}},\mathsf{id}_{\bar{C}}]$ is an $\mathbf{NCP}$ isomorphism. Thus it remains to show that $(T,\bar{C},⊗)$ is a $\mathbf{CsetP}$ preform. By definition, it suffices to show [Cset1] and [Cset2].

For [Cset1], first note that $\bar{T}$ is a collection of (finite) sequences by assumption. Hence $T$ is a collection of finite sets by the definitions of $T$ and $R$. Further, $⎨⎬$ belongs to $\bar{T}$ by [Csq1]. Hence $R(⎨⎬)=⎨⎬$ belongs to $T$.

For [Cset2], take $(t,\bar{c},t^{\sharp})⋅∈⋅⊗\mspace{1.0mu}^{\mathsf{gr}}$. Then by the definition of $⊗$, there are $\bar{t}⋅∈⋅\bar{T}$ and $\bar{t}^{\sharp}⋅∈⋅\bar{T}$ such that

$[$a$]$ $R(\bar{t})=t$,

(2) $R(\bar{t}^{\sharp})=t^{\sharp}$, and

(3) $(\bar{t},\bar{c},\bar{t}^{\sharp})⋅∈⋅\bar{⊗}$. 3 and [Csq2] implies

(4) $\bar{t}±(\bar{c})=\bar{t}^{\sharp}$. Finally, I argue, in steps, that $t∪⎨\bar{c}⎬$ by $[$a$]$ equals $R(\bar{t})∪⎨\bar{c}⎬$, which by inspection equals $R(\bar{t}±(\bar{c}))$, which by (4) equals $R(\bar{t}^{\sharp})$, which by 2 equals $t^{\sharp}$.

(b). Lemma B.4[(a)$⇒$(e)] implies $R|_{\bar{T}}{:}\bar{T}\textrightarrow T$ is a bijection. Thus the assumptions of Lemma A.15 are met at [1] its $(I,T,(C_{i})_{i∈I},⊗)$ equal to $({\bar{I}},\bar{T},(\bar{C}_{\bar{i}})_{{\bar{i}}∈{\bar{I}}},\bar{⊗})$ here, [2] its $ι{:}I\textrightarrow I′$ equal to $\mathsf{id}_{{\bar{I}}}{:}{\bar{I}}\textrightarrow{\bar{I}}$ here, [3] its $τ{:}T\textrightarrow T′$ equal to $R|_{\bar{T}}{:}\bar{T}\textrightarrow T$ here, and [4] its $δ{:}∪_{i∈I}C_{i}\textrightarrow C′$ equal to $\mathsf{id}_{∪_{{\bar{i}}∈{\bar{I}}}\bar{C}_{\bar{i}}}{:}∪_{{\bar{i}}∈{\bar{I}}}\bar{C}_{\bar{i}}\textrightarrow∪_{{\bar{i}}∈{\bar{I}}}\bar{C}_{\bar{i}}$ here. Also, the definition of $⊗′$ in Lemma A.15 coincides with the definition of $⊗$ here. Also, the transparent definitions of $δ$ and $ι$ here, and the definition of $(C′_{i′})_{i′∈I′}$ in Lemma A.15, imply $(C′_{i′})_{i′∈I′}$ there equals $(\bar{C}_{\bar{i}})_{{\bar{i}}∈{\bar{I}}}$ here. Hence Lemma A.15 implies that $({\bar{I}},T,(\bar{C}_{\bar{i}})_{{\bar{i}}∈{\bar{I}}},⊗)$ is an $\mathbf{NCF}$ form, and that $[({\bar{I}},\bar{T},(\bar{C}_{\bar{i}})_{{\bar{i}}∈{\bar{I}}},\bar{⊗}),$ $\!({\bar{I}},T,(\bar{C}_{\bar{i}})_{{\bar{i}}∈{\bar{I}}},⊗),$ $\!\mathsf{id}_{{\bar{I}}},R|_{\bar{T}},\mathsf{id}_{∪_{{\bar{i}}∈{\bar{I}}}C_{\bar{i}}}]$ is an $\mathbf{NCF}$ isomorphism.

It remains to show that $({\bar{I}},T,(\bar{C}_{\bar{i}})_{{\bar{i}}∈{\bar{I}}},⊗)$ is a $\mathbf{CsetF}$ form. Since the previous paragraph showed that it is an $\mathbf{NCF}$ form, it suffices to show that its preform $(T,∪_{{\bar{i}}∈{\bar{I}}}\bar{C}_{\bar{i}},⊗)$ is an $\mathbf{CsetP}$ preform. By assumption, $(\bar{T},∪_{{\bar{i}}∈{\bar{I}}}\bar{C}_{\bar{i}},\bar{⊗})$ is a $\mathbf{CsqP_{\tilde{a}}}$ preform. Thus the assumption of part (a) is met at $(\bar{T},\bar{C},\bar{⊗})=(\bar{T},∪_{{\bar{i}}∈{\bar{I}}}\bar{C}_{\bar{i}},\bar{⊗})$. Further, part (b) defines $T$ and $⊗$ just as part (a) does. Hence part (a) implies $(T,∪_{{\bar{i}}∈{\bar{I}}}\bar{C}_{\bar{i}},⊗)$ is an $\mathbf{CsetP}$ preform. $\Box$