# Smullyan Incompleteness

a guest
Apr 2nd, 2015
2,172
0
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.