### Nuprl Lemma : es-knows-not

[poss:EO ─→ ℙ']. ∀[R:PossibleEvent(poss) ─→ PossibleEvent(poss) ─→ ℙ'].
(EquivRel(PossibleEvent(poss))(R _1 _2)
(∀[P:PossibleEvent(poss) ─→ ℙ']. ∀e:PossibleEvent(poss). K(λe.(¬K(P)@e))@e supposing ¬K(P)@e))

Proof

Definitions occuring in Statement :  es-knows: K(P)@e possible-event: PossibleEvent(poss) event_ordering: EO equiv_rel: EquivRel(T;x,y.E[x; y]) uimplies: supposing a uall: [x:A]. B[x] prop: all: x:A. B[x] not: ¬A implies:  Q apply: a lambda: λx.A[x] function: x:A ─→ B[x]
Lemmas :  all_wf possible-event_wf not_wf equiv_rel_wf event_ordering_wf
\mforall{}[poss:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[R:PossibleEvent(poss)  {}\mrightarrow{}  PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].
(EquivRel(PossibleEvent(poss))(R  \$_{1}\$  \$_{2}\$)
{}\mRightarrow{}  (\mforall{}[P:PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}e:PossibleEvent(poss).  K(\mlambda{}e.(\mneg{}K(P)@e))@e  supposing  \mneg{}K(P)@e))

Date html generated: 2015_07_17-AM-08_52_09
Last ObjectModification: 2015_01_27-PM-01_17_46

Home Index