(* SSL.thy Logical Introduction Rules for Substructural Logics Gore, Substructural Logics on Display *) SSL = SSS + consts ext0 :: "formula" ("F") ext1 :: "formula" ("T") int0 :: "formula" ("0") int1 :: "formula" ("1") (* Logical Connectives *) intt :: "[formula, formula] => formula" ("_ x _" [68,68] 67) extt :: "[formula, formula] => formula" ("_ & _" [68,68] 67) intp :: "[formula, formula] => formula" ("_ + _" [64,64] 63) extp :: "[formula, formula] => formula" ("_ v _" [64,64] 63) larr :: "[formula, formula] => formula" ("_ <- _" [62,62] 61) rarr :: "[formula, formula] => formula" ("_ -> _" [62,61] 61) butnot :: "[formula, formula] => formula" ("_ -< _" [62,62] 61) notbut :: "[formula, formula] => formula" ("_ >- _" [62,62] 61) (* s9 *) nor :: "[formula, formula] => formula" ("_ <~> _" [62,62] 61) nand :: "[formula, formula] => formula" ("_ >~< _" [62,62] 61) (* Explicit negations, s7, Fig 5 *) "negz" :: "formula => formula" ("_:0" [70] 70) "negw" :: "formula => formula" ("_:1" [70] 70) "zneg" :: "formula => formula" ("0:_" [71] 71) "wneg" :: "formula => formula" ("1:_" [71] 71) (* Modalities, s10, Fig 7 *) "wbx" :: "formula => formula" ("wbx _" [71] 71) "wdm" :: "formula => formula" ("wdm _" [71] 71) "bbx" :: "formula => formula" ("bbx _" [71] 71) "bdm" :: "formula => formula" ("bdm _" [71] 71) rules (* Logical Introduction rules, s2.2, Fig 2 *) tA "$I |- $X ==> T |- $X" tS "$I |- T" fA "F |- $I" fS "$X |- $I ==> $X |- F" r1A "$phi |- $X ==> 1 |- $X" r1S "$phi |- 1" r0A "0 |- $phi" r0S "$X |- $phi ==> $X |- 0" timesA "A, B |- $X ==> A x B |- $X" timesS "[| $X |- A ; $Y |- B |] ==> $X, $Y |- A x B" plusA "[| A |- $X ; B |- $Y |] ==> A + B |- $X, $Y" plusS "$X |- A, B ==> $X |- A + B" andal "A |- $X ==> A & B |- $X" andar "B |- $X ==> A & B |- $X" ands "[| $Z |- A ; $Z |- B |] ==> $Z |- A & B" ora "[| A |- $Z ; B |- $Z |] ==> A v B |- $Z" orsl "$X |- A ==> $X |- A v B" orsr "$X |- B ==> $X |- A v B" larrA "[| A |- $X ; $Y |- B |] ==> A <- B |- $X < $Y" larrS "$X |- A < B ==> $X |- A <- B" rarrA "[| $X |- A ; B |- $Y |] ==> A -> B |- $X > $Y" rarrS "$X |- A > B ==> $X |- A -> B" butnotA "A < B |- $X ==> A -< B |- $X" butnotS "[| $X |- A ; B |- $Y |] ==> $X < $Y |- A -< B" notbutA "A > B |- $X ==> A >- B |- $X" notbutS "[| A |- $X ; $Y |- B |] ==> $X > $Y |- A >- B" (* s9 *) norA "A -- B |- $X ==> A <~> B |- $X" nandS "$X |- A -- B ==> $X |- A >~< B" nandA "[| $X |- A ; $Y |- B |] ==> A >~< B |- $X -- $Y" norS "[| A |- $X ; B |- $Y |] ==> $X -- $Y |- A <~> B" (* Explicit negations, s7, Fig 5 *) znegA "$Z |- A ==> 0:A |- b $Z" negzA "$Z |- A ==> A:0 |- # $Z" wnegA "(b A |- $Z) ==> 1:A |- $Z" negwA "(# A |- $Z) ==> A:1 |- $Z" znegS "$Z |- b A ==> $Z |- 0:A" negzS "$Z |- # A ==> $Z |- A:0" wnegS "A |- $Z ==> b $Z |- 1:A" negwS "A |- $Z ==> # $Z |- A:1" (* Modalities, s9, Fig 6 *) wbxA "A |- $Z ==> wbx A |- @ $Z" bbxA "A |- $Z ==> bbx A |- o $Z" wbxS "$Z |- @ A ==> $Z |- wbx A" bbxS "$Z |- o A ==> $Z |- bbx A" wdmA "(o A |- $Z) ==> wdm A |- $Z" bdmA "(@ A |- $Z) ==> bdm A |- $Z" wdmS "$Z |- A ==> o $Z |- wdm A" bdmS "$Z |- A ==> @ $Z |- bdm A" end