How to "understand" the membership in ZFC? I am trying to be comfortable with logic and set theory. In particular, I am trying to be able to understand the axioms of ZFC, written in first order logic plus the signature consisting of the membership symbol, from no underlying and prior knowledge whatsoever. I find not very aesthetic to use set theoretic language to define first order logic (as done in quite a few books), since first order logic is a pre-requisite to set theory.
I have no problem in considering there is no prior knowledge in propositional logic, or in quantifiers.
My main question is on the membership symbol: membership seems a "physical" property. The only way out I can find is if all the sets the axioms of set theory will analyze are explicitly constructed. In this way, I have no problem: I can perfectly say if an object belongs to a set or not. This is typical from the construction of the natural numbers. And I believe most, or all, the sets used in standard mathematics.
Is this the "right" way to think about the membership symbol?
 A: Don't be too quick to dismiss the naive Platonist picture of sets:

Sets exist. They're out there somehow, in the same way as the real numbers of analysis or the ideal lines and points of geometry exist, in and of themselves. We don't need to construct them or to do anything to make them exist -- they're already there, all of them. Some of them have other sets as elements. That's how it is; they just do.
Cantor thought that for every meaningful property of things there's a set whose members are exactly all the things with that property.  Russell proved that cannot be the case: the property of "not being a set that has itself as an element" cannot possibly describe a set.
Nevertheless, some sets exist. We have intuitive experience with thinking about finite sets and certain well-defined sets of reals, points, and so forth. We intuitively believe that there must be an universe of sets out there, whose behavior and relation to each other sufficiently resemble what we can see in the simple sets our mind can handle, that we can use them for mathematical reasoning.
The axioms of set theory are a limited list of assumptions that we hope are true about that actually existing universe of sets. As long as they are true, then whatever we conclude from them by valid reasoning steps must also be true. If it ever turns out they are not true, we'll be in trouble, and then we'll need to start figuring out which of our proofs depended on a false axiom and whether they can be repaired.
However, the axioms do not "create" or "define" the sets -- as stated, the sets already exists. The axioms are not even "beyond doubt" like the ancients thought axioms ought to be.  On the contrary, since all of ordinary mathematics can be developed from those axioms, they provide us with a neat list of all we ever need to doubt.

There are a lot of philosophical and technical arguments that can be leveled against the viewpoint I have described here -- it is not called "naive" for nothing. I'm certainly not expecting you to take it as gospel just on my say-so, and it should not be the only way of thinking about sets you have available.  But this viewpoint should at least be kept in mind, for several reasons:

*

*It's a somewhat close approximation of how most working mathematicians outside set theory probably tend to view things when they don't go out of their way to be philosophical about it.

*If you want to be a set theorist, you had better be acquainted with a wide variety of philosophical viewpoints of what sets are and what they should be. The naive Platonist viewpoint has been influential in the development of set theory.

*Many competing viewpoints are best understood by contrasting them to the Platonist one.

*One of the most obvious criticisms of the Platonist picture is, "but how do we know those axioms are actually true, then?"  This is a fundamental question, one that Gödel gave the disappointing answer "we can't".  It also applies, with minor variants, to other ways of viewing sets, but many of them are a lot better at hiding it among the technicalities.  Keeping the naive view in mind helps with keeping in mind that we don't know everything, no matter how fancy symbols we dress up our ignorance with.

