It's my understanding that ZFC is axiomatized in terms of propositional logic. However, propositional logic is just a logic which deals with propositions, and on its own has no inherent axioms. Yet, mathematics is clearly subject to certain rules of inference and tautologies not explicitly stated in ZFC, such as modus ponens or the law of the excluded middle. When searching online, I'm finding several different propositional calculi, but none seem to be definitively "the one" that ZFC is built from. Intuitively, given historical context, I would suspect that the Hilbert system is what I'm looking for, but even this seems to have no agreed upon axiomatization.
What exactly is the calculus which ZFC is built upon, and what exactly are the axioms or axiom schema of said calculus?
Any help would be greatly appreciated. Thank you!
ZFC is based on first order classical logic: this includes inference rules that tell you what constitutes a valid proof. A proof consists of a sequence of statements, each following from the previous ones using one of those rules.
Among those rules, you have introduction/elimination of logical connectives and quantifiers, some rules involving equality, variable replacement, etc. And also you can just use any tautology. This is what makes first order classical logic "classical": you can use the tautologies of classical logic (as opposed to intuitionistic logic for instance) without justification.