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

Contents

The Natural Deduction Logic of Huth and Ryan

Introduction

Syntax

wff::=Well Formed Formula.
The book defines wff like this:
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:
wff::= implication | disjunction | conjunction | negation | atomic_proposition | compound.
implication::= "if" wff1 "then" disjunction.
```
 		if p then q
```
```
 		if p and q then q or p
```
disjunction::= conjunction #("or" conjunction).
```
 		p or q or not r or s and t
```
conjunction::= negation #("and" negation).
```
 		p and not q
```

negation::= #("not") ( atomic_proposition | compound).

 		not p

 		not( p or not q)

 		( p or not q)

compound::= "(" wff ")".
```
 		( p or not q)
```
atomic_proposition::=given.

Semantics
semantic_structure::= atomic | Structure with op:Operators & rands:#Operands.
Operators::={ and, or, not, if_then ).
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:
(name_of_the_rule): conclusion:-premise, premise,....
It is used in a proof like this:
(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".
HuthRyan::=following,
Net
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
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).)
(above) |- (l6): not not (P or not P).
(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
O::=optional.
TBA::="To Be Announced".
Links
LOGIC::= See http://www.csci.csusb.edu/dick/maths/logic_0_Intro.html.
MATHS::= See http://www.csci.csusb.edu/dick/maths/.
PROOFS::= See http://www.csci.csusb.edu/dick/maths/logic_2_Proofs.html.
XBNF::= See http://www.csci.csusb.edu/dick/maths/intro_ebnf.html.
Structure::=MATHS equivalent of a C/C++ structure -- a class with all parts public.
with::=Adds new parts to a Structure to derive a new Structure.
. . . . . . . . . ( end of section The Natural Deduction Logic of Huth and Ryan) <<Contents | Index>>

Formulae and Definitions in Alphabetical Order