Proof of Nuprl Lemma : dl_forces

Step * 1 of Lemma dl_forces_wf

1. K : dl_KS
2. a : Prop
3. s : worlds(K)
4. pos : 𝔹
5. ∀[aprog:x:ℕ ⟶ worlds(K) ⟶ worlds(K) ⟶ ℙ]. ∀[comp,choose:x:Prog

                                                              ⟶ x1:Prog

                                                              ⟶ (worlds(K) ⟶ worlds(K) ⟶ ℙ)

                                                              ⟶ (worlds(K) ⟶ worlds(K) ⟶ ℙ)

                                                              ⟶ worlds(K)

                                                              ⟶ worlds(K)

                                                              ⟶ ℙ]. ∀[iterate:x:Prog

                                                                               ⟶ (worlds(K) ⟶ worlds(K) ⟶ ℙ)

                                                                               ⟶ worlds(K)

                                                                               ⟶ worlds(K)

                                                                               ⟶ ℙ]. ∀[test:x:Prop

                                                                                             ⟶ (𝔹 ⟶ worlds(K) ⟶ ℙ)

                                                                                             ⟶ worlds(K)

                                                                                             ⟶ worlds(K)

                                                                                             ⟶ ℙ]. ∀[aprop:x:ℕ

                                                                                                            ⟶ 𝔹

                                                                                                            ⟶ worlds(K)

                                                                                                            ⟶ ℙ].

∀[false:𝔹 ⟶ worlds(K) ⟶ ℙ]. ∀[implies,and,or:x:Prop
⟶ x1:Prop

                                                  ⟶ (𝔹 ⟶ worlds(K) ⟶ ℙ)

                                                  ⟶ (𝔹 ⟶ worlds(K) ⟶ ℙ)

⟶ 𝔹
⟶ worlds(K)

                                                  ⟶ ℙ]. ∀[box,diamond:x:Prog

                                                                       ⟶ x1:Prop

                                                                       ⟶ (worlds(K) ⟶ worlds(K) ⟶ ℙ)

                                                                       ⟶ (𝔹 ⟶ worlds(K) ⟶ ℙ)

                                                                       ⟶ 𝔹

                                                                       ⟶ worlds(K)

                                                                       ⟶ ℙ].

     (dl-ind(
             dl-aprog(x0)⇒ aprog[x0];
             dl-comp(x1,x2)⇒ x3,x4.comp[x1;x2;x3;x4];
             dl-choose(x5,x6)⇒ x7,x8.choose[x5;x6;x7;x8];
             dl-iterate(x9)⇒ x10.iterate[x9;x10];
             dl-test(x11)⇒ x12.test[x11;x12];
             dl-aprop(x13)⇒ aprop[x13];
             dl-false⇒ false;
             dl-implies(x14,x15)⇒ x16,x17.implies[x14;x15;x16;x17];
             dl-and(x18,x19)⇒ x20,x21.and[x18;x19;x20;x21];
             dl-or(x22,x23)⇒ x24,x25.or[x22;x23;x24;x25];
             dl-box(x26,x27)⇒ x28,x29.box[x26;x27;x28;x29];
             dl-diamond(x30,x31)⇒ x32,x33.diamond[x30;x31;x32;x33])  ∈ d:dl-Obj() ⟶ if dl-kind(d) =a "prog"

                                                                                      then worlds(K) ⟶ worlds(K) ⟶ ℙ

                                                                                      else 𝔹 ⟶ worlds(K) ⟶ ℙ

                                                                                      fi )

⊢ 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 ∈ ℙ
BY
{ ((Assert 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 )  ∈ d:dl-Obj() ⟶ if dl-kind(d) =a "prog"

                                                                     then worlds(K) ⟶ worlds(K) ⟶ ℙ

                                                                     else 𝔹 ⟶ worlds(K) ⟶ ℙ

                                                                     fi  BY

          (BHyp -1 THEN Complete (Auto)))
   THEN Auto
   ) }

Latex:

Latex:
1. K : dl\_KS 2. a : Prop 3. s : worlds(K) 4. pos : \mBbbB{} 5. \mforall{}[aprog:x:\mBbbN{} {}\mrightarrow{} worlds(K) {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}]. \mforall{}[comp,choose:x:Prog {}\mrightarrow{} x1:Prog {}\mrightarrow{} (worlds(K) {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}) {}\mrightarrow{} (worlds(K) {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}) {}\mrightarrow{} worlds(K) {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}]. \mforall{}[iterate:x:Prog {}\mrightarrow{} (worlds(K) {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}) {}\mrightarrow{} worlds(K) {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}]. \mforall{}[test:x:Prop {}\mrightarrow{} (\mBbbB{} {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}) {}\mrightarrow{} worlds(K) {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}]. \mforall{}[aprop:x:\mBbbN{} {}\mrightarrow{} \mBbbB{} {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}]. \mforall{}[false:\mBbbB{} {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}]. \mforall{}[implies,and,or:x:Prop {}\mrightarrow{} x1:Prop {}\mrightarrow{} (\mBbbB{} {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}) {}\mrightarrow{} (\mBbbB{} {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}) {}\mrightarrow{} \mBbbB{} {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}]. \mforall{}[box,diamond:x:Prog {}\mrightarrow{} x1:Prop {}\mrightarrow{} (worlds(K) {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}) {}\mrightarrow{} (\mBbbB{} {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}) {}\mrightarrow{} \mBbbB{} {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{}]. (dl-ind( dl-aprog(x0){}\mRightarrow{} aprog[x0]; dl-comp(x1,x2){}\mRightarrow{} x3,x4.comp[x1;x2;x3;x4]; dl-choose(x5,x6){}\mRightarrow{} x7,x8.choose[x5;x6;x7;x8]; dl-iterate(x9){}\mRightarrow{} x10.iterate[x9;x10]; dl-test(x11){}\mRightarrow{} x12.test[x11;x12]; dl-aprop(x13){}\mRightarrow{} aprop[x13]; dl-false{}\mRightarrow{} false; dl-implies(x14,x15){}\mRightarrow{} x16,x17.implies[x14;x15;x16;x17]; dl-and(x18,x19){}\mRightarrow{} x20,x21.and[x18;x19;x20;x21]; dl-or(x22,x23){}\mRightarrow{} x24,x25.or[x22;x23;x24;x25]; dl-box(x26,x27){}\mRightarrow{} x28,x29.box[x26;x27;x28;x29]; dl-diamond(x30,x31){}\mRightarrow{} x32,x33.diamond[x30;x31;x32;x33]) \mmember{} d:dl-Obj() {}\mrightarrow{} if dl-kind(d) =a "prog" then worlds(K) {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{} else \mBbbB{} {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{} fi ) \mvdash{} 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 \mmember{} \mBbbP{} By Latex: ((Assert 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 ) \mmember{} d:dl-Obj() {}\mrightarrow{} if dl-kind(d) =a "prog" then worlds(K) {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{} else \mBbbB{} {}\mrightarrow{} worlds(K) {}\mrightarrow{} \mBbbP{} fi BY (BHyp -1 THEN Complete (Auto))) THEN Auto ) Home Index