Erdős problem 623

Let $X$ be a set of cardinality $\aleph_\omega$ and $f$ a function from the finite subsets of $X$ to $X$ such that $f(A)\not\in A$ for all $A$ . Must there exist an infinite independent $Y\subseteq X$ , i.e. with $f(B)\not\in Y$ for all finite $B\subset Y$ ? Claimed resolution: the positive assertion is equivalent to Koepke's free-subset property, hence independent of ZFC, with consistency strength exactly a measurable cardinal.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

623.lean

Retained formal statement1 of 1

Let $X$ be a set of cardinality $\aleph_\omega$ and $f$ be a function from the finite subsets of $X$ to $X$ such that $f(A)\not\in A$ for all $A$ . Must there exist an infinite $Y\subseteq X$ that is independent - that is, for all finite $B\subset Y$ we have $f(B)\not\in Y$ ?

FormalConjectures/ErdosProblems/623.leanErdos623.erdos_6234 linesExact file

1True ↔2  ∀ (X : Type u),3    Cardinal.mk X = Cardinal.aleph Ordinal.omega0 →4      ∀ (f : Finset X → X), (∀ (A : Finset X), f A ∉ A) → ∃ Y, Y.Infinite ∧ ∀ (B : Finset X), ↑B ⊆ Y → f B ∉ Y

OpenStatement only, no proof