Papers With

← All papers
First page of Baire measurable functions and automorphisms of the truth-table degrees

Baire measurable functions and automorphisms of the truth-table degrees

Bjørn Kjos-Hanssen

math.LO Oct 12, 2026 · v1
formalization logic ai-agents
Read PDF arXiv abstract Code
TL;DR
The main results were formalized in Lean 4 using Harmonic's Aristotle, with the code in a public GitHub repository.
Abstract
We show that if an automorphism $π$ of the truth-table degrees is induced by a Baire measurable function $F\colon 2^ω\to 2^ω$, or merely induced on some comeager set by a continuous function, then $π$ is the identity. The same results hold for the weak truth-table degrees. The argument is an adaptation to truth-table reducibility of OpenAI's recent proof that the Turing degrees are rigid.
Problem

Whether automorphisms of the truth-table degrees can be nontrivial when induced by well-behaved functions. The question follows the recent proof that the Turing degrees are rigid.

Approach

The coding lemma from the Turing-degree rigidity proof is adapted to truth-table reducibility. Comeager sets and a Baire-category uniformity lemma replace Cohen forcing, and the group structure of the 2-adic integers is used. The relevant sets are closed, which gives an elementary proof in the continuous case. The main results were formalized in Lean 4 with Aristotle.

Results

Any automorphism of the tt-degrees induced by a Baire measurable function, or induced on a comeager set by a continuous function, is the identity. The same holds for the wtt-degrees. Under ZF+AD, every automorphism of the tt-degrees is trivial.