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?
Best Answer
The first one needs, in addition to Modus Ponens rule, a Rule of substitution :
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.