Church's thesis (
The crucial consequence of
Similarly, we can define enumerability of predicates as
Since the halting problem of the underlying model of computation is enumerable and undecidable and furthermore its complement is undecidable, we have that
This allows proving that certain other problems are undecidable, e.g.
and its complement.
Lemma: If
Lemma:
Lemma: If
Corrollary:
We can now turn to
In particular, the
Lemma
Furthermore, functional extensionality would imply that such a coding function treats its inputs extensionally. However, such an extensional coding function implies that
Lemma Let
In short: Funect+CT in MLTT implies that the problem of determining whether
Agenda: We interpret MLTT+CT in MLTT with some constants + reduction rules. Then consistency of MLTT+CT follows by strong normalization of the target type theory.
Target theory := MLTT plus
-
an inductive type
$\Lambda$ , similar toAst.term
in MetaCoq, reifying the syntax of MLTT + the constants we are introducing in the next lines. The constructors use the same symbol as the corresponding construction/constant but with an upper dot. -
an evaluation relation
$\downarrow : \Lambda \to \Lambda \to \square$ -
a constant
$\chi : (\mathbb{N} \to \mathbb{N}) \to \Lambda$ -
a reduction rule for
$\chi$ on closed normal forms (in empty context):- for
$\vdash t : \mathbb{N} \to \mathbb{N}$ in normal form,$\chi t$ is the "code/syntax of t - otherwise
$\chi\ t$ is stuck. The important point is to ensure that no convertible terms give different codes (in particular,$\chi$ is stable under substitution).
- for
-
a constant
$\vdash R : \Pi (f : \mathbb{N} \to \mathbb{N}). \Pi (n : \mathbb{N}). (\chi f) @ [n] \downarrow [f n]$ where$\ @\ : \Lambda \to \Lambda \to \Lambda$ is the constructor for application in$\Lambda$ , and$[ \cdot ] : \mathbb{N} \to \Lambda$ computes the syntax of a natural number. -
a reduction rule for
$R$
Now the challenge is to design a "good" type of codes (
Current (?) plan :
- include a constructor
$q : \Lambda \rightarrow \Lambda$ in$\Lambda$ - describe reduction using the meta-operation from objects
$t$ in normal form to codes, denoted$\lceil t \rceil$ , which basically "dots" everything. Except for a few cases, and the open questions are, e.g., what should$\lceil \chi t \rceil$ be? ($q\lceil t\rceil$ ? ) And$\lceil q \rceil$ ? What is the evaluation of :$\dot{\chi} @ (\dot{\lambda} (size @(e (Var 0)))$ with$e : \mathbb{N} \rightarrow \Lambda$ and$size : \Lambda \rightarrow \mathbb{N}$ ?
Meta-operations on the object type theory:
$\mathrm{Tm}(\Gamma \vdash A) := \Sigma (t : Tm) \Gamma \vdash t : A$ -
$\mathrm{Nf}(\Gamma \vdash A)$ is the subtype of$\mathrm{Tm}(\Gamma \vdash A)$ that are in (deep) normal form $\lceil \cdot \rceil : \mathrm{Nf}( \cdot \vdash A) \to \mathrm{Tm}(\cdot \vdash \Lambda)$ $\ulcorner \cdot \urcorner : \mathrm{Tm}( \Gamma \vdash A) \to \mathrm{Tm}(\cdot \vdash \Lambda)$ -
$\lceil v \rceil := \ulcorner \texttt{injNf} v \urcorner$ where$\texttt{injNf} : \mathrm{Nf}(\Gamma \vdash A) \to \mathrm{Tm}(\Gamma \vdash A)$ $\sharp : \mathbb{N} \to \mathrm{Nf}(\cdot \vdash \mathbb{N})$ -
$\mathcal{O} : (f : \mathrm{Nf}(\cdot \vdash \mathbb{N} \to \mathbb{N}))(n : \mathrm{Nf}(\cdot \vdash \mathbb{N})). \mathrm{Nf}(\cdot \vdash \lceil f \rceil @ [n]^{\mathbb{N}} \downarrow [f,n]^{\mathbb{N}}) \to \square$ (not needed actually)
Employed to specify the object operations
- If
$f \in \mathrm{Nf}(\cdot \vdash \mathbb{N} \to \mathbb{N})$ then$\mathrm{Cv}(\cdot \vdash \chi\ f \equiv \lceil f \rceil)$ - If
$f \in \mathrm{Nf}(\cdot \vdash \mathbb{N} \to \mathbb{N})$ ,$n \in \mathrm{Nf}(\cdot \vdash \mathbb{N})$ ,$r \in \mathrm{Nf}(\cdot \vdash \lceil f \rceil @\ [n]^{\mathbb{N}} \downarrow [f\ n]^{\mathbb{N}})$ then$\mathrm{Cv}(\cdot \vdash R\ f\ n \equiv r)$
To prove in the NbE model:
- If
$t \in \mathrm{Tm}(\Gamma \vdash A), v \in \mathrm{Nf}(\Gamma \vdash A), p : Red(t,v)$ then$\mathrm{Nf}(\cdot \vdash \ulcorner t \urcorner \downarrow \ulcorner v\urcorner)$
PM: Instead of the oracle
⊢ t : ℕ → ℕ ⊢ n : ℕ ⊢ r : (χ t) @ [n]ℕ ↓ [m]ℕ ——————————————————————————————— ⊢ R t n ≡ r : (χ t) @ [n]ℕ ↓ [m]ℕ
Consequence that we need: (f : Nf(ℕ ⊢ ℕ))(n : Nf(⊢ ℕ))(m : Nf(⊢ ℕ)) → Cv(⊢ f{n} ≡ m) → Nf( ⊢ subst(⌜f⌝, ⌈n⌉) ↓ ⌈m⌉)
Quotation lemma: (t : Tm(Γ ⊢ A)) (v : Nf(Γ ⊢ A)) → Cv(Γ ⊢ t ≡ v : A) → Nf(Γ ⊢ ⌜t⌝ ↓ ⌈v⌉)
Main issue with respect to conversion and unique normal forms: Assuming (strong) CT, we can derive a quote function (the χ : (ℕ → ℕ) → ℕ above) that needs to map convertible arguments Γ ⊢ f ≡ g : ℕ → ℕ to convertible results Γ ⊢ χ f ≡ χ g : ℕ (by congruence of application)