Some of the strangest implications of AC are the "infinite hat" puzzles, which are on Wikipedia, and have been talked about on MO several times, including some variants.
There are different ways to formalize these puzzles, but most of them follow the same basic principle:
- There is a countably-indexed sequence of things (reals, naturals, bits, etc).
- You only have information about some partial subsequence: usually with one value missing, or an initial segment missing, etc.
- You get to use the axiom of choice to "mysteriously" infer some value from the original sequence that isn't in your partial subsequence.
- Informally, this inference can be made to agree with the original "arbitrarily often", such as failing in only a finite set of cases, despite having no knowledge of what the original sequence was.
The basic gist is usually that you use AC to get a "chosen" representative from each equivalence class of sequences with the same infinite "tail." Then, for your partial sequence, you interpolate some missing value based on what the representative says. This strategy is correct for all but a finite set of cases in some initial segment, leading to bizarre consequences.
My question:
It would be interesting to see what happens if you take, as an axiom, the deliberate negation that "infinite hat" puzzles admit any such strategy, and see how strong it is compared to just the negation of $AC$.
The simplest way to formalize this, that I can think of, is as follows:
- Let $a$ be some sequence $\Bbb N \to S$, for some arbitrary set $S$.
- For some $k \in \Bbb N$, let the knockout sequence $a \setminus k$ be the restriction of $a$ to the domain $\Bbb N \setminus k$. (i.e., one (index, value) pair is missing)
- Let an interpolation function be some $f$ that takes as input some $a \setminus k$, and returns some value $s \in S$, which we interpret as its "suggestion" for the missing value at $k$.
- For any such interpolation function $f$ and sequence $a$, we can define an agreement sequence $A_{f,a}[k]$, for which $A_{f,a}[k] = 1$ if $f(a \setminus k) = a[k]$ and $A_{f,a} = 0$ otherwise.
- Likewise, we can define the agreement set $A_{f,a} = \{k: A_{f,a}[k] = 1\}$, the set of indices for which the agreement sequence is 1.
AC, then, says that for each choice of $S$, there exists an interpolation function $f$ such that for all $S$-sequences $a$, $A_{f,a}[k]$ is eventually constant at 1. Just let $f(a \setminus k) = r(a)[k]$, where $r(a)$ is the chosen representative from the equivalence class for $a$.
However, our negation can be much stronger: we can declare that no interpolation function $f$ can be guaranteed, for all sequences $a$, to have an agreement set with natural density greater than $1/|S|$ if $S$ is finite, or $0$ if it is infinite. That is, any such $f$ may do better for some particular sequence $a$, but cannot be guaranteed to do better for all $a$.
For uncountable $S$ we can get even stronger: not only should the natural density of the agreement set be $0$, but the agreement set can never be guaranteed to even be any larger than the empty set for all $a$. That is, given a sequence of reals, there can be no interpolator $f$ that is guaranteed, for all such sequences, to interpolate even one missing value correctly.
There is probably some better way to formalize the above, but at least it isn't that complicated, and formalizes the basic reservation that people often have with infinite hat puzzles. So I'm simply interested in what set theory looks like if we take that perspective and formalize it.
- Have axioms similar to these been studied?
- Are they known to be equivalent to, to imply, or to be implied by other well-known axioms that are incompatible with AC?
- Is there some simpler way to formalize the above?