How to write that two specific sets are the same set in first-order naive set theory?

Question

Consider the following true statement

(1) The set whose only members are the prime numbers between 6 and 12 is the same as the set whose only members are the solutions to the equation x^2-18x+77=0.

How do I translate statement (1) above to first-order naive set theory?

The book I am following seems to define a set as follows: ∃a ∀x (x ∈ a ↔ P(x)).

But doesn't this say rather that a set "a" exists such that its members have the property P?

If I write

∃a ∀x (x ∈ a ↔ Prime(x) & 6<x<12)

∃b ∀x (x ∈ b ↔ x^2-18x+77=0)

My attempt would be:

(∃a ∀x (x ∈ a ↔ Prime(x) & 6<x<12)) & (∃b ∀x (x ∈ b ↔ x^2-18x+77=0)) & a=b

Note that informally (ie outside of FOL) we write {x | P(x)} to mean the same thing as ∃a ∀x (x ∈ a ↔ P(x)).

Thus, informally, I believe statement (1) is {x | Prime(x) & 6<x<12} = {x | x^2-18x+77=0}.

Is this attempt at translating to first-order naive set theory correct?

Answer 1

No, this does not work. The problem is that a and b are bound to their respective statements. That is, when you say ∃a ∀x (x ∈ a ↔ Prime(x) & 6<x<12), you can't invoke 'a' outside of the scope of the existential statement. I don't quite know what the right answer is because I don't know what the notation is for naive set theory. I'm pretty sure that ∀a∀b((∀x (x ∈ a ↔ Prime(x) & 6<x<12) & ∀x (x ∈ b ↔ x^2-18x+77=0)) → a = b ) is true since conditionals are only ever false if the antecedent is true, and the consequent is false. This is impossible in this scenario, so the statement is true.

Answer 2

∃a∀x(x∈a ⇔ P(x)) says for every property there is a set which includes objects with that property. Basically saying you can have any sort of set you can think of. That's not really a formula for you to follow more of an "axiom".

Naive set−theory has the same logical and non−logical symbols as ZFC with the only difference between the two being that of axioms.

{x|P(x): 6 < x < 12} ={7,11}

You cannot state the above identity in a purely logical language. You need the extralogical bits because "<" is a binary non−logical relation symbol that says something about some set. If you want to do so without involving any particular semantic, then that makes it easy:

P(x): x is prime

G(x,y): x is greater than y

L(x,y): x is less than y

a=6

b=12

c=7

d=11

∀x[((P(x) ∧(G(x,a) ∧ L(x,b))) ⇔ [(x=c ∨ x=d) ∧ ¬(x=c ∧ x=d)]] you can also split it fi you want but you will be missing ALOT of information in either case. The non−logical symbols are to an extent essential.

I might be missing a clause in the formulation.