A: The axioms of set theory define what is a set, they don't construct anything explicitly. They restrict all possible objects which could exist down to something which could reasonably be considered a set by specifying the properties the set must have. It does this through defining the $\in$ relation. I also think "physical" is a bad choice of word. Set theory is just a theory, you can prove things from it by assuming set theoretical axioms or logical axioms in finite steps. So if something is allowed or not follows from whether there exists such a proof.
A: I had a similar question thirty years ago.  For the last thirty years I have studied the sentences,
$\forall x \forall y 
( 
   x \sqsubset y 
\leftrightarrow 
   ( 
      \forall z ( y \sqsubset z \rightarrow x \sqsubset z ) 
   \wedge 
      \exists z ( x \sqsubset z \wedge \neg y \sqsubset z )
   ) 
)$
$\forall x \forall y 
( 
   x \in y 
\leftrightarrow 
   ( 
      \forall z ( y \sqsubset z \rightarrow x \in z ) 
   \wedge 
      \exists z ( x \in z \wedge \neg y \sqsubset z )
   ) 
)$
Originally, I took the symbol "$\sqsubset$" as the proper subset relation.  However, by studying Frege and his references back to Leibniz, I learned that Leibnizian logic had been formulated as an order inversion with respect to the semantics for Aristotelian term logic.  Frege referred to this distinction as "intension" and "extension".  So, I now view "$\sqsubset$" as an intensional proper part relation and introduce an extensional proper subset, "$\subset$", with definitions.
What motivated these sentences had been Cantor's nested set theorem for closed sets of vanishing diameter.  My intension had been to identify equality with topological indistinguishability.  I had observed that transitive closures satisfied Kuratowski's axioms and began thinking about the set universe as a topology.  I wanted to know the details.  I did not know that this would be leading me to "apartness" in intuitionistic mathematics.
With regard to the original topological motivation, let me observe that I would find Csaszar's theory of topogenous orders.  In this theory, the (reflexive) subset relation is a limiting relation of a class of orders to which it belongs.  So, treating what is essentially the same relation in both an "intensional" context and an "extensional" context is supported in a mathematical theory that has the (reflexive) subset relation serving two roles.
With regard to a philosophical motivation, I would eventually look to mereology.  However, this had not been quite right because of how mereology is typically presented in the modern literature.  To the extent that the sentences above relate to mereology, one must look to mereology as it has been described by Michael Potter in his book "Set Theory and Its Philosophy".  When describing Dedekind's contributions to foundations, Potter holds that Dedekind originally conflated the membership relation and the subset relation.  He claims that this is an indicator of mereology.
For my part, I had simply been trying to enforce the "no proper classes" description of Zeremlo-Fraenkel set theory.  Following a typical mathematical characterization of sets as collections, I took the statements,


*

*A set is a collection taken as an object.

*A class is any collection of sets.

*All sets are classes.

*A set is a class that is an element of a class.


