Nuprl Definition : dl_forces

dl_forces(K;pos;a;s) ==
  dl-ind(
         dl-aprog(n)⇒ λk1,k2. (k1Rk2 ∧ atmFrc_prog(K;n;k1;k2));
         dl-comp(alpha,beta)⇒ r1,r2.λk1,k3. ∃k2:worlds(K). ((r1 k1 k2) ∧ (r2 k2 k3));
         dl-choose(alpha,beta)⇒ r1,r2.λk1,k2. ((r1 k1 k2) ∨ (r2 k1 k2));
         dl-iterate(alpha)⇒ r.r^*;
         dl-test(phi)⇒ p.λk1,k2. ((p tt k1) ∧ (k2 = k1 ∈ worlds(K)));
         dl-aprop(m)⇒ λpos,k. atmFrc_prop(K;m;k);
         dl-false⇒ λpos,k. if pos then False else True fi ;
         dl-implies(phi,psi)⇒ p,q.λpos,k. if pos
                                          then ∀k':worlds(K). (kRk' ⇒ (p tt k') ⇒ (q tt k'))
                                          else ∃t:worlds(K). (kRt ∧ (p tt t) ∧ (q ff t))
                                          fi ;
         dl-and(phi,psi)⇒ p,q.λpos,k. if pos then (p tt k) ∧ (q tt k) else (p ff k) ∨ (q ff k) fi ;
         dl-or(phi,psi)⇒ p,q.λpos,k. if pos then (p tt k) ∨ (q tt k) else (p ff k) ∧ (q ff k) fi ;
         dl-box(alpha,phi)⇒ r,p.λpos,k. if pos
                                        then ∀k':worlds(K). (kRk' ⇒ (r k k') ⇒ (p tt k))
                                        else ∃t:worlds(K). ((kRt ∧ (r k t)) ∧ (p ff k))
                                        fi ;
         dl-diamond(alpha,phi)⇒ r,p.λpos,k. if pos
                                            then ∃k':worlds(K). (kRk' ∧ (r k k') ∧ (p tt k'))
                                            else ∀t:worlds(K). (kRt ⇒ (r k t) ⇒ (p ff k))
                                            fi )  
  prop(a) 
  pos 
  s


Definitions occuring in Statement :  atmFrc_prog: atmFrc_prog(k;a;r;s),  atmFrc_prop: atmFrc_prop(k;a;s),  KrRel: sRt,  worlds: worlds(k),  dl-ind: dl-ind,  dl-prop-obj: prop(x),  rel_star: R^*,  ifthenelse: if b then t else f fi ,  bfalse: ff,  btrue: tt,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  false: False,  true: True,  apply: f a,  lambda: λx.A[x],  equal: s = t ∈ T
Definitions occuring in definition :  apply: f a,  bfalse: ff,  and: P ∧ Q,  btrue: tt,  or: P ∨ Q,  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  KrRel: sRt,  worlds: worlds(k),  exists: ∃x:A. B[x],  implies: P ⇒ Q,  all: ∀x:A. B[x],  true: True,  false: False,  atmFrc_prop: atmFrc_prop(k;a;s),  equal: s = t ∈ T,  rel_star: R^*,  atmFrc_prog: atmFrc_prog(k;a;r;s),  dl-ind: dl-ind,  dl-prop-obj: prop(x)
FDL editor aliases :  dl_forces
Latex:
dl\_forces(K;pos;a;s)  ==
    dl-ind(
                  dl-aprog(n){}\mRightarrow{}  \mlambda{}k1,k2.  (k1Rk2  \mwedge{}  atmFrc\_prog(K;n;k1;k2));
                  dl-comp(alpha,beta){}\mRightarrow{}  r1,r2.\mlambda{}k1,k3.  \mexists{}k2:worlds(K).  ((r1  k1  k2)  \mwedge{}  (r2  k2  k3));
                  dl-choose(alpha,beta){}\mRightarrow{}  r1,r2.\mlambda{}k1,k2.  ((r1  k1  k2)  \mvee{}  (r2  k1  k2));
                  dl-iterate(alpha){}\mRightarrow{}  r.rel\_star(worlds(K);  r);
                  dl-test(phi){}\mRightarrow{}  p.\mlambda{}k1,k2.  ((p  tt  k1)  \mwedge{}  (k2  =  k1));
                  dl-aprop(m){}\mRightarrow{}  \mlambda{}pos,k.  atmFrc\_prop(K;m;k);
                  dl-false{}\mRightarrow{}  \mlambda{}pos,k.  if  pos  then  False  else  True  fi  ;
                  dl-implies(phi,psi){}\mRightarrow{}  p,q.\mlambda{}pos,k.  if  pos
                                                                                    then  \mforall{}k':worlds(K).  (kRk'  {}\mRightarrow{}  (p  tt  k')  {}\mRightarrow{}  (q  tt  k'))
                                                                                    else  \mexists{}t:worlds(K).  (kRt  \mwedge{}  (p  tt  t)  \mwedge{}  (q  ff  t))
                                                                                    fi  ;
                  dl-and(phi,psi){}\mRightarrow{}  p,q.\mlambda{}pos,k.  if  pos  then  (p  tt  k)  \mwedge{}  (q  tt  k)  else  (p  ff  k)  \mvee{}  (q  ff  k)  fi  ;
                  dl-or(phi,psi){}\mRightarrow{}  p,q.\mlambda{}pos,k.  if  pos  then  (p  tt  k)  \mvee{}  (q  tt  k)  else  (p  ff  k)  \mwedge{}  (q  ff  k)  fi  ;
                  dl-box(alpha,phi){}\mRightarrow{}  r,p.\mlambda{}pos,k.  if  pos
                                                                                then  \mforall{}k':worlds(K).  (kRk'  {}\mRightarrow{}  (r  k  k')  {}\mRightarrow{}  (p  tt  k))
                                                                                else  \mexists{}t:worlds(K).  ((kRt  \mwedge{}  (r  k  t))  \mwedge{}  (p  ff  k))
                                                                                fi  ;
                  dl-diamond(alpha,phi){}\mRightarrow{}  r,p.\mlambda{}pos,k.  if  pos
                                                                                        then  \mexists{}k':worlds(K).  (kRk'  \mwedge{}  (r  k  k')  \mwedge{}  (p  tt  k'))
                                                                                        else  \mforall{}t:worlds(K).  (kRt  {}\mRightarrow{}  (r  k  t)  {}\mRightarrow{}  (p  ff  k))
                                                                                        fi  )   
    prop(a) 
    pos 
    s


Date html generated: 2020_05_20-AM-09_01_45
Last ObjectModification: 2019_12_13-AM-09_39_39

Theory : dynamic!logic


Home Index