Nuprl Definition : mFO-Kripke-struct
mKripkeStruct ==
K:G:Type × R:G ⟶ G ⟶ ℙ × D:G ⟶ Type × (i:G ⟶ FOStruct(D i)) × let G,R,D,S = K
in (∀i,j:G.
((R i j)
⇒ (((D i) ⊆r (D j))
∧ (∀A:Atom. ∀L:(D i) List.
((S i A L) ⊆r (S j A L))))))
∧ (∀i:G. (R i i))
∧ (∀i,j,k:G. ((R i j) ⇒ (R j k) ⇒ (R i k)))
Definitions occuring in Statement :
FOStruct: FOStruct(Dom),
list: T List,
spreadn: spread4,
subtype_rel: A ⊆r B,
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
atom: Atom,
universe: Type
Definitions occuring in definition :
prop: ℙ,
product: x:A × B[x],
universe: Type,
function: x:A ⟶ B[x],
FOStruct: FOStruct(Dom),
spreadn: spread4,
atom: Atom,
list: T List,
subtype_rel: A ⊆r B,
and: P ∧ Q,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a
FDL editor aliases :
m-K-s
Latex:
mKripkeStruct ==
K:G:Type \mtimes{} R:G {}\mrightarrow{} G {}\mrightarrow{} \mBbbP{} \mtimes{} D:G {}\mrightarrow{} Type \mtimes{} (i:G {}\mrightarrow{} FOStruct(D i)) \mtimes{} let G,R,D,S = K
in (\mforall{}i,j:G.
((R i j)
{}\mRightarrow{} (((D i) \msubseteq{}r (D j))
\mwedge{} (\mforall{}A:Atom.
\mforall{}L:(D i) List.
((S i A L)
\msubseteq{}r (S j A
L))))))
\mwedge{} (\mforall{}i:G. (R i i))
\mwedge{} (\mforall{}i,j,k:G.
((R i j)
{}\mRightarrow{} (R j k)
{}\mRightarrow{} (R i k)))
Date html generated:
2019_10_16-AM-11_43_50
Last ObjectModification:
2018_10_15-PM-06_04_33
Theory : minimal-first-order-logic
Home
Index