### Nuprl Lemma : weakly-infinite-cases

`∀[S:ℕ ⟶ ℙ]. (w∃∞x.S[x] `` (∀[A:ℕ ⟶ ℙ]. ((∀n:ℕ. (A[n] `` S[n])) `` (¬¬(w∃∞n.A[n] ∨ w∃∞n.S[n] ∧ (¬A[n]))))))`

Proof

Definitions occuring in Statement :  weakly-infinite: `w∃∞p.S[p]` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` not: `¬A` false: `False` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` and: `P ∧ Q` subtype_rel: `A ⊆r B` or: `P ∨ Q` all: `∀x:A. B[x]` nat: `ℕ` exists: `∃x:A. B[x]` uiff: `uiff(P;Q)` uimplies: `b supposing a` weakly-infinite: `w∃∞p.S[p]` iff: `P `⇐⇒` Q` guard: `{T}` decidable: `Dec(P)` cand: `A c∧ B` le: `A ≤ B` rev_implies: `P `` Q` subtract: `n - m` top: `Top` less_than': `less_than'(a;b)` true: `True`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin hypothesis sqequalHypSubstitution independent_functionElimination voidElimination extract_by_obid isectElimination sqequalRule lambdaEquality applyEquality functionExtensionality hypothesisEquality productEquality universeEquality functionEquality dependent_functionElimination because_Cache cumulativity isect_memberEquality inlFormation setElimination rename productElimination independent_isectElimination unionElimination dependent_pairFormation addLevel impliesFunctionality levelHypothesis inrFormation independent_pairFormation addEquality natural_numberEquality voidEquality intEquality minusEquality promote_hyp

Latex:
\mforall{}[S:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}]
(w\mexists{}\minfty{}x.S[x]  {}\mRightarrow{}  (\mforall{}[A:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}n:\mBbbN{}.  (A[n]  {}\mRightarrow{}  S[n]))  {}\mRightarrow{}  (\mneg{}\mneg{}(w\mexists{}\minfty{}n.A[n]  \mvee{}  w\mexists{}\minfty{}n.S[n]  \mwedge{}  (\mneg{}A[n]))))))

Date html generated: 2017_09_29-PM-05_47_37
Last ObjectModification: 2017_07_26-PM-01_25_15

Theory : bar-induction

Home Index