Main derivation
S01 · definition
Before
\forall x\in U\,P(x),\quad \exists x\in U\,E(x)
After
\forall x\,(x\in U\Rightarrow P(x)),\quad \exists x\,(x\in U\land E(x))
Conditions: none
Rule: restricted_quantifier · Uses: G1, G2, G3, mko_quantifier_def
Leaf basis: mko_quantifier_def + restricted_quantifier
The MKO makes the domain and the predicate part of the statement itself, so first fix U={−2,−1,0,1,2,3} and the three predicates P(x): x²<10, Q(x): x²>x, E(x): x²=2, under classical truth semantics. Restricted quantifiers unfold as follows: ∀x∈U P(x) means 'for every x, if x∈U then P(x)'; ∃x∈U E(x) means 'some x satisfies both x∈U and E(x)'. Every later step is decided on this explicit domain.
S02 · equivalent
Before
(-2)^2,\ (-1)^2,\ 0^2,\ 1^2,\ 2^2,\ 3^2
After
4,\ 1,\ 0,\ 1,\ 4,\ 9
Conditions: none
Rule: numeric_evaluation · Uses: G1
Leaf basis: numeric_evaluation + neg_mul
Square each of the six elements of U exactly: (−2)²=4, (−1)²=1, 0²=0, 1²=1, 2²=4, 3²=9. Squares of negatives use (−u)(−u)=u·u. This table is shared later by the three predicates P, Q and E.
S03 · implies
Before
x^2\in\{4,1,0,1,4,9\}\ \text{for the six}\ x\in UAfter
P(-2)\land P(-1)\land P(0)\land P(1)\land P(2)\land P(3)
Conditions: none
Rule: numeric_evaluation · Uses: S02, G2
Leaf basis: numeric_evaluation + order_basics + and_intro_elim
P(x) is x²<10. By S02 the six squares 4, 1, 0, 1, 4, 9 are all less than 10 (the largest is 9<10), so P holds at every listed element of U; conjunction then combines the six facts.
S04 · equivalent
Before
P(-2)\land P(-1)\land P(0)\land P(1)\land P(2)\land P(3)
After
\forall x\in U\,P(x)
Conditions: U=\{-2,-1,0,1,2,3\}\ \text{listed completely}
Rule: L_finite_forall · Uses: S03, G1, L_finite_forall
Leaf basis: forall_elim + forall_intro + case_analysis + roster_membership
U is given by listing: a₁=−2, a₂=−1, a₃=0, a₄=1, a₅=2, a₆=3. By Lemma L_finite_forall (n=6), ∀x∈U P(x) is equivalent to the conjunction of the six P(a_i), which S03 established, so φ₁ is true. This is complete enumeration: the conclusion holds precisely because every element of U was checked.
S05 · implies
Before
\forall x\in U\,P(x)\ \text{is true}After
\neg\forall x\in\mathbb{Z}\,P(x)Conditions: 4\in\mathbb{Z}; 4\notin U
Rule: contradiction · Uses: S04, forall_elim, contradiction
Leaf basis: forall_elim + contradiction + numeric_evaluation + order_basics
The truth of φ₁ does not extend to ℤ. If ∀x∈ℤ P(x) held, instantiating at 4∈ℤ would give 4²<10, that is 16<10, contradicting 16≥10; so ∀x∈ℤ, x²<10 is false. The MKO stresses that complete enumeration settles the statement only on the specified finite domain: 4 is not in U, so it does not affect φ₁, but it refutes the different statement obtained by changing the domain to ℤ.
S06 · implies
Before
Q(0):\ 0^2>0
After
0\in U\land\neg Q(0)
Conditions: none
Rule: numeric_evaluation · Uses: S02, G2
Leaf basis: numeric_evaluation + order_basics + roster_membership
Q(x) is x²>x. Take x=0: 0²=0, and 0>0 fails (by trichotomy, 0=0 rules out both 0>0 and 0<0). 0 is a listed element of U, so 0∈U and ¬Q(0). x=1 also gives 1>1, which fails, but one witness is enough.
S07 · implies
Before
0\in U\land\neg Q(0)
After
\exists x\in U\,\neg Q(x)
Conditions: none
Rule: exists_intro · Uses: S06, exists_intro
Leaf basis: exists_intro
By ∃-introduction, the element 0 of U satisfies ¬Q(0), so ∃x∈U ¬Q(x) is true. An existential statement needs only one admissible witness.
S08 · equivalent
Before
\exists x\in U\,\neg Q(x)
After
\neg\forall x\in U\,Q(x)
Conditions: none
Rule: L_restricted_negation · Uses: S07, L_restricted_negation
Leaf basis: quantifier_negation + classical_implication + restricted_quantifier
By part (i) of Lemma L_restricted_negation, ∃x∈U ¬Q(x) is equivalent to ¬∀x∈U Q(x). So the negation of φ₂ is true and φ₂ is false. Negating a universal switches ∀ to ∃ and negates the predicate at the same time, while the domain U stays the same.
S09 · implies
Before
\forall x\in U\,\neg Q(x)
After
\neg\forall x\in U\,\neg Q(x)\quad(\text{since } 2\in U,\ 2^2>2)Conditions: 2\in U
Rule: contradiction · Uses: S02, G2, forall_elim, contradiction
Leaf basis: forall_elim + contradiction + numeric_evaluation + order_basics
A common error writes ¬∀x∈U Q(x) as ∀x∈U ¬Q(x) ('every element fails'). Test the latter: if it held, instantiating at 2∈U would give ¬Q(2), that is, 4>2 would fail; but 2²=4>2 holds, a contradiction. So ∀x∈U ¬Q(x) is false, whereas S07 and S08 showed that the correct negation ∃x∈U ¬Q(x) is true. The two have different truth values, so they are not equivalent.
S10 · implies
Before
x^2\in\{4,1,0,1,4,9\}\ \text{for the six}\ x\in UAfter
\neg E(-2)\land\neg E(-1)\land\neg E(0)\land\neg E(1)\land\neg E(2)\land\neg E(3)
Conditions: none
Rule: numeric_evaluation · Uses: S02, G2
Leaf basis: numeric_evaluation + and_intro_elim
E(x) is x²=2. By S02 none of the six squares 4, 1, 0, 1, 4, 9 equals 2; these are exact integer comparisons. So E fails at every listed element.
S11 · equivalent
Before
\neg E(-2)\land\neg E(-1)\land\neg E(0)\land\neg E(1)\land\neg E(2)\land\neg E(3)
After
\forall x\in U\,\neg E(x)
Conditions: U\ \text{listed completely}
Rule: L_finite_forall · Uses: S10, L_finite_forall
Leaf basis: forall_elim + forall_intro + case_analysis + roster_membership
Apply Lemma L_finite_forall to the predicate ¬E (the lemma holds for any predicate R): the conjunction of the six ¬E(a_i) is equivalent to ∀x∈U ¬E(x).
S12 · equivalent
Before
\forall x\in U\,\neg E(x)
After
\neg\exists x\in U\,E(x)
Conditions: none
Rule: L_restricted_negation · Uses: S11, L_restricted_negation
Leaf basis: quantifier_negation + de_morgan_logic + classical_implication + restricted_quantifier
By part (ii) of the lemma, ∀x∈U ¬E(x) is equivalent to ¬∃x∈U E(x). So φ₃ is false, and its negation ∀x∈U, x²≠2 is true. To show an existential false, every admissible element must be checked; finding one failure is not enough.
S13 · implies
Before
\neg\exists x\in U\,E(x)
After
\exists x\in\mathbb{R}\,E(x)Conditions: 2\ge 0
Rule: exists_intro · Uses: G2, sqrt_def, exists_intro
Leaf basis: sqrt_def + exists_intro
Put the same predicate E on the domain ℝ: since 2≥0, √2 exists, √2∈ℝ and (√2)²=2; by ∃-introduction, ∃x∈ℝ, x²=2 is true. φ₃ is false on U and true on ℝ, which shows that the domain is part of the statement and may not be dropped or swapped freely.
S14 · implies
Before
\forall x\in\varnothing\,R(x)
After
\forall x\,(x\in\varnothing\Rightarrow R(x))\ \text{holds}Conditions: none
Rule: forall_intro · Uses: restricted_quantifier, empty_set_def, classical_implication, forall_intro
Leaf basis: restricted_quantifier + empty_set_def + classical_implication + forall_intro
Replace the domain by the empty set. Unfold to ∀x(x∈∅⇒R(x)). For an arbitrary x, x∈∅ is false, and an implication with a false antecedent is true under classical semantics; since x is arbitrary, ∀-introduction makes the universal true. No element can be a counterexample, so ∀x∈∅ R(x) is true whatever R is.
S15 · implies
Before
\exists x\in\varnothing\,R(x)
After
\neg\exists x\,(x\in\varnothing\land R(x))
Conditions: none
Rule: quantifier_negation · Uses: restricted_quantifier, empty_set_def, and_intro_elim, quantifier_negation
Leaf basis: restricted_quantifier + empty_set_def + and_intro_elim + forall_intro + quantifier_negation
∃x∈∅ R(x) unfolds to ∃x(x∈∅∧R(x)). For every x the first conjunct x∈∅ is false, so the conjunction is false, that is ∀x ¬(x∈∅∧R(x)); by quantifier negation this is ¬∃x(x∈∅∧R(x)). The empty domain offers no witness, so the existential is false.
S16 · implies
Before
\text{S04, S08, S12, S14, S15}After
\varphi_1\ \text{true},\ \varphi_2\ \text{false},\ \varphi_3\ \text{false};\ \forall x\in\varnothing\ \text{true},\ \exists x\in\varnothing\ \text{false}Conditions: none
Rule: and_intro_elim · Uses: S04, S08, S09, S12, S14, S15
Leaf basis: and_intro_elim
Summary: φ₁ is true (S04, complete enumeration); φ₂ is false, and its negation is ∃x∈U, x²≤x with witness x=0 (S08), not ∀x∈U, x²≤x (shown false in S09); φ₃ is false, and its negation is ∀x∈U, x²≠2 (S12); over the empty domain the universal is true and the existential is false (S14, S15).
Substeps and lemmas
S04.1 · implies
Before
\forall x\in U\,R(x)
After
\bigwedge_{i=1}^{n}R(a_i)Conditions: U=\{a_i\mid 1\le i\le n\}
Rule: forall_elim · Uses: roster_membership, forall_elim
Leaf basis: forall_elim + roster_membership + and_intro_elim
Let U={a_i ∣ 1≤i≤n} and let R be any predicate. For each i, roster membership gives a_i∈U; ∀-elimination of ∀x∈U R(x) at x=a_i gives R(a_i). Combine the n results by conjunction. This is the '⇒' direction of the lemma.
S04.2 · implies
Before
\bigwedge_{i=1}^{n}R(a_i)After
\forall x\in U\,R(x)
Conditions: U=\{a_i\mid 1\le i\le n\}
Rule: forall_intro · Uses: roster_membership, case_analysis, eq_replace, forall_intro
Leaf basis: forall_intro + case_analysis + roster_membership + eq_replace
Assume the conjunction. Take an arbitrary x∈U with no further assumption on x. By roster membership, x=a_i for some i, giving n cases. In the case x=a_i the conjunction gives R(a_i), and replacing a_i by the equal x gives R(x). The n cases cover every element of U, so R(x) holds; since x was arbitrary, ∀-introduction gives ∀x∈U R(x). S04.1 and S04.2 together prove Lemma L_finite_forall.
S08.1 · equivalent
Before
\neg\forall x\in U\,R(x)
After
\exists x\,\neg(x\in U\Rightarrow R(x))
Conditions: none
Rule: quantifier_negation · Uses: restricted_quantifier, quantifier_negation
Leaf basis: restricted_quantifier + quantifier_negation
For any predicate R: first unfold the restricted universal to ∀x(x∈U⇒R(x)), then apply the unrestricted negation law ¬∀x ψ(x) ⇔ ∃x ¬ψ(x) with ψ(x) being x∈U⇒R(x).
S08.2 · equivalent
Before
\exists x\,\neg(x\in U\Rightarrow R(x))
After
\exists x\,(x\in U\land\neg R(x))=\exists x\in U\,\neg R(x)
Conditions: none
Rule: classical_implication · Uses: S08.1, classical_implication
Leaf basis: classical_implication + de_morgan_logic + restricted_quantifier
Under classical semantics ¬(A⇒B) ⇔ A∧¬B (since A⇒B is equivalent to ¬A∨B; then apply De Morgan and double negation). Taking A as x∈U and B as R(x) for each x gives ∃x(x∈U∧¬R(x)), which is ∃x∈U ¬R(x). S08.1 and S08.2 prove part (i) of the lemma.
S08.3 · equivalent
Before
\neg\exists x\in U\,R(x)
After
\forall x\in U\,\neg R(x)
Conditions: none
Rule: de_morgan_logic · Uses: restricted_quantifier, quantifier_negation, de_morgan_logic, classical_implication
Leaf basis: quantifier_negation + de_morgan_logic + classical_implication + restricted_quantifier + logic_chain
Part (ii): ¬∃x(x∈U∧R(x)) ⇔ ∀x ¬(x∈U∧R(x)) (quantifier negation) ⇔ ∀x(x∉U ∨ ¬R(x)) (De Morgan) ⇔ ∀x(x∈U⇒¬R(x)) (classical implication ¬A∨B ⇔ A⇒B), which is ∀x∈U ¬R(x). S08.3 proves part (ii) of the lemma.