Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- (*see http://blog.plover.com/math/Gdl-Smullyan.html*)
- Inductive Token :=
- |P : Token
- |PR : Token
- |N : Token.
- Inductive Formula :=
- |T : Formula (*empty string*)
- |l_app : Token -> Formula -> Formula.
- Fixpoint concat(F F':Formula) :=
- match F with
- |T => F'
- |(l_app t F'') => l_app t (concat F'' F')
- end.
- Infix "+" := l_app.
- Infix "++" := concat.
- Variable Printed : Formula -> Prop. (*set of formulas printed by computer*)
- Fixpoint Truth(F:Formula):Prop := (*semantics*)
- match F with
- |T => True
- |(P+F') => Printed(F')
- |(PR+F') => Printed(F'++F')
- |(N+F') => ~Truth(F')
- end.
- Definition Consistent := forall F:Formula, Printed F -> Truth F.
- Definition Complete := forall F:Formula, Truth F -> Printed F.
- Lemma Incompleteness : ~(Consistent /\ Complete).
- Proof.
- unfold Complete, Consistent.
- intro.
- destruct H as [Cons Comp].
- assert (~Printed (N+(PR+(N+(PR+T))))).
- intro.
- assert (Truth (N+(PR+(N+(PR+T))))).
- apply Cons.
- exact H.
- simpl in H0.
- contradiction.
- assert (Printed (N + (PR + (N + (PR + T))))).
- apply Comp.
- simpl.
- exact H.
- contradiction.
- Qed.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement