再帰理論

Shoenfield. Mathematical Logic.

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

Set Implicit Arguments.

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

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

Definition multiplication : nats 2 -> nat.
nats 2 -> nat
Proof.
nats 2 -> nat
  intro.
X: nats 2
nat
  destruct X as [m [n _]].
m, n: nat
nat
  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.
A: Type
P: partial_subset A
A ⇀ nat
Proof.
A: Type
P: partial_subset A
A ⇀ nat
  unshelve econstructor.
A: Type
P: partial_subset A
power A
A: Type
P: partial_subset A
{a : A | a ∈ ?dom} -> nat
  -
A: Type
P: partial_subset A
power A
    exact (P.(dom_)).
  -
A: Type
P: partial_subset A
{a : A | a ∈ dom_ P} -> nat
    intro.
A: Type
P: partial_subset A
X: {a : A | a ∈ dom_ P}
nat
    pose proof (every_proposition_is_decidable (X ∈ P.(S))).
A: Type
P: partial_subset A
X: {a : A | a ∈ dom_ P}
H: (X ∈ P) + (~ X ∈ P)
nat
    destruct H.
A: Type
P: partial_subset A
X: {a : A | a ∈ dom_ P}
m: X ∈ P
nat
A: Type
P: partial_subset A
X: {a : A | a ∈ dom_ P}
n: ~ X ∈ P
nat
    +
A: Type
P: partial_subset A
X: {a : A | a ∈ dom_ P}
m: X ∈ P
nat
      exact 0.
    +
A: Type
P: partial_subset A
X: {a : A | a ∈ dom_ P}
n: ~ X ∈ P
nat
      exact 1.
Defined.