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.