Substitution in Propositional calculus.

Question

There are two axiom system of propositional calculus. One has only atomic variables in its axioms. Another has schemes of axioms with variables of well-formed formulas.

https://en.wikipedia.org/wiki/Propositional_calculus#Example_1._Simple_axiom_system https://en.wikipedia.org/wiki/Propositional_calculus#Axioms How to prove that they are equivalent?

Any tiny example of proof is welcome.

My ideas:

1) First of all to simplify the task we need to get rid of connectives and prove it about implicative fragments of the calculi.

2) We can prove that "schematic" calculus is correct, and that "atomic" one is complete. (with respect to the same semantics in both cases). Therefore they are proving essentially the same things. With trivial fact that "schematic" calculus contains everything that "atomic" has we obtain that they are equivalent. That is not an easy way of doing it.
May be it is possible to prove it semantically? If it's not possible, where can I find a completeness proof for "atomic" calculus?

3) It is also may be proved with substitution theorem for "atomic" calculus. Where can I find a good proof of the substitution theorem?

Answer 1

The first one needs, in addition to Modus Ponens rule, a Rule of substitution :

"if $A$ and $B$ are formulas and $p$ a sentential letter, from $A$ infer $\text S_B^p(A)$",

where $\text S_B^p(A)$ is the formula resulting from $A$ by susbtitution of each occurence of $p$ in $A$ with $B$.

See Alonzo Church, Introduction to Matematical Logic (1956), page 72.

Answer 2

I would show how you can emulate the rules of one system in the other, and vice versa where, as you say, we restrict ourselves to those rules involving negation and implication.

This is not easy though! In fact, without relying on the Deduction theorem (this is referred to as the 'Meta-Inference' rule on that same Wikipedia page), this is a major pain in the ass. So, let's assume we at least can make use of the Deduction Theorem to show that certain things are provable. (the good news is that the Deduction Theorem can be proven for any system that has $\phi \to (\psi \to \phi)$ and $(\phi \to (\psi \to \chi)) \to ((\phi \to \psi) \to (\phi \to \chi))$ among their axioms, which both systems do)

In fact, here is a simple example of the use of the Deduction Theorem. Let's first show that $\phi \to \psi, \psi \to \chi, \phi \vdash \chi$:

\begin{array}{lll} 1& \phi \to \psi&Assumption\\ 2& \psi \to \chi&Assumption\\ 3&\phi&Assumption\\ 4&\psi&MP \ 1,3\\ 5&\chi&MP \ 2,4\\ \end{array}

OK, so then we can apply the Deduction Theorem to conclude that:

$\phi \to \psi, \psi \to \chi \vdash \phi \to \chi$ (HS)

Now, you can go here to see how you can use the first system (again using the Deduction Theorem), to see that:

$\vdash (\neg \phi \to \phi) \to \phi$ (Law of Clavius)

and

$\vdash \neg \neg \phi \to \phi$ (DNE)

And once you have those, you can do:

\begin{array}{lll} 1&\phi \to \psi&Assumption\\ 2&\phi \to \neg \psi&Assumption\\ 3&\neg \neg \phi \to \phi&DNE\\ 4&\neg \neg \phi \to \psi&HS \ 3,1\\ 5&\neg \neg \phi \to \neg \psi&HS \ 3,2\\ 6&(\neg \neg \phi \to \neg \psi) \to (\psi \to \neg \phi)&Axiom \ 3\\ 7&\psi \to \neg \phi&MP \ 5,6\\ 8&\neg \neg \phi \to \neg \phi&HS \ 4,7\\ 9&(\neg \neg \phi \to \neg \phi) \to \neg \phi&Law \ Of \ Clavius\\ 10&\neg \phi&MP \ 8,9\\ \end{array}

And doing Deduction Theorem twice, this tells us that:

$\vdash (\phi \to \psi) \to ((\phi \to \neg \psi) \to \neg \phi)$

and hence we know that we can emulate the NOT-1 rule from the second system in the first system.