Nuprl Definition : complete
complete{i:l}(S) ==
(∀n∈S.(∃y∈snd(n). |= dl-conj(fst(n)) ⇒ y))
∨ (∃K:dl_KS
∃f:node ⟶ worlds(K). (∀n∈S.(∀phi∈fst(n).dl_forces(K;tt;phi;f n)) ∧ (∀phi∈snd(n).dl_forces(K;ff;phi;f n))))
Definitions occuring in Statement :
node: node,
dl_forces: dl_forces(K;pos;a;s),
dl_KS: dl_KS,
worlds: worlds(k),
dl-conj: dl-conj(L),
dl-valid: |= phi,
dl-implies: x1 ⇒ x,
l_exists: (∃x∈L. P[x]),
l_all: (∀x∈L.P[x]),
bfalse: ff,
btrue: tt,
pi1: fst(t),
pi2: snd(t),
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x]
Definitions occuring in definition :
or: P ∨ Q,
l_exists: (∃x∈L. P[x]),
dl-valid: |= phi,
dl-implies: x1 ⇒ x,
dl-conj: dl-conj(L),
dl_KS: dl_KS,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
node: node,
worlds: worlds(k),
and: P ∧ Q,
pi1: fst(t),
btrue: tt,
l_all: (∀x∈L.P[x]),
pi2: snd(t),
dl_forces: dl_forces(K;pos;a;s),
bfalse: ff,
apply: f a
FDL editor aliases :
complete
Latex:
complete\{i:l\}(S) ==
(\mforall{}n\mmember{}S.(\mexists{}y\mmember{}snd(n). |= dl-conj(fst(n)) {}\mRightarrow{} y))
\mvee{} (\mexists{}K:dl\_KS
\mexists{}f:node {}\mrightarrow{} worlds(K)
(\mforall{}n\mmember{}S.(\mforall{}phi\mmember{}fst(n).dl\_forces(K;tt;phi;f n)) \mwedge{} (\mforall{}phi\mmember{}snd(n).dl\_forces(K;ff;phi;f n))))
Date html generated:
2019_10_16-AM-11_25_00
Last ObjectModification:
2019_05_06-PM-05_06_04
Theory : dynamic!logic
Home
Index