Mathematical Logic

Introduction

The Cook-Levin theorem states that CNF SAT is NP-complete. This mission formalizes the theorem over a multi-tape Turing machine model in Lean 4.

Main Goal

Prove CookLevin.cook_levin_theorem:

$$NPComplete SAT$$

under the decider and reduction hypotheses.

Motivation

In 1998 Smale listed eighteen problems for the twenty-first century; the eighteenth asks: What are the limits of intelligence, both artificial and human? (Smale 1998). The paper of Acharjee and Gogoi (arXiv:2310.10792) proposes a mathematical model of a mind, the cognitive-consequence space, built from a Tarski consequence operator, and claims that two theorems about this model (its Theorems 3.3 and 3.4) show that "human intelligence is limitless" (Discussion, p. 22; Conclusion, p. 23).

This mission records that model and its results in Lean 4 exactly as stated, so that each claim becomes a checkable statement: proved, or refuted, by the verifier rather than by argument.

Setting

A cognitive-consequence space is a set $C$ of mental representations (thoughts) with a consequence operator $\mathrm{Cn} : \mathcal P(C) \to \mathcal P(C)$ and an implication connective $X \Rightarrow Y$ satisfying Tarski's axioms as listed in the paper (p. 5):

1. $C$ is countable;
2. $A \subseteq \mathrm{Cn}(A)$;
3. $A \subseteq B \Rightarrow \mathrm{Cn}(A) \subseteq \mathrm{Cn}(B)$;
4. $\mathrm{Cn}(\mathrm{Cn}(A)) = \mathrm{Cn}(A)$;
5. if $X \in \mathrm{Cn}(A)$ then $X \in \mathrm{Cn}(B)$ for some finite $B \subseteq A$;
6. if $Y \in \mathrm{Cn}(A \cup \{X\})$ then $(X \Rightarrow Y) \in \mathrm{Cn}(A)$;

together with the paper's standing assumption $\mathrm{Cn}(\varnothing) \neq \varnothing$ (p. 5, after Definition 3.2).

A set $A$ is deductive if $\mathrm{Cn}(A) = A$. The cognitive-consequence topology is

$$\tau = \{A \subseteq C : \mathrm{Cn}(C \setminus A) = C \setminus A\},$$

and members of $\tau$ are consequence-wise open (CWO). The cognitive closure $\mathrm{Cl}^{\square}(A)$ is the intersection of all deductive sets containing $A$.

Separately, a cognitive similarity distance is a function $\mathrm{Cog} : C \times C \to [0,1]$ together with a relation $x \approx y$ ("$x$ and $y$ cognitively coincide") such that $\mathrm{Cog}(x,y) = 0 \iff x \approx y$, $\mathrm{Cog}$ is symmetric, $x \approx z \Rightarrow \mathrm{Cog}(x,y) = \mathrm{Cog}(z,y)$, and the triangle inequality holds. A sequence of thoughts $(x_n)$ converges to $x$ if for every $\varepsilon \in (0,1)$ we have $\mathrm{Cog}(x, x_n) < \varepsilon$ for all large $n$.

Formalization targets

Goal: "human intelligence is limitless" (Theorems 3.3 and 3.4)

For every cognitive-consequence space,

$$\Bigl(\exists f \in C\ \forall A \in \tau,\ f \notin A\Bigr) \ \wedge\ \Bigl(\exists f \in C\ \exists A \in \tau,\ f \in A\Bigr).$$

Milestones

Theorems 3.1, 3.2, 3.3, 3.5, 3.6, 3.7 and Corollary 3.5 (the topology $\tau$ and the cognitive closure), Theorems 3.8 and 3.12 (cognitive limits), Theorem 4.3 (the filter $f_d$) and Theorem 5.1 (Gödel's incompleteness black hole).

Significance

The paper presents the goal as its answer to the human-intelligence half of Smale's eighteenth problem. A machine-checked verdict on the goal settles whether that conclusion follows from the paper's own axioms. The milestones are the paper's structural results about $\tau$, cognitive closure and cognitive limits.

Status: to the best of current knowledge none of these results has a published machine-checked proof. The first conjunct of the goal (Theorem 3.3) follows from the standing assumption $\mathrm{Cn}(\varnothing) \neq \varnothing$. The second conjunct (Theorem 3.4) is not implied by the listed axioms as formalized: the consequence operator with $\mathrm{Cn}(A) = C$ for every $A$, on a one-point language, satisfies all of them and has $\tau = \{\varnothing\}$. The goal is therefore expected to be resolved by a disproof.

Difficulty

The content of the goal is the existence of a nonempty CWO set, equivalently of a deductive set different from $C$ (a consistent theory). The paper's argument for Theorem 3.4 derives $\bigcap_i A_i = \varnothing$ and calls this a contradiction; nothing in the axioms forbids it.

Formalization scope

• CogCons.CognitiveConsequenceSpace C bundles $\mathrm{Cn}$, the connective imp, axioms (i)–(vi) and $\mathrm{Cn}(\varnothing) \neq \varnothing$. The syntax $\sigma$ and interpretation $I$ of the paper are not modelled beyond imp.
• The paper also asserts $\mathrm{Cn}(C) \neq C$ (p. 5). This contradicts axiom (ii), since $C \subseteq \mathrm{Cn}(C) \subseteq C$; including it would make every statement vacuously true, so it is omitted. For the same reason the second half of Corollary 3.4 ($\mathrm{Cl}^{\square}(C) \neq C$) is not included.
• Theorem 4.4 (the family $\{A : f \in \mathrm{Cn}(A)\}$ is a filter) is not included: closure under intersection fails in a four-element model satisfying all the axioms.
• Results relying on informal notions (the practical topology of Section 2, Theorems 3.9–3.11 and 3.13, Theorems 4.1–4.2, and the "solution space" of Section 5) are not formalized.
• CogCons.CognitiveSimilarityDistance C is independent of $\mathrm{Cn}$; sequences are indexed by $\mathbb N$ starting at $0$; $\approx$ is an arbitrary relation constrained only by the listed axioms.

Selected references

• S. Acharjee, U. Gogoi, The limit of human intelligence, arXiv:2310.10792v2 [math.GM], 2023. https://arxiv.org/abs/2310.10792
• S. Smale, Mathematical problems for the next century, The Mathematical Intelligencer 20(2), 7–15, 1998. https://doi.org/10.1007/BF03025291

Motivation

How large can the power set of an infinite set be? For a regular cardinal $\kappa$ (one that is not the supremum of fewer than $\kappa$ smaller ordinals) the answer is: almost anything. Easton's theorem (1970) shows that the function $\kappa \mapsto 2^{\kappa}$ on regular cardinals can be prescribed arbitrarily in any model of ZFC, subject only to monotonicity and König's inequality $\operatorname{cf}(2^{\kappa}) > \kappa$. For a long time it was expected that singular cardinals — those that are such a supremum, like $\aleph_{\omega}$ — would behave the same way.

They do not. In 1974 Jack Silver proved that the Generalized Continuum Hypothesis cannot fail for the first time at a singular cardinal of uncountable cofinality: if $2^{\alpha} = \alpha^{+}$ for every infinite $\alpha < \kappa$ and $\operatorname{cf}\kappa > \omega$, then $2^{\kappa} = \kappa^{+}$. This was the first ZFC theorem constraining the continuum function at singular cardinals, and it opened the area now called the singular cardinal problem.

A short timeline:

• 1970 — Easton: the continuum function on regular cardinals is essentially arbitrary.
• 1974 — Silver (ICM Vancouver): GCH cannot first fail at a singular cardinal of uncountable cofinality; more generally the Singular Cardinal Hypothesis is decided at cofinality $\omega$.
• 1975 — Galvin and Hajnal: elementary inequalities for cardinal powers at singular cardinals of uncountable cofinality.
• 1976–77 — Baumgartner and Prikry, and independently Jensen, give elementary (non-forcing, non-ultrapower) proofs of Silver's theorem; the proof reproduced in Jech's Chapter 8 is of this kind.
• 1977 — Magidor: it is consistent, relative to large cardinals, that GCH holds below $\aleph_{\omega}$ while $2^{\aleph_{\omega}} > \aleph_{\omega+1}$ — so Silver's restriction to uncountable cofinality is necessary.
• 1980s onwards — Shelah's pcf theory, whose flagship result $\aleph_{\omega}^{\aleph_0} < \aleph_{\omega_4}$ (when $\aleph_\omega$ is a strong limit) grows out of exactly the stationary-set machinery assembled here.

This mission is the first in a series formalizing Thomas Jech, Set Theory (Third Millennium Edition, Springer 2003). It covers Chapter 8, "Stationary Sets" (pp. 91–98).

Setting

Fix a regular uncountable cardinal $\kappa$ and regard it as the well-ordered set of ordinals below it. A set $C \subseteq \kappa$ is closed unbounded, or a club, if it is unbounded in $\kappa$ and contains all of its limit points below $\kappa$ (an ordinal $\alpha > 0$ is a limit point of $C$ when $\sup(C \cap \alpha) = \alpha$). A set $S \subseteq \kappa$ is stationary if $S \cap C \neq \emptyset$ for every club $C$. Clubs are closed under intersections of fewer than $\kappa$ of them, so they generate a $\kappa$-complete filter, the club filter; its dual is the nonstationary ideal.

The club filter has a second closure property with no analogue for ordinary filters. The diagonal intersection of a $\kappa$-indexed family is

$$\mathop{\triangle}_{\alpha<\kappa} X_\alpha \;=\; \Bigl\{ \xi < \kappa \;:\; \xi \in \bigcap_{\alpha<\xi} X_\alpha \Bigr\},$$

and a filter closed under diagonal intersections is called normal. A function $f$ defined on $S \subseteq \kappa$ is regressive if $f(\alpha) < \alpha$ for all nonzero $\alpha \in S$.

For cardinal arithmetic, $\operatorname{cf}\kappa$ denotes the cofinality of $\kappa$ (the least length of an unbounded sequence in $\kappa$), $\kappa^{+}$ the cardinal successor, and $\kappa$ is singular when $\operatorname{cf}\kappa < \kappa$. The Singular Cardinal Hypothesis (SCH) is the assertion that $\kappa^{\operatorname{cf}\kappa} = \kappa^{+}$ for every singular $\kappa$ with $2^{\operatorname{cf}\kappa} < \kappa$. A sequence of cardinals is normal if it is strictly increasing and continuous at limits.

Formalization targets

Goal — Silver's theorem (Jech 8.12)

$$\kappa \text{ singular},\ \operatorname{cf}\kappa > \omega,\ \bigl(\forall \alpha \ \aleph_0 \le \alpha < \kappa \Rightarrow 2^{\alpha} = \alpha^{+}\bigr) \;\Longrightarrow\; 2^{\kappa} = \kappa^{+}.$$

This is the weakest statement of the chapter that still needs the full machinery: it fixes no particular $\kappa$ and no particular cofinality, and it stays correct no matter how the singular cardinal problem develops above it.

Milestones, in dependency order

1. Lemma 8.4 — the diagonal intersection of $\kappa$ clubs is a club; equivalently the club filter is normal.
2. Theorem 8.7 (Fodor) — a regressive function on a stationary set is constant on a stationary subset.
3. Theorem 8.10 (Solovay) — every stationary subset of $\kappa$ is the union of $\kappa$ pairwise disjoint stationary sets.
4. Lemma 8.14 — if $\langle \kappa_\alpha\rangle$ is normal with limit $\kappa$, $\lambda^{\operatorname{cf}\kappa} < \kappa$ for $\lambda < \kappa$, and $\{\alpha : \kappa_\alpha^{\operatorname{cf}\kappa_\alpha} = \kappa_\alpha^{+}\}$ is stationary in $\operatorname{cf}\kappa$, then $\kappa^{\operatorname{cf}\kappa} = \kappa^{+}$.
5. Theorem 8.13 (Silver) — SCH at every cardinal of cofinality $\omega$ implies SCH everywhere.

Significance

Silver's theorem is the boundary between the two halves of cardinal arithmetic. Above it sit the ZFC theorems of pcf theory; below it sit the consistency results (Magidor, Prikry, Radin forcing) that show how much freedom is left, and they are confined to cofinality $\omega$ precisely because Theorems 8.12 and 8.13 close off everything else. Its proof also packages tools used throughout set theory: the normality of the club filter, Fodor's pressing-down lemma, and the technique of bounding almost disjoint families of functions by a stationary-set argument.

Formalization status: Mathlib already has clubs and stationary sets in an arbitrary well-ordered type (IsClub, IsStationary), with the finite and $<\kappa$-indexed intersection lemmas — Jech's Lemma 8.2 and Theorem 8.3. It does not have diagonal intersections, Fodor's theorem, Solovay's splitting theorem, or any singular cardinal arithmetic beyond the definitions of regular and singular cardinals. Each milestone below is therefore a genuine addition, and the first three are reusable well outside this mission.

Difficulty

The naive route to the goal — induct on $\alpha < \kappa$ and pass to the limit — fails immediately: $2^{\kappa}$ for singular $\kappa$ is not determined by the values $2^{\alpha}$ for $\alpha < \kappa$ in any elementary way; that is exactly the content of the independence results. What the proof must do instead is bound the number of functions on $\operatorname{cf}\kappa$, and it gets that bound from a stationary set rather than from a club: uncountable cofinality is what makes the set of relevant stages stationary, and stationarity is what survives the diagonal argument. Cofinality $\omega$ breaks this at the first step, since every subset of $\omega$ that is unbounded is already a club and Fodor's theorem is empty.

The two hard pieces are Lemma 8.14 and, inside it, Lemma 8.16: given an almost disjoint family $F$ of functions with $f(\alpha) \in A_\alpha$ and $|A_\alpha| \le \aleph_\alpha$ on a stationary set of $\alpha$, one must show $|F| \le \aleph_{\omega_1}$ by assigning to each $f$ a pair (stationary set, bounded restriction) and checking the assignment is injective. That argument uses Fodor's theorem on a set of functions, and the bookkeeping does not simplify.

Formalization scope

The ambient order is Mathlib's type of ordinals below a cardinal, k.ord.ToType (written Below k in the mission's definition bundle); clubs and stationary sets are Mathlib's IsClub and IsStationary on that type, so a set is closed in the sense of being closed under suprema of directed subsets — equivalent, for a well-order with the order topology, to Jech's "contains its limit points". Families indexed by "$\alpha < \kappa$" are functions out of that same type, which is what makes the diagonal intersection typecheck without a side condition. Cardinal exponentiation, cofinality (Ordinal.cof of k.ord) and the successor cardinal (Order.succ) are Mathlib's.

