Nuprl Lemma : mFOL-definition

[A:Type]. ∀[R:A ─→ mFOL() ─→ ℙ].
((∀name:Atom. ∀vars:ℤ List.  {x:A| R[x;name(vars)]} )
(∀knd:Atom. ∀left,right:mFOL().  ({x:A| R[x;left]}   {x:A| R[x;right]}   {x:A| R[x;mFOconnect(knd;left;right)]}\000C ))
(∀isall:𝔹. ∀var:ℤ. ∀body:mFOL().  ({x:A| R[x;body]}   {x:A| R[x;mFOquant(isall;var;body)]} ))
{∀v:mFOL(). {x:A| R[x;v]} })

Proof

Definitions occuring in Statement :  mFOquant: mFOquant(isall;var;body) mFOconnect: mFOconnect(knd;left;right) mFOatomic: name(vars) mFOL: mFOL() list: List bool: 𝔹 uall: [x:A]. B[x] prop: guard: {T} so_apply: x[s1;s2] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  function: x:A ─→ B[x] int: atom: Atom universe: Type
Lemmas :  mFOL-induction set_wf mFOL_wf all_wf bool_wf mFOquant_wf mFOconnect_wf list_wf mFOatomic_wf
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  mFOL()  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}name:Atom.  \mforall{}vars:\mBbbZ{}  List.    \{x:A|  R[x;name(vars)]\}  )
{}\mRightarrow{}  (\mforall{}knd:Atom.  \mforall{}left,right:mFOL().
(\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;mFOconnect(knd;left;right)]\}  ))
{}\mRightarrow{}  (\mforall{}isall:\mBbbB{}.  \mforall{}var:\mBbbZ{}.  \mforall{}body:mFOL().    (\{x:A|  R[x;body]\}    {}\mRightarrow{}  \{x:A|  R[x;mFOquant(isall;var;body)]\}  ))
{}\mRightarrow{}  \{\mforall{}v:mFOL().  \{x:A|  R[x;v]\}  \})

Date html generated: 2015_07_17-AM-07_53_50
Last ObjectModification: 2015_01_27-AM-10_06_56

Home Index