Logiweb(TM)

8.6.2 A complete set of connectives

Prev Up Next Page 348 of 800 Search internet


Mendelson: 'Introduction to mathematical logic' bases Propositional Calculus on the connectives x imply y and not x. Those two connectives form a complete set of connectives in the sense that any Boolean function of arity 1 or more can be expressed using nothing but function parameters and those two connectives. As an example, Boolean 'or' may be expressed thus:

math define x or y as not x imply y end define

There are, however, two Boolean functions of arity zero. They are the Boolean constants tt (truth) and ff (falsehood). One cannot define them from x imply y and not x without resorting to something extra like a free variable or an arbitrary constant.

To get a completely complete set of connectives, we use x imply y and ff instead of x imply y and not x. And we define not x and tt thus:

math define not x as x imply ff end define

math define tt as ff imply ff end define

Having tt and ff allows to state Propositional Calculus differently from the way Mendelson does. But we nevertheless follow Mendelson closely so that you can sit with Mendelsons book and the present pages and see a close correspondence.

Having tt and ff, however, also allows to formulate and prove some new proofs. Here is a proof that tt is indeed true:

Prop lemma LTruth : tt end lemma

prepare proof indentation,proof of LTruth : line L01 : Premise >> Prop ; line L02 : Mend1.8 >> ff imply ff ; line L03 : Def ponens L02 >> tt qed

And here comes a proof which states that if we can prove #x under the assumption tt then we can drop the assumption:

Prop lemma LElimHyp : All #x : tt imply #x infer #x end lemma

prepare proof indentation,proof of LElimHyp : line L01 : Premise >> Prop ; line L02 : Arbitrary >> #x ; line L03 : Premise >> tt imply #x ; line L04 : LTruth >> tt ; line L05 : MP ponens L03 ponens L04 >> #x qed

Prev Up Next Page 348 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05