Lemma: simp_lemma1
[P:ℙ]. (P supposing False ⇐⇒ True)

Lemma: ite_false
b:𝔹. ∀[x:ℙ]. (if then else False fi  ⇐⇒ (↑b) ∧ x)

Lemma: iflift_1
[A,B:Type]. ∀[c:𝔹]. ∀[f:A ⟶ B]. ∀[x,y:A].  (f[if then else fi if then f[x] else f[y] fi  ∈ B)

Lemma: iflift_sq_1
[c:𝔹]. ∀[f,x,y:Top].  (f[if then else fi if then f[x] else f[y] fi )

Lemma: cand_functionality_wrt_iff
[a1,a2,b1,b2:ℙ].  ((a1 ⇐⇒ a2)  (b1 ⇐⇒ b2)  (a1 c∧ b1 ⇐⇒ a2 c∧ b2))

Lemma: trivial_ite_2
[b:𝔹]. ∀[a:Top].  (if then else fi  a)

Lemma: ite_and_reduce
[b1,b2:𝔹]. ∀[x,y:Top].  (if b1 then if b2 then else fi  else fi  if b1 ∧b b2 then else fi )

Definition: hide
HIDDEN ==  x

Lemma: hide_wf
[T:Type]. ∀[x:T].  (HIDDEN ∈ T)

Definition: !hyp_hide
==  x

Definition: opt
(b?x) ==  if then inl else inr ⋅  fi 

Lemma: opt_wf
[T:Type]. ∀[x:T]. ∀[b:𝔹].  ((b?x) ∈ T?)

Definition: Russell
Russell ==  {T:Type ⋂ Base| ¬(T ∈ T)} 

Lemma: Russell_wf
Russell ∈ 𝕌'

Lemma: Russell-property
¬(Russell ∈ Russell)

Lemma: Russell-paradox
¬(𝕌' ⊆Type)

Lemma: Russell-theorem
¬(Type ∈ Type)

Lemma: Russell-theorem-take2
¬(Type ∈ Type)

Lemma: Russell-theorem-ext
¬(Type ∈ Type)

Definition: decision
Decision ==  Top Top

Lemma: decision_wf
Decision ∈ Type

Definition: dec2bool
dec2bool(d) ==  case of inl(x) => tt inr(x) => ff

Lemma: dec2bool_wf
[d:Decision]. (dec2bool(d) ∈ 𝔹)

Lemma: inr_eq_bfalse
[x:Top]. ((inr ff ∈ Decision)

Lemma: inl_eq_btrue
[x:Top]. ((inl x) tt ∈ Decision)

Lemma: bool_decision
[x:𝔹]. (x ∈ Decision)

Lemma: decidable_decision
[P:ℙ]. ∀[x:Dec(P)].  (x ∈ Decision)

Lemma: dec2bool_decidable
[P:ℙ]. ∀p:Dec(P). {↑dec2bool(p) ⇐⇒ P}

Lemma: eqtt_assert_2
[b:Decision]. uiff(b tt ∈ Decision;↑b)

Lemma: eqff_assert_2
[b:Decision]. uiff(b ff ∈ Decision;¬↑b)

Lemma: assert_dec2bool
[d:Decision]. uiff(↑dec2bool(d);↑d)

Lemma: decidable__cand
[P:ℙ]. ∀[Q:⋂x:P. ℙ].  (Dec(P)  (P  Dec(Q))  Dec(P c∧ Q))

Definition: limited-omniscience
The limited principle of omniscience (LPO) is simple, classically true, 
proposition that is not true in intuitionistic mathematics.
It contradicts even weak form of Brouwer's continutity principle.
Nuprl satisfies strong versions of continuity 
(see rules--proved true in the Nuprl-in-Coq model--
StrongContinuity2 and weak continuity rule Continuity).
Therfore we can prove the negation of LPO:

LPO ==  ∀f:ℕ ⟶ 𝔹((∀n:ℕff) ∨ (∃n:ℕtt))

Lemma: limited-omniscience_wf

Definition: type-functor
Functor ==
  {p:F:Type ⟶ Type × (⋂T,S:Type.  ((T ⟶ S) ⟶ (F T) ⟶ (F S)))| 
   let F,M 
   in (∀T:Type. ((M x.x)) x.x) ∈ ((F T) ⟶ (F T))))
      ∧ (∀T,S,V:Type. ∀f:T ⟶ S. ∀g:S ⟶ V.  ((M (g f)) ((M g) (M f)) ∈ ((F T) ⟶ (F V))))} 

Lemma: type-functor_wf
Functor ∈ 𝕌'

Definition: identity-functor
Id ==  <λx.x, λf.f>

Lemma: identity-functor_wf
Id ∈ Functor

Definition: constant-type-functor
constant-type-functor(X) ==  <λT.X, λf,x. x>

Lemma: constant-type-functor_wf
[X:Type]. (constant-type-functor(X) ∈ Functor)

Definition: type-functor-product
==  let F,MF in let G,MG in <λT.(F T × (G T)), λf,p. let x,y in <MF x, MG y>>

Lemma: type-functor-product_wf
[F,G:Functor].  (F G ∈ Functor)

Definition: type-functor-sum
  let F,MF 
  in let G,MG 
     in <λT.(F (G T)), λf,d. case of inl(x) => inl (MF x) inr(y) => inr (MG y) >

Lemma: type-functor-sum_wf
[F,G:Functor].  (F G ∈ Functor)

Definition: type-functor-compose
==  let F,MF in let G,MG in <G, MF MG>

Lemma: type-functor-compose_wf
[F,G:Functor].  (F G ∈ Functor)

Definition: type-functor-iterate
F^n ==  primrec(n;Id;λi,G. (F G))

Lemma: type-functor-iterate_wf
[n:ℕ]. ∀[F:Functor].  (F^n ∈ Functor)

Definition: compact-type
compact-type(T) ==  ∀p:T ⟶ 𝔹((∃x:T. ff) ∨ (∀x:T. tt))

Lemma: compact-type_wf
[T:Type]. (compact-type(T) ∈ ℙ)

Definition: p-selector
is "root" of the decidable property p
if ff  
(thinking of ff as being and tt as non-zero).

is selector for decidable property if
is root of if and only if has root.
non-void, compact type has selector
  see: compact-type-compact-type2)⋅

p-selector(T;x;p) ==  (∃y:T. ff)  ff

Lemma: p-selector_wf
[T:Type]. ∀[x:T]. ∀[p:T ⟶ 𝔹].  (p-selector(T;x;p) ∈ ℙ)

Definition: compact-type2
compact-type2(T) ==  ∀p:T ⟶ 𝔹(∃x:T [p-selector(T;x;p)])

Lemma: compact-type2_wf
[T:Type]. (compact-type2(T) ∈ ℙ)

Lemma: compact-type-compact-type2
[T:Type]. (compact-type(T) ∧ ⇐⇒ compact-type2(T))

Lemma: compact-type-corec-lemma0
[F:Type ⟶ Type]
  (Monotone(T.F T)
   (((⋂n:ℕ(F^n Top)) ⟶ 𝔹) ⊆r ⋃n:ℕ.((F^n Top) ⟶ 𝔹))
   ((⋂n:ℕcompact-type2(F^n Top)) ⊆compact-type2(corec(T.F T))))

Lemma: compact-type-corec-lemma1
[F:Type ⟶ Type]
  (Monotone(T.F T)
   (((⋂n:ℕ(F^n Top)) ⟶ 𝔹) ⊆r ⋃n:ℕ.((F^n Top) ⟶ 𝔹))
   (∀[T:Type]. (compact-type2(T)  compact-type2(F T)))
   compact-type2(corec(T.F T)))

Lemma: compact-product
[T:Type]. ∀[S:T ⟶ Type].  (compact-type(T)  (∀t:T. compact-type(S[t]))  compact-type(t:T × S[t]))

Lemma: compact-union
[T,S:Type].  (compact-type(T)  compact-type(S)  compact-type(T S))

Lemma: compact-finite

Lemma: compact_functionality_wrt_surject
[T,S:Type].  ((∃f:T ⟶ S. Surj(T;S;f))  compact-type(T)  compact-type(S))

Lemma: compact_functionality_wrt_equipollent
[T,S:Type].  (T  compact-type(T)  compact-type(S))

Lemma: decidable__equal_compact_domain
[T,S:Type].  ((∀a,b:S.  Dec(a b ∈ S))  compact-type(T)  (∀f,g:T ⟶ S.  Dec(f g ∈ (T ⟶ S))))

Lemma: CCC-compact
K:Type. (CCCNSet(K)  compact-type(K))

Lemma: compact-dCCC
K:Type. (K  compact-type(K)  dCCC(K))

Definition: weak-continuity
weak-continuity(T;V) ==
  ∀F:(ℕ ⟶ T) ⟶ V. ∀f:ℕ ⟶ T.  (↓∃n:ℕ. ∀g:ℕ ⟶ T. ((∀i:ℕn. ((f i) (g i) ∈ T))  ((F f) (F g) ∈ V)))

Lemma: weak-continuity_wf
[T,V:Type].  (weak-continuity(T;V) ∈ ℙ)

Lemma: weak-continuity-bool-bool

Lemma: no-weak-limited-omniscience
¬(∀f:ℕ ⟶ 𝔹Dec(∀n:ℕff))

Lemma: no-limited-omniscience

Definition: nat-inf
ℕ∞ ==  {f:ℕ ⟶ 𝔹| ∀n:ℕ((↑(f (n 1)))  (↑(f n)))} 

Lemma: nat-inf_wf
ℕ∞ ∈ Type

Definition: nat2inf
n∞ ==  λi.i <n

Lemma: nat2inf_wf
[n:ℕ]. (n∞ ∈ ℕ∞)

Lemma: nat2inf-one-one
[a,b:ℕ].  ((a∞ b∞ ∈ ℕ∞ (a b ∈ ℕ))

Lemma: nat2inf-injection

Definition: nat-inf-infinity
∞ ==  λn.tt

Lemma: nat-inf-infinity_wf
∞ ∈ ℕ∞

Lemma: nat-inf-infinity-new
[n:ℕ]. (∞ n∞ ∈ ℕ∞))

Lemma: equal-nat-inf-infinity
[x:ℕ∞]. uiff(x = ∞ ∈ ℕ∞;∀i:ℕ(x i∞ ∈ ℕ∞)))

