Smullyan Incompleteness

(*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.