How to formally prove using first-order set theory that {7,8,9}={7,8,10} is a false statement?

Question

I am trying to prove that the sets {7,8,9} and {7,8,10} are different sets, using only the two basic axioms in naive set theory (Axiom of Comprehension and Axiom of Extensionality), and first-order logic.

Informally, it seems trivial to prove.

Here is my formal attempt:

The green arrows represent rows that are tautologically valid steps in the proof. As you can see, starting on step 11, I have written the steps but I haven't specified a rule and so those rows don't check out. Additionally, I don't believe the proof is correct starting on step 11, though I believe the general idea of the last few steps is correct.

A few observations:

• The only way for steps 9 and 10 to be simultaneously true is for c to be neither 9 nor 10. But our assumption is that c is in a, so it can assume the value 9. But then step 10 is false.

• The program I used doesn't have knowledge of predicates related to natural numbers. I believe some predicates taken as axioms are necessary to complete this proof. In particular, I don't think we can prove that steps 9 and 10 aren't compatible in this proof without recourse to extra axioms about numbers.

• Note that this question is centered on FOL, not on complex mathematics. I posted this question on Math Stack Exchange a few days ago, but wasn't satisfied with the answer. In particular, when you do math you are usually using notation that abbreviates what is happening at the level of the underlying basic FOL language. For example, {7,8,9} is an abbreviation. The symbol for "not in" is also not available in the basic version of first-order set theory I am using. The only symbol specifically from the domain of set theory is ∈.

- I'd like to know how to complete this proof. It doesn't matter if you provide the steps, or just an outline of the steps that would be required. Conceptually, I am trying to understand what it is at the very fundamental level that makes a proof of such a simple result possible.

Answer 1

Long comment

I believe some predicates taken as axioms are necessary to complete this proof. In particular, I don't think we can prove that steps 9 and 10 aren't compatible in this proof without recourse to extra axioms about numbers.

Axioms for numbers are not necessary; we can re-phrase the problem considering A = { a,b,c } and B= { a,b,d } and nothing will change.

The second move, in order to "measure" how much set-theoretic commitment is needed, is to avoid the "belongs to" relation: ∈, and use a more "neutral" binary predicate R(x,y).

We can easily prove, using the Substitution axiom for equality that:

∃x (R(x,A) ∧ ¬R(x,B)) → ¬(A=B).

The needed instance of the equality axiom is: A=B → (R(x,z)[A/z] ↔ R(x,z)[B/z]).

Thus, the conclusion is straightforward from the "fact": ∃x (R(x,A) ∧ ¬R(x,B)), that is the translation of c ∈ A and ¬(c ∈ B).

As suggested by @TenO'Four's comment above, this "fact" is not provable by logic alone, because a model of the above formula needs at least two objects and thus the formula is not valid, i.e. it is not true in every model.

---

Having convinced ourselves that we cannot prove ¬({ a,b,c } = { a,b,d }) by logic alone, we can try to understand where set theory "creeps in", and the answer is: in the use of the set-builder notation (or: abstraction operator)): { x | phi(x) }.

This operator, that transform a formula with one free variable into a term (a "name"), is not part of first order language.

It must be added to the first order language of set theory with the following definitional extension:

{ x | phi(x) }=y ↔ (Set(y) ∧ ∀x(x ∈ y ↔ phi(x))).

From the definition, we have immediately that: a ∈ { x | phi(x) } ↔ phi(a).

Using it, from A = { a,b,c }, that means A = { x | x=a ∨ x=b ∨ x=c }, we deduce that c ∈ A and similarly that ¬(c ∈ B).

Finally, to exploit the above considerations in terms of naive set theory, we need a "minimal" model with at least two different sets: we can use ∅ and { ∅ }.