Nuprl Lemma : classical-markov

P:ℕ ⟶ ℙ((∀n:ℕDec(P[n]))  (∀n:ℕP[n])))  (∃n:ℕP[n]))


Proof




Definitions occuring in Statement :  nat: decidable: Dec(P) prop: so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] not: ¬A implies:  Q function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] classical: {P} not: ¬A false: False exists: x:A. B[x] squash: T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] guard: {T} uimplies: supposing a and: P ∧ Q
Lemmas referenced :  mu-dec_wf it_wf unit_wf2 mu-dec-property exists_wf decidable_wf nat_wf all_wf not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis sqequalRule lambdaEquality applyEquality hypothesisEquality functionEquality cumulativity universeEquality introduction independent_functionElimination dependent_pairFormation voidElimination classicalIntroduction rename setElimination imageMemberEquality baseClosed imageElimination dependent_functionElimination independent_isectElimination equalityTransitivity equalitySymmetry productElimination

Latex:
\mforall{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}n:\mBbbN{}.  Dec(P[n]))  {}\mRightarrow{}  (\mneg{}(\mforall{}n:\mBbbN{}.  (\mneg{}P[n])))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  P[n]))



Date html generated: 2016_05_14-AM-07_30_25
Last ObjectModification: 2016_01_14-PM-09_58_04

Theory : int_2


Home Index