# Proving things about a formal logical system

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.

• Does this answer to a similar question help? (You might just read the last sentence first.) – Andrej Bauer Nov 11 '20 at 19:40
• It helps. I understand the inevitability of leaving philosophical questions to philosophers and the methodology of thinking about and doing research in mathematical logic as one would in any mathematical discipline (cue: "mathematical" is the adjective in front of "logic") using human logic and ordinary mathematics. – Wei Nov 11 '20 at 21:56
• One point there is, why do you expect logicians to have different standard for doing mathematics than all the other mathematicians? Do you think it's somehow their task to "build a foundation"? I think that's a very misguided task. – Andrej Bauer Nov 11 '20 at 23:09
• That's a good point! I did have the impression that one of logicians' job was to create a formal foundation from scratch but soon realized the difficulty of not using mathematics and then the ambiguity of logical operations permitted to use. Now I understand, or at least, I can agree with your stand on this issue. – Wei Nov 12 '20 at 4:55