Axiomatisation of propositional logic using $\land$ and $\neg$

I am looking for a simple axiomatisation of a particular version of propositional logic that is defined in terms of $\land$ and $\neg$ only.

I am guessing that it only needs one rule of inference: $p, \neg(p \land \neg q) \vdash q$.

Can you give me a short set of axioms to add to this inference rule?

(I did look around on the googly internet, and found this http://en.wikipedia.org/wiki/List_of_logic_systems but it did not answer my question).

thanks, Richard

• Do you really mean $p\land \neg(p\land \neg q)\vdash q$? Or rather $p, \neg(p\land \neg q)\vdash q$? – Hagen von Eitzen Nov 8 '13 at 16:22
• Oops yes, I mean the latter. – Richard Evans Nov 8 '13 at 16:24
• I edited the question. Thanks Hagen. – Richard Evans Nov 8 '13 at 16:25
• Out of the blue, we want to be able to infer $p$ and $q$ from $p\land q$, so I suggest to include $\neg((p\land q)\land \neg p)$ and $\neg((p\land q)\land \neg q)$ in the axioms. To infer $p\land q$ from $p,q$, we could use $\neg(p\land\neg\neg(q\land\neg(p\land q)))$. To infer $p$ from $\neg\neg p$ and vice versa, we could use $\neg(\neg\neg p\land\neg p)$ and $\neg(p\land\neg\neg\neg p)$. This would essentially add the relevant rules of inference expected for $\land$ and $\neg$, but I'm not sure if these are enough (or redundant). – Hagen von Eitzen Nov 8 '13 at 16:32
• Thanks for explaining the thought-process. I like the way you translate the introduction and elimination rules directly into axioms. – Richard Evans Nov 8 '13 at 16:42

A query rather than a straight answer. It is something of an unfortunate historical accident that early formal systems of logic (Frege, Russell/Whitehead, Hilbert) went for many-axioms/few-rules. These systems are pretty unnatural, and indeed in the background there is arguably a mistake about what logic is about. For the early founding fathers tended to speak as if logic was about cataloguing logical truths, rather than valid proofs -- take the latter view, and you'll conceive of the natural way of presenting a logic as a system of rules of inference which you can use in constructing mathematical and other proofs, rather than as a system of logically true axioms from which more logically true propositions can be derived.

So I do wonder why, other than for a somewhat pointless technical exercise, we should nowadays be interested in presenting a many-axioms/one-rule system of logic for negation/conjunction, rather than a much more natural no-axioms/many-rules system? And for the latter, lots of standard textbooks deliver the goods for free. To get a complete natural deduction system for negation and conjunction just take the system for the usual four or five connectives and leave out the rules for disjunction and the (bi)conditional.

• The reason I want an axiomatisation is because I want a translation from propositional logic to an unfamiliar modal logic. I want the simplest possible formulation of propositional logic(/\,~) to minimize the number of translations I need to do. If I used natural deduction, I would have to translate the structural rules as well. – Richard Evans Nov 11 '13 at 10:56

I found a suitable axiomatisation in Mendelson (he cites Rosser 1953).

It uses Modus Ponens ($p, \neg(p \land \neg q) \vdash q$) plus three axioms:

• $\neg (p \land \neg (p \land p))$
• $\neg ((p \land q) \land \neg p)$
• $\neg (\neg (p \land \neg q) \land \neg (q \land r) \land r \land p)$