Lemma: equal-nat-inf-infinity2
[x:ℕ∞]. uiff(x = ∞ ∈ ℕ∞;∀i:ℕ(↑(x i)))

Definition: coW2natinf
coW2natinf(w;n) ==  if (fst(w) =z 1) then if (n =z 0) then tt else coW2natinf(coW-item(w;⋅);n 1) fi  else ff fi 

Lemma: coW2natinf_wf
[n:ℕ]. ∀[w:coW(ℕ2;x.if (x =z 0) then Void else Unit fi )].  (coW2natinf(w;n) ∈ 𝔹)

Definition: ni-selector
ni-selector(p) ==  λn.(¬b(∃i<1.¬b(p i∞))_b)

Lemma: ni-selector_wf
[p:ℕ∞ ⟶ 𝔹]. (ni-selector(p) ∈ ℕ∞)

Lemma: ni-selector-property
p:ℕ∞ ⟶ 𝔹(∃x:ℕ∞ff ⇐⇒ ni-selector(p) ff)

Lemma: compact-nat-inf
p:ℕ∞ ⟶ 𝔹((∃x:ℕ∞ff) ∨ (∀x:ℕ∞tt))

Lemma: nat-inf-attach-unit
F:ℕ ⟶ Type. ∃G:ℕ∞ ⟶ Type. ((∀n:ℕn∞ n) ∧ G ∞ ~ ℕ1)

