Pipeline-generated

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.

Formal Set-Theoretic Syntax, Structures, and Satisfaction: Examples and Counterexamples

1 · Prerequisites

2 · Summary

These examples calculate satisfaction in small structures, expose variable capture and the failure of agreement at a single assignment under substitution, and evaluate empty-class guards. The final refutation concerns the explicitly stated truth-with-parameters scheme; it does not presume a sentence-only arithmetization theorem.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Parsing and evaluating a membership formula

Example

In the membership structure on $M = {0, 1}$ , where $0 = \emptyset$ and $1 = {0}$ , let $ϕ = \exists v_{1} (v_{1} \in v_{0})$ . Then $FV (ϕ) = {v_{0}}$ . It is false when $s (v_{0}) = 0$ and true when $s (v_{0}) = 1$ .

Facts & Assumptions

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

[F1]

Assignments agreeing on $FV (e)$ give equal denotations when $e$ is a term and the same truth value when $e$ is a formula. Also, passage to a reduct preserves denotations and satisfaction for expressions in the smaller signature. In particular sentence truth is independent of assignment; the truth of a formula can be specified by any tuple assigning all its free variables. (Coincidence for term values and satisfaction)

Verification

1.1

The outer code is $(e x i s t s, v_{1}, (r e l, \in, (v a r, v_{1}), (v a r, v_{0})))$ . The body has both variables free; the outer binder removes $v_{1}$ . By coincidence all other assignment values are irrelevant.

2.1

The only membership pair in $M^{2}$ is $(0, 1)$ . For value $0$ at $v_{0}$ , neither candidate witness is a member of $0$ . For value $1$ , witness $0$ works. These are the two asserted truth values.

step 1.1given∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Variable capture changes satisfaction

Statement refuted

False claim: replacing free occurrences by a variable without first avoiding capture always has the intended substitution semantics. In $ϕ = \exists v_{2} (v_{2} \in v_{1})$ , naively substitute $v_{2}$ for $v_{1}$ .

Facts & Assumptions

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement refuted.

[F1]

There is a canonical total capture-avoiding substitution $ϕ ⟨ t / x ⟩$ on formulas, obtained by renaming obstructing binders using least unused variable indices. It replaces the original free occurrences of $x$ and satisfies $M, s ⊨ ϕ ⟨ t / x ⟩ ⟺ M, s [x : = ⟦ t ⟧_{s}] ⊨ ϕ .$ Canonicity refers to the specified coding and traversal, not to literal invariance under other fresh-variable conventions. (Canonical capture-avoiding substitution)

Counterexample

1.1

In $M = {\emptyset, {\emptyset}}$ with restricted membership, take $s (v_{2}) = {\emptyset}$ . The intended substitution truth, supplied by capture-avoiding substitution, is the truth of $ϕ$ after setting $v_{1}$ to $s (v_{2})$ . It is true, with witness $\emptyset$ .

2.1

Naive replacement gives $\exists v_{2} (v_{2} \in v_{2})$ , false since neither carrier element belongs to itself. Renaming the binder to $v_{3}$ first gives $\exists v_{3} (v_{3} \in v_{2})$ , true at the displayed assignment. Thus the naive operation changes the required truth value.

step 1.1given∎

ExampleConstruction: AI-adaptedVerification: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Relativization to the empty class

Example

For $C = {z : z \neq z}$ , the relativization of $\exists x (x = x)$ is false and that of $\forall x (x = x)$ is true. The empty class is not an admitted structure.

Facts & Assumptions

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

[F1]

Fix a pure membership formula $δ (z, \vec{p})$ defining a class $C = {z : δ (z, \vec{p})}$ . This is eliminable notation for a predicate, not a class object. For a fixed pure membership formula $ϕ$ , first rename its binders away from the parameter variables $\vec{p}$ . Define $ϕ^{C}$ by keeping atoms, commuting with Boolean constructors, and setting $(\exists x ψ)^{C} = \exists x (δ (x, \vec{p}) \land ψ^{C}), (\forall x ψ)^{C} = \forall x (δ (x, \vec{p}) \to ψ^{C}) .$ Copies of $δ (x, \vec{p})$ are inserted by capture-avoiding substitution and fresh internal bound variables. In the set case $C = M$ use the predicate $z \in M$ , with a fresh parameter variable for $M$ . This operation is meaningful even for an empty class. It does not make the empty class an admitted structure: carriers of structures remain nonempty. For proper classes, evaluation of $ϕ^{C}$ means a separate ambient formula for each fixed $ϕ$ , not a uniform universe satisfaction relation. Conventions and prerequisites: prop-capture-avoiding-substitution. (Relativization to sets and definable classes)

