daily pastebin goal
22%
SHARE
TWEET

Smullyan Incompleteness

a guest Apr 2nd, 2015 523 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  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
Top