5

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

Richard Evans
  • 303
  • 2
    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 08 '13 at 16:22
  • 1
    Oops yes, I mean the latter. – Richard Evans Nov 08 '13 at 16:24
  • I edited the question. Thanks Hagen. – Richard Evans Nov 08 '13 at 16:25
  • 1
    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 08 '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 08 '13 at 16:42
  • I can't see how you get $p \land q \vdash q \land p$ from those axioms. – Richard Evans Nov 08 '13 at 16:43

2 Answers2

3

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.

Peter Smith
  • 54,743
  • 1
    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
1

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)$
Richard Evans
  • 303