Wiki

Sequent Calculus for Classical Logic

In this section, we introduce some modules to simulate deductions in LK, a system of sequent calculus for the first order classical predicate logic. One of the aim to introduce modules simulating LK is to represent conditional equations of CafeOBJ as a term to ease verifications in CafeOBJ.

#!python

    cq l(x) = r(x,y) if p(x,y,z)

Using modules introduced here, the above conditional equation is represented by the following term.

#!python

    p(x,y,z) |- (l(x) = r(x,y))

SET of PROPs

The module SET/PROP is to represent and manipulate a set of propositions. This module is an instantiation of the parameterized module SET with PROP.

#!python
make SET/PROP
(
  SET(
    PROP { sort Elt -> Prop }
  ) * {
    sort Set -> Set/Prop
  }
)

SEQUENT and SET of SEQUENTs

The module SEQUENT declares a sort of sequents for LK.

#!python

module SEQUENT
{
  imports
  {
    pr(SET/PROP)
  }
  signature
  {
    [ Sequent ]
    op _|-_ : Set/Prop Set/Prop -> Sequent
  }
  axioms
  {
    vars P : Prop
    vars L R : Set/Prop
--  eq true,L |- R = L |- R .
--  eq L |- R,false = L |- R .
--  eq false,L |- R = false |- R .
--  eq L |- R,true = L |- true .
  }
}

The module SEQUENTS declares a sort of sets of sequents． This module is an instantiation of SET with SEQUENT.

#!python

make SET/SEQUENT
(
  SET(
    SEQUENT { sort Elt -> Sequent }
  ) * {
    sort Set -> Set/Sequent
  }
)

INFERENCE

The module INFERENCE represents deductive inference between sequents.

#!python
module INFERENCE
{
  imports
  {
    pr(SET/SEQUENT)
    pr(RWL)
  }
  signature
  {
    [ Inference ]
    op antecedent : Inference -> Set/Sequent
    op consequent : Inference -> Set/Sequent
    op proper : Inference -> Prop
  }
  axioms
  {
    vars I : Inference
    cq proper(I) = true
       if antecedent(I) ==> consequent(I) .
  }
}

The operation antecedent represents sequents which are used as an premise of a given inference, and the operation consequent represents sequents which are obtained through a given inference. In this module, an inference I is called proper, if consequent(I) is rewritten from antecedent(I).

DEDUCIBLE

The module DEDUCIBLE includes deduction rules defined in LK which can not be described as rewriting rules of CafeOBJ, including weakening rule. In this module, consequent(i) is called deducible if i is proper and antecedent(i) is deducible.

#!python

module DEDUCIBLE
{
  imports
  {
    pr(INFERENCE)
  }
  signature
  {
    op deducible : Set/Sequent -> Prop
  }
  axioms
  {
    vars P Q : Prop
    vars L R : Set/Prop
    vars S T : Set/Sequent
    vars I : Inference
    cq deducible(consequent(I)) = true
       if (proper(I) = true) /\ (deducible(antecedent(I)) = true) .
    eq deducible(nil |- nil) = false .
--  cq deducible(L |- P) = true
--     if (P = true) .
--  cq deducible(P |- R) = true
--     if (P = false) .
    eq deducible(L |- true,R) = true .
    eq deducible(false,L |- R) = true .
    eq deducible(P,L |- R,P) = true .
    cq deducible(L |- R,P) = true
       if deducible(L |- R) = true .
    cq deducible(L,P |- R) = true
       if deducible(L |- R) = true .
    eq deducible(nil) = true .
    eq deducible(S,T) = deducible(S) /\ deducible(T) .
  }
}

A set of sequents S is called deducible if S is derived from some proper inference I whose premise antecedent(I) is also deducible.

PROVABLE

The module PROVABLE is used to decide if a given proposition P can be deduced from axioms or not. In this module, a proposition P is provable if and only if the sequent (nil |- P) is deducible.

#!python

module PROVABLE
{
  imports
  {
    pr(DEDUCIBLE)
  }
  signature {
    op provable : Prop -> Prop
  }
  axioms
  {
    vars P : Prop
    vars S : Set/Sequent
--  cq provable(P) = true
--     if P == true .
    eq provable(P) = deducible(nil |- P) .
--  cq provable(P) = true
--     if deducible(nil |- P) ==> true .
  }
}

RULE

The module RULE declares deductive rules which can be represented as rewriting rules of CafeOBJ.

