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