I guess, I do not need to reference axioms used by Mendelson; though, rules of inference are Gen and MP. Here is the statement of Exercise 2.28 in Mendelson's Introduction to Mathematical Logic, 6th edition:
Let $K$ be a first-order theory and let $K^\#$ be an axiomatic theory having the following axioms:
- $(\forall y_1) \dots (\forall y_n) \mathscr B$, where $\mathscr B$ is any axiom of $K$ and $y_1,\dots,y_n$ $(n \geq 0)$ are any variables (none at all when $n=0$);
- $(\forall y_1) \dots (\forall y_n) (\mathscr B \rightarrow \mathscr C) \rightarrow [(\forall y_1) \dots (\forall y_n) \mathscr B \rightarrow (\forall y_1) \dots (\forall y_n) \mathscr C]$, where $\mathscr B$ and $\mathscr C$ are any wfs and $y_1,\dots,y_n$ are any variables.
Moreover, $K^\#$ has modus ponens as its only rule of inference. Then $K^\#$ has the same theorems as $K$.
My proof attempt:
Assume $\vdash_K \mathscr B$ has a proof in $K^\#$. This assumption is justified, since proofs involving only MP are valid in $K^\#$. So we only want to show that $\vdash_{K^\#} (\forall y) \mathscr B$. Let $\mathscr D_1,\dots,\mathscr D_n$ be a proof of $\mathscr B$ in $K^\#$. If $\mathscr B$ is an axiom, clearly $\vdash_{K^\#} \mathscr (\forall y) \mathscr B$. If it is not, there are $\mathscr D_i$ and $(\mathscr D_i \rightarrow \mathscr B)_j$ steps from which $\mathscr B$ follows by MP. We can derive $(\forall y) \mathscr B$ from $$ (\forall y)(\mathscr D_i \rightarrow \mathscr B)_j \rightarrow [(\forall y) \mathscr D_i \rightarrow (\forall y) \mathscr B]. $$ If both $\mathscr D_i$ and $(\mathscr D_i \rightarrow \mathscr B)_j$ are axioms, we have $\vdash_{K^\#} (\forall y) \mathscr B$. If some of them is not an axiom, say $\mathscr D_i$, we can derive $(\forall y) \mathscr D_i$ with the same procedure. So, in the end, we have $\vdash_{K^\#} (\forall y) \mathscr B$.
My questions:
- Is the proof correct and rigorous? If it is not, what is the flaw in my reasoning?
- I used induction implicitly, is it allowed? I know that in logic you are supposed to use induction frequently, but what about using it in the vagueness? I suppose, this makes my argument less rigorous and more draft-like?
- Continuing on my question about induction; did I use it correctly, in terms of the overall correctness of the argument?