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.
Finite-Support Iterations and Martin's Axiom: Examples and Counterexamples
1 · Prerequisites
- Areas of Elementary Plane Figures
- Arithmetization, Incompleteness, and Relative Consistency
- Binary Operations, Monoids, Groups and Subgroups
- Boolean Algebras, Stone Duality, and the Prime Ideal Theorem
- Cardinal Arithmetic, Cofinality and the Alephs
- Compactness
- Compactness in Metric Spaces
- Complete Metrizability, Čech-Completeness, and Baire Category
- Completeness, Completion, and Uniform Continuity
- Condensation, GCH, and Diamond in L
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Countability and Uncountability
- Deduction, Soundness, Completeness, and Compactness
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite-Support Iterations and Martin's Axiom
- Forcing Orders, Names, and Generic Extensions
- Formal Set-Theoretic Syntax, Structures, and Satisfaction
- Foundations of the Real Numbers for Analysis
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Measures and Their Basic Properties
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Outer Measure and the Caratheodory Extension Theorem
- Preservation, Cohen Forcing, and the Continuum
- Reflection, Absoluteness, and Elementary Submodels
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Series: Convergence and the Nonnegative Tests
- Set-Theoretic Trees, Delta Systems, and Diamond
- Sigma Algebras and Borel Sets
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Arithmetical Hierarchy and Post's Theorem
- The Constructible Hierarchy and Inner Models
- The Forcing Theorem and Formal Consistency Transfer
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Well-Founded Relations, Rank, and the Cumulative Hierarchy
2 · Summary
The two-step Cohen example writes down the product isomorphism. Two MA examples build a real outside a small listed family and specialize the category and measure union theorems to small sets of reals.
The final false statement is separated from the valid implication : the bookkeeping model satisfies MA and not CH, so the converse fails relative to the same explicit consistency assumptions.
The consistency implication used here is external fixed finite-fragment transfer. Each hypothetical target refutation is handled separately; the MA iteration supplies no asserted PA-verified uniform selector of proof certificates.
3 · Logical flowchart
4 · Definitions, theorems and proofs
A two-step Cohen iteration is a product
Statement
When is the constant check-name for , is forcing-equivalent to , and its extension adjoins two mutually generic Cohen reals in either order.
Facts & Assumptions
Given: The hypotheses, objects, and conventions in the Statement.
Two-step forcing iterations defines the pair order.
Generic factorization and ccc preservation for two-step iterations factors its generic.
Cohen coordinates are distinct and mutually generic identifies the two coordinates.
Proof
The check names for occur in the constant name , hence lie in F1's bounded carrier . They form a dense suborder of the restricted iteration: for any , the forcing membership clause gives a strengthening that forces for some ground , and extends . On this dense check-name suborder, exactly when and . Send this pair to the finite function on with and . Restriction is the inverse on the dense suborder, proving forcing equivalence.
F2 factors the generic into the two one-coordinate generics; F3 says their union reconstitutes the full generic and either coordinate is Cohen-generic over the extension by the other.
MA produces a real outside a small listed family
Statement
Assume . Given at most reals, the Cohen finite-function order and coordinate-domain/disagreement dense sets produce a real distinct from every listed real. Hence implies .
Facts & Assumptions
Given: The hypotheses, objects, and conventions in the Statement.
Martin's Axiom at a cardinal and Martin's Axiom supplies a filter meeting the dense family.
Proof
List the given reals as for . In let and . Extending at one fresh coordinate proves all these sets dense; is countable and hence ccc.
F1 supplies a filter meeting the at most many and countably many . Its union is a total real , and meeting gives . Thus no family of at most reals exhausts , so .
A small set of reals is both null and meagre under MA
Statement
Under MA, if is a set of reals with , then is both Lebesgue null and meagre, though these notions are independent for arbitrary sets.
Facts & Assumptions
Given: The hypotheses, objects, and conventions in the Statement.
MA makes unions of fewer than continuum many meagre sets meagre handles small unions of meagre sets.
MA makes unions of fewer than continuum many null sets null handles small unions of null sets.
Proof
Write . Every singleton is closed nowhere dense and has Lebesgue measure zero.
Since the index family has size below the continuum, F1 makes its union meagre and F2 makes it null. The two conclusions are proved separately; neither is inferred from the other.
Martin's Axiom implies CH
False statement
Martin's Axiom implies the Continuum Hypothesis.
Facts & Assumptions
Given: The hypotheses, objects, and conventions in the Statement.
MA(aleph_0) and the implication from CH to MA proves the valid direction .
Externally fixed-fragment relative consistency of MA and not CH gives the external implication by fixed finite-fragment transfer.
Counterexample
Assuming ZFC is consistent, F2 gives the consistency of a theory in which MA holds and CH fails. Thus the implication is not a theorem of ZFC, on the same metatheoretic consistency assumption under which the false statement is posed.
F1 records that reversing the arrows would confuse the valid implication with its false converse. The refutation rests on the fixed-fragment model argument of F2; it does not assume a countable transitive model of full ZFC.
5 · Examples, counterexamples and false statements
None yet.