Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-06 (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.

Sets aa and bb with P(a)P(b)P(ab)\mathcal{P}(a) \cup \mathcal{P}(b) \subsetneq \mathcal{P}(a \cup b)

Statement refuted

Refuted claim: P(a)P(b)=P(ab)\mathcal{P}(a) \cup \mathcal{P}(b) = \mathcal{P}(a \cup b) for all sets aa and bb. The witness is a:={}a := \{\varnothing\} and b:={{}}b := \{\{\varnothing\}\}, for which the inclusion from left to right is proper: aba \cup b is a subset of aba \cup b, so it lies in the right-hand side, but it is a subset of neither aa nor bb.

Facts & Assumptions

Given: a:={}a := \{\varnothing\} and b:={{}}b := \{\{\varnothing\}\}.

[L3]

zP(x)z \in \mathcal{P}(x) holds if and only if zxz \subseteq x (The power set P(x)={z:zx}\mathcal{P}(x) = \{\, z : z \subseteq x \,\}).

[L5]

{x,y}\{x,y\} is the set whose elements are exactly xx and yy, and {x}:={x,x}\{x\} := \{x,x\} (The unordered pair {x,y}\{x,y\} and the singleton {x}={x,x}\{x\} = \{x,x\}).

[L7]

Counterexample

technique · direct
1.1

Neither of the two sets is included in the other. The only element of aa is \varnothing and the only element of bb is {}\{\varnothing\}, and these differ because {}\{\varnothing\} has an element while \varnothing has none; so a\varnothing \in a with b\varnothing \notin b, and {}b\{\varnothing\} \in b with {}a\{\varnothing\} \notin a.

L4L5L7
2.1

The general inclusion holds, and it is an equality exactly when one of the two sets is included in the other; by step 1.1 that fails here, so the inclusion is proper.

L1L2step 1.1
3.1

The witnessing element is aba \cup b itself: it is a subset of aba \cup b, hence an element of P(ab)\mathcal{P}(a \cup b), whereas abaa \cup b \subseteq a would force bab \subseteq a and abba \cup b \subseteq b would force aba \subseteq b, both excluded by step 1.1; so aba \cup b is in neither P(a)\mathcal{P}(a) nor P(b)\mathcal{P}(b).

L3L4L6L8step 1.1step 2.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 17 results over 7 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources