I don't really know much about formal logic. But there is a kind-of-philosophical question that has always been bothering me. It seems to me that, in the context of mathematical logic, we are permitted to use mathematics and "common" logic to reason about logical systems we study. I want to know if my understanding is correct. More precisely, I want to know the answers to the following (very vague) questions.


Consider a statement A about a deduction system $\mathcal{D}$. For instance, A is the statement that a certain formula is formally provable from $\mathcal{D}$.


(1) Is it true that this statement A and a proof of it are on the meta-mathematical level?


(2) What are the rules that we are permitted to use to prove statement A? I will illustrate this by an example: in proving Goedel's Completeness Theorem, mathematical induction (a mathematical construct, supposedly having some mathematical content, at least meta-mathematically) and proof-by-contradiction (a logical construct) are apparently being used. Base upon this example, let me rephrase question (2) in the following smaller parts:


(2.a) Is there an agreement among practitioners of mathematical logic on the kinds of ordinary mathematics that are allowed?


(2.b) Consider a certain piece of mathematics, denoted by $\mathcal{M}$, together with the collection $\mathfrak{F}(\mathcal{M})$ of formalizations\axiomatizations of $\mathcal{M}$. Is it a sensible question to ask about the dependencies of the deduction system $\mathcal{D}$ upon each $\mathcal{F}\in\mathfrak{F}(\mathcal{M})$ based on the results about $\mathcal{D}$ that are deducible from $\mathcal{M}$? Here, the word "deducible" should be taken to mean "meta-mathematically deducible" if the answer to (1) is yes. More specifically, can we make sense of the following diagram or perhaps the reversed arrow?


$\{\text{dependencies of }\mathcal{D}\text{ on }\mathcal{F}\in\mathfrak{F}(\mathcal{M})\}\longrightarrow\{\text{results }A\text{ about }\mathcal{D}\text{ deducible from }\mathcal{M}\}$.


If we can, what kind of structures do these things have? This is the place in my question where I think category theory or homotopy theory might be relevant.


(2.c) As for the logical constructs, it seems we are allowed to use usual, everyday logic. But if we were to prove something about a formal logical system that is somewhat intuitionistic where proof-by-contradiction is not formally available, it would lead to a philosophical problem of using a meta-mathematical reasoning framework (everyday human logic, so to speak) where proof-by-contradiction is allowed to deduce results about a formal system where proof-by-contradiction is not allowed.


I would really appreciate it if you could also give me some references.



Proving things about a formal logical system
So in a usual mathematical proof you choose some system if axioms from which you prove it. For instance, there are claims about the natural numbers you can prove in ZFC but not from the axioms of Peano Arithmetic.


Exactly the same thing is true when you prove things about a formal system (eg proof system or logic). There aren't abstract proofs just floating out there in no system at all you always have to specify the meta-system in which you are proving your results in (at a formal level when you prove things about proofs you are usually treating the proof relation just as a particular sort of relation on integers which are regarded as coding sentences or sequences of sentences) and depending on which system you use at the meta-level you may be able to prove different things. So strictly speaking results should always be of the form ZFC (or PA or ...) proves such and such about logic/proof system blah. But that's frequently omitted when it won't cause a confusion.


As for your later questions about proving things about intuitionistic logic classically that really depends on your motivations for caring about intuitionistic logic. A philosopher who is using intuitionistic logic because they think classical logic is suspect and inferences in it not truth preserving would, of course, only trust results about intuitionism proved intuitionisticly (very few people seem to really take that position even in philosophy). OTOH if your interest is in the practical use of intuitionistic logic in certain CS applications you'll be happy with proofs about it in ZFC.


Does that kinda answer your question?