as a guide.  I had no knowledge of the logical objections to "collections" as 
"second order".  I still do not accept those criticisms.  Cantor and Frege were different people with different motivations.  There is nothing in the four statements above describing a set as being defined by the extension of concepts.  And, in the Fregean account, the usual axiom of extension corresponds with "concept identity" rather than "object identity".  So, I have found no reason within my own deliberations for any mathematician to concede to the Skolemite position that set theory is a first-order theory.  For an alternative to the Skolemite view, you might seek out Scott's paper, "Axiomatizing Set Theory", Boolos' paper, "The Iterative Conception of Set", and Drake's book, "Set Theory".  But, the introduction of "levels" makes these two-sorted theories.  For my objectives, this is just as bad a proper classes.
Understanding the sentences above, however, is quite problematic.  One must use a defined identity and then use axioms to establish the usual extensional interpretation of a subset/part.  A power set axiom seems necessary.
The defined identity is, itself, problematic.  Set theory, as typically presented, defers to the theory of identity in predicate logic.  A defined identity is "eliminable".  It is almost obvious to every student of set theory that one could simply write the axiom of extension as 
$\forall x \forall y 
( 
   x = y 
\leftrightarrow 
   \forall z( z \in x \leftrightarrow z \in y ) 
)$
But, a defined identity does not address the need of a logical calculus to interpret the sign of equality as substitutivity.
To address this problem, I had to write additional forms based upon negations,
$\forall x \forall y ( x \not\sqsubset y \leftrightarrow ( ... ) )$
$\forall x \forall y ( x \not\in y \leftrightarrow ( ... ) )$
and introduce axioms based upon exclusive disjunctions,
$\forall x \forall y \neg ( x \sqsubset y \leftrightarrow x \not\sqsubset y )$
$\forall x \forall y \neg ( x \in y \leftrightarrow x \not\in y )$
If you ever study Quine's "Set Theory and Its Logic", you will find that addressing substitutivity is essential when using defined identities.  You can also find mention of this in Kelley's "General Topology".  It is a footnote in his appendix on set theory.
Note that addressing substitutivity still does not address the "eliminability" problem.  To solve this, I began studying Tarski's axiom from his work on cylindric algebras.  He uses
$\forall x \forall y
(
   x = y
\leftrightarrow
   \exists z ( x = z \wedge z = y )
)$
to implement transitivity in his algebraization of first-order logic.  I would be using it as a mathematical axiom introducing "$=$" as a language parameter.  Obviously, it is "non-eliminable" by virtue of its syntax.  But, I have had to rewrite the logic in support of this axiom.
If you consider the one direction of the biconditional,
$\forall x \forall y
(
   \exists z ( x = z \wedge z = y )
\rightarrow
   x = y
)$
you can see that it can serve as a "semantic warrant" for uses of "$x = y$" in a logical calculus if it is treated as a schema.  As such, it replace the identity of indiscernibles, which is an epistemic warrant.  But, this truly complicates the logic since you must rewrite the quantifier rules to support the relationship with instances of "$x = x$".  That is, instances of "$x = x$" must now be introduced only when an existential quantifier is eliminated (the identity statement enters as a witness).
Let me note that first-order logic arises from simply denying the identity of indiscernibles.  There is no warranting of identity statements.  This has been portrayed in the literature as "contingent identity".  Authors such as Quine have argued against it.
As for the sentence, 
$\forall x \forall y
(
   \exists z ( x = z \wedge z = y )
\rightarrow
   x = y
)$
you will find the closely related sentence,
$\forall x \forall y
(
   \neg \forall z ( z \neq x \vee z \neq y )
\rightarrow
   x = y
)$
discussed in the paper "Equality in The Presence of Apartness" by van Dalen and Statman.  Unfortunately, it is not freely available on the internet to the best of my knowledge.
Van Dalen conjectured that the apartness axioms he had been considering ($AP$) would be conservative over the theory,
$EQ + 
\forall x \forall y
(
   \neg \forall z ( z \neq x \vee z \neq y )
\rightarrow
   x = y
)$
where $EQ$ are the standard identity axioms with the indiscernibility of identity restricted to a single statement axiomatizing substitutivity with respect to identity statements,
$\forall x \forall y \forall z
( 
   x = y 
\rightarrow 
   ( z = x \rightarrow y = z ) 
)$
The paper proves that the conjecture is wrong.  Instead, they are forced to define a countable infinity of apartness relations based on the form above.  They devise a countable infinity of axioms based upon these definitions and add them to $EQ$.  This is denoted $SEQ^\omega$.  If only a subcollection of axioms, based upon an initial segment of the apartness relations, is added to $EQ$, the theory is denoted $SEQ^n$.
Their conclusions are summarized in their paper with the statements, 


*

*$AP$ is conservative over $SEQ^\omega$.

*$SEQ^\omega$ is a proper extension of each $SEQ^n$.

