(*|
再帰理論
========

Shoenfield. Mathematical Logic.
|*)

Require Import classical_logic.
Require Import partial_function.
Require Import power.

Set Implicit Arguments.

Definition nats (n : nat) : Type.
Proof.
  induction n.
  -
    exact unit.
  -
    exact (prod nat IHn).
Defined.

Definition addition : nats 2 -> nat.
Proof.
  intro.
  destruct X as [m [n _]].
  exact (m + n).
Defined.

Definition multiplication : nats 2 -> nat.
Proof.
  intro.
  destruct X as [m [n _]].
  exact (m * n).
Defined.

Inductive recursive_function
  : forall n : nat,
    (nats n -> nat) ->
    Prop :=
  | add  : recursive_function 2 addition
  | mult : recursive_function 2 multiplication.

Record partial_subset (A : Type) : Type :=
  make_partial_subset {
    dom_ :  power A;
    S    :> power ({ a : A | a ∈ dom_ });
  }.

Definition representation
  (A : Type)
  (P : partial_subset A)
  : A ⇀ nat.
Proof.
  unshelve econstructor.
  -
    exact (P.(dom_)).
  -
    intro.
    pose proof (every_proposition_is_decidable (X ∈ P.(S))).
    destruct H.
    +
      exact 0.
    +
      exact 1.
Defined.