I'm learning logic from Michael O'Leary's A First Course in Mathematical Logic and Set Theory. In chapter 1 he carefully explains the meaning of logical implication (p ⊨ q), logical inference (p ⟹ q), proof (p ⊢ q), and "star" proof (p ⊢* q). (The "star" proof p ⊢* q means q is provable from p using only a certain restricted set of inference rules—I don't know if any of his terminology/notation is standard.)
As he introduces this material, he also states certain "theorems" and "proofs" about these logical structures. For example,
For all propositional forms p and q, p ⊢* q if and only if p ⊢ q.
Never mind for the moment exactly what his inference rules are and what the exact definition of ⊢* is. What concerns me is what it means exactly that we are "proving" the above result. To be sure, I understand his proof and even agree with it intuitively (he shows that all the inference rules of ⊢ can be achieved using only the restricted rules of ⊢*). What I don't understand is whether it is logically rigorous to say that we are "proving" anything about this logical system, which itself is supposed to be telling us precisely what it means to prove things.
These "meta" theorems and proofs (such as 1.4.2) are certainly not the kind of theorems/proofs that fit within this logical system and proof theory (which tells us nothing about how to formally manipulate strings involving ⊢). Here are some ideas about what they might be instead:
- Informal arguments that could serve as guides for some meta-logical system that is able to rigorously prove statements about this logical system.
- Informal arguments whose sole purpose is to guide how we casually think about, feel about, or interpret our formal logic.
- I'm missing something, and these really are theorems and proofs that could fit within the logical system and proof theory already laid out.