One trivializing formalization is ruled out explicitly: the GCH hypothesis of the goal is stated for infinite cardinals $\alpha < \kappa$ only. Quantified over all cardinals it would be unsatisfiable — $2^{2} = 4 \neq 3 = 2^{+}$ — and Silver's theorem would become vacuous.

A complete development needs: diagonal intersections and the normality of the club filter; Fodor's theorem; the sets $E^{\kappa}_{\lambda} = \{\alpha < \kappa : \operatorname{cf}\alpha = \lambda\}$ and their stationarity; Solovay's splitting theorem via Lemmas 8.8 and 8.9; almost disjoint families of ordinal functions and the counting Lemmas 8.15 and 8.16; and Theorem 5.22(ii) on cardinal powers, which Jech's proof of Theorem 8.13 cites. Contributions of any of these as separate reductions are welcome, as are alternative proofs of the goal (for instance via a generic elementary embedding) that bypass some of the chain.

Selected references

• Thomas Jech, Set Theory, The Third Millennium Edition, revised and expanded. Springer Monographs in Mathematics, Springer, 2003 (ISBN 3-540-44085-2). Chapter 8, "Stationary Sets", pp. 91–98 — the source of every statement in this mission.
• Jack Silver, On the singular cardinals problem. Proceedings of the International Congress of Mathematicians (Vancouver, 1974), vol. 1, pp. 265–268.
• William B. Easton, Powers of regular cardinals. Annals of Mathematical Logic 1 (1970), pp. 139–178.
• Fred Galvin and András Hajnal, Inequalities for cardinal powers. Annals of Mathematics 101 (1975), pp. 491–498.
• James E. Baumgartner and Karel Prikry, Singular cardinals and the generalized continuum hypothesis. American Mathematical Monthly 84 (1977), pp. 108–113.
• Menachem Magidor, On the singular cardinals problem I. Israel Journal of Mathematics 28 (1977), pp. 1–31.

Comparing undecidable problems

Computability theory studies which questions admit algorithms and how the unsolvable questions compare with one another. A decision problem can be represented by a set of natural numbers: the question on input $n$ is whether $n$ belongs to the set. Even when there is no algorithm that always answers this question, there may be an algorithm that eventually recognizes every positive instance. Understanding the relative difficulty of such problems is the setting of the Friedberg–Muchnik theorem.

The original paper by Richard M. Friedberg appeared in 1957 under the title Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944). It supplies the historical paper source for this formalization. A. A. Muchnik's independent contribution appeared in Russian in 1956. Friedberg, PNAS 43(2), 236–238; Muchnik, Math-Net bibliography, 1956 entry.

Sets, enumeration, and oracle access

A set $A\subseteq\mathbb N$ is computably enumerable, abbreviated c.e., if membership has a semidecision procedure: on input $n$, the procedure halts exactly when $n\in A$. The older terminology is recursively enumerable, abbreviated r.e. The Lean predicate CEnumerable A uses Mathlib's REPred for this property. A computable set has a decision procedure that terminates on every input and answers membership correctly; this is expressed separately by ComputableSet A using ComputablePred.

For each set $A$, define its characteristic function by

$$\chi_A(n)=\begin{cases}1&n\in A,\\0&n\notin A.\end{cases}$$

