# Would I be able to prove different theorems under different propositional logic systems?

I can find many different formulations of propositional logic systems (i.e. the axioms and transformation rules) all that are sound and complete. Am I correct in understanding that some theorems might be provable (and hence semantically valid) in one system but not in another? In that case, what is semantically valid really depends on the set of axioms I start with? I just want to confirm this. This seems like the case because for example in some formulations of number theory, I cannot prove as many theorems if I don't include axiom of choice.

Thanks!

• Yes, this is accurate. Commented Apr 30, 2020 at 17:06

There are two different concept of "logic" in place here.

We have the so-called Classical Logic, with its semantics, and we have many proof systems (Hilbert-style, Natural Deduction, Truth Tree, Sequent Calculs) that are all sound and complete for it.

All proof systems for Classical Logic proves all and only the same valid formulas.

We have Intuitionistic Logic and we have again many proof systems (Hilbert-style, Natural Deduction, Truth Tree, Sequent Calculs) that are all sound and complete for it.

All proof systems for IL proves all and only the intuitionistically valid formulas.

• I see. Thanks. Are there some (meta) theorems that you can prove about propositional logic independent of specific axioms and deduction rules? Commented Apr 30, 2020 at 17:45
• @ShuhengZheng - meta-theorems are theorem about a system, like e.g. the Deduction Theorem, stating properties of the proof system. Soundness and Completeness are such properties, as well as consistency and decidability. Commented Apr 30, 2020 at 18:33
• But those theorems depend on the choices we make as axioms & deduction rules right? Commented May 1, 2020 at 21:15