TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)

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.

Los theorem for set ultraproducts

Statement

In ZFC, for every first-order formula phi and product representatives $f_{1}, \dots, f_{n}$ ,

$\prod_{i} M_{i} / U ⊨ ϕ ([f_{1}], \dots, [f_{n}]) ⟺ {i : M_{i} ⊨ ϕ (f_{1} (i), \dots, f_{n} (i))} \in U .$

In particular the diagonal map into an ultrapower of a nonempty set structure is elementary.

Facts & Assumptions

Given: ZFC. Term induction gives atomic compatibility, ultrafilter operations handle Booleans, and both existential directions are proved with AC spent on coordinate witnesses/defaults; constant truth sets prove elementarity.

[F1]

The ultraproduct is a well-defined nonempty structure: The quotient symbols are independent of representatives and coordinatewise.

[F2]

Existence and uniqueness of set satisfaction: First-order satisfaction follows its atomic, Boolean and existential clauses.

[F3]

Characterisation of ultrafilters: every set or its complement: Complement decisions and finite intersections match Boolean truth operations.

[F4]

The Axiom of Choice: AC selects coordinate witnesses and default elements from the nonempty carriers.

Proof

1.1

Induction on terms shows the value of a term on classes [f_j] is represented by its coordinate values. Constants and variables give the base cases and function symbols give the induction step by F1. Thus equality and relation atoms satisfy the asserted equivalence. Negation uses the complementary truth set and F3; conjunction uses intersection, which is in U exactly when both factors are (finite closure and upward closure).

F1F2F3

2.1

At an existential formula, a witness [g] in the quotient gives, by the induction hypothesis on its matrix, a U-large set of coordinates where g(i) witnesses that matrix. The coordinate existential truth set contains it, hence is in U. Conversely suppose that truth set E is in U. For each i in E, choose a matrix witness in M_i; outside E choose a default element of M_i. These choices are from a set family of nonempty subsets of the supplied carriers, so F4 applies and gives a product function g. Its matrix truth set contains E, and induction makes [g] a quotient witness. This proves both existential directions and completes formula induction.

F2F3F4step 1.1

3.1

In a constant family with constant parameter functions, each coordinate has the same formula truth value. Its truth set is I when the original structure satisfies the formula, and empty otherwise. Properness and step 2.1 show precisely that the diagonal map preserves and reflects each formula; F1 already gives injectivity.

F1F3step 2.1∎

Depends on

Used by

Infinitary Los theorem Theorem
Los schema for the universe ultrapower Theorem

Dependency tree · two levels

11 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

Marks Theorem 13.2 pp.56–57 (standard reference, not scraped)