The question is: Let K be a theory in the language of PA with just one proper axiom: (∀x1)(∀x2)x1 = x2. Show that K is a consistent theory with equality.
To show K is a theory with equality is to show that: (A6) (∀x)x=x (A7) x=y⇒(ϕ(x,x)⇒ ϕ(x,y)) while (A6) is easy to prove, I have no clues on how to prove (A7) after supposing the hypothesis x=y and ϕ(x,x), should I use the Existential Rule to generate (∃t)ϕ(x,t)?
Also, it suffices to prove K's consistency by reduction to absurdity, the other way is to find a formula which cannot be proved, but there doesn't seem something intuitive to start with.