[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> logic
[Index] || [Contents] || [Grades] Tue Aug 5 11:45:02 PDT 2003

# The Natural Deduction Logic of Huth and Ryan

## Introduction

This is a translation of the natural deduction systems of logic in [HuthRyan00] into my own MATHS notation.

## Syntax

The following uses XBNF to describe well formed formula.

1. wff::=Well Formed Formula.

The book defines wff like this:

2. Rough_Syntax::=following,
Net
1. atomic_proposition::=given.
2. wff::=atomic_proposition | "(" "not" wff ") | "(" wff "and" wff ")" | "(" wff "or" wff ")" | "(" "if" wff "then" wff ")".

.As-is (if (P and Q) then (R and S)) .As-is ((P and Q) or (R and S))

(End of Net)
The book then appeals to using operator priorities to avoid parentheses: .As-is if P and Q then R and S .As-is P and Q or R and S

It is possible to express operator priorities directly in the syntax instead. Here is the result:

3. wff::= implication | disjunction | conjunction | negation | atomic_proposition | compound.
4. implication::= "if" wff1 "then" disjunction.
` 		if p then q`
` 		if p and q then q or p`
5. disjunction::= conjunction #("or" conjunction).
` 		p or q or not r or s and t`
6. conjunction::= negation #("and" negation).
` 		p and not q`
7. negation::= #("not") ( atomic_proposition | compound).
` 		p`
` 		not p`
` 		not( p or not q)`
` 		( p or not q)`
8. compound::= "(" wff ")".
` 		( p or not q)`
9. atomic_proposition::=given.

## Semantics

10. semantic_structure::= atomic | Structure with op:Operators & rands:#Operands.
11. Operators::={ and, or, not, if_then ).
12. Operands::=semantic_structure.
` 	 the semantic_structure(and, p, q).`
` 	 the semantic_structure(and, p, the semantic_structure(if_then, p, q)).`

## Parsing

This is a matter of defining a map from syntax to semantics.
1. if P and Q then R or S +> the semantic_structure(if_then, the semantic_structure(and, P, Q), the semantic_structure(or, R,S)).

More TBA.

## Meaning

Meaning is normally provided by rules evaluating a semantic structure as either true or false. We therefore would define a function that evaluates a semantic structure as a boolean. This is very easy using recursion. For example, to evaluate the_sematic_structure(and, P, Q) for the two structures P and Q, in C++ we would
` 		return evaluate(P) && evaluate(Q);`

## Reasoning

Examples of reasoning are given as [ Proofs of Derived Rules ] below.

### Notation for rules

Inference rule is shown like this:
13. (name_of_the_rule): conclusion:-premise, premise,....

It is used in a proof like this:

14. (labels_of_premisses_and_ruls) |- (label_of_conclusion): conclusion.

In a MATHS rule a wff like if P then Q often becomes a Let-block like this:
Let

1. |- (premise_label): P.
2. ...
3. Q

(Close Let P)

### Rules

The names of the rules have been translated. Instead of "^i" for example I would use "andi".

15. HuthRyan::=following,
Net

#### Propositions

from page 31.
1. |- (andi): P and Q :- P, Q.
2. |- (ande1): P:-P and Q.
3. |- (ande2): Q:-P and Q.
4. |- (ande): repeated use of ande1 and ande2 to extract on part of a conjunction.
5. |- (ori1): P or Q:-P.
6. |- (ori2): P or Q:-Q.
7. |- (ori): repeated applications of ori1 and ore2 to assemble ... or P or ... from P.
8. |- (ore): R :- (P or Q), if P then R, if Q then R
9. |- (ife): Q:-P, if P then Q.
10. |- (ifi): if P then Q :-
Let
1. P.
2. ...
3. Q.

(Close Let P)

11. |- (noti): not P :- if P then \bottom.
12. |- (note): \bottom :-P, not P.
13. |- (bottome): P:-\bottom.
14. |- (notnote): P:-not not P.

##### Derived rules

15. (above) |- (MT): not P:-if P then Q, not Q.
16. (above) |- (notnoti): not not P :- P.
17. (above) |- (RAA): P :- if not P then \bottom.
18. (above) |- (LEM): P or not P.
##### Note
In practice the above rules are very well known. If you are working with a team of people who know this logic you can usually omit the names of the rules you are using.

. . . . . . . . . ( end of section Propositions) <<Contents | Index>>

#### Predicates

Notation
19. For t:term, x:variable, P: wff, if free(t,x,P),
20. P(t/x)::= P with every free x changed to term t.
21. free(t,x,P)::=No free variable in t is bound in a part of P that has a free x, -- no variables will be captured if t is substituted for x.

22. |- (eqi): t = t.
23. |- (eqe): P(t2/x) :- t1=t2, P(t1/x).
24. |- (alle): P(t/x):- for all x(P).
25. |- (alli): for all x (P) :-
Let
1. x.
`	...`

2. (above) |- P.

(Close Let )

26. |- (somei): for some x(P) :- P(t/x) .
27. |- (somee): Q :- for some x(P).
Let
1. x0, P(x0/x).
`	...`

2. (above) |- Q.

(Close Let )

Notice that we could derive several other rules to simplify proofs. Here is an example. The wff for all x, if P then Q can always proved by using two nested let-blocks:
Let

1. x
Let

1. |-P
` 		...`

2. (above) |- Q.

(Close Let P)

(Close Let x)
and so we can compress this to
Let
1. x
2. |-P
` 		...`

3. (above) |- Q.

(Close Let x)

. . . . . . . . . ( end of section Predicates) <<Contents | Index>>

(End of Net)

. . . . . . . . . ( end of section Rules) <<Contents | Index>>

. . . . . . . . . ( end of section Reasoning) <<Contents | Index>>

## Proofs of Derived Rules

### Proof of MT

Given if P then Q, not Q, prove not P.
Let

1. |- (MT1): if P then Q.
2. |- (MT2): not Q.
Let

1. |- (MT2a): P.
2. (MT1, MT2a) |- (M2b): Q.
3. (M2b, MT2) |- \bottom.

(Close Let P)

3. (above) |- not P.

(Close Let MT1 MT2)

### Proof of notnoti

Given P prove not not P
Let

1. |- (dn1): P.
Let

1. |- (dn2): not P.
2. (dn1, dn2) |- \bottom.

(Close Let not P)

2. (above) |- not not P.

(Close Let P)

### Proof of RAA

Given if not P then \bottom, then prove P.
Let

1. |- (r1): if not P then \bottom.
Let

1. |-(r2) not P.
2. (r1, r2, ife) |- \bottom.

(Close Let not P)

2. (above) |- P.

(Close Let r1)

### Proof of LEM

16. Prove P or not P.
Let

1. |- (l1): not(P or not P).
Let

1. |- (l2): P
2. (l2, ori1) |- (l3): P or not P.
3. (l3, l1) |- \bottom.

(Close Let P)

2. (above) |- (l4): not P.
3. (l4, ori2) |- (l5): P or not P.
4. (l5, l1, note) |- \bottom.

(Close Let not(P or not P).)

17. (above) |- (l6): not not (P or not P).
18. (l6, notnote) |- P or not P

. . . . . . . . . ( end of section Proofs of Derived Rules) <<Contents | Index>>

. . . . . . . . . ( end of section The Natural Deduction Logic of Huth and Ryan) <<Contents | Index>>

# Glossary

19. O::=optional.
20. TBA::="To Be Announced".