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.