Supporting results for pointwise provable equality.

A concrete primitive recursive normal-form predicate for Mathlib's numbering. A witness pairs a fuel bound with the output. It is not asserted to be the historical computation-history coding of Odifreddi or Di Paola--Montagna. All theorems in this module concern standard natural numbers, not PA derivations.

def PointwiseComposition.FailureOfComposition.Kleene.eval (e x : ℕ) : Part ℕ

The eval construction in FailureOfComposition.Kleene.

Equations

• PointwiseComposition.FailureOfComposition.Kleene.eval e x = (Denumerable.ofNat Nat.Partrec.Code e).eval x

def PointwiseComposition.FailureOfComposition.Kleene.T₁ (e x s : ℕ) : Prop

The T₁ construction in FailureOfComposition.Kleene.

Equations

• PointwiseComposition.FailureOfComposition.Kleene.T₁ e x s = (Nat.Partrec.Code.evaln (Nat.unpair s).1 (Denumerable.ofNat Nat.Partrec.Code e) x = some (Nat.unpair s).2)

def PointwiseComposition.FailureOfComposition.Kleene.U (s : ℕ) : ℕ

The U construction in FailureOfComposition.Kleene.

Equations

• PointwiseComposition.FailureOfComposition.Kleene.U s = (Nat.unpair s).2

@[instance_reducible]

instance PointwiseComposition.FailureOfComposition.Kleene.instDecidableT₁ (e x s : ℕ) : Decidable (T₁ e x s)

Equations

• PointwiseComposition.FailureOfComposition.Kleene.instDecidableT₁ e x s = PointwiseComposition.FailureOfComposition.Kleene.instDecidableT₁._aux_1 e x s

theorem PointwiseComposition.FailureOfComposition.Kleene.T₁_primrec : PrimrecPred fun (p : (ℕ × ℕ) × ℕ) => T₁ p.1.1 p.1.2 p.2

theorem PointwiseComposition.FailureOfComposition.Kleene.U_primrec : Primrec U

theorem PointwiseComposition.FailureOfComposition.Kleene.normal_form (e x y : ℕ) : y ∈ eval e x ↔ ∃ (s : ℕ), T₁ e x s ∧ U s = y

theorem PointwiseComposition.FailureOfComposition.Kleene.halts_iff (e x : ℕ) : (eval e x).Dom ↔ ∃ (s : ℕ), T₁ e x s

theorem PointwiseComposition.FailureOfComposition.Kleene.output_unique {e x s t : ℕ} (hs : T₁ e x s) (ht : T₁ e x t) : U s = U t

theorem PointwiseComposition.FailureOfComposition.Kleene.least_witness (e x : ℕ) (h : ∃ (s : ℕ), T₁ e x s) : T₁ e x (Nat.find h) ∧ (∀ t < Nat.find h, ¬T₁ e x t) ∧ ∀ (y : ℕ), y ∈ eval e x ↔ U (Nat.find h) = y

The least successful witness computes the same output as any successful witness.

theorem PointwiseComposition.FailureOfComposition.Kleene.normal_form_equation (e x : ℕ) : eval e x = Part.map U (Nat.rfind fun (s : ℕ) => Part.some (decide (T₁ e x s)))

Kleene's least-witness equation, with the concrete coding above.

def PointwiseComposition.FailureOfComposition.Kleene.compIndex (f g : ℕ) : ℕ

The comp Index construction in FailureOfComposition.Kleene.

Equations

• PointwiseComposition.FailureOfComposition.Kleene.compIndex f g = Encodable.encode ((Denumerable.ofNat Nat.Partrec.Code f).comp (Denumerable.ofNat Nat.Partrec.Code g))

theorem PointwiseComposition.FailureOfComposition.Kleene.compIndex_primrec : Primrec₂ compIndex

theorem PointwiseComposition.FailureOfComposition.Kleene.eval_compIndex (f g x : ℕ) : eval (compIndex f g) x = (eval g x).bind (eval f)

theorem PointwiseComposition.FailureOfComposition.Kleene.normal_form_comp (f g x z : ℕ) : (∃ (s : ℕ), T₁ (compIndex f g) x s ∧ U s = z) ↔ ∃ (y : ℕ), (∃ (s : ℕ), T₁ g x s ∧ U s = y) ∧ ∃ (t : ℕ), T₁ f y t ∧ U t = z

theorem PointwiseComposition.FailureOfComposition.Kleene.diagonalHalts_iff (d : ℕ) : diagonalHalts d ↔ ∃ (s : ℕ), T₁ d d s