Need a unique gift idea?
A Pastebin account makes a great Christmas gift
SHARE
TWEET

Smullyan Incompleteness

a guest Apr 2nd, 2015 664 Never
Upgrade to PRO!
ENDING IN00days00hours00mins00secs
 
  1. (*see http://blog.plover.com/math/Gdl-Smullyan.html*)
  2.  
  3. Inductive Token :=
  4.   |P : Token
  5.   |PR : Token
  6.   |N : Token.
  7.  
  8. Inductive Formula :=
  9.   |T : Formula (*empty string*)
  10.   |l_app : Token -> Formula -> Formula.
  11.  
  12. Fixpoint concat(F F':Formula) :=
  13.   match F with
  14.   |T => F'
  15.   |(l_app t F'') => l_app t (concat F'' F')
  16.   end.
  17.  
  18. Infix "+" := l_app.
  19. Infix "++" := concat.
  20.  
  21. Variable Printed : Formula -> Prop. (*set of formulas printed by computer*)
  22.  
  23. Fixpoint Truth(F:Formula):Prop :=  (*semantics*)
  24.   match F with
  25.   |T => True  
  26.   |(P+F') => Printed(F')
  27.   |(PR+F') => Printed(F'++F')
  28.   |(N+F') => ~Truth(F')
  29.   end.
  30.  
  31. Definition Consistent := forall F:Formula, Printed F -> Truth F.
  32. Definition Complete := forall F:Formula, Truth F -> Printed F.
  33.  
  34. Lemma Incompleteness : ~(Consistent /\ Complete).
  35. Proof.
  36.   unfold Complete, Consistent.
  37.   intro.
  38.   destruct H as [Cons Comp].
  39.   assert (~Printed (N+(PR+(N+(PR+T))))).
  40.   intro.
  41.   assert (Truth (N+(PR+(N+(PR+T))))).
  42.   apply Cons.
  43.   exact H.
  44.   simpl in H0.
  45.   contradiction.
  46.   assert (Printed (N + (PR + (N + (PR + T))))).
  47.   apply Comp.
  48.   simpl.
  49.   exact H.
  50.   contradiction.
  51. Qed.
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top