Nuprl Definition : dl-logical-eq-atomic
(a ⇐⇒a b) == ∀p:ℕ. (|= <a> atm(p) ⇒ <b> atm(p) ∧ |= <b> atm(p) ⇒ <a> atm(p))
Definitions occuring in Statement :
dl-valid: |= phi,
dl-diamond: <x1> x,
dl-implies: x1 ⇒ x,
dl-aprop: atm(x),
nat: ℕ,
all: ∀x:A. B[x],
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[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-atomic
Latex:
(a \mLeftarrow{}{}\mRightarrow{}a b) == \mforall{}p:\mBbbN{}. (|= <a> atm(p) {}\mRightarrow{} <b> atm(p) \mwedge{} |= <b> atm(p) {}\mRightarrow{} <a> atm(p))
Date html generated:
2019_10_15-AM-11_46_00
Last ObjectModification:
2019_03_26-PM-00_12_58
Theory : dynamic!logic
Home
Index