---

Step * of Lemma notAC20

∀T:Type
  (⇃T
  ⇒ (¬(∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
          ((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃∃m:T. (P n m)) ⇒ ⇃∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n))))))
BY
{ ((UnivCD THENA Auto) THEN (D 0 THENA Auto)) }

1
1. T : Type@i'
2. ⇃T@i
3. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
     ((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃∃m:T. (P n m)) ⇒ ⇃∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n)))@i'
⊢ False

---

Latex:

---

Latex:
\mforall{}T:Type
    (\00D9T
    {}\mRightarrow{}  (\mneg{}(\mforall{}P:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
                    ((\mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \00D9\mexists{}m:T.  (P  n  m))
                    {}\mRightarrow{}  \00D9\mexists{}f:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T.  \mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (P  n  (f  n))))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index