Step * 1 2 1 of Lemma CCC-omni-2


1. Type
2. CCCNSet(K)
3. ∀P:K ⟶ ℙ((∀k:K. Dec(P[k]))  ((∃k:K. P[k]) ∨ (∀k:K. P[k]))))
4. K ⟶ K ⟶ ℙ
5. ∀k,m:K.  Dec(P[k;m])
6. K
7. ∀k@0:K. (¬¬P[k;k@0])
8. K
9. ¬¬P[k;m]
⊢ P[k;m]
BY
SupposeNot }


Latex:


Latex:

1.  K  :  Type
2.  CCCNSet(K)
3.  \mforall{}P:K  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}k:K.  Dec(P[k]))  {}\mRightarrow{}  ((\mexists{}k:K.  P[k])  \mvee{}  (\mforall{}k:K.  (\mneg{}P[k]))))
4.  P  :  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}k,m:K.    Dec(P[k;m])
6.  k  :  K
7.  \mforall{}k@0:K.  (\mneg{}\mneg{}P[k;k@0])
8.  m  :  K
9.  \mneg{}\mneg{}P[k;m]
\mvdash{}  P[k;m]


By


Latex:
SupposeNot




Home Index