What are the rules of inference used for syntactic consequence in Gödel's Completeness Theorem?

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?

• Their are lots of different formalisms that work, it's basically a matter of taste. You can have only a few rules (e.g. $A,A\rightarrow B \vdash B$) and lots of axioms, or no axioms and lots of rules. Anything that is called first-order logic should do. See: en.wikipedia.org/wiki/First-order_logic#Deductive_systems – James Jan 3 '15 at 0:05
• As James says, you have a lot of choice. Wikipedia doesn't seem to have one joined up account. There is one here mathworld.wolfram.com/First-OrderLogic.html. – Rob Arthan Jan 3 '15 at 15:49
• Godels proofs uses old fashioned Hilbert style proof methods where the only rule of inference is modus ponens but has many axioms, the reason for this that other proof systems are not convertible to godel numbers – Willemien Jan 6 '15 at 3:48

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.

• Your answer is misusing the usual terminology, particular as regards the term "theory" (in the usual terminology, a theory is just a set of sentences, and doesn't have a system of rules of inference associated with it). The completeness theorem says that valid formulas are provable. That's it. It doesn't come in two flavours (although you can view it as a family of theorems parametrised by the signature of the first-order system). The Wikipedia page on this topic is pretty good en.wikipedia.org/wiki/Gödel's_completeness_theorem, – Rob Arthan Jan 6 '15 at 21:35
• Obviously, "my" fo-theory completeness is just a generalization of fol completeness to fo-theory completeness. I made the distinction purely to demonstrate that completeness theorem for fo-theories isn't about a single theory (as in propositional compl.) And I wanted to emphasize that for my last paragraph, where I'm saying that it's not perfectly legal to talk about first order rules of inference as if they are fixed and same for all fo-theories. – Luka Mikec Jan 6 '15 at 22:53
• I am sorry, but that's incomprehensible. – Rob Arthan Jan 7 '15 at 0:20
• Answer or comment? – Luka Mikec Jan 7 '15 at 2:00
• What is incomprehensible is the distinction you are trying to make. The terms "fol completeness" and "fo-theory completeness" are your inventions and have no evident meaning. – Rob Arthan Jan 7 '15 at 8:52