Nuprl Lemma : Form-definition
∀[C,A:Type]. ∀[R:A ⟶ Form(C) ⟶ ℙ].
((∀name:Atom. {x:A| R[x;Vname]} )
⇒ (∀value:C. {x:A| R[x;Const(value)]} )
⇒ (∀var:Atom. ∀phi:Form(C). ({x:A| R[x;phi]} ⇒ {x:A| R[x;{var | phi}]} ))
⇒ (∀left,right:Form(C). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left = right]} ))
⇒ (∀element,set:Form(C). ({x:A| R[x;element]} ⇒ {x:A| R[x;set]} ⇒ {x:A| R[x;element ∈ set]} ))
⇒ (∀left,right:Form(C). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left ∧ right)]} ))
⇒ (∀left,right:Form(C). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left ∨ right]} ))
⇒ (∀body:Form(C). ({x:A| R[x;body]} ⇒ {x:A| R[x;¬(body)]} ))
⇒ (∀var:Atom. ∀body:Form(C). ({x:A| R[x;body]} ⇒ {x:A| R[x;∀var. body]} ))
⇒ (∀var:Atom. ∀body:Form(C). ({x:A| R[x;body]} ⇒ {x:A| R[x;∃var. body]} ))
⇒ {∀v:Form(C). {x:A| R[x;v]} })
Proof
Definitions occuring in Statement :
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: ℙ,
guard: {T},
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
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,
implies: P ⇒ Q,
guard: {T},
so_lambda: λ2x.t[x],
so_apply: x[s1;s2],
subtype_rel: A ⊆r B,
so_apply: x[s],
prop: ℙ,
all: ∀x:A. B[x]
Lemmas referenced :
Form-induction,
set_wf,
Form_wf,
all_wf,
FormExists_wf,
FormAll_wf,
FormNot_wf,
FormOr_wf,
FormAnd_wf,
FormMember_wf,
FormEqual_wf,
FormSet_wf,
FormConst_wf,
FormVar_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
lambdaFormation,
sqequalRule,
lambdaEquality,
cumulativity,
applyEquality,
functionExtensionality,
because_Cache,
independent_functionElimination,
atomEquality,
functionEquality,
universeEquality,
setEquality,
setElimination,
rename
Latex:
\mforall{}[C,A:Type]. \mforall{}[R:A {}\mrightarrow{} Form(C) {}\mrightarrow{} \mBbbP{}].
((\mforall{}name:Atom. \{x:A| R[x;Vname]\} )
{}\mRightarrow{} (\mforall{}value:C. \{x:A| R[x;Const(value)]\} )
{}\mRightarrow{} (\mforall{}var:Atom. \mforall{}phi:Form(C). (\{x:A| R[x;phi]\} {}\mRightarrow{} \{x:A| R[x;\{var | phi\}]\} ))
{}\mRightarrow{} (\mforall{}left,right:Form(C). (\{x:A| R[x;left]\} {}\mRightarrow{} \{x:A| R[x;right]\} {}\mRightarrow{} \{x:A| R[x;left = right]\} ))
{}\mRightarrow{} (\mforall{}element,set:Form(C). (\{x:A| R[x;element]\} {}\mRightarrow{} \{x:A| R[x;set]\} {}\mRightarrow{} \{x:A| R[x;element \mmember{} set]\} \000C))
{}\mRightarrow{} (\mforall{}left,right:Form(C). (\{x:A| R[x;left]\} {}\mRightarrow{} \{x:A| R[x;right]\} {}\mRightarrow{} \{x:A| R[x;left \mwedge{} right)]\} ))
{}\mRightarrow{} (\mforall{}left,right:Form(C). (\{x:A| R[x;left]\} {}\mRightarrow{} \{x:A| R[x;right]\} {}\mRightarrow{} \{x:A| R[x;left \mvee{} right]\} ))
{}\mRightarrow{} (\mforall{}body:Form(C). (\{x:A| R[x;body]\} {}\mRightarrow{} \{x:A| R[x;\mneg{}(body)]\} ))
{}\mRightarrow{} (\mforall{}var:Atom. \mforall{}body:Form(C). (\{x:A| R[x;body]\} {}\mRightarrow{} \{x:A| R[x;\mforall{}var. body]\} ))
{}\mRightarrow{} (\mforall{}var:Atom. \mforall{}body:Form(C). (\{x:A| R[x;body]\} {}\mRightarrow{} \{x:A| R[x;\mexists{}var. body]\} ))
{}\mRightarrow{} \{\mforall{}v:Form(C). \{x:A| R[x;v]\} \})
Date html generated:
2018_05_21-PM-11_25_46
Last ObjectModification:
2017_10_13-PM-07_03_14
Theory : PZF
Home
Index