*The equality fragment of $AP$ is not finitely axiomatizable.
I sincerely apologize for the length of this answer.  As I cannot know how you might view membership as "physical", I do not know if any of my thoughts will be found helpful.  But, I have spent a great deal of time trying to understand the membership relation (relative to a theory of "collections"), and, my deliberations are detailed enough to dissuade anyone from making the same mistakes.
Good luck in all of your mathematical endeavors.
A: The syntactical side of propositional logic is straightforward, it's just about finite strings of symbols and some rules for manipulating them. These things are uncontroversial to speak about even without formalising them in set theory. So no set theory is needed to define them. It's like the natural numbers, which existed and we could work with them way before they were axiomatised in Peano Arithmetic (PA). 
The fun (and somewhat mind-blowing) thing is that later, once we developed set theory, we can re-discover the concepts of propositional logic, formulas, proofs and models, inside of set theory by coding everything up as sets, and use set theory to prove things about them. Worse, we can do some of this already in PA and code up formulas and proofs as numbers. There are then numbers that mirror the outside PA-axioms and we can turn the question "is there a number that encodes a proof of a contradiction" into a question about numbers which we can treat with the PA axioms (the answer to that is Gödel's famous incompleteness theorem). 
I hope this help you see that the definitions are not circular.

There is nothing special about the membership symbol at all. Indeed, the language of set theory is extremely simple: there is just a single binary relation called $\in$.
So in an interpretation of ZFC, there are things $A,B,C$ and a way of determining if any two of these are in relation. This is precisely the data we need to define a directed graph. 
You can start with the graph that has a single node and no edges. And you can be happy because this already satisfies the first axiom of ZFC: There is a thing that has no relations incoming. You'd call the node "empty set".
$$\circ$$
Take the graph with two nodes and no edges.
$$ \bullet\,\circ $$
Both nodes could be called empty sets. But this doesn't satisfy our set-theoretic intuition, because of extensionality: If two things are related to the same things, they are already equal. 
Now look at the graph $$\bullet \to \circ.$$ This is extensional, has an empty set, and we can agree to call the nodes $\{\emptyset\}$ and $\emptyset$. However, is there a pair set? A thing that is related to precisey $\circ$ and $\bullet$?
If you wish, a model of set theory is just a directed graph that satisfied a bunch of axioms that allow us to think set theoretically about them. If you want to have some hands-on examples, draw the first 4 of the finite stages of the von Neumann hierarchy. Those are tiny graphs that satisfy a lot of set theory but not all of it. Full models of ZFC will have to be infinite graphs, and there is no known constructive way of obtaining one.
A: Just as the intuition came first for the successor relation on the natural numbers, it also came first for the membership relation on sets. 
In the axioms for the natural numbers (see Peano/Dedekind), we have a formal, supposedly minimal list of the essential, self-evident properties of the successor relation on the natural numbers. They are based on the common intuition of numbers from antiquity. From these axioms, we can formally prove most if not all other properties of interest. 
Likewise in the axioms for set theory (e.g. ZFC), we have a formal, supposedly minimal list of the essential, more or less self-evident properties of the membership relation on sets. For the most part, they are based on the common intuition of sets developed early in the 20th century. From these axioms, we can formally prove most if not all other properties of interest. 
A: Let me describe a method to define the membership relation, and please correct me if I am wrong somewhere in my argument:
A class can be defined as the collection of objects satisfying a given property.
For me, first order predicate theory has no problems in its definitions: first order predicate theory is just a way to put order into our metalanguage (English), such that all statements are true or false. It is a somewhat "limited" language (in comparison to English) but it is useful nonetheless.
So, if x is an object (a "name") and p is a property (an "adjective"), we can define p(x) as "has the object x the property p?" and this is false or true.
Then, a class A is the collection of objects x such that p(x) is true.
We can define $x \in A$ as "p(x) is true", where p is the property defining A.
To sum up: we have defined $\in$ just with the language of first order predicate theory.
Then, what are sets?
Sets are classes. But not all classes: only those classes satisfying a series of statements in first order predicate theory (which include also the membership relation; but this is not a problem, since we perfectly understand what the membership relation is: we have defined it earlier above in this post), the axioms of set theory.
If a class does not satisfy these axioms, it is not a set.
And then, we state that "all mathematics" can be built out of sets (not classes; well, some foundational issues use classes which are not sets, such as the class of all ordinals, but anyway).
If my explanation were right, then everything is fine for my intuition: the membership relation is just DEFINED as a property in first order predicate theory. And sets are just defined as classes (which are a relabeling of properties) which satisfy a series of "strange" axioms (the axioms of set theory). One finds these "strange" axioms are useful, and only those classes that satisfy those axioms (the sets) are necessary to build all mathematics, which is a great feature to have.
Any comments?
