---

Step * 1 of Lemma Kripke2b


1. a : ℕ ⟶ ℕ
2. is-absolutely-free{i:l}(a)
3. init0(a)
4. increasing-sequence(a)
5. ∀m:ℕ. ∃n:ℕ. ((a n) ≥ m )
⊢ False
BY
{ (Unfold `is-absolutely-free` 2 THEN (InstHyp [⌜λa.∀m:ℕ. ∃n:ℕ. ((a n) ≥ m )⌝] 2⋅ THENA Auto)) }

1
1. a : ℕ ⟶ ℕ
2. ∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ((P a) ⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((a = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))))
3. init0(a)
4. increasing-sequence(a)
5. ∀m:ℕ. ∃n:ℕ. ((a n) ≥ m )
6. ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((a = g ∈ (ℕk ⟶ ℕ)) ⇒ ((λa.∀m:ℕ. ∃n:ℕ. ((a n) ≥ m )) g)))
⊢ False

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  is-absolutely-free\{i:l\}(a)
3.  init0(a)
4.  increasing-sequence(a)
5.  \mforall{}m:\mBbbN{}.  \mexists{}n:\mBbbN{}.  ((a  n)  \mgeq{}  m  )
\mvdash{}  False


By

---

Latex:
(Unfold  `is-absolutely-free`  2  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}a.\mforall{}m:\mBbbN{}.  \mexists{}n:\mBbbN{}.  ((a  n)  \mgeq{}  m  )\mkleeneclose{}]  2\mcdot{}  THENA  Auto))

---

Home Index