Nuprl Lemma : PZF-induction
∀C:Type
∀[F:PZF-Formula(C) ⟶ ℙ]. ∀[T:PZF-Term(C) ⟶ ℙ].
((∀name:Atom. T[Vname])
⇒ (∀value:C. T[Const(value)])
⇒ (∀x:Atom. ∀phi:PZF-Formula(C). (F[phi] ⇒ PZF-safe(phi;[x]) ⇒ T[{x | phi}]))
⇒ (∀a,b:PZF-Term(C). (T[a] ⇒ T[b] ⇒ F[a = b]))
⇒ (∀a,b:PZF-Term(C). (T[a] ⇒ T[b] ⇒ F[a ∈ b]))
⇒ (∀a,b:PZF-Formula(C). (F[a] ⇒ F[b] ⇒ F[a ∧ b)]))
⇒ (∀a,b:PZF-Formula(C). (F[a] ⇒ F[b] ⇒ F[a ∨ b]))
⇒ (∀a:PZF-Formula(C). (F[a] ⇒ F[¬(a)]))
⇒ (∀a:PZF-Formula(C). ∀x:Atom. (F[a] ⇒ F[∀x. a]))
⇒ (∀a:PZF-Formula(C). ∀x:Atom. (F[a] ⇒ F[∃x. a]))
⇒ ((∀phi:PZF-Formula(C). F[phi]) ∧ (∀t:PZF-Term(C). T[t])))
Proof
Definitions occuring in Statement :
PZF-Formula: PZF-Formula(C),
PZF-Term: PZF-Term(C),
PZF-safe: PZF-safe(phi;vs),
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,
cons: [a / b],
nil: [],
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
atom: Atom,
universe: Type
Definitions unfolded in proof :
true: True,
FormExists: ∃var. body,
FormAll: ∀var. body,
FormNot: ¬(body),
FormOr: left ∨ right,
FormAnd: left ∧ right),
FormMember: element ∈ set,
FormEqual: left = right,
band: p ∧b q,
FormSet: {var | phi},
FormConst: Const(value),
wfFormAux: wfFormAux(f),
Form_ind: Form_ind,
FormVar: Vname,
wfForm: wfForm(f),
SafeForm: SafeForm(f),
termForm: termForm(f),
not: ¬A,
PZF-Formula: PZF-Formula(C),
false: False,
assert: ↑b,
bnot: ¬bb,
guard: {T},
sq_type: SQType(T),
or: P ∨ Q,
exists: ∃x:A. B[x],
bfalse: ff,
subtype_rel: A ⊆r B,
PZF-Form: PZF-Form(C),
cand: A c∧ B,
PZF-Term: PZF-Term(C),
so_apply: x[s],
prop: ℙ,
ifthenelse: if b then t else f fi ,
uimplies: b supposing a,
and: P ∧ Q,
uiff: uiff(P;Q),
btrue: tt,
it: ⋅,
unit: Unit,
bool: 𝔹,
so_lambda: λ2x.t[x],
member: t ∈ T,
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
rev_uimplies: rev_uimplies(P;Q),
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
istype-universe,
PZF-Formula_wf,
PZF-Term_wf,
FormVar_wf,
istype-atom,
FormConst_wf,
FormSet_wf2,
PZF-safe_wf,
FormEqual_wf2,
FormMember_wf2,
FormAnd_wf2,
FormOr_wf2,
FormNot_wf2,
FormAll_wf2,
FormExists_wf2,
wfFormAux_wf,
bfalse_wf,
nil_wf,
cons_wf,
PZF_safe_wf,
btrue_wf,
band_wf,
bool_cases,
istype-true,
Form_wf,
istype-void,
assert-bnot,
bool_subtype_base,
bool_wf,
subtype_base_sq,
bool_cases_sqequal,
eqff_to_assert,
istype-assert,
SafeForm_wf,
wfForm_wf,
assert_wf,
eqtt_to_assert,
termForm_wf,
Form-induction,
assert_of_band,
wfFormAux-unique,
assert_elim,
btrue_neq_bfalse,
assert_functionality_wrt_uiff,
assert-PZF_safe,
bool_sim_true,
iff_imp_equal_bool,
assert_of_ff
Rules used in proof :
universeEquality,
natural_numberEquality,
atomEquality,
universeIsType,
functionIsType,
voidElimination,
independent_functionElimination,
cumulativity,
instantiate,
dependent_functionElimination,
promote_hyp,
equalityIstype,
dependent_pairFormation_alt,
equalitySymmetry,
equalityTransitivity,
rename,
setElimination,
productIsType,
independent_pairFormation,
dependent_set_memberEquality_alt,
applyEquality,
because_Cache,
functionEquality,
independent_isectElimination,
productElimination,
equalityElimination,
unionElimination,
inhabitedIsType,
hypothesis,
lambdaEquality_alt,
sqequalRule,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
isect_memberFormation_alt,
lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
isect_memberEquality_alt
Latex:
\mforall{}C:Type
\mforall{}[F:PZF-Formula(C) {}\mrightarrow{} \mBbbP{}]. \mforall{}[T:PZF-Term(C) {}\mrightarrow{} \mBbbP{}].
((\mforall{}name:Atom. T[Vname])
{}\mRightarrow{} (\mforall{}value:C. T[Const(value)])
{}\mRightarrow{} (\mforall{}x:Atom. \mforall{}phi:PZF-Formula(C). (F[phi] {}\mRightarrow{} PZF-safe(phi;[x]) {}\mRightarrow{} T[\{x | phi\}]))
{}\mRightarrow{} (\mforall{}a,b:PZF-Term(C). (T[a] {}\mRightarrow{} T[b] {}\mRightarrow{} F[a = b]))
{}\mRightarrow{} (\mforall{}a,b:PZF-Term(C). (T[a] {}\mRightarrow{} T[b] {}\mRightarrow{} F[a \mmember{} b]))
{}\mRightarrow{} (\mforall{}a,b:PZF-Formula(C). (F[a] {}\mRightarrow{} F[b] {}\mRightarrow{} F[a \mwedge{} b)]))
{}\mRightarrow{} (\mforall{}a,b:PZF-Formula(C). (F[a] {}\mRightarrow{} F[b] {}\mRightarrow{} F[a \mvee{} b]))
{}\mRightarrow{} (\mforall{}a:PZF-Formula(C). (F[a] {}\mRightarrow{} F[\mneg{}(a)]))
{}\mRightarrow{} (\mforall{}a:PZF-Formula(C). \mforall{}x:Atom. (F[a] {}\mRightarrow{} F[\mforall{}x. a]))
{}\mRightarrow{} (\mforall{}a:PZF-Formula(C). \mforall{}x:Atom. (F[a] {}\mRightarrow{} F[\mexists{}x. a]))
{}\mRightarrow{} ((\mforall{}phi:PZF-Formula(C). F[phi]) \mwedge{} (\mforall{}t:PZF-Term(C). T[t])))
Date html generated:
2020_05_20-AM-09_12_40
Last ObjectModification:
2020_01_28-PM-05_25_34
Theory : PZF
Home
Index