Published package / CLIR
stacks.sets
v0.1.0Set Theory
A package can be printed as a standalone module in a general-purpose language that answers without the rules engine: an answer and its status, with no proof, hashes or canonical document. Everything on this page comes from the generation plan built with the index; the gallery computes nothing of its own.
Generation plan
The plan builds: the package can be printed as a module.
- plan format
- law-backend-plan/0.7
- capabilities
- base layer only
Checked against package scenarios
Not checked: the package scenarios have not been run against generated modules. A plan that builds does not yet show that the answers coincide.
Target languages
bslcsdarterlexgojavaktluaphppyrbrsscalaswiftts
./law dev backend corpus/clir/stacks-sets.lawir.json --target ts --target py --target go --out DIR
Module interface
Questions are public relations with a producing rule; inputs are the facts a question reads. Function names follow the language: ask_… in Python, ask.… in TypeScript, Ask… in Go.
Questions · 5
| Name | Parameters | Meaning | Reads | Sources |
|---|---|---|---|---|
| countable | text | 000D: the set is countable | at_most_aleph_nullcardinality_of | tag/000D |
| exists_ordinal_of_large_cofinality | text | 05N3: there exists an ordinal whose cofinality is bigger than the cardinal — the cofinality of an ordinal being the least cardinality of a cofinal subset of it (000E) | infinite | tag/05N3tag/000E |
| lies_in_some_stage | text | 000C: the set is an element of \(V_alpha\) for some ordinal \(alpha\) | element_ofhas_rankis_ordinalis_partial_universeis_setstage_of | tag/000Ctag/000B |
| product_is | text, text, text | 000D: the cardinal product of the first two cardinals equals the third: \(k (x) l = m\), the cardinality of the product | at_leastinfinite | tag/000D |
| sum_is | text, text, text | 000D: the cardinal sum of the first two cardinals equals the third: \(k (+) l = m\), the cardinality of the disjoint union | at_leastinfinite | tag/000D |
Inputs · 10
| Name | Parameters | Meaning |
|---|---|---|
| at_least | text, text | 000D: the first cardinal is greater than or equal to the second in the well-ordering of the ordinals: \(k >= l\) |
| at_most_aleph_null | text | 000D: the cardinal is at most \(aleph_0\) |
| cardinality_of | text, text | 000D: the cardinality of the set is the cardinal — the least ordinal admitting a bijection with the set, written \(k = |s|\) |
| element_of | text, text | 000B: the set is an element of the partial universe: \(s\) in \(V_alpha\) |
| has_rank | text, text | 000B: the rank of the set is the ordinal — the least \(alpha\) such that \(s\) is an element of \(V_{alpha+1}\) |
| infinite | text | 000D: the cardinal is infinite — it is at least the first infinite cardinal \(aleph_0 = omega\) |
| is_ordinal | text | 05N1: the set is an ordinal — transitive and well-ordered by the membership relation |
| is_partial_universe | text | 000B: the set is a partial universe — a suitably large set of the form \(V_alpha\), transitive by construction |
| is_set | text | 0009: the object is a set — every mathematical object unravels into a set |
| stage_of | text, text | 000B: the partial universe is the stage of the given ordinal: \(v = V_alpha\), defined by transfinite recursion \(V_0 = 0\), \(V_{alpha+1} = P(V_alpha)\), \(V_alpha\) = union of earlier stages at a limit |