What kind of system are we in if we explicitly take its negation as an axiom?
Here's the identity of indiscernibles.
(1) ( ∀P.P(x)↔P(y) ) → x = y
Here it is written in prenex normal form
(2) ∀x∀y.∃P.(x=y) ∨ (P(x)↮P(y))
The negation of (2) can be though of as giving us two indistinguishable but otherwise
d in our domain.
Are there any go-to paradoxes / counterintuitive results if we take (3) as an axiom in a second-order logic system?