Nuprl Definition : church-inductive
church-inductive{i:l}(x) == ∀[P:cNat ⟶ ℙ]. ((P cZ) ⇒ (∀[y:cNat]. ((P y) ⇒ (P (cS y)))) ⇒ (P x))
Definitions occuring in Statement :
church-succ: cS,
church-zero: cZ,
church-Nat: cNat,
uall: ∀[x:A]. B[x],
prop: ℙ,
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
function: x:A ⟶ B[x],
prop: ℙ,
church-zero: cZ,
uall: ∀[x:A]. B[x],
church-Nat: cNat,
implies: P ⇒ Q,
church-succ: cS,
apply: f a
FDL editor aliases :
church-inductive
Latex:
church-inductive\{i:l\}(x) == \mforall{}[P:cNat {}\mrightarrow{} \mBbbP{}]. ((P cZ) {}\mRightarrow{} (\mforall{}[y:cNat]. ((P y) {}\mRightarrow{} (P (cS y)))) {}\mRightarrow{} (P x))
Date html generated:
2020_05_20-AM-08_05_28
Last ObjectModification:
2019_11_15-PM-10_34_00
Theory : general
Home
Index