Library godel

Require Import types.
Require Import Logic.ClassicalDescription.
Require Import Logic.ClassicalChoice.
Require Import Logic.IndefiniteDescription.

Definition computable (P:Prop):=
{proof:P|True}.

Inductive decidable (P:Prop):Prop:=
|decidable_intro: {P}+{~P} ->decidable P.

Lemma decidable_computable: forall P:Prop,
decidable P -> computable P \/ computable (~ P).

Section Godel.
Definition Formula:=nat->Prop.
Definition PF:=(Prop+Formula)%type.
Variable G: PF-> nat.
Notation "# x":=(G x) (at level 50).
Hypothesis G_injective: forall P Q:PF, G P=G Q->P=Q.
Lemma G_injective_n: forall P Q:PF, P<>Q->G P<>G Q.

Definition F_PF(F:Formula):=inr Prop F.
Definition P_PF(P:Prop):=inl Formula P.

Inductive repeater: nat->nat->Prop:=
|repeater_intro: forall (F:Formula),
repeater (#(F_PF F)) (#(P_PF (F(#(F_PF F))))).

Require Import Classical.
Lemma repeater_exists: forall (m:nat), (exists! n:nat,
repeater m n)\/(~exists F:Formula, m=#(F_PF F)).

Lemma reaper_func: exists f:nat->nat,
forall m:nat, (repeater m (f m))\/(~exists F:Formula, m=#(F_PF F)).

Definition fr:nat->nat.
Defined.

Lemma fr_reaper: forall m:nat,
(repeater m (fr m))\/(~exists F:Formula, m=#(F_PF F)).

Lemma DiagonalLemma: forall (F:nat->Prop), exists P,
computable (P<->F(#(P_PF P))).

Theorem Godel: exists P:Prop, ~ decidable P.

Theorem ugh:False.
End Godel.

Theorem notinjective: ~exists f:PF->nat, forall P Q:PF,
f P=f Q-> P=Q.
Print Assumptions notinjective.