An oracle for $A$ answers requests for this function's values. It always supplies an answer, even if membership in $A$ cannot be computed without an oracle. The declaration setOracle A represents this total function inside Mathlib's type of partial functions from natural numbers to natural numbers.

Write $A\le_T B$ when an algorithm with access to the membership oracle for $B$ computes $\chi_A$ on every input. This is Turing reducibility, expressed by SetTuringReducible A B. The algorithm may make several queries, with later queries depending on earlier answers. Incomparability requires both $A\not\le_T B$ and $B\not\le_T A$; it is stronger than saying the two sets merely have different degrees. These conventions specify the mathematical reading of the supplied Lean definitions.

Formalization target

The goal is the following unconditional existence statement:

$$\exists A,B\subseteq\mathbb N,\qquad A\text{ is c.e.}\ \land\ B\text{ is c.e.}\ \land\ A\not\le_T B\ \land\ B\not\le_T A.$$

Its Lean name is Computability.friedberg_muchnik. No enumeration, pair of sets, or oracle program is supplied as a hypothesis. Both sets must be obtained as witnesses to the conclusion. The statement matches Theorem 26.2 in Arnold W. Miller's Lecture notes in Recursion Theory, Section 26, with the theorem on page 51 and its proof on pages 51–54. Miller, December 3, 2008 version.

Mathematical and formal significance

The target establishes that the c.e. problems have incomparable levels of computational difficulty. Its witnesses cannot be computable: a computable membership procedure would also work in the presence of any other oracle simply by making no queries, contradicting the required nonreducibility. The stronger historical consequence is a positive solution of Post's problem: a c.e. degree can lie strictly between the computable degree and the halting degree. Miller records this consequence separately as Corollary 26.3 on page 54. Miller, Section 26.

The mathematical theorem is established; the work requested here is its Lean 4 formalization. A completed development must construct witnesses, prove their computable enumerability, and exclude oracle computations in each direction using Mathlib's actual reducibility relation. The provided goal currently ends in sorry. Successful compilation of this statement checks its formulation and imports; it does not constitute a proof of the existence result.

Difficulty of simultaneous requirements

The main obstacle is preserving decisions about oracle computations while both sets are still being enumerated. An additional element in one set can change an oracle answer used by an earlier computation, undermining the attempt to separate the other set from it. There are infinitely many candidate programs in both directions. Thus a formal treatment has to justify the eventual stability of the relevant computations as well as the effectiveness of the enumeration. This is the setting of the finite injury argument developed in Miller's proof of Theorem 26.2. Miller, pages 51–54.

Formalization scope

The sets are arbitrary Set ℕ, including the natural number zero in their ambient domain. The oracle answers use natural numbers, with one for membership and zero for nonmembership. Classical reasoning is used to define the oracle for an arbitrary set; it supplies no assertion that this function is computable. Each oracle is nevertheless total. Replacing it with a partial membership recognizer would change the meaning of the target.

The foundation consists of Mathlib.Computability.RE and Mathlib.Computability.TuringDegree, together with the supplied definitions in namespace Computability. SetTuringEquivalent records reducibility in both directions. degreeOfSet maps a characteristic-function oracle to its Turing degree, and CEnumerableDegree says that a degree has a c.e. representative. These additional definitions are retained as useful interfaces, while the root theorem itself is expressed directly with sets and TuringIncomparable.

A complete proof will need representations of effective finite stages and oracle computations, and lemmas relating those representations to the imported predicates. Such infrastructure can support later formalizations involving oracle use, computable enumerations, and priority constructions. Contributions should establish these connections with Mathlib's definitions and finish the unconditional target. The theorem must not be replaced by mere degree inequality, weakened reducibility, or a conditional assertion that assumes the required incomparable sets already exist.

Selected references

• Richard M. Friedberg, Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944), Proceedings of the National Academy of Sciences of the USA 43(2), 236–238, 1957. DOI; free archived paper.
• A. A. Muchnik, On the unsolvability of the problem of reducibility in the theory of algorithms (Russian: Неразрешимость проблемы сводимости теории алгоритмов), Doklady Akademii Nauk SSSR 108(2), 194–197, 1956. Math-Net bibliography, 1956 entry.
• Arnold W. Miller, Lecture notes in Recursion Theory, University of Wisconsin–Madison, version dated December 3, 2008, Section 26, Theorem 26.2, pages 51–54. Author-hosted PDF.