Propositional Calculus - Example 2. Natural Deduction System

Example 2. Natural Deduction System

Let, where, are defined as follows:

• The alpha set, is a finite set of symbols that is large enough to supply the needs of a given discussion, for example:

• The omega set partitions as follows:

In the following example of a propositional calculus, the transformation rules are intended to be interpreted as the inference rules of a so-called natural deduction system. The particular system presented here has no initial points, which means that its interpretation for logical applications derives its theorems from an empty axiom set.

• The set of initial points is empty, that is, .
• The set of transformation rules, is described as follows:

Our propositional calculus has ten inference rules. These rules allow us to derive other true formulae given a set of formulae that are assumed to be true. The first nine simply state that we can infer certain wffs from other wffs. The last rule however uses hypothetical reasoning in the sense that in the premise of the rule we temporarily assume an (unproven) hypothesis to be part of the set of inferred formulae to see if we can infer a certain other formula. Since the first nine rules don't do this they are usually described as non-hypothetical rules, and the last one as a hypothetical rule.

In describing the transformation rules, we may introduce a metalanguage symbol . It is basically a convenient shorthand for saying "infer that". The format is, in which is a (possibly empty) set of formulae called premises, and is a formula called conclusion. The transformation rule means that if every proposition in is a theorem (or has the same truth value as the axioms), then is also a theorem. Note that considering the following rule Conjunction introduction, we will know whenever has more than one formula, we can always safely reduce it into one formula using conjunction. So for short, from that time on we may represent as one formula instead of a set. Another omission for convenience is when is an empty set, in which case may not appear.

Reductio ad absurdum (negation introduction)

From and, infer .

That is, .

Double negative elimination

From, infer .

That is, .

Conjunction introduction

From and, infer .

That is, .

Conjunction elimination

From, infer .

From, infer .

That is, and .

Disjunction introduction

From, infer .

From, infer .

That is, and .

Disjunction elimination

From and and, infer .

That is, .

Biconditional introduction

From and, infer .

That is, .

Biconditional elimination

From, infer .

From, infer .

That is, and .

Modus ponens (conditional elimination)

From and, infer .

That is, .

Conditional proof (conditional introduction)

From, infer .

That is, .