# Using logic to do metalogical proofs? Is there a circularity problem here?

(1) If modus tollens were not correct, then I could have (P-->Q), ~Q and P.

(2) But I cannot have (P--> Q) , ~Q and P. For, in that case, I would have (~P v Q) and ~Q and P; which means I would have ~P and P, which is impossible.

(3) Therefore it's not the case modus tollens is not correct, that is, modus tollens is a correct rule of reasoning.

Here I have used modus tollens to justify the correctness of modus tollens.

That seems circular.

The question I am asking myself is: what allows logicians to use logic in metalogical proofs, that is , when they prove that such and such formula is valid or that such and such rule of inference is correct?

• Do you have a specific example of a metalogical proof that proves that an inference rule is correct? Usually metalogical proofs are such that prove things about the mathematical structure of a given logic, e.g., completeness for S4 modal logic. – Eliran Nov 16 '19 at 22:44
• No. There would be a problem if the goal was to justify everything based on nothing, and it is of regress (of logics at different levels) rather than of circularity. Carrol made a nice play on it in What the Tortoise Said to Achilles. But the goal is instead to apply what we have to master operationally anyway, reasoning skills. And they can be applied within a theory (object language) just as well as to reason about theories (meta-language). – Conifold Nov 16 '19 at 23:19
• The part in notation is not a statement about reality. it is a collection of conventionalized symbols linked to some set of rules. Modus tollens is a statement about reality. You can prove the notation and its prescribed set of rules works in a manner parallel to modus tollens, but you cannot prove modus tollens. You have to accept it by introspection. – user9166 Nov 17 '19 at 1:56
• There is no way to justify laws of logic without some sort of argument, and every argument needs logic. – Mauro ALLEGRANZA Nov 17 '19 at 10:47
• The "standard" approach is to justify laws of logic with semantical arguments, that of course use some basic logic pronciple. – Mauro ALLEGRANZA Nov 17 '19 at 10:48

You cannot use logic in metalogic to justify logic. Logic simply cannot be justified. It can be reasoned about, but there is no kind of reasoning about it that can validate, verify or strengthen it. And that kind of reasoning is not metalogic. It is just straightforward epistemology.

In fact, there are examples like Steven Kleene, who did both. He did significant metalogical work in a classical sense and proposed philosophically that our current practices in mathematical logic should be changed significantly. He was an intuitionist, but he also took part in metamathematical research of the ordinary variety. If the point of metalogic was to somehow justify logic, that would not just be circular, it would be a contradiction.

Verifying human logic is not what metalogic does.

Metalogic investigates what alternatives for the ordinary rules of logic might work, what happens if you trade out one rule for another, for instance.

Model theory and category theory imagine smaller models of sets of axioms than the entire world of application that are selected to reproduce as many of the same combinations and processes as possible that are actually related directly to the rules and are not spurious additions from experience. Then it studies the relationships between those objects.

Other approaches to metalogic study the process of proof the way one would debug an algorithm. The intention is not to justify the proofs, but to see if there are techniques that we are used to, that do not accomplish the same things in different environments.

The question is always, what would happen if things were slightly different, slightly simpler, or slightly more complex than ordinary cases. It is not to justify current practices. We get results like Goedel's theorem out of metalogic by looking at a significantly simplified case, not at ordinary logic. It makes no attempt to prove our logic correct, though there is a step that proves that we largely get what we expect out of the formalism with which the rest of the proof is going to proceed.