LPC exposition of first order logic in the new Logic Lab

[Mark Tarver]

Logic, Proof and Computation introduced an exposition of  first order logic that I have now reproduced in the Logic Lab (LL).   The LL exposition now codes directly into sequent calculus and produces performant type secure code.  It is likely that the Logic Lab version will replace the old hand-coded Provedit!  that I used for LPC.

FYI here is the code in LL for the deduction rules for FOL in LPC.   

(s-rule hyp ()

   

     ______________

     P >> P;)

   

   (s-rule vr1 ()

     P;

     ______________

     [P v Q];)

   

   (s-rule vr2 ()

     Q;

     ______________

     [P v Q];)

   

   (s-rule vl ()

     Q >> P;

     R >> P;

     ______________

     [Q v R] >> P;)

   

   (s-rule &r ()

   

      P; Q;

      _____

      [P & Q];)

    

    (s-rule &l ()

    

      P, Q >> R;

      __________

      [P & Q] >> R;)

      

    (s-rule =>r ()

    

      P >> Q;

      _______

      [P => Q];)

      

     (s-rule =>l ()

     

       [P => Q] >> P;

       ______________

       [P => Q] >> Q;)

       

     (s-rule <=>r ()

     

       [[P => Q] & [Q => P]];

       ______________________

       [P <=> Q];)

       

     (s-rule <=>l ()

     

       [[P => Q] & [Q => P]] >> R;

       ______________________

       [P <=> Q] >> R;) 

       

     (s-rule ~r ()

     

       [P => falsum];

       ______________

       [~ P];)

       

     (s-rule ~l ()

     

       [P => falsum] >> Q;

       ______________

       [~ P] >> Q;)                

   

     (s-rule lemma (Q : prop)

   

       Q;

       Q >> P;

       _______

       P;)

       

     (s-rule lem (P : prop)

      

       [P v [~ P]] >> Q;

       _________________

       Q;)

       

     (s-rule exp ()

      

       falsum;

       _______

       P;)      

          

     (s-rule thin (N : number)

     

      let Hypotheses (remove-nth N Hypotheses)

      P;

      _________________________________________

      P;)      

      

      (s-rule swap (M : number N : number)

      

        let Hypotheses (exchange M N Hypotheses)

        P;

        _________________________________________

        P;)

      

      (s-rule =r ()

      

       _______

       [X = X];)     

        

       (s-rule =l ()

      

       let PX/Y (replace X Y P)

       [X = Y] >> PX/Y;

       ________________________

       [X = Y] >> P;)       

           

     (s-rule alll (T : term)

      

       let PX/T (replace X T P)

       PX/T, [all X P] >> Q;

       ________________________

       [all X P] >> Q;)

       

     (s-rule allr (T : term)

      

       if (= (occurrences T Hypotheses) 0)

       let PX/T (replace X T P)

       PX/T;

       ________________________

       [all X P];)

       

     (s-rule existsl (T : term)

      

       if (= (occurrences T Hypotheses) 0)

       let PX/T (replace X T P)

       PX/T, [exists X P] >> Q;

       ________________________

       [exists X P] >> Q;)

       

     (s-rule existsr (T : term)

      

       let PX/T (replace X T P)

       PX/T;

       ________________________

       [exists X P];)

       

     (s-rule =r ()

     

       ________

       [X = X];)

       

     (s-rule =l ()

     

      let PX/Y (replace X Y P) 

      [X = Y] >> PX/Y;

      ________________

      [X = Y] >> P;) 

The code is about 150 lines in total excluding the code for the side-conditions and the definition of FOL syntax.    Here it is being loaded into SP 30.  Note that the LL generates a whole bunch of 'logic' functions which are help functions generated to execute the the user spec.

(14+) (load "D:\Google Drive\Shen Professional\Shen\Logic\folrules.shen")

tactics#type : symbol

(fn logic.f7686) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn logic.f7685) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn hyp) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7689) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn vr1) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7690) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn vr2) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7692) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn logic.f7691) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn vl) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7695) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn &r) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7697) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn logic.f7696) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn &l) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7700) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn =>r) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7702) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn logic.f7701) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn =>l) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7705) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn <=>r) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7707) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((l

ist prop) * prop)) --> (list ((list prop) * prop))))))

(fn logic.f7706) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn <=>l) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7710) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn ~r) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7712) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn logic.f7711) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn ~l) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7715) : ((list prop) --> ((list prop) --> (prop --> ((list prop) -->

((list ((list prop) * prop)) --> (list ((list prop) * prop)))))))

(fn lemma) : (prop --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))

(fn logic.f7716) : ((list prop) --> ((list prop) --> (prop --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop)))))))

(fn lem) : (prop --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))

(fn logic.f7717) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn exp) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn remove-nth) : (number --> ((list A) --> (list A)))

(fn logic.f7718) : ((list prop) --> ((list prop) --> (number --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop)))))))

(fn thin) : (number --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))

(fn logic.f7719) : ((list prop) --> ((list prop) --> (number --> (number --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))))

(fn swap) : (number --> (number --> ((list ((list prop) * prop)) --> (list ((list prop) * prop)))))

(fn logic.f7720) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn =r) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7722) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn logic.f7721) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn =l) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7726) : ((list prop) --> ((list prop) --> (term --> ((list prop) -->

((list ((list prop) * prop)) --> (list ((list prop) * prop)))))))

(fn logic.f7725) : ((list prop) --> ((list prop) --> (term --> ((list prop) -->

((list ((list prop) * prop)) --> (list ((list prop) * prop)))))))

(fn alll) : (term --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))

(fn logic.f7729) : ((list prop) --> ((list prop) --> (term --> ((list prop) -->

((list ((list prop) * prop)) --> (list ((list prop) * prop)))))))

(fn allr) : (term --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))

(fn logic.f7731) : ((list prop) --> ((list prop) --> (term --> ((list prop) -->

((list ((list prop) * prop)) --> (list ((list prop) * prop)))))))

(fn logic.f7730) : ((list prop) --> ((list prop) --> (term --> ((list prop) -->

((list ((list prop) * prop)) --> (list ((list prop) * prop)))))))

(fn existsl) : (term --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))

(fn logic.f7734) : ((list prop) --> ((list prop) --> (term --> ((list prop) -->

((list ((list prop) * prop)) --> (list ((list prop) * prop)))))))

(fn existsr) : (term --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))

(fn logic.f7735) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn =r) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

(fn logic.f7737) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn logic.f7736) : ((list prop) --> ((list prop) --> ((list prop) --> ((list ((list prop) * prop)) --> (list ((list prop) * prop))))))

(fn =l) : ((list ((list prop) * prop)) --> (list ((list prop) * prop)))

run time: 1.0290002822875977 secs

typechecked in 51449 inferences

loaded : symbol

The Logic Lab will appear in SP 31 this summer, but the documentation will take a while longer. 

Mark