Nuprl Lemma : AF-uniform-induction

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].`
`  (∀[Q:T ⟶ ℙ]. uniform-TI(T;x,y.¬R[x;y];t.Q[t])) supposing `
`     (AFx,y:T.R[x;y] and `
`     (∀x,y,z:T.  ((¬R[x;y]) `` (¬R[y;z]) `` (¬R[x;z]))))`

Proof

Definitions occuring in Statement :  almost-full: `AFx,y:T.R[x; y]` uniform-TI: `uniform-TI(T;x,y.R[x; y];t.Q[t])` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` not: `¬A` false: `False` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` prop: `ℙ` almost-full: `AFx,y:T.R[x; y]` squash: `↓T` uniform-TI: `uniform-TI(T;x,y.R[x; y];t.Q[t])` nat: `ℕ` decidable: `Dec(P)` consistent-seq: `R-consistent-seq(n)` so_lambda: `λ2x.t[x]` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` so_apply: `x[s]` int_seg: `{i..j-}` lelt: `i ≤ j < k` guard: `{T}` eq_int: `(i =z j)` subtract: `n - m` ifthenelse: `if b then t else f fi ` btrue: `tt` so_lambda: `λ2x y.t[x; y]` AFbar: `AFbar()` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` top: `Top` true: `True` isr: `isr(x)` assert: `↑b` bfalse: `ff` exposed-it: `exposed-it` bool: `𝔹` unit: `Unit` it: `⋅` exists: `∃x:A. B[x]` sq_type: `SQType(T)` bnot: `¬bb` ge: `i ≥ j ` nequal: `a ≠ b ∈ T ` int_upper: `{i...}` sq_stable: `SqStable(P)` AF-spread-law: `AF-spread-law(x,y.R[x; y])` cand: `A c∧ B` outl: `outl(x)` isl: `isl(x)` less_than: `a < b`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality voidElimination applyEquality functionExtensionality cumulativity hypothesis universeEquality extract_by_obid isectElimination rename imageElimination imageMemberEquality baseClosed functionEquality isect_memberEquality because_Cache strong_bar_Induction unionEquality natural_numberEquality setElimination dependent_set_memberEquality equalityTransitivity equalitySymmetry independent_isectElimination independent_pairFormation lambdaFormation intEquality setEquality productElimination independent_functionElimination unionElimination addEquality voidEquality minusEquality equalityElimination dependent_pairFormation promote_hyp instantiate impliesFunctionality hypothesis_subsumption axiomEquality int_eqReduceTrueSq int_eqReduceFalseSq multiplyEquality inlEquality productEquality isectEquality hyp_replacement applyLambdaEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
(\mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].  uniform-TI(T;x,y.\mneg{}R[x;y];t.Q[t]))  supposing
(AFx,y:T.R[x;y]  and
(\mforall{}x,y,z:T.    ((\mneg{}R[x;y])  {}\mRightarrow{}  (\mneg{}R[y;z])  {}\mRightarrow{}  (\mneg{}R[x;z]))))

Date html generated: 2017_04_14-AM-07_28_07
Last ObjectModification: 2017_02_27-PM-02_58_25

Theory : bar-induction

Home Index