Nuprl Definition : dl-logical-eq-weak
(a ⇐⇒w b) ==
∃p:ℕ
((¬(p ∈ dl-prop-atoms() prog(a)))
∧ (¬(p ∈ dl-prop-atoms() prog(b)))
∧ |= <a> atm(p) ⇒ <b> atm(p)
∧ |= <b> atm(p) ⇒ <a> atm(p))
Definitions occuring in Statement :
dl-valid: |= phi,
dl-prop-atoms: dl-prop-atoms(),
dl-diamond: <x1> x,
dl-implies: x1 ⇒ x,
dl-aprop: atm(x),
dl-prog-obj: prog(x),
l_member: (x ∈ l),
nat: ℕ,
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q,
apply: f a
Definitions occuring in definition :
exists: ∃x:A. B[x],
not: ¬A,
l_member: (x ∈ l),
apply: f a,
dl-prop-atoms: dl-prop-atoms(),
dl-prog-obj: prog(x),
nat: ℕ,
and: P ∧ Q,
dl-valid: |= phi,
dl-implies: x1 ⇒ x,
dl-diamond: <x1> x,
dl-aprop: atm(x)
FDL editor aliases :
dl-logical-eq-weak
Latex:
(a \mLeftarrow{}{}\mRightarrow{}w b) ==
\mexists{}p:\mBbbN{}
((\mneg{}(p \mmember{} dl-prop-atoms() prog(a)))
\mwedge{} (\mneg{}(p \mmember{} dl-prop-atoms() prog(b)))
\mwedge{} |= <a> atm(p) {}\mRightarrow{} <b> atm(p)
\mwedge{} |= <b> atm(p) {}\mRightarrow{} <a> atm(p))
Date html generated:
2019_10_15-AM-11_45_54
Last ObjectModification:
2019_03_26-PM-00_11_47
Theory : dynamic!logic
Home
Index