If 1 ∈ 2 is neither provable nor refutable, then you're not working with anything. The proposition literally has no meaning. It's not a syntax error, but you can't use its value for anything. Its value is undefined.

This actually comes in handy: While 1 ∈ 2 is undefined, `(2 > 1) ∨ (1 ∈ 2)` is true, and `(1 > 2) ∧ (1 ∈ 2)` is false, and this is useful because it means you can write:

    x = 0  ∨  1/x ≠ 0

    y = 0  ∨  1/x ≠ 0

To make this convenient, typed theories will often define 1/0 = 0 or somesuch (but they don't complain about that). In untyped set theory, 1 ∈ 2 and 1/0 can remain valid yet undefined.

And of course a ZF set theory operates with different objects than Peano arithmetic - it's a different theory. But Peano arithmetic nevertheless applies to any encoding of the integers, even the ones where 1 ∈ 2 is undefined.