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.

#!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))

Unfortunately, the above conditional equation can not be reflected in term rewriting systems produced by the CafeOBJ processor, because the right hand side r(x,y) and the condition p(x,y,z) contain variables which is not contained in the left hand side l(x). One of the aim to introduce modules simulating deductions in LK is to use such a equation in verification in CafeOBJ.

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

The module SEQUENT declares a sort and a constructor of sequents for LK.

#!python
module SEQUENT
{
  imports
  {
    pr(SET/PROP)
  }
  signature
  {
    [ Sequent ]
    op _|-_ : Set/Prop Set/Prop -> Sequent
  }
}

SET/SEQUENT

This module is an instantiation of SET with SEQUENT. It is used to declare ond manipulate sets of sequents.

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

INFERENCE

he module INFERENCE declares a sort representing inferences between sequents. Let i be a term of Inference. Then antecedent(i) and consequent(i) represent a source sequents of i and a target sequents of i, respectively. An inference i is called proper if antecedent(i) can be rewritten to consequent(i).

#!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) .
  }
}

DEDUCIBLE

The module DEDUCIBLE includes rules defined in LK which can not be described as rewriting rules of CafeOBJ. A set of sequents s is called deducible if there exists some proper inference i such that s = consequent(i) 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 .
    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) .
  }
}

PROVABLE

A proposition p is called 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
    eq provable(P) = deducible(nil |- P) .
  }
}

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) .
  }
}

LK

The module LK can be declared as a sum of the module DEDUCIBLE and the module RULE.

#!python
make LK
(
    DEDUCIBLE
  + RULE
)

COROLLARY1/RULE

For any propositions X, Y and Z, the sequent (X,Y├ Z) can be rewritten to the sequent (├ ((X ∧ Y) ⇒ Z)) in the module RULE.

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

SCORE/COROLLARY1/RULE

The proof score of the above corollary is very simple.

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

The result of the above score is:

#!python
-- 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)

COROLLARY1/LK

In LK, the sequent (├ ((X ∧ Y) ⇒ Z)) is deducible if the sequent (X,Y├ Z) is deducible, for any propositions X, Y and Z.

#!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 .
  }
}

SCORE/COROLLARY1/LK

The proof score of the above corollary is:

#!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 execution of the above score is:

#!python
-- 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)

DISTRIBUTIVE

This module declares distributive laws for disjunction and conjunction.

#!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 .
  }
}