[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

    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".

    Links

  21. LOGIC::= See http://www.csci.csusb.edu/dick/maths/logic_0_Intro.html.
  22. MATHS::= See http://www.csci.csusb.edu/dick/maths/.
  23. PROOFS::= See http://www.csci.csusb.edu/dick/maths/logic_2_Proofs.html.
  24. XBNF::= See http://www.csci.csusb.edu/dick/maths/intro_ebnf.html.
  25. Structure::=MATHS equivalent of a C/C++ structure -- a class with all parts public.
  26. 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