Nuprl Definition : language1
language1{i:l}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]) ==
∀[D:Type]. ∀[A:ℙ]. ∀[B,C:D ⟶ ℙ]. ∀[P,Q,R:D ⟶ D ⟶ ℙ]. ∀[H:D ⟶ D ⟶ D ⟶ ℙ]. fml[D;A;B;C;P;Q;R;H]
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
prop: ℙ,
function: x:A ⟶ B[x],
universe: Type
FDL editor aliases :
language1
Latex:
language1\{i:l\}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]) ==
\mforall{}[D:Type]. \mforall{}[A:\mBbbP{}]. \mforall{}[B,C:D {}\mrightarrow{} \mBbbP{}]. \mforall{}[P,Q,R:D {}\mrightarrow{} D {}\mrightarrow{} \mBbbP{}]. \mforall{}[H:D {}\mrightarrow{} D {}\mrightarrow{} D {}\mrightarrow{} \mBbbP{}].
fml[D;A;B;C;P;Q;R;H]
Date html generated:
2016_05_16-AM-09_07_35
Last ObjectModification:
2012_07_12-AM-10_34_31
Theory : first-order!and!ancestral!logic
Home
Index