What assumptions and methodology do metaproofs of logic theorems use and employ?

Question

In logic modules, theorems like Soundness and completeness of first order logic are proved. Later, Godel's incompleteness theorem is proved. May I ask what are assumed at the metalevel to prove such statements? It seems to me that whatever is assumed at the metalevel should not be more than whatever is being formulated at the symbolic level.

I'm also asking about methodology. at the meta level, it seems like classical logic is used. So if proving statements about other kinds of logic like paraconsistent logic, then isn't there a discrepancy between what methodology is being formulated and what methodology is being used to prove the statement?

Answer 1

It depends on what you're trying to prove, and for what purpose you are proving these metatheorems.

So, the notion of "more" you're appealing to in asking about the metalevel is not completely well-defined. One common definition of the strength of a logic is "proof-theoretic strength", which basically amounts to the strongest induction principle the logic can justify (in set-theoretic terms, this is the same as identifying the largest set the logic's consistency proves well-ordered). The theory of ordinals classifies logic by this idea. This is natural for two reasons, both arising from Godel's incompleteness theorem. The incompleteness theorem tells us that we cannot prove the consistency of a stronger theory using a weaker one, so to prove consistency it's always the case that you need to assume a stronger logic in the metatheory than of the logic you're proving consistency of. More abstractly, this fact gives rise to a natural partial order on formal logical systems.

However, consistency proofs are not the only thing people are interested in!

Another purpose for giving semantics of logic is to help understand what people who use a different language than you do mean, in your own terms. For example, giving a classical semantics to intuitionistic logic gives traditional mathematicians a way of understanding what an intuitionist means, in their own terms. Likewise, semantics of classical logic in intuitionistic terms explains to intuitionists what classical logics mean. For this purpose, it doesn't matter how much mathematical machinery you bring to bear, as long as it brings insight.

This is the end that something that ends up having big mathematical payoffs. It can illuminate all sorts of surprising facts. For example, Brouwer didn't just have strong opinions about logic, he also made assertions about geometry -- for instance, that the continuum was indivisible -- that are flat-out false, in naive classical terms. A priori, it's not clear what this has to do with the excluded middle. But it turns out that he wasn't just a crazy Dutchman; the logic of smooth analysis is intuitionistic, and using intuitionistic logic exactly manages piles of side-conditions that you'd have to manage by hand if you worked explicitly in its model.

Conversely, studying classical logic in intuitionistic terms gives you a way of exploring the computational content of classical logic. Often, non-classical arguments (such as the use of double-negation elimination) amount to an appeal to the existence of a kind of backtracking search procedure, and sometimes you can show that an apparently-classical proof is constructive because this search is actually decidable. Martin Escardo's work on "exhaustible sets" is a delightful example of this, like a magician's trick. He shows that exhaustive search over some kinds of infinite sets is decidable (it's related to the fact that e.g. the Cantor space is compact).

Answer 2

Here is some more information for the first question. I think that to prove the meta theorems in mathematics, in particular, soundness, completeness, incompleteness, heuristic logic does not exhaust the meta principles being used. Some meta principles relating to heuristic set theory or heuristic category theory must to be used as well. That is because when we talk about a model and a statements true in a model we need to have some notion of set or something equivalent.

It is difficult to understand these meta principles, so we need to cast them into the language of formal logic, formal set theory. I choose Zermelo Fraenkel set theory here. The formal counter part of your question can be considered the question which axioms of set theory necessary for the proof of the formalized version of the theorems. The choice of Zermerlo Fraenkel set theory is in a sense general enough. You might decide that category theory is the genuine language of mathematics but to phrase and prove soundness, completeness, you need to use something of equal strength. The expression may change with different choices of mathematical language, but the mathematical phenomenon remains invariant.

The following is not a very precise answer ( I did not checked the material carefully). I think this might be an approximation to the answer that you want:

Soundness for First Order Logic: We need classical logic, ZF \ {Powerset,Replacement, Infinity}. The checking of Soundness is basically mechanical so we don't need much.

Completeness for First Order Logic: Need all these thing and some weak version of choice, may be Konig lemma. The proof of completness is basically cook up a model of the theory base on the language. We need to add in many constant to make the theory have Henkin property, and this is an iterated process, so we need choice somewhere. I don't think we need power set.

First incompleteness: We need axiom of foundation and axiom of power set in the universe of set and the identification of theory of natural number with theory of $\omega$ with the respectively defined +, x, <. I don't think we need choice here.

Second incompleteness: We still need axiom of founation (PA still must be enumerated by $\omega$ in this situation). I don't think we need power set anymore.

To have the precise answer, we can always look closely at the steps of the proof or search the existing material.

Answer 3

Certainly, classical logic is used in metalogic. I can't think, offhand, of any cases where I think its use is necessary. The methodology of reverse mathematics seems to offer a suitable, constructivist framework for discussing the kind of result that Tran Chieu Minh speaks of: our weak metalogic tells us that, e.g., we need something at least as strong as König's lemma to prove completeness, and as it happens, the converse implication is also true.

I agree with the questioner that "whatever is assumed at the metalevel should not be more than whatever is being formulated at the symbolic level." The danger is that one's metalogical assumptions might be leakier than one thinks.

If you accept this, then it follows some things that some people take to be the task of the metalogic are not: in particular, it is not the purpose of the metalogic to justify the system being studied; indeed, if one can, that tells one that the metalogic may not be well fitted to the task. And, furthermore, the strength of, say, constructivist logics as metalogics provides no kind of case that mathematics should be constructivist.