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?



What assumptions and methodology do metaproofs of logic theorems use and employ?
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). 


