CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Two maximal elements and no greatest element

Statement refuted

Refuted claim: in every poset a maximal element is a greatest element, so that having nothing strictly above it forces an element to lie above everything (FALSE: every maximal element is a greatest element, Maximal element and greatest element).

The witness is

$P = P ({1, 2}) ∖ {{1, 2}} = {\emptyset, {1}, {2}},$

ordered by inclusion (Partial order and partially ordered set). Both ${1}$ and ${2}$ are maximal in $P$ , neither is greatest, and $P$ has no greatest element at all.

Facts & Assumptions

Given: $P = P ({1, 2}) ∖ {{1, 2}} = {\emptyset, {1}, {2}}$ , ordered by inclusion; every member of $P$ is a subset of ${1, 2}$ , and ${1, 2} \notin P$ .

[L1]

$m$ is maximal in $P$ when no $x \in P$ satisfies $m < x$ , and greatest when $x \leq m$ for every $x \in P$ (Maximal element and greatest element).

[L2]

A partial order is reflexive, antisymmetric and transitive, and it need not make every two elements comparable; $x < y$ abbreviates $x \leq y$ together with $x \neq y$ (Partial order and partially ordered set).

Counterexample

technique · direct

1.1

Inclusion is reflexive, antisymmetric and transitive on any collection of sets, so $(P, \subseteq)$ is a poset, and it has the three elements $\emptyset$ , ${1}$ , ${2}$ , which are pairwise distinct.

givenL2

1.2

${1}$ and ${2}$ are incomparable: $1 \notin {2}$ gives ${1} \subseteq̸ {2}$ , and $2 \notin {1}$ gives ${2} \subseteq̸ {1}$ .

givenL2

2.1

${1}$ is maximal: if $x \in P$ and ${1} \subseteq x$ then $1 \in x$ , and of the three members of $P$ only ${1}$ contains $1$ , so $x = {1}$ ; hence no $x \in P$ satisfies ${1} ⊊ x$ .

step 1.1L1

2.2

${2}$ is maximal, by the same argument with $2$ in place of $1$ : the only member of $P$ containing $2$ is ${2}$ .

step 1.1L1

2.3

Neither of them is greatest: ${2} \subseteq̸ {1}$ , so ${1}$ fails to dominate ${2}$ , and symmetrically ${2}$ fails to dominate ${1}$ .

step 1.2L1

2.4

$P$ has no greatest element at all: a greatest $M \in P$ would satisfy ${1} \subseteq M$ and ${2} \subseteq M$ , hence ${1, 2} \subseteq M$ ; but $M \subseteq {1, 2}$ , so $M = {1, 2}$ , which is not a member of $P$ .

step 1.1givenL1

3.1

So $(P, \subseteq)$ is a poset with two maximal elements and no greatest element, which refutes the claim: having nothing strictly above it does not force an element to lie above everything.

step 2.1step 2.2step 2.3step 2.4∎

Remarks

This witness is not the smallest one. The refutation in FALSE: every maximal element is a greatest element uses a two element antichain, which is minimal, but not for the reason one might expect: the empty poset satisfies the claim vacuously, having no maximal element at all, while a one element poset satisfies it outright, since its single element is maximal and is greatest by reflexivity. Two elements is therefore the least size at which the claim can fail, and it does fail there. Vacuous satisfaction is not confined to the empty poset, incidentally: $(N, \leq)$ has no maximal element either ( $(N, \leq)$ has no maximal element: Zorn's chain hypothesis fails), and satisfies the claim for that reason. The witness here adds a least element $\emptyset$ below both maximal elements, which matters because it shows the failure is not caused by the poset splitting into unrelated pieces. Even a poset with a bottom, in which every element is comparable to something, can carry several maximal elements.
The general pattern. Order the proper subsets of a set $X$ with at least two elements by inclusion. The maximal elements are exactly the sets $X ∖ {x}$ for $x \in X$ : any proper $A ⊊ X$ sits inside $X ∖ {x}$ for any $x \in X ∖ A$ , and nothing lies strictly between $X ∖ {x}$ and $X$ . Distinct points give distinct maximal elements, so there is one for each point of $X$ , and there is no greatest element. The poset above is the case $X = {1, 2}$ .
What would rescue the claim is totality. In a totally ordered set a maximal element is greatest, since every other element is comparable to it and cannot be strictly above it, which is why the confusion survives in intuition trained on $R$ .
Maximality says nothing about comparability: here each maximal element is incomparable to the other, and both are above only $\emptyset$ . Applications of Zorn's lemma must therefore be arranged so that "nothing is strictly above it" already means "it cannot be extended", since nothing stronger is available.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Greatest element and least element (Wikipedia) (standard reference, not scraped)
Maximal and minimal elements (Wikipedia) (standard reference, not scraped)
Partially ordered set (Wikipedia) (standard reference, not scraped)