Verification

1.1

The existential relativization is $\exists x (x \neq x \land x = x)$ . Its matrix is false at every set, so it has no witness.

2.1

The universal relativization is $\forall x (x \neq x \to x = x)$ . Its antecedent is always false, so it is true. These computations concern guarded formulas; the nonempty-carrier convention remains in force.

F1∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Agreement at one assignment is insufficient

Statement refuted

False claim: if two formulas agree at one assignment, they still agree there after the same free-for substitution. Use the two-element equality structure $M = {0, 1}$ with constant $c^{M} = 1$ , distinct variables $x, y$ , and $s (x) = s (y) = 0$ .

Facts & Assumptions

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement refuted.

[F1]

If $t$ is free for $x$ in $ϕ$ , then for every structure $M$ and assignment $s$ , $M, s ⊨ ϕ [t / x] ⟺ M, s [x : = ⟦ t ⟧_{s}] ⊨ ϕ .$ (Free-for substitution commutes with satisfaction)

Counterexample

1.1

At $s$ , the formulas $x = y$ and $y = y$ are both true. The constant $c$ has no variables, so is free for $x$ in each formula. The free-for identity evaluates substitution by changing $s (x)$ to $1$ .

2.1

After substitution the formulas are $c = y$ and $y = y$ . Their truth values are respectively false ( $1 \neq 0$ ) and true ( $0 = 0$ ). The original agreement at $s$ imposes no agreement at the updated assignment, which is exactly the missing hypothesis.

F1step 1.1∎

False statementConstruction: AI-adaptedVerification: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

V has a definable truth predicate

Statement

False statement, in the truth-with-parameters sense: there is a pure membership formula $T (w, x, y, z)$ and a set $t$ such that for every pure membership formula $ψ$ with free variables among $x, y$ and every pair of sets $r, s$ ,

$ψ (r, s) ⟺ T (⌜ ψ ⌝, r, s, t) .$

The displayed universal demand is a scheme of biconditionals for the proposed $T, t$ .

Facts & Assumptions

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

[F1]

Set satisfaction and relativization must be distinguished. Set satisfaction is uniform in the code of a formula and the data of a set structure. Relativization to a definable proper class supplies an ambient formula separately for each fixed input formula. Writing $V ⊨ ϕ (\vec{a})$ in this latter sense merely abbreviates $ϕ (\vec{a})$ . For the truth-with-parameters interface, a proposed pure membership formula $T (w, x, y, z)$ and a set parameter $t$ would have to satisfy, for every pure membership formula $ψ$ with free variables among $x, y$ and all sets $r, s$ , the biconditional $ψ (r, s) \leftrightarrow T (⌜ ψ ⌝, r, s, t)$ . Here $⌜ ψ ⌝$ is its finite set code. This is a scheme of requirements, not a single first-order assertion quantifying over ambient truths. The companion refutation tests this exact scheme by one formula built from the proposed $T$ . No sentence-only arithmetized diagonal lemma or representability theorem is asserted here. Conventions and prerequisites: thm-relativization-and-set-satisfaction. (Set truth and the Tarski interface)

[F2]

Refutation

1.1

Fix a proposed $T, t$ . Rename bound variables and use capture-avoiding simultaneous replacement of its four free slots to form the pure membership formula $ψ (x, y) = \neg T (x, x, y, y)$ . This notation means slot replacement in $T$ , not an added predicate symbol. Its only possible free variables are $x, y$ , and its finite code $q = ⌜ ψ ⌝$ is a set.

F1F2

2.1

The demanded instance for this $ψ$ , $r = q$ and $s = t$ gives $ψ (q, t) ⟺ T (q, q, t, t)$ . The definition of $ψ$ gives $ψ (q, t) ⟺ \neg T (q, q, t, t)$ . Therefore that one instance equates a proposition with its negation, which is impossible in classical logic. This refutes every proposed $T, t$ without a sentence-only arithmetization theorem.

step 1.1F1∎

Formal Set-Theoretic Syntax, Structures, and Satisfaction: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Parsing and evaluating a membership formula

Example

Facts & Assumptions

Verification

Variable capture changes satisfaction

Statement refuted

Facts & Assumptions

Counterexample

Relativization to the empty class

Example

Facts & Assumptions

Verification

Agreement at one assignment is insufficient

Statement refuted

Facts & Assumptions

Counterexample

V has a definable truth predicate

Statement

Facts & Assumptions

Refutation

Sources