Who proved that it is possible to express any proof by using the language and notation of set theory?

Question

Disclaimer: Please excuse any lack of precise mathematical expression, I am just trying to wrap my head around the concepts right now.

I often read that it is possible to express and/or deduce all other mathematical theories, theorems and axioms (is this correct?) from the axioms and/or notation of set theory. Based on this, I ask myself the following questions:

• To what extent is this true? What is there that cannot be expressed in terms of set-theoretical notation, and is there anything that cannot be deduced using the axioms of ZFC?
• Who exactly came to the conclusion that all this is possible? I have read that Bertrand Russell tried to formalize and break down all of mathematics so that it can be expressed in terms of formal logic (Principia Mathematica), but I haven't found anything about a mathematician who has managed to break down all of mathematics so that it can be expressed in terms of set theory. Can someone provide me with some historical background - how did mathematicians find out that all of mathematics can be expressed in terms of ZFC?

Thank you very much in advance! You are helping out a high schooler in great despair.

Answer 1

What is there that cannot be expressed in terms of set-theoretical notation?

Basically nothing : we express things using some alphabet (a set of symbols), say $\Sigma$. Any statement is hence some sequence of symbols from $\Sigma$, ie an element of $\Sigma^{< \omega}$ (often written $\Sigma^*$).

Is there anything that cannot be deduced using the axioms of ZFC?

Yes, anything that is independent of ZFC, eg the continuum hypothesis.

Who exactly came to the conclusion that all this is possible?

Nobody proved this, since "it is possible to express any proof by using the language and notation of set theory" is not a mathematical statement. Ratter, it is a meta-statement. Where would a proof of this statement take place? using which language? in which axiom system?

This thesis is well-founded, though. One can encode proofs using sets, and it seems that this encoding mirrors the "real" logic in the sense that one has deduction rules that empirically seem to be sound (if the code of $B$ is derived from the code of $A$ using deduction rules, then you can use it to get a proof that $A \Rightarrow B$) and complete (if you can deduce statement $B$ from statement $A$, then the code of $B$ can be derived - within ZFC - using deduction rules from the code of $A$).