GPT 6 Astra Ultra attempt on Math-1148

MSO alternation hierarchy over pictures

Definitions and mathematical statement

A picture over a fixed finite alphabet $A$ is a map $P:[h]\times[w]\to A$, where $h,w\ge1$ and $[h]=\{1,\ldots,h\}$. Regard it as a finite relational structure with horizontal and vertical successor relations and one unary predicate for each letter. Monadic second-order logic (MSO) permits quantification over cells and over sets of cells. A $\Sigma_k$ MSO sentence has at most $k$ alternating blocks of set quantifiers, beginning existentially, followed by a first-order formula; first-order quantifiers inside that formula do not count as set alternations.

Fix a class $\mathcal B$ of balanced pictures. Strictness asks, for every $k\ge1$, for a language $L\subseteq\mathcal B$ definable by a $\Sigma_{k+1}$ sentence but by no $\Sigma_k$ sentence on $\mathcal B$. The source asks this for linearly and polynomially balanced rectangles. To make the balance uniform, take fixed constants $C\ge1,d\ge1$ and require \[ \max(h,w)\le C\min(h,w)^d. \] Investigate strictness for these fixed classes, separating $d=1$ from $d>1$; square pictures $h=w$ are the basic special case. This explicit family of balance conventions resolves the source's unspecified polynomial. Allowing a different bound for each picture would impose no restriction. Equivalence of sentences is tested only on the chosen class of pictures.

Short English statement

Does each additional alternation of set quantifiers express genuinely new properties even for pictures whose two side lengths remain comparable?

Research attempt

Scope and method.

This research attempt by GPT-6 Astra Ultra is dated 2 October 2026. It preserves the catalogue statement and distinguishes elementary proofs below from cited prior work. No novelty claim or formal proof-assistant verification is made. The final paragraph states the precise remaining scope. The finite checks described below are reproducible in scripts/check_attempt_batch03_root_2026_10_02.py.

A restriction that destroys familiar witnesses.

The constants $C,d$ are fixed for the class, rather than chosen separately for each rectangle. The source discussion [S2] describes known hierarchy witnesses on very unbalanced rectangles, whose long side grows as an exponential tower in the short side. Restricting such a witness language to the balanced class is not a proof of separation on that class. We make the obstruction precise and isolate a valid first-level transfer argument.

Finite picture languages are first-order.

For any particular finite picture with $N$ cells, quantify first-order variables $x_1,\ldots,x_N$. Require them to be pairwise distinct and require every cell to equal one of them. For every ordered pair of these variables, specify whether the horizontal and vertical successor relations hold, and specify each cell's letter predicates. This sentence characterizes the picture up to isomorphism. A finite disjunction characterizes any finite language of pictures. It uses no set quantifiers at all. In particular, every property restricted to a bounded total number of cells is first-order definable; inspecting a finite collection of pictures cannot prove a strict set-quantifier hierarchy.

Applying the lemma to tower-shaped supports.

Suppose a proposed separator is supported on rectangles of dimensions $n$ by $f(n)$, where $f(n)\ge2^n$ for all sufficiently large $n$. Balance would require $f(n)\le Cn^d$ once $f(n)\ge n$. But $2^n/(Cn^d)$ tends to infinity for fixed $C,d$. There are therefore only finitely many admissible values of $n$. Over a fixed finite alphabet, those finitely many shapes admit only finitely many pictures. The restricted language is first-order by the preceding lemma, no matter how high its unrestricted alternation complexity was. For the concrete support $f(n)=2^n$, $C=1,d=2$, the admissible positive integers are exactly $2,3,4$. At $n=5$ the inequality fails, and the ratio $2^n/n^2$ is strictly increasing for $n\ge3$, since $2n^2>(n+1)^2$ there. This small example exhibits the loss of the unbounded witness parameter explicitly.

What complement nonclosure really gives.

Let $\mathcal B$ be a fixed class of pictures. Assume a language $L\subseteq\mathcal B$ has an existential MSO definition $\exists X_1\cdots\exists X_s\,\varphi$, with $\varphi$ first-order, and that its complement inside $\mathcal B$ has no such definition. That complement is defined by $\forall X_1\cdots\forall X_s\,\neg\varphi$. Prefixing an unused existential set variable puts it in $\Sigma_2$. Hence this nonclosure hypothesis implies $\Sigma_1\ne\Sigma_2$ on the class. The source reports the relevant nonclosure result for squares; this paragraph proves the logical implication, not that imported result. The identical transfer works at any level if nonclosure at that level is known. Nonclosure at level one alone does not give the required hypothesis at every later level.

The padding gap.

One might place a thin witness rectangle in a much larger square and mark the active region. To transfer a lower bound, however, one must pull every hypothetical low-alternation definition on the padded objects back to one on the original rectangles without increasing the number of set-quantifier blocks. Merely encoding the rectangle injectively does not supply that translation. Sets quantified over the large padding can contain many more independent bits than sets on the original domain. No suitable alternation-preserving interpretation is constructed here.

Verification and final status.

The root script checks the explicit exponential-versus-square example; the monotonicity and finite-language arguments prove its tail and its logical consequence. The attempt establishes why direct restriction fails and gives a conditional separation lemma. It does not construct a balanced separator at each level, so the full hierarchy question remains unresolved here.

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, supplied problems.json, record 3341 (OPG-37448), OpenGarden collection. Catalogue identity and source transcription; CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Open Problem Garden, MSO alternation hierarchy over pictures. Original problem and discussion; the mathematical formulation below is expanded from the supplied source record. http://www.openproblemgarden.org/op/mso_alternation_hierarchy_over_pictures.