Are inference laws consistent?

Question

Please forgive me if this question sounds too naive... Well, in mathematics a formal theory consists of a collection of axioms $T$ (such as Peano arithmetics, or Group Theory, or ZFC), which essentially are certain structured chains of symbols, and theorems can be derived from them by applying certain deduction rules (or "inference laws"). These deduction rules are themselves formalizable by some axioms $\Lambda$ (such as the Hilbert-Frege deduction system).

Gödel's second incompleteness theorem states, roughly, that we cannot prove (and, to be able to prove something, we leave some fixed inference laws $\Lambda$ as understood) the consistency of any set of axioms $T$ (working within $T$).

What about the consistency of the inference system $\Lambda$ itself alone? That is, does Gödel's theorem apply somehow also to $\Lambda$ so that nobody is able to "prove" that it will not lead to a contradiction?

Answer 1

First, Gödel’s theorem says only that the theory itself cannot prove its own consistency (under some assumptions). It’s perfectly possible (and not particularly difficult) to prove the consistency of, say, Peano arithmetic (in usual mathematics, i.e., in ZFC).

Likewise, we can prove the consistency of the predicate calculus without non-logical axioms (your $\Lambda$). One possibility is as follows: take a proof of contradiction, and show by induction on the length of proof that all formulas in the proof are valid in the one-element model which does not satisfy any predicates. (Note that satisfaction in a one-element model is easy to define, as it’s essentially just propositional logic: you can ignore quantifiers and terms.)

If you are more syntactically-minded, you can also regard this as a reduction of first-order logic to variable-free propositional logic: strip all quantifiers, and replace all atomic formulas with $\bot$ (or any fixed false formula, if you do not have $\bot$ in the basic list of connectives). Then it suffices to show the consistency of (the variable-free fragment of) propositional calculus.

Answer 2

A somewhat stronger property than mere consistency, which is universally desired in a proof system, is the property of soundness.

A formal system is sound, if whenever it proves a statement $\varphi$ from some axioms $T$, then indeed $\varphi$ is true in any model satisfying $T$. In particular, when $T$ is the empty theory, then we want every statement $\varphi$ proved in the system to be true in every structure. This is usually very easy to prove for a given formal system, usually by induction on the length of the proof, simply by observing that the inference rules are truth-preserving. In contrast, the formal system is complete if it succeeds in proving $\varphi$ from $T$ whenever $\varphi$ is true in all models of $T$, and this is the nontrivial part of the completeness theorem.

Answer 3

If I understand your question correctly, you're wondering whether the consistency of first-order logic without any axioms can be proved using first-order logic, without assuming any axioms.

The trouble is that if you don't allow yourself any axioms, then it's unclear how you would even express the statement "first-order logic is consistent." The reason that Goedel's incompleteness theorem applies to systems that encode at least a minimal amount of arithmetic is so that you can encode concepts such as "axiom" and "inference rule," without which we cannot even define what "consistency" means.

Answer 4

First, a remark. You formulate both Gödel's theorem and your question in a subjective way "we cannot prove", etc. However, this theorem is a mathematical one, therefore it is not about our ability to do something, but about the nonexistence of a mathematical object, namely a formal proof within the system concerned. You can draw some e.g. philosophical conclusions from this theorem, but this is a completely another matter.

Now, as far as your question concerned, it is almost certain that nothing analogous to Gödel's theorem can even be stated for the pure first order logic itself. The reason is simple. The analogous theorem would claim the unprovability of the formula expressing the the fact that a contradiction is unprovable within the pure first order logic. But, in the absence of the formal provability predicate, this theorem cannot even be stated. Actually, what we would like to show is that there is a formula $Pr(x)$ such that, on the one hand, it can be considered a provability predicate (that is, for any formula $\varphi$, $Pr(\ulcorner \varphi \urcorner)$ is true just in case $\vdash \varphi$ (here, of course, $\ulcorner \varphi \urcorner$ is the Gödel number of $\varphi$), on the other hand, the formula expressing the fact that a contradiction is unprovable is itself unprovable: $\not\vdash \lnot Pr(\ulcorner 0=1\urcorner)$. Now, the proof of the existence of a provability predicate seems to require much more than pure logic.