Advertisement
Guest User

Smullyan Incompleteness

a guest
Apr 2nd, 2015
2,172
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 1.13 KB | None | 0 0
  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.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement