Nuprl Lemma : FOLRule_ind_wf
∀[A:Type]. ∀[R:A ⟶ FOLRule() ⟶ ℙ]. ∀[v:FOLRule()]. ∀[andI:{x:A| R[x;andI]} ]. ∀[impI:{x:A| R[x;impI]} ].
∀[allI:var:ℤ ⟶ {x:A| R[x;allI with var]} ]. ∀[existsI:var:ℤ ⟶ {x:A| R[x;existsI with var]} ].
∀[orI:left:𝔹 ⟶ {x:A| R[x;fRuleorI(left)]} ]. ∀[hyp:{x:A| R[x;hyp]} ]. ∀[andE:hypnum:ℕ ⟶ {x:A| R[x;andE on hypnum]} ].
∀[orE:hypnum:ℕ ⟶ {x:A| R[x;orE on hypnum]} ]. ∀[impE:hypnum:ℕ ⟶ {x:A| R[x;impE on hypnum]} ].
∀[allE:hypnum:ℕ ⟶ var:ℤ ⟶ {x:A| R[x;allE on hypnum with var]} ]. ∀[existsE:hypnum:ℕ
                                                                            ⟶ var:ℤ
                                                                            ⟶ {x:A| R[x;existsE on hypnum with var]} ].
∀[falseE:hypnum:ℕ ⟶ {x:A| R[x;falseE on hypnum]} ].
  (case(v)
   andI => andI
   impI => impI
   allI with var => allI[var]
   existsI with var => existsI[var]
   orI (left?left) => orI[left]
   hyp => hyp
   andE @hypnum => andE[hypnum]
   orE @hypnum => orE[hypnum]
   impE @hypnum => impE[hypnum]
   allE @hypnum with var => allE[hypnum;var]
   existsE @hypnum with var => existsE[hypnum;var]
   falseE @hypnum => falseE[hypnum] ∈ {x:A| R[x;v]} )
Proof
Definitions occuring in Statement : 
FOLRule_ind: FOLRule_ind, 
fRulefalseE: falseE on hypnum
, 
fRuleexistsE: existsE on hypnum with var
, 
fRuleallE: allE on hypnum with var
, 
fRuleimpE: impE on hypnum
, 
fRuleorE: orE on hypnum
, 
fRuleandE: andE on hypnum
, 
fRulehyp: hyp
, 
fRuleorI: fRuleorI(left)
, 
fRuleexistsI: existsI with var
, 
fRuleallI: allI with var
, 
fRuleimpI: impI
, 
fRuleandI: andI
, 
FOLRule: FOLRule()
, 
nat: ℕ
, 
bool: 𝔹
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
so_apply: x[s1;s2]
, 
so_apply: x[s]
, 
member: t ∈ T
, 
set: {x:A| B[x]} 
, 
function: x:A ⟶ B[x]
, 
int: ℤ
, 
universe: Type
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
FOLRule_ind: FOLRule_ind, 
so_apply: x[s]
, 
so_apply: x[s1;s2]
, 
FOLRule-definition, 
FOLRule-induction, 
FOLRule-ext, 
ext-eq_weakening, 
eq_atom: x =a y
, 
btrue: tt
, 
it: ⋅
, 
bfalse: ff
, 
bool_cases_sqequal, 
eqff_to_assert, 
any: any x
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
has-value: (a)↓
, 
so_lambda: so_lambda4, 
so_apply: x[s1;s2;s3;s4]
, 
so_lambda: λ2x.t[x]
, 
uimplies: b supposing a
, 
subtype_rel: A ⊆r B
, 
prop: ℙ
, 
guard: {T}
Lemmas referenced : 
FOLRule-definition, 
has-value_wf_base, 
is-exception_wf, 
lifting-strict-atom_eq, 
strict4-decide, 
fRuleandI_wf, 
fRuleimpI_wf, 
istype-int, 
fRuleallI_wf, 
fRuleexistsI_wf, 
bool_wf, 
fRuleorI_wf, 
fRulehyp_wf, 
istype-nat, 
fRuleandE_wf, 
fRuleorE_wf, 
fRuleimpE_wf, 
fRuleallE_wf, 
fRuleexistsE_wf, 
fRulefalseE_wf, 
FOLRule_wf, 
subtype_rel_function, 
nat_wf, 
subtype_rel_self, 
istype-universe, 
FOLRule-induction, 
FOLRule-ext, 
ext-eq_weakening, 
bool_cases_sqequal, 
eqff_to_assert
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
cut, 
sqequalRule, 
Error :memTop, 
inhabitedIsType, 
hypothesis, 
lambdaFormation_alt, 
thin, 
sqequalSqle, 
divergentSqle, 
callbyvalueDecide, 
sqequalHypSubstitution, 
hypothesisEquality, 
unionElimination, 
sqleReflexivity, 
equalityIstype, 
equalityTransitivity, 
equalitySymmetry, 
dependent_functionElimination, 
independent_functionElimination, 
introduction, 
decideExceptionCases, 
axiomSqleEquality, 
exceptionSqequal, 
baseApply, 
closedConclusion, 
baseClosed, 
extract_by_obid, 
isectElimination, 
independent_isectElimination, 
lambdaEquality_alt, 
isectIsType, 
functionIsType, 
universeIsType, 
universeEquality, 
setIsType, 
because_Cache, 
applyEquality, 
functionEquality, 
setEquality, 
instantiate, 
functionExtensionality, 
intEquality
Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  FOLRule()  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:FOLRule()].  \mforall{}[andI:\{x:A|  R[x;andI]\}  ].  \mforall{}[impI:\{x:A| 
                                                                                                                                                                              R[x;impI]\}  ].
\mforall{}[allI:var:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;allI  with  var]\}  ].  \mforall{}[existsI:var:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;existsI  with  var]\}  ].
\mforall{}[orI:left:\mBbbB{}  {}\mrightarrow{}  \{x:A|  R[x;fRuleorI(left)]\}  ].  \mforall{}[hyp:\{x:A|  R[x;hyp]\}  ].
\mforall{}[andE:hypnum:\mBbbN{}  {}\mrightarrow{}  \{x:A|  R[x;andE  on  hypnum]\}  ].  \mforall{}[orE:hypnum:\mBbbN{}  {}\mrightarrow{}  \{x:A|  R[x;orE  on  hypnum]\}  ].
\mforall{}[impE:hypnum:\mBbbN{}  {}\mrightarrow{}  \{x:A|  R[x;impE  on  hypnum]\}  ].  \mforall{}[allE:hypnum:\mBbbN{}
                                                                                                              {}\mrightarrow{}  var:\mBbbZ{}
                                                                                                              {}\mrightarrow{}  \{x:A|  R[x;allE  on  hypnum  with  var]\}  ].
\mforall{}[existsE:hypnum:\mBbbN{}  {}\mrightarrow{}  var:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;existsE  on  hypnum  with  var]\}  ].
\mforall{}[falseE:hypnum:\mBbbN{}  {}\mrightarrow{}  \{x:A|  R[x;falseE  on  hypnum]\}  ].
    (case(v)
      andI  =>  andI
      impI  =>  impI
      allI  with  var  =>  allI[var]
      existsI  with  var  =>  existsI[var]
      orI  (left?left)  =>  orI[left]
      hyp  =>  hyp
      andE  @hypnum  =>  andE[hypnum]
      orE  @hypnum  =>  orE[hypnum]
      impE  @hypnum  =>  impE[hypnum]
      allE  @hypnum  with  var  =>  allE[hypnum;var]
      existsE  @hypnum  with  var  =>  existsE[hypnum;var]
      falseE  @hypnum  =>  falseE[hypnum]  \mmember{}  \{x:A|  R[x;v]\}  )
Date html generated:
2020_05_20-AM-09_10_02
Last ObjectModification:
2020_02_03-PM-02_54_00
Theory : minimal-first-order-logic
Home
Index