Transforming Hilbert-style Axiom Systems for Classical Propositional Logic and Retaining Soundness and Completeness

Question

First off, I will use ~ for negation, & for conjunction, V for disjunction, -> for implication, and <-> for bi-conditional.

To the question:

The axioms of classical propositional logic (CPL) are dependent upon the logical signature of the language. For example, if one uses the signature {~, ->}, then the following three axioms with modus ponens give a sound and complete axiomatization for classical propositional logic:

• p -> (q -> p)
• (~q -> ~p) -> (p -> q)
• (p -> (q -> r)) -> ((p -> q) -> (p -> r))
• A, A->B |- B (modus ponens)

However, if we look at the axiomatization on the wiki page (https://en.wikipedia.org/wiki/Propositional_calculus) for CPL with the signature {~,&,V,->,<->} it consists of more axioms (each encoding introduction and elimination facts about each connective).

My question is the following: If we change from one logical signature to another, then does an axiom system for one signature serve as an axiom system for another signature? (Of course, we would have to re-write the axioms in the language of the new signature; e.g. re-write A -> B := ~A V B) If so, why is this true? More specifically, would it be correct to say that if I am working with formulae in negation normal form NNF (using the signature {~,&,V}), then does the axiom system I provided above (which is written in the signature {~,->}) qualify as a sound and complete axiomatization for NNF CPL when the formulae are translated to the signature {~,&,V} accordingly?

Answer 1

Also, it appears that one can argue as follows. Suppose that the axiom system in my initial question is called A1 and let A2 be the axiom system obtained by transforming each axiom (and modus ponens) into NNF. We know that A1 is sound and complete with the signature {~,->}. Also, let T1 be a translation that translates (in the usual way) formulae from the signature {~,->} into an NNF formula (which is in the signature {~,&,V}), and let T2 be a translation function that does the opposite.

(1) Completeness: Suppose that a formula X in NNF is CPL-valid. Then, it is easy to see that T2(X) is CPL-valid. Hence, T2(X) is derivable in A1. It seems that one can show that every derivation in A1 can be transformed into a derivation in A2 by applying T1 to all of the formulae of the derivation. Therefore, we will obtain a derivation in A2 of T1(T2(X)) = X.

(2) Soundness: Simple; by induction on the length of the derivation in A2.

Answer 2

It doesn't hold in general that by switching connectives, that we'll still get a sound and complete axiom set.

One example of an axiom set for classical logic, in Polish notation, is:

1. CpCqp
2. CCpCqrCCpqCpr
3. CCCpq0p

But, if we switch to using 'N', with an instance of Cx0 replaced by Nx, then the above system would have

3' CNCpqp

instead of 3. above. However, {1, 2, 3'} is not an axiom set capable of deriving all of C-N tautologies under modus ponens and uniform substitution.