Nuprl Lemma : Form_ind_wf
∀[C,A:Type]. ∀[R:A ⟶ Form(C) ⟶ ℙ]. ∀[v:Form(C)]. ∀[Var:name:Atom ⟶ {x:A| R[x;Vname]} ].
∀[Const:value:C ⟶ {x:A| R[x;Const(value)]} ]. ∀[Set:var:Atom
⟶ phi:Form(C)
⟶ {x:A| R[x;phi]}
⟶ {x:A| R[x;{var | phi}]} ]. ∀[Equal:left:Form(C)
⟶ right:Form(C)
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A| R[x;left = right]} ].
∀[Member:element:Form(C) ⟶ set:Form(C) ⟶ {x:A| R[x;element]} ⟶ {x:A| R[x;set]} ⟶ {x:A| R[x;element ∈ set]} ].
∀[And:left:Form(C) ⟶ right:Form(C) ⟶ {x:A| R[x;left]} ⟶ {x:A| R[x;right]} ⟶ {x:A| R[x;left ∧ right)]} ].
∀[Or:left:Form(C) ⟶ right:Form(C) ⟶ {x:A| R[x;left]} ⟶ {x:A| R[x;right]} ⟶ {x:A| R[x;left ∨ right]} ].
∀[Not:body:Form(C) ⟶ {x:A| R[x;body]} ⟶ {x:A| R[x;¬(body)]} ]. ∀[All:var:Atom
⟶ body:Form(C)
⟶ {x:A| R[x;body]}
⟶ {x:A| R[x;∀var. body]} ].
∀[Exists:var:Atom ⟶ body:Form(C) ⟶ {x:A| R[x;body]} ⟶ {x:A| R[x;∃var. body]} ].
(Form_ind(v;
FormVar(name)⇒ Var[name];
FormConst(value)⇒ Const[value];
FormSet(var,phi)⇒ rec1.Set[var;phi;rec1];
FormEqual(left,right)⇒ rec2,rec3.Equal[left;right;rec2;rec3];
FormMember(element,set)⇒ rec4,rec5.Member[element;set;rec4;rec5];
FormAnd(left,right)⇒ rec6,rec7.And[left;right;rec6;rec7];
FormOr(left,right)⇒ rec8,rec9.Or[left;right;rec8;rec9];
FormNot(body)⇒ rec10.Not[body;rec10];
FormAll(var,body)⇒ rec11.All[var;body;rec11];
FormExists(var,body)⇒ rec12.Exists[var;body;rec12]) ∈ {x:A| R[x;v]} )
Proof
Definitions occuring in Statement :
Form_ind: Form_ind,
FormExists: ∃var. body,
FormAll: ∀var. body,
FormNot: ¬(body),
FormOr: left ∨ right,
FormAnd: left ∧ right),
FormMember: element ∈ set,
FormEqual: left = right,
FormSet: {var | phi},
FormConst: Const(value),
FormVar: Vname,
Form: Form(C),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2],
so_apply: x[s],
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
atom: Atom,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
Form_ind: Form_ind,
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s],
Form-definition,
Form-induction,
uniform-comp-nat-induction,
Form-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],
uimplies: b supposing a,
subtype_rel: A ⊆r B,
prop: ℙ,
guard: {T}
Lemmas referenced :
Form-definition,
has-value_wf_base,
is-exception_wf,
lifting-strict-atom_eq,
strict4-decide,
Form_wf,
istype-atom,
FormVar_wf,
FormConst_wf,
FormSet_wf,
FormEqual_wf,
FormMember_wf,
FormAnd_wf,
FormOr_wf,
FormNot_wf,
FormAll_wf,
FormExists_wf,
all_wf,
set_wf,
subtype_rel_function,
subtype_rel_self,
istype-universe,
Form-induction,
uniform-comp-nat-induction,
Form-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,
because_Cache,
functionIsType,
universeIsType,
universeEquality,
setIsType,
applyEquality,
functionEquality,
setEquality,
instantiate,
functionExtensionality,
atomEquality,
setElimination,
rename,
dependent_set_memberEquality_alt
Latex:
\mforall{}[C,A:Type]. \mforall{}[R:A {}\mrightarrow{} Form(C) {}\mrightarrow{} \mBbbP{}]. \mforall{}[v:Form(C)]. \mforall{}[Var:name:Atom {}\mrightarrow{} \{x:A| R[x;Vname]\} ].
\mforall{}[Const:value:C {}\mrightarrow{} \{x:A| R[x;Const(value)]\} ]. \mforall{}[Set:var:Atom
{}\mrightarrow{} phi:Form(C)
{}\mrightarrow{} \{x:A| R[x;phi]\}
{}\mrightarrow{} \{x:A| R[x;\{var | phi\}]\} ].
\mforall{}[Equal:left:Form(C)
{}\mrightarrow{} right:Form(C)
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left = right]\} ]. \mforall{}[Member:element:Form(C)
{}\mrightarrow{} set:Form(C)
{}\mrightarrow{} \{x:A| R[x;element]\}
{}\mrightarrow{} \{x:A| R[x;set]\}
{}\mrightarrow{} \{x:A| R[x;element \mmember{} set]\} ].
\mforall{}[And:left:Form(C)
{}\mrightarrow{} right:Form(C)
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left \mwedge{} right)]\} ]. \mforall{}[Or:left:Form(C)
{}\mrightarrow{} right:Form(C)
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left \mvee{} right]\} ]. \mforall{}[Not:body:Form(C)
{}\mrightarrow{} \{x:A| R[x;body]\}
{}\mrightarrow{} \{x:A|
R[x;\mneg{}(body)]\} ].
\mforall{}[All:var:Atom {}\mrightarrow{} body:Form(C) {}\mrightarrow{} \{x:A| R[x;body]\} {}\mrightarrow{} \{x:A| R[x;\mforall{}var. body]\} ].
\mforall{}[Exists:var:Atom {}\mrightarrow{} body:Form(C) {}\mrightarrow{} \{x:A| R[x;body]\} {}\mrightarrow{} \{x:A| R[x;\mexists{}var. body]\} ].
(Form\_ind(v;
FormVar(name){}\mRightarrow{} Var[name];
FormConst(value){}\mRightarrow{} Const[value];
FormSet(var,phi){}\mRightarrow{} rec1.Set[var;phi;rec1];
FormEqual(left,right){}\mRightarrow{} rec2,rec3.Equal[left;right;rec2;rec3];
FormMember(element,set){}\mRightarrow{} rec4,rec5.Member[element;set;rec4;rec5];
FormAnd(left,right){}\mRightarrow{} rec6,rec7.And[left;right;rec6;rec7];
FormOr(left,right){}\mRightarrow{} rec8,rec9.Or[left;right;rec8;rec9];
FormNot(body){}\mRightarrow{} rec10.Not[body;rec10];
FormAll(var,body){}\mRightarrow{} rec11.All[var;body;rec11];
FormExists(var,body){}\mRightarrow{} rec12.Exists[var;body;rec12]) \mmember{} \{x:A| R[x;v]\} )
Date html generated:
2020_05_20-AM-09_12_23
Last ObjectModification:
2020_01_24-PM-01_52_09
Theory : PZF
Home
Index