Lemma: nat-inf-attach
F:ℕ ⟶ Type. ∀T:Type.  ∃G:ℕ∞ ⟶ Type. ((∀n:ℕn∞ n) ∧ G ∞ T)

Lemma: nat-inf-limit
p:ℕ∞ ⟶ 𝔹((∀n:ℕn∞ ff)  p ∞ ff)

Comment: decidable properties of types
Are there any non-trivial, decidable properties of types?
If F ∈ Type ⟶ 𝔹 and is not constant, then
1) can exists at all?
2) if it can, then can it respect extensional equality
    (i.e.  can X ≡  Y) ?
3) if it could respect extensional equality, then could it
   repsect equipollence?
  (i.e   Y)

  The answer to 3) is No.
  This was proved by Escardo, and we did the proof in Nuprl.

If we had ⌜Type ⊆Base⌝ (which might be possible, but doesn't seem 
provable now) and if there we canonical form tests for some of the
types, say test isInt, and if Type were value type (which also seems
possible), then isInt could give us function ⌜Type ⟶ 𝔹⌝ that would
be non-constant. So the answer to 1) could possibly be Yes.

But such function would be very intensional so it wouldn't answer 2)
with Yes.  It seems likely that the answer to 2) is No, but we have not
proved that.⋅

Lemma: Rice-theorem-for-Type
F:Type ⟶ 𝔹((∀X,Y:Type.  (X  Y))  ((F T.tt) ∈ (Type ⟶ 𝔹)) ∨ (F T.ff) ∈ (Type ⟶ 𝔹))))

Definition: ni-max
ni-max(f;g) ==  λi.((f i) ∨b(g i))

Lemma: ni-max_wf
[f,g:ℕ∞].  (ni-max(f;g) ∈ ℕ∞)

Lemma: ni-max-nat
[n,m:ℕ].  (ni-max(n∞;m∞imax(n;m)∞ ∈ ℕ∞)

Lemma: ni-max-com
[x,y:ℕ∞].  (ni-max(x;y) ni-max(y;x) ∈ ℕ∞)

Lemma: ni-max-assoc
[x,y,z:ℕ∞].  (ni-max(ni-max(x;y);z) ni-max(x;ni-max(y;z)) ∈ ℕ∞)

Lemma: ni-max-identity
[x:ℕ∞]. (ni-max(x;∞= ∞ ∈ ℕ∞)

Lemma: ni-max-zero
[x:ℕ∞]. (ni-max(x;0∞x ∈ ℕ∞)

Lemma: ni-max-idemp
[x:ℕ∞]. (ni-max(x;x) x ∈ ℕ∞)

Definition: ni-min
ni-min(f;g) ==  λi.((f i) ∧b (g i))

Lemma: ni-min_wf
[f,g:ℕ∞].  (ni-min(f;g) ∈ ℕ∞)

Lemma: ni-min-nat
[n,m:ℕ].  (ni-min(n∞;m∞imin(n;m)∞ ∈ ℕ∞)

Lemma: ni-min-com
[x,y:ℕ∞].  (ni-min(x;y) ni-min(y;x) ∈ ℕ∞)

Lemma: ni-min-assoc
[x,y,z:ℕ∞].  (ni-min(ni-min(x;y);z) ni-min(x;ni-min(y;z)) ∈ ℕ∞)

Lemma: ni-min-identity
[x:ℕ∞]. (ni-min(x;∞x ∈ ℕ∞)

Lemma: ni-min-zero
[x:ℕ∞]. (ni-min(x;0∞0∞ ∈ ℕ∞)

Lemma: ni-min-idemp
[x:ℕ∞]. (ni-min(x;x) x ∈ ℕ∞)

Definition: ni-iterated-min
ni-iterated-min(n;f) ==  primrec(n;∞m,s. ni-min(f m;s))

Lemma: ni-iterated-min_wf
[n:ℕ]. ∀[f:ℕn ⟶ ℕ∞].  (ni-iterated-min(n;f) ∈ ℕ∞)

Definition: ni-eventually-equal
ni-eventually-equal(f;g) ==  ∃n:ℕ. ∀m:{n...}. m

Lemma: ni-eventually-equal_wf
[f,g:ℕ∞].  (ni-eventually-equal(f;g) ∈ ℙ)

Lemma: ni-eventually-equal-equiv

Lemma: not-ni-eventually-equal-inf
[x:ℕ∞]. ni-eventually-equal(x;0∞⇐⇒ = ∞ ∈ ℕ∞)

Home Index