Nuprl Lemma : excluded-middle-lower-level

(P:'. (P  (P)))  (P:. (P  (P)))


Proof



Definitions occuring in Statement :  prop: ,  all: x:A. B[x],  not: A,  squash: T,  implies: P  Q,  or: P  Q
Definitions :  implies: P  Q,  all: x:A. B[x],  prop: ,  squash: T,  true: True,  member: t  T,  so_lambda: x.t[x],  uall: [x:A]. B[x],  so_apply: x[s],  guard: {T}
Lemmas :  all_wf,  squash_wf,  or_wf,  not_wf
(\mforall{}P:\mBbbP{}'.  (\mdownarrow{}P  \mvee{}  (\mneg{}P)))  {}\mRightarrow{}  (\mforall{}P:\mBbbP{}.  (\mdownarrow{}P  \mvee{}  (\mneg{}P)))


Date html generated: 2013_03_20-AM-10_49_18
Last ObjectModification: 2013_02_25-PM-05_38_16

Home Index