I am trying to understand the Completeness Theorem, and I was just looking at its explanation in the answer to this question: What is the difference between Gödel's Completeness and Incompleteness Theorems?
To repeat the description of the Completeness Theorem: The completeness theorem applies to any first order theory: If $T$ is such a theory, and $\phi$ is a sentence (in the same language) and any model of $T$ is a model of $\phi$, then there is a (first-order) proof of $\phi$ using the statements of $T$ as axioms. One sometimes says this as "anything true is provable."
In other words, semantic entailment from the axioms of $T$ should imply syntactic entailment from the axioms of $T.$ I am wondering, what is meant by syntactic entailment (i.e. proof) in this context? Whenever we use the word, "proof," I think we need to be working with some set of inference rules, which allow us to proceed from our premises to our conclusion. I was wondering, what are these inference rules? I was looking at these and I was wondering if they are the rules being used?
As was mentioned in comments, there is more than one way to define a first order proof system (equivalent in the sense that all these proof systems have the same set of theorems).
There are two similar but distinct notions of completeness concerning first order logic. One is, well, first order logic (FOL) completeness, and the second one is first order theory completeness. FOL is a concrete system with theorems such as $\forall x_0 R_0x_0 \to \exists x_0 R_0x_0$. But there are many first order theories. Completeness of first order theories applies to all first order theories, but their proof systems are slightly different. Namely, they differ with respect to their signature (set of non-logical symbols, i.e. $+$ and $=$) and non-logical axioms, i.e. $\forall x (x + 0 = 0)$.
In a sense, all first order theories can share the same rules of inference. Namely, modus ponens ($\{A,A \to B\} \vdash B$) and generalization ($\{A\} \vdash \forall x A$), for any formulas $A,B$ and any variable $x$. These are the rules of inference that, when coupled with appropriate axioms schemas, give everything needed for a first order theory.
You can be nitpicky though. If I'm not mistaken, the rules of inference are usually defined (formally) as sets of n-tuples. First (n-1) elements are premises and the nth element is a conclusion. Modus ponens for FOL would be something like $\{(R_0 c_0,\ R_0 c_0 \to R_1 c_0,\ R_1 c_0), \dots\}$. However, Peano arithmetic's modus ponens would contain $(0=0,\ 0=0 \to 0=0,\ 0=0)$, whilst FOL's modus ponens wouldn't. So, in this nitpicky sense, rules of inference of different first order theories aren't the same; they depend on your theory's signature. In a less nitpicky sense, they are the same; and can be chosen to be exactly modus ponens and generalization.