Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / 02_SequentCalculus
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) .
#!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
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
#!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
#!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 . } }
Updated