Use negation introduction on the unwanted existential quantification, and existential quantifier elimination rule with a fresh witness :The witness name occurs neither in the surrounding assumptions nor in the conclusion of its subproof. This satisfies the eigenvariable condition; it is not an arbitrarily chosen fixed element assumed to witness the existential quantification. The result is .
1 ∀x. ¬P(x) premise
2 | ∃x. P(x) assumption
3 | | P(a) assumption, a fresh
4 | | ¬P(a) ∀-elim 1
5 | | ⊥ ¬-elim 3,4
6 | ⊥ ∃-elim 2,3–5
7 ¬(∃x. P(x)) ¬-intro 2–6Choose a fresh parameter . The universal quantifier elimination rule supplies both the implication and its premise at that same parameter:The eigenvariable condition holds because is absent from both undischarged assumptions at line 6. Hence the universally quantified implication is proved.
1 ∀x. (P(x) → Q(x)) premise
2 | ∀x. P(x) assumption
3 | P(a) ∀-elim 2
4 | P(a) → Q(a) ∀-elim 1
5 | Q(a) →-elim 4,3
6 | ∀x. Q(x) ∀-intro 5, a fresh
7 (∀x. P(x)) → (∀x. Q(x)) →-intro 2–6The proposed version with merely in the antecedent is not derivable. For a counterexample, take a two-element domain with and both true precisely at zero. The universal premise holds. Under the assignment , is true but is false. By soundness, a formal proof cannot exist. Attempting the previous derivation would fail exactly at universal quantifier introduction rule: the parameter would occur in the undischarged assumption , so it would not be fresh.
Write . Use negation introduction on the existential claim. For its fresh witness , instantiate ; the resulting self-application says both and its reverse. The given law of excluded middle then provides the two cases.Both case assumptions are discharged at line 15; the witness assumption is discharged at line 16. Since is absent from the surrounding premise and the exported conclusion , existential quantifier elimination rule is valid. Line 17 is the required negated existential. This is the diagonal self-application underlying the barber paradox.
1 ∀x. ∀y. (S(x,y) ∨ ¬S(x,y)) premise
2 | ∃b. H(b) assumption
3 | | H(b) assumption, b fresh
4 | | (S(b,b) → ¬S(b,b)) ∧ (¬S(b,b) → S(b,b)) ∀-elim 3, p := b
5 | | S(b,b) → ¬S(b,b) ∧-elim-L 4
6 | | ¬S(b,b) → S(b,b) ∧-elim-R 4
7 | | ∀y. (S(b,y) ∨ ¬S(b,y)) ∀-elim 1, x := b
8 | | S(b,b) ∨ ¬S(b,b) ∀-elim 7, y := b
9 | | | S(b,b) assumption
10 | | | ¬S(b,b) →-elim 5,9
11 | | | ⊥ ¬-elim 9,10
12 | | | ¬S(b,b) assumption (new case)
13 | | | S(b,b) →-elim 6,12
14 | | | ⊥ ¬-elim 13,12
15 | | ⊥ ∨-elim 8,9–11,12–14
16 | ⊥ ∃-elim 2,3–15
17 ¬∃b. H(b) ¬-intro 2–16Equality introduction rule is reflexivity; equality elimination rule permits substitution of equals in a formula:Terms substituted into must be free for substitution, so no variable becomes captured. The notation means substitution into the same designated free variable positions of one formula; other occurrences may remain fixed. These rules express first-order equality without assuming symmetry or transitivity as additional axioms.
For transitivity of first-order equality, take the substitution formula :For symmetry, use reflexivity and :Thus both transitivity and symmetry follow from the two equality rules. In the symmetry proof, only the designated first occurrence in is replaced; the second remains fixed.
1 T₁ = T₂ premise
2 T₂ = T₃ premise
3 T₁ = T₃ =-elim 2,1; φ(u) := (T₁ = u)1 T₁ = T₂ premise
2 T₁ = T₁ =-intro
3 T₂ = T₁ =-elim 1,2; ψ(u) := (u = T₁)Choose distinct fresh parameters . Within the assumption , equality elimination rule gives the forward implication directly. Derive the reverse equality explicitly before using it for the reverse implication:The equality assumption is discharged before either universal quantifier introduction rule. There are then no undischarged assumptions, so both eigenvariable condition requirements hold. The final universal theorem expresses that equal arguments are interchangeable in the predicate in both directions.
1 | a = b assumption
2 | | P(a) assumption
3 | | P(b) =-elim 1,2
4 | P(a) → P(b) →-intro 2–3
5 | a = a =-intro
6 | b = a =-elim 1,5; φ(u) := (u = a)
7 | | P(b) assumption
8 | | P(a) =-elim 6,7
9 | P(b) → P(a) →-intro 7–8
10 | (P(a) → P(b)) ∧ (P(b) → P(a)) ∧-intro 4,9
11 a = b → ((P(a) → P(b)) ∧ (P(b) → P(a))) →-intro 1–10
12 ∀y. a = y → ((P(a) → P(y)) ∧ (P(y) → P(a))) ∀-intro 11, b fresh
13 ∀x. ∀y. x = y → ((P(x) → P(y)) ∧ (P(y) → P(x))) ∀-intro 12, a fresh Articles by others on the same topic
There are currently no matching articles.