INDEPENDENT WORK Theme:Deduction theorem

Plan: 1.Introduction 2.What is theorem? 3.Examples of deduction theorem 4.Useful theorems

1. In   mathematical logic,  a   deduction  theorem   is   a   metatheorem   that  justifies  doing   conditional  proofs   —  to   prove  an  implication   A   →   B ,  assume   A   as  an  hypothesis  and   then  proceed  to  derive   B   —  in  systems  that  do  not  have  an   explicit   inference  rule   for  this.  Deduction  theorems  exist  for   both   propositional  logic   and   first-order  logic   The  deduction   theorem  is  an  important  tool  in   Hilbert-style  deduction   systems  because  it permits  one  to  write  more   comprehensible  and  usually  much  shorter  proofs  than  would be  possible  without  it.  In  certain  other  formal  proof  systems   the  same  conveniency  is  provided  by  an  explicit  inference   rule;  for  example   natural  deduction   calls  it   implication   introduction. In  more  detail,  the  propositional  logic  deduction  theorem   states  that  if a formula     is  deducible  from  a set  of   assumptions     t={A}  then  the  implication  A   B     is  deducible   from   ;  in  symbols,   =  {A}+B   implies   .  B  In  the  special  case   where     is  the   empty  set,  the  deduction  theorem  claim  can  be   more  compactly  written  as:  A     B  implies   .  The  deduction   theorem  for  predicate  logic  is  similar,  but  comes  with  some   extra  constraints  (that  would  for  example  be  satisfied  if   A   is   a   closed  formula.  In  general  a deduction  theorem  needs  to   take  into  account  all  logical  details  of  the  theory  under   consideration,  so  each  logical  system  technically  needs  its   own  deduction  theorem,  although  the  differences  are  usually   minor. The  deduction  theorem  holds  for  all  first-order  theories  with   the  usual   deductive  systems   for  first-order  logic.   However,   there  are  first-order  systems  in  which  new  inference  rules  are added  for  which  the  deduction  theorem  fails.   Most  notably,   the  deduction  theorem  fails  to  hold  in  Birkhoff–von   Neumann   quantum  logic,  because  the  linear  subspaces  of   a   Hilbert  space   form  a   non-distributive  lattice . 2.

In   mathematics, a   theorem   is  a   statement  that  has   been   proved  or  can  be  proved.The   proof   of  a theorem  is   a   logical  argument   that  uses  the  inference  rules  of   a   deductive  system   to  establish  that  the  theorem  is  a   logical   consequence   of  the   axioms   and  previously  proved  theorems. In  the  mainstream  of  mathematics,  the  axioms  and  the   inference  rules  are  commonly  left  implicit,  and,  in  this  case,   they  are  almost  always  those  of   Zermelo–Fraenkel  set   theory   with  the   axiom  of  choice,  or  of  a less  powerful  theory,   such  as   Peano  arithmetic.  A  notable  exception  is   Wiles's   proof  of  Fermat's  Last  Theorem   which  involves   the   Grothendieck  universes   whose  existence  requires  to  add   a  new  axiom  to  the  set  theory.   Generally,  an  assertion  that  is   explicitly  called  a theorem  is  a proved  result  that  is  not  an   immediate  consequence  of  other  known  theorems.  Moreover, many  authors  qualify  as   theorems   only  the  most  important   results,  and  use  the   terms   lemma ,   proposition   and   corollary   for  less  important   theorems. In   mathematical  logic  the  concepts  of  theorems  and  proofs   have  been   formalized   in  order  to  allow  mathematical   reasoning  about  them.  In  this  context,  statements   become   well-formed  formulas   of  some   formal  language.   A   theory   consists  of  some  basis  statements  called   axioms ,   and  some   deducing rules   (sometimes  included  in  the   axioms).  The  theorems  of  the  theory  are  the  statements  that   can  be  derived  from  the  axioms  by  using  the  deducing   rules.   This  formalization  led  to   proof  theory,  which  allows   proving  general  theorems  about  theorems  and  proofs.  In   particular,   Gödel's  incompleteness  theorems   show  that   every   consistent   theory  containing  the  natural  numbers  has   true  statements  on  natural  numbers  that  are  not  theorems  of   the  theory  (that  is  they  cannot  be  proved  inside  the  theory). As  the  axioms  are  often  abstractions  of  properties  of   the   physical  world,  theorems  may  be  considered  as  the   expression  some  truth,  but  in  contrast  to  the  notion  of   a   scientific  law ,   which is   experimental ,  the  justification  of  the truth  of  a theorem  is  purely   deductive.

3 1. "Prove" axiom  1: o P   1.  hypothesis o Q   2.  hypothesis  P   3.  reiteration  of  1 o Q → P   4.  deduction  from  2 to  3 P →( Q → P )  5.  deduction  from  1 to  4 QED 2. "Prove"  axiom  2: o P →( Q → R )  1.  hypothesis  P → Q   2.  hypothesis  P   3.  hypothesis  Q   4.  modus  ponens  3,2  Q → R   5.  modus  ponens  3,1  R   6.  modus  ponens  4,5  P → R   7.  deduction  from  3 to  6 o ( P → Q )→( P → R )  8.  deduction  from  2 to  7 ( P →( Q → R ))→(( P → Q )→( P → R ))  9.  deduction  from  1 to  8  QED 3. Using  axiom  1 to  show  (( P →( Q → P ))→ R )→ R : o ( P →( Q → P ))→ R   1.  hypothesis o P →( Q → P )  2.  axiom  1 o R   3.  modus  ponens  2,1 (( P →( Q → P ))→ R )→ R   4.  deduction  from  1 to  3 QED Virtual rules of inference From  the  examples,  you  can  see  that  we  have  added  three   virtual  (or  extra  and  temporary)  rules  of  inference  to  our   normal  axiomatic  logic.  These  are  "hypothesis",   "reiteration",  and  "deduction".  The  normal  rules  of  inference   (i.e.  "modus  ponens"  and  the  various  axioms)  remain   available. 1.   Hypothesis   is  a step  where  one  adds  an  additional  premise to  those  already  available.   So,  if your  previous  step   S   was   deduced  as: