Equality 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.