alt Hacker News1 ∈ 2 is operating at a _different layer of abstraction_ than peano arithmetic is. It's like doing bitwise operations on integers in a computer program. You can do it, but at that point you aren't really working with integers as _integers_.
1 ∈ 2 is operating at a _different layer of abstraction_ than peano arithmetic is. It's like doing bitwise operations on integers in a computer program. You can do it, but at that point you aren't really working with integers as _integers_.
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:
which is a provable theorem despite the fact that the clause `1/x` is difficult to typecheck. This comes in even more handy once you apply substitutions. E.g. it is very useful to write: and separately prove that y = x.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.
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.