5
$\begingroup$

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

$\endgroup$
6
  • 2
    $\begingroup$ Do you really mean $p\land \neg(p\land \neg q)\vdash q$? Or rather $p, \neg(p\land \neg q)\vdash q$? $\endgroup$ Nov 8, 2013 at 16:22
  • 1
    $\begingroup$ Oops yes, I mean the latter. $\endgroup$ Nov 8, 2013 at 16:24
  • $\begingroup$ I edited the question. Thanks Hagen. $\endgroup$ Nov 8, 2013 at 16:25
  • 1
    $\begingroup$ 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). $\endgroup$ Nov 8, 2013 at 16:32
  • $\begingroup$ Thanks for explaining the thought-process. I like the way you translate the introduction and elimination rules directly into axioms. $\endgroup$ Nov 8, 2013 at 16:42

2 Answers 2

3
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ 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. $\endgroup$ Nov 11, 2013 at 10:56
1
$\begingroup$

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)$
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .