On the Logic of Logics

Question

I am teaching myself logic (from various sources), and I was viewing this video: https://youtu.be/IOiZatlZtGU. I had a few questions about 'proving' statements about logic in logic.

• At 16:50 (https://youtu.be/IOiZatlZtGU?t=996), the speaker talks about how we can prove that Gentzen's system of Natural Deduction is consistent (that is, there is no proof of ⊥). The argument goes as follows: "the sub-formula property says a proof of ⊥ should have ⊥ and only sub-formulas of ⊥. Since there is no sub-formula of ⊥, there is no proof of ⊥".

• This argument seems quite simple, and it seems to me (perhaps incorrectly) that one should be able to formalize this argument (about Natural Deduction) formally using Natural Deduction itself.

  • However, this seems to contradict Gödel's second incompleteness theorem (that is, a (powerful enough) logical system cannot prove its own consistency).
  • Clearly, I've made a mistake somewhere. Perhaps:
    1. Natural Deduction is not powerful enough, and therefore can prove its own consistency?
    2. Natural Deduction cannot encode itself / 'talk about itself'?
    3. We cannot formalize the argument presented in the video in Natural Deduction.
  • I think at least one of these 3 should be incorrect. I am curious to know what they are.

• I think, more generally, I am curious about how one formally proves 'things' (like consistency, etc.) about logics themselves:

  • If L1 is a logic, and we want to formally reason about L1, I think we'd need to encode L1 (all its axioms and rules of inference) in another (equally or more powerful?) logic L2, where we can make statements like 'L1 is consistent', etc. Is this true? What makes a logic 'more powerful' than another logic?

Answer 1

If we are discussing Gentzen’s natural deductive system as a mathematical object itself, we must be in a suitably expressive metatheory such as Peano Arithmetic or ZFC. We can then prove in that theory (using induction, a fairly powerful mathematical tool) that natural deduction cannot prove $\bot$.

It is not clear how one could encode the statement “Natural deduction is consistent” in pure first-order logic, which is the system natural deduction uses. Instead, one must consider a particular first-order theory like Peano Arithmetic, think about its intended model, and then perform definitions which, in the intended model, define the statement “natural deduction is consistent”. This is a fundamentally metamathematical task.