#!python
module RULE
{
  imports
  {
    pr(SET/SEQUENT)
  }
  axioms
  {
    vars P Q : Prop
    vars L R : Set/Prop
    vars S T : Set/Prop
-- cut
    rl (L,P |- R),(S |- P,T) => L,S |- R,T .
-- right introduction of negation
    rl L,P |- R => L |- (neg P),R .
-- right introduction of conjunction
    rl (L |- P,R),(S |- Q,T) => L,S |- (P /\ Q),R,T .
-- right introduction of disjunction
    rl L |- P,Q,R => L |- (P \/ Q),R .
-- right introduction of implication
    rl L,P |- Q,R => L |- (P => Q),R .
-- right elimination of implication
    rl L |- (P => Q),R => L,P |- Q,R .
-- left introduction of negation
    rl L |- P,R => L,(neg P) |- R .
-- left introduction of conjunction
    rl L,P,Q |- R => L,(P /\ Q) |- R .
-- left introduction of disjunction
    rl (L,P |- R),(S,Q |- T) => L,S,(P \/ Q) |- R,T .
-- left introduction of implication
    rl (L |- P,R),(S,Q |- T) => L,S,(P => Q) |- R,T .
-- substitution
    crl L,P |- R => L,Q |- R
        if (P = Q) .
-- substitution
    crl L |- P,R => L |- Q,R
        if (P = Q) .
  }
}

COROLLARY1 for RULE

Let p,q and r be arbitrary proposisions. Then, a sequent (p,q |- r) can be rewritten to (nili |- ((p /\ q) => r)).

#!python
open RULE .
ops p q r : -> Prop .
red (p,q |- r) ==> (nil |- ((p /\ q) => r)) .
close

The result of the above proof score is:

#!python
-- opening module RULE.. done.
%RULE> %RULE> _*
-- reduce in %RULE : (((p , q) |- r) ==> (nil |- ((p /\ q) => r))):Bool

** Found [state 17] (nil |- ((q /\ p) => r)):Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 47 rewrites(0.020 sec), 732 matches, 17 memo hits)

#!python
module COROLLARY1/RULE
{
  imports
  {
    pr(RULE)
  }
  axioms
    {
    vars X Y Z : Prop
    rl (X,Y |- Z) => (nil |- ((X /\ Y) => Z)) .
  }
}

LK

The module LK can be declared as a sum of the module DEDUCIBLE and the module RULE. Please notice that only a subset of deduction rules in LK is declared in the following module.

#!python

make LK
(
  DEDUCIBLE + RULE
)

Corollary1 for LK

Let p,q and r be arbitrary proposisions. Then, if a sequent (p,q |- r) can be deducible, a sequent (nili |- ((p /\ q) => r)) is also deducible.

#!python
open LK + COROLLARY1/RULE .
ops p q r : -> Prop .
ops i : -> Inference .
eq antecedent(i) = (p,q |- r) .
eq (nil |- ((p /\ q) => r)) = consequent(i) .
eq deducible(p,q |- r) = true .
red deducible(nil |- ((p /\ q) => r)) .
close

The result of the above proof score is:

#!python
-- opening module LK + COROLLARY1/RULE.. done.
%LK + COROLLARY1/RULE> %LK + COROLLARY1/RULE> %LK + COROLLARY1/RULE> _
%LK + COROLLARY1/RULE> %LK + COROLLARY1/RULE> %LK + COROLLARY1/RULE> *
-- reduce in %LK + COROLLARY1/RULE : (deducible((nil |- ((p /\ q) => r)))):Prop

** Found [state 7] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 23 rewrites(0.010 sec), 215 matches, 2 memo hits)

Now, we can declare the following module.

#!python
module COROLLARY1/LK
{
  imports
  {
    pr(LK)
  }
  axioms
    {
    vars X Y Z : Prop
    cq deducible(nil |- ((X /\ Y) => Z)) = true
       if deducible(X,Y |- Z) = true .
  }
}

Distributive Laws on Conjunction and Disjunction defined in PROP

The following desutibutive laws can not be declared in the module PROP, because they might cause infinite reduction.

So, we decide to declare these laws as sequents as follows.

#!python
module DISTRIBUTIVE
{
  imports
  {
    pr(DEDUCIBLE)
  }
  axioms
  {
    vars P Q R : Prop
    eq deducible(((P /\ Q) \/ R) |- ((P \/ R) /\ (Q \/ R))) = true .
    eq deducible(((P \/ Q) /\ R) |- ((P /\ R) \/ (Q /\ R))) = true .
    eq deducible(((P \/ R) /\ (Q \/ R)) |- ((P /\ Q) \/ R)) = true .
    eq deducible(((P /\ R) \/ (Q /\ R)) |- ((P \/ Q) /\ R)) = true .
  }
}