It is said that the ZFC axiom system is a foundation of mathematics.
In my understanding, for something to truly be a foundation, if you gave this system to an entity without any intuition or understanding of the matters at hand, but with enough processing power to work through it without any mistakes (like a computer, or an alien), this entity would develop the same mathematical theory that we use.
However, the symbols and terms used to formulate the axioms, such as logical symbols or the concept of sets, are not formulated explicitly in the given axioms. When being taught set theory, one first uses a "naive" notion of sets, as it is "good enough" to understand basic concepts. This approach relies on an intuitive understanding of sets, one which such entities may not have, and which turns out to be false when going deeper into the theory.
Is it possible to express the axioms in a way which reduces them to their structural properties, such that a "fully formal" being could deduce the whole theory compacted in it without any understanding of what the axioms actually refer to?
Is my understanding of what an axiom system is correct? Do the axioms require a concept of sets beforehand or are all things which obey their structure sets, thus making the axioms implicit definitions?
For context, this question came to me while studying set theory and wondering how we even know what we are talking about in midst of all this formalism, while not admitting that it's actually heavily intuition based.
I welcome all responses to the questions and further reading suggestions, this topic really interests me.
Best Answer
First of all, ZFC is a foundation for mathematics only in a technical sense: almost all of modern math can be "coded" into ZFC, and the vast majority of theorems can be proved from ZFC. But a differential geometer (to take a random example) doesn't need to know the ZFC axioms; just naive set theory. I cannot think of a field, other than axiomatic set theory (which is thriving), where a practitioner makes deep use of the axioms. As an analogy, ZFC is a foundation for mathematics in the same sense that the binary is a foundation for programming.
Second, answering your question about a "fully formal being" deducing "the whole theory compacted in it": in principle that's true of the axioms as given; they don't need to be rewritten. In other words, a mindless, "brute force" program could generate all consequences of the axioms. This is absurdly inefficient and utterly impractical as a way to answer unsolved problems.
When set theorists use ZFC, they do rely heavily on their intuition. The purpose of ZFC is not to replace intuition, but to sharpen it. For example, you've probably heard that the continuum hypothesis can neither be proven nor disproven from the ZFC axioms. First point: these results are built on top of the ZFC formalization of set theory. Second point: the results don't sweep away all questions concerning the continuum problem, but they do change the whole character of the discussion.
You ask, "Do the axioms require a concept of sets beforehand"? This is partly a philosophical and partly a historical question. The Stanford Encyclopedia of Philosophy is an excellent online resource for exploring the philosophical issues; you might start with the article Zermelo’s Axiomatization of Set Theory or Hilbert’s Program, and explore links from there. Gregory Moore wrote a paper, "The Origins of Zermelo's Axiomatization of Set Theory" (Journal of Philosophical Logic, Vol. 7, No. 1 (Jan., 1978), pp. 307-329) and a whole book Zermelo's Axiom of Choice: Its Origins, Development, and Influence that deals with many of the historical questions.
Briefly, in the early years of the 20th century, a lot of controversy swirled around naive (Cantorian) set theory, partly because of the paradoxes (Russell, Burali-Forti), and partly because many leading mathematicians were not convinced by Zermelo's proof of the well-ordering theorem. That's just the kind of situation where an axiomatization can clarify matters.