Nuprl Lemma : mFOL_ind_wf
∀[A:Type]. ∀[R:A ⟶ mFOL() ⟶ ℙ]. ∀[v:mFOL()]. ∀[atomic:name:Atom ⟶ vars:(ℤ List) ⟶ {x:A| R[x;name(vars)]} ].
∀[connect:knd:Atom
⟶ left:mFOL()
⟶ right:mFOL()
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A| R[x;mFOconnect(knd;left;right)]} ]. ∀[quant:isall:𝔹
⟶ var:ℤ
⟶ body:mFOL()
⟶ {x:A| R[x;body]}
⟶ {x:A| R[x;mFOquant(isall;var;body)]} ].
(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]) ∈ {x:A| R[x;v]} )
Proof
Definitions occuring in Statement :
mFOL_ind: mFOL_ind,
mFOquant: mFOquant(isall;var;body),
mFOconnect: mFOconnect(knd;left;right),
mFOatomic: name(vars),
mFOL: mFOL(),
list: T List,
bool: 𝔹,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2;s3;s4;s5],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
int: ℤ,
atom: Atom,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
mFOL_ind: mFOL_ind,
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2;s3;s4;s5],
so_apply: x[s1;s2],
mFOL-definition,
mFOL-induction,
uniform-comp-nat-induction,
mFOL-ext,
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_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
subtype_rel: A ⊆r B,
prop: ℙ,
guard: {T}
Lemmas referenced :
mFOL-definition,
has-value_wf_base,
is-exception_wf,
lifting-strict-atom_eq,
strict4-decide,
istype-atom,
list_wf,
mFOatomic_wf,
mFOconnect_wf,
bool_wf,
istype-int,
mFOquant_wf,
mFOL_wf,
subtype_rel_function,
subtype_rel_self,
istype-universe,
mFOL-induction,
uniform-comp-nat-induction,
mFOL-ext,
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,
intEquality,
setIsType,
because_Cache,
applyEquality,
functionEquality,
setEquality,
instantiate,
functionExtensionality,
atomEquality
Latex:
\mforall{}[A:Type]. \mforall{}[R:A {}\mrightarrow{} mFOL() {}\mrightarrow{} \mBbbP{}]. \mforall{}[v:mFOL()]. \mforall{}[atomic:name:Atom
{}\mrightarrow{} vars:(\mBbbZ{} List)
{}\mrightarrow{} \{x:A| R[x;name(vars)]\} ].
\mforall{}[connect:knd:Atom
{}\mrightarrow{} left:mFOL()
{}\mrightarrow{} right:mFOL()
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;mFOconnect(knd;left;right)]\} ]. \mforall{}[quant:isall:\mBbbB{}
{}\mrightarrow{} var:\mBbbZ{}
{}\mrightarrow{} body:mFOL()
{}\mrightarrow{} \{x:A| R[x;body]\}
{}\mrightarrow{} \{x:A|
R[x;mFOquant(isall;var;body)]\} ].
(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{} \{x:A| R[x;v]\} )
Date html generated:
2020_05_20-AM-09_08_09
Last ObjectModification:
2020_01_23-PM-05_34_40
Theory : minimal-first-order-logic
Home
Index