Nuprl Lemma : mFOL_ind_wf_simple

∀[A:Type]. ∀[v:mFOL()]. ∀[atomic:name:Atom ⟶ vars:(ℤ List) ⟶ A]. ∀[connect:knd:Atom
                                                                             ⟶ left:mFOL()
                                                                             ⟶ right:mFOL()
                                                                             ⟶ A
                                                                             ⟶ A
                                                                             ⟶ A]. ∀[quant:isall:𝔹
                                                                                            ⟶ var:ℤ
                                                                                            ⟶ body:mFOL()
                                                                                            ⟶ A
                                                                                            ⟶ A].
  (mFOL_ind(v;
            mFOatomic(name,vars)⇒ atomic[name;vars];
            mFOconnect(knd,left,right)⇒ rec1,rec2.connect[knd;left;right;rec1;rec2];
            mFOquant(isall,var,body)⇒ rec3.quant[isall;var;body;rec3])  ∈ A)


Proof



Definitions occuring in Statement :  mFOL_ind: mFOL_ind,  mFOL: mFOL(),  list: T List,  bool: 𝔹,  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2;s3;s4;s5],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2],  member: t ∈ T,  function: x:A ⟶ B[x],  int: ℤ,  atom: Atom,  universe: Type
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  subtype_rel: A ⊆r B,  prop: ℙ,  uimplies: b supposing a,  true: True,  so_lambda: λ2x.t[x],  so_apply: x[s],  all: ∀x:A. B[x]
Lemmas referenced :  mFOL_ind_wf,  true_wf,  mFOL_wf,  subtype_rel_function,  list_wf,  subtype_rel_self,  istype-true,  subtype_rel_dep_function,  istype-int,  bool_wf,  istype-atom,  istype-universe
Rules used in proof :  cut,  introduction,  extract_by_obid,  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  hypothesis,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesisEquality,  sqequalRule,  lambdaEquality_alt,  universeIsType,  functionExtensionality,  applyEquality,  intEquality,  because_Cache,  setEquality,  independent_isectElimination,  dependent_set_memberEquality_alt,  natural_numberEquality,  closedConclusion,  atomEquality,  functionEquality,  inhabitedIsType,  lambdaFormation_alt,  setIsType,  setElimination,  rename,  applyLambdaEquality,  functionIsType,  instantiate,  universeEquality
Latex:
\mforall{}[A:Type].  \mforall{}[v:mFOL()].  \mforall{}[atomic:name:Atom  {}\mrightarrow{}  vars:(\mBbbZ{}  List)  {}\mrightarrow{}  A].  \mforall{}[connect:knd:Atom
                                                                                                                                                          {}\mrightarrow{}  left:mFOL()
                                                                                                                                                          {}\mrightarrow{}  right:mFOL()
                                                                                                                                                          {}\mrightarrow{}  A
                                                                                                                                                          {}\mrightarrow{}  A
                                                                                                                                                          {}\mrightarrow{}  A].
\mforall{}[quant:isall:\mBbbB{}  {}\mrightarrow{}  var:\mBbbZ{}  {}\mrightarrow{}  body:mFOL()  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (mFOL\_ind(v;
                        mFOatomic(name,vars){}\mRightarrow{}  atomic[name;vars];
                        mFOconnect(knd,left,right){}\mRightarrow{}  rec1,rec2.connect[knd;left;right;rec1;rec2];
                        mFOquant(isall,var,body){}\mRightarrow{}  rec3.quant[isall;var;body;rec3])    \mmember{}  A)


Date html generated: 2020_05_20-AM-09_08_12
Last ObjectModification: 2020_02_03-PM-02_23_20

Theory : minimal-first-order-logic


Home Index