dd1ccae Merged Formalism and Classical Logic chapters teg authored Jun 30, 2009 1 \chapter{Propositional Classical Logic}\label{chapter:PropositionalClassicalLogic} beb7e3e Defined a formalism teg authored Apr 20, 2009 2 531eaf8 Informal comments teg authored Jul 26, 2009 3 The traditional formalism in deep inference is \emph{the calculus of structures} \cite{Gugl:06:A-System:kl}. ed87c95 Minor fixes teg authored Jul 24, 2009 4 9fd7aef Submitted teg authored Aug 6, 2009 5 The idea of a new formalism, named \emph{formalism A} based on the calculus of structures, but where derivations contain less bureaucracy, was proposed by Guglielmi in \cite{Gugl:04:Formalis:am}, and later Br\"{u}nnler and Lengrand developed a term calculus around these ideas \cite{BrunLeng:05:On-Two-F:jf}. fa2ca18 Defined inference rule instance teg authored Jun 21, 2009 6 b6eadfb Remove mention of bureaucracy teg authored Dec 10, 2009 7 In this chapter I define a formalism based on the ideas of formalism A and call it (as suggested by Fran\c{c}ois Lamarche) \emph{the functorial calculus}. The reason to introduce a new formalism is that it greatly simplifies the presentation of some of the more technical results in this thesis (in particular Section~\vref{subsection:ThresholdFormulae}). 280d92f Informal text teg authored Jul 25, 2009 8 9 After presenting the functorial calculus we compare it briefly with the calculus of structures before we introduce the standard deductive system for classical logic in deep inference and show some preliminary results. 10 11 We now define formulae' and inference rules', which are in common between both the functorial calculus and the calculus of structures. Definitions~\vrefrange{definition:Formula}{definition:InferenceRuleInstance} are based on definitions given in \cite{BrusGugl:07:On-the-P:fk}. The focus of this thesis is classical propositional logic, and the following definitions reflect this. However, it is worth noting that the definitions can be generalised to other units and connectives, if one wants to present other logics. f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 12 8e3c317 Added informal text and minor cleanups teg authored Jul 21, 2009 13 %--------------------------- 0675709 TODO's teg authored Jun 22, 2009 14 \newcommand{\fff}{\mathsf f} 15 \newcommand{\ttt}{\mathsf t} 16 \newcommand{\size}[1]{{\left\vert #1\right\vert}}\vlupdate\size fa2ca18 Defined inference rule instance teg authored Jun 21, 2009 17 \begin{definition}\label{definition:Formula} 8c3033c Added index teg authored Jul 19, 2009 18 We define a set of \emph{formulae}\index{formulae}, denoted by $\alpha$, $\beta$, $\gamma$, $\delta$ to be: fa2ca18 Defined inference rule instance teg authored Jun 21, 2009 19 \begin{itemize} f43d5b2 Minor fixes teg authored Jul 21, 2009 20 \item \emph{atoms}, denoted by $a$, $b$, $c$, $d$ and $\bar a$, $\bar b$, $\bar c$, $\bar d$; 21 \item \emph{formula variables}, denoted by $A$, $B$, $C$, $D$; 22 \item \emph{units} $\fff$ (false) and $\ttt$ (true); and 23 \item the \emph{disjunction} and \emph{conjunction} of formulae $\alpha$ and $\beta$, denoted by $\vlsbr[\alpha.\beta]$ and $\vlsbr(\alpha.\beta)$, respectively. fa2ca18 Defined inference rule instance teg authored Jun 21, 2009 24 \end{itemize} 8c3033c Added index teg authored Jul 19, 2009 25 A formula is \emph{ground}\index{formula!ground} if it contains no variables. We usually omit external brackets of formulae, and sometimes we omit dispensable brackets under associativity. We use $\equiv$ to denote literal equality of formulae. The \emph{size}\index{formula!size} $\size\alpha$ of a formula $\alpha$ is the number of unit, atom and variable occurrences appearing in it. On the set of atoms there is an involution $\bar\cdot$, called \emph{negation}\index{atoms!negation} (\emph{i.e.}, $\bar\cdot$ is a bijection from the set of atoms to itself such that $\bar{\bar a}\equiv a$); we require that $\bar a\not\equiv a$ for every $a$; when both $a$ and $\bar a$ appear in a formula, we mean that atom $a$ is mapped to by $\bar a$ by $\bar\cdot$. A \emph{context}\index{formula!context} is a formula where one \emph{hole}\index{hole} $\vlhole$ appears in the place of a subformula; for example, $\vls[a.(b.\vlhole)]$ is a context; the generic context is denoted by $\xi\vlhole$. The hole can be filled with formulae; for example, if $\xi\vlhole\equiv\vls(b.[\vlhole.c])$, then $\xi\{a\}\equiv\vls(b.[a.c])$, $\xi\{b\}\equiv\vls(b.[b.c])$ and $\xi\{\vls(a.b)\}\equiv\vls(b.[(a.b).c])$. The \emph{size}\index{formula!context!size} of $\xi\vlhole$ is defined as $\size{\xi\vlhole}=\size{\xi\{a\}}-1$. fa2ca18 Defined inference rule instance teg authored Jun 21, 2009 26 \end{definition} 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 27 %--------------- fa2ca18 Defined inference rule instance teg authored Jun 21, 2009 28 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 29 %-------------------------------------------------------- fa2ca18 Defined inference rule instance teg authored Jun 21, 2009 30 \begin{definition}\label{definition:RenamingSubstitution} 8c3033c Added index teg authored Jul 19, 2009 31 A \emph{renaming}\index{atoms!renaming} is a map from the set of atoms to itself, and it is denoted by $\{a_1/b_1,a_2/b_2,\dots\}$. A renaming of $\alpha$ by $\{a_1/b_1,a_2/b_2,\dots\}$ is indicated by $\alpha\{a_1/b_1,a_2/b_2,\dots\}$ and is obtained by simultaneously substituting every occurrence of $a_i$ in $\alpha$ by $b_i$ and every occurrence of $\bar a_i$ by $\bar b_i$; for example, if $\alpha\equiv\vls(a.[b.(a.[\bar a.c])])$ then $\alpha\{a/\bar b,\bar b/c\}\equiv\vls(\bar b.[\bar c.(\bar b.[b.c])])$. A \emph{substitution}\index{substitution} is a map from the set of formula variables to the set of formulae, denoted by $\{A_1/\beta_1,A_2/\beta_2,\dots\}$. An \emph{instance}\index{formula!instance} of $\alpha$ by $\{A_1/\beta_1,A_2/\beta_2,\dots\}$ is indicated by $\alpha\{A_1/\beta_1,A_2/\beta_2,\dots\}$ and is obtained by simultaneously substituting every occurrence of variable $A_i$ in $\alpha$ by formula $\beta_i$; for example if $\alpha\equiv\vls[A.(b.c)]$ then $\alpha\{A/\vlsbr(c.\bar b)\}\equiv\vls[(c.\bar b).(b.c)]$. fa2ca18 Defined inference rule instance teg authored Jun 21, 2009 32 \end{definition} 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 33 %--------------- fa2ca18 Defined inference rule instance teg authored Jun 21, 2009 34 02b68f1 Allow substitution on atom occurrences teg authored Jul 22, 2009 35 \begin{convention} 36 By the above definition, formula variables will only be used to define inference rules, and will never appear in derivations. However, when we perform normalisation we will sometimes single out atom occurrences (by decorating them) and substitute on them as if they were formula variables. 37 \end{convention} 0b6498c Minor fixes teg authored Jun 29, 2009 38 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 39 %--------------------------------------------------------- e3571b7 Added labels and minor fixes teg authored Jun 13, 2009 40 \begin{definition}\label{definition:InferenceRuleInstance} 8c3033c Added index teg authored Jul 19, 2009 41 An \emph{inference rule}\index{inference rule} $\rho$ is an expression $\vlinf{\rho}{}{\beta}{\alpha}$, where the formulae $\alpha$ and $\beta$ are called \emph{premiss}\index{inference rule!premiss} and \emph{conclusion}\index{inference rule!conclusion}, respectively. A (\emph{deductive}) \emph{system}\index{system} is a finite set of inference rules. An \emph{inference rule instance}\index{inference rule!instance} $\vlinf{\rho}{}{\delta}{\gamma}$ of $\vlinf{\rho}{}{\beta}{\alpha}$ is such that $\gamma$ and $\delta$ are ground, and $\gamma\equiv\alpha\{a_1/b_1,a_2/b_2,\dots\}\{A_1/\beta_1,A_2/\beta_2,\dots\}$ and $\delta\equiv\beta\{a_1/b_1,a_2/b_2,\dots\}\{A_1/\beta_1,A_2/\beta_2,\dots\}$, for some renaming $\{a_1/b_1,a_2/b_2,\dots\}$ and substiution $\{A_1/\beta_1,A_2/\beta_2,\dots\}$. 7d910ed Defined inference rule and changed notation of composition of derivat… teg authored Apr 21, 2009 42 \end{definition} 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 43 %--------------- 44 45 %================================================================== 46 \section{The Functorial Calculus}\label{section:FunctorialCalculus} 7d910ed Defined inference rule and changed notation of composition of derivat… teg authored Apr 21, 2009 47 280d92f Informal text teg authored Jul 25, 2009 48 We now present the functorial calculus in the context of classical propositional logic and give some basic results. 49 be3798e Informal comments teg authored Jul 19, 2009 50 The intuition behind derivations in the functorial calculus is that we can compose derivations by the same connectives we can compose formulae. 51 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 52 %---------------------------------------------- e3571b7 Added labels and minor fixes teg authored Jun 13, 2009 53 \begin{definition}\label{definition:Derivation} 8c3033c Added index teg authored Jul 19, 2009 54 Given a deductive system $\mathcal S$, and formulae $\alpha$ and $\beta$; a (\emph{functorial calculus}) \emph{derivation $\Psi$ in $\mathcal S$ from $\alpha$ to $\beta$}\index{derivation!functorial calculus}, denoted $\vlder{\Psi}{\mathcal{S}}{\beta}{\alpha}$, is defined to be beb7e3e Defined a formalism teg authored Apr 20, 2009 55 \begin{enumerate} 0b6498c Minor fixes teg authored Jun 29, 2009 56 \item\label{definition:Derivation:item:Formula} a formula: $\Psi\;=\;\alpha\equiv\beta$; ebcb22a Added TODO's teg authored May 17, 2009 57 8c3033c Added index teg authored Jul 19, 2009 58 \item\label{definition:Derivation:item:Vertical} a \emph{vertical composition}\index{derivation!functorial calculus!vertical composition}: beb7e3e Defined a formalism teg authored Apr 20, 2009 59 $0b6498c Minor fixes teg authored Jun 29, 2009 60 \Psi\;=\; d8f02e0 Defined size of derivations and minor fixes teg authored Jun 22, 2009 61 \vlderivation 2133672 Remarked associativity of vertical composition of derivations teg authored Jun 21, 2009 62 { d8f02e0 Defined size of derivations and minor fixes teg authored Jun 22, 2009 63 \vlde{\Phi_2}{} 2133672 Remarked associativity of vertical composition of derivations teg authored Jun 21, 2009 64 { d8f02e0 Defined size of derivations and minor fixes teg authored Jun 22, 2009 65 \beta 2133672 Remarked associativity of vertical composition of derivations teg authored Jun 21, 2009 66 } 67 { d8f02e0 Defined size of derivations and minor fixes teg authored Jun 22, 2009 68 \vlin{\rho}{} 69 { 70 \alpha' 71 } 72 { 73 \vlde{\Phi_1}{} 74 { 75 \beta' 76 } 77 { 78 \vlhy 79 { 80 \alpha 81 } 82 } 83 } 2133672 Remarked associativity of vertical composition of derivations teg authored Jun 21, 2009 84 } 85 } 86 \quad, beb7e3e Defined a formalism teg authored Apr 20, 2009 87$ 0b6498c Minor fixes teg authored Jun 29, 2009 88 where $\vlinf{\rho}{}{\alpha'}{\beta'}$ is an instance of an inference rule from $\mathcal{S}$, and $\vlder{\Phi_1}{\mathcal S}{\beta'}{\alpha}$ and $\vlder{\Phi_2}{\mathcal S}{\beta}{\alpha'}$ are derivations; or f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 89 8c3033c Added index teg authored Jul 19, 2009 90 \item\label{definition:Derivation:item:Horizontal} a \emph{horizontal composition}\index{derivation!functorial calculus!horizontal composition}: beb7e3e Defined a formalism teg authored Apr 20, 2009 91 $dd1ccae Merged Formalism and Classical Logic chapters teg authored Jun 30, 2009 92 \Psi\;=\; 93 \vls 94 ( d8f02e0 Defined size of derivations and minor fixes teg authored Jun 22, 2009 95 \vlder{\Phi_1}{}{\beta_1}{\alpha_1} dd1ccae Merged Formalism and Classical Logic chapters teg authored Jun 30, 2009 96 \;\;.\;\; 97 \vlder{\Phi_2}{}{\beta_2}{\alpha_2} 98 ) 99 \qquad\mbox{or}\qquad 100 \Psi\;=\; 101 \vls 102 [ 103 \vlder{\Phi_1}{}{\beta_1}{\alpha_1} 104 \;\;.\;\; 105 \vlder{\Phi_2}{}{\beta_2}{\alpha_2} b7b6849 Trailing whitespace teg authored Dec 10, 2009 106 ] d8f02e0 Defined size of derivations and minor fixes teg authored Jun 22, 2009 107 \quad, beb7e3e Defined a formalism teg authored Apr 20, 2009 108$ dd1ccae Merged Formalism and Classical Logic chapters teg authored Jun 30, 2009 109 where $\vlder{\Phi_1}{}{\beta_1}{\alpha_1}$ and $\vlder{\Phi_2}{}{\beta_2}{\alpha_2}$ are derivations, and $\alpha\equiv\vls[\alpha_1.\alpha_2]$ and $\beta\equiv\vls[\beta_1.\beta_2]$, or $\alpha\equiv\vls(\alpha_1.\alpha_2)$ and $\beta\equiv\vls(\beta_1.\beta_2)$, respectively. beb7e3e Defined a formalism teg authored Apr 20, 2009 110 \end{enumerate} 9fd7aef Submitted teg authored Aug 6, 2009 111 112 A derivation with premiss $\ttt$ is, from now on, called a \emph{proof}. 113 0b6498c Minor fixes teg authored Jun 29, 2009 114 The size of a derivation $\Psi$, denoted $\size{\Psi}$, is defined to be the sum of the size of the formulae appearing in $\Psi$. beb7e3e Defined a formalism teg authored Apr 20, 2009 115 \end{definition} 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 116 %--------------- beb7e3e Defined a formalism teg authored Apr 20, 2009 117 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 118 %------------------------------------------------------------- d846ecd Started using Notation and Convention macros teg authored Jul 19, 2009 119 \begin{convention}\label{convention:DerAssociativeComposition} 2133672 Remarked associativity of vertical composition of derivations teg authored Jun 21, 2009 120 Given derivations $\vlder{\Phi_1}{}{\beta_1}{\alpha_1}$, $\vlder{\Phi_2}{}{\beta_2}{\alpha_2}$ and $\vlder{\Phi_3}{}{\beta_3}{\alpha_3}$, and inference rule instances $\vlinf{\rho_1}{}{\alpha_2}{\beta_1}$ and $\vlinf{\rho_2}{}{\alpha_3}{\beta_2}$ we consider 121 $122 \vlinf{\rho_2}{} 123 { 124 \vlder{\Phi_3}{} 125 { 126 \beta_3 127 } 128 { 129 \alpha_3 130 } 131 } 132 { 133 \left( 134 \vlinf{\rho_1}{} 135 { 136 \vlder{\Phi_2}{} 137 { 138 \beta_2 139 } 140 { 141 \alpha_2 142 } 143 } 144 { 145 \vlder{\Phi_1}{} 146 { 147 \beta_1 148 } 149 { 150 \alpha_1 151 } 152 } 153 \right) 154 } 65497be Minor fixes teg authored Jul 19, 2009 155 \qquad\mbox{and}\qquad 2133672 Remarked associativity of vertical composition of derivations teg authored Jun 21, 2009 156 \vlinf{\rho_1}{} 157 { 158 \left( 159 \vlinf{\rho_2}{} 160 { 161 \vlder{\Phi_3}{} 162 { 163 \beta_3 164 } 165 { 166 \alpha_3 167 } 168 } 169 { 170 \vlder{\Phi_2}{} 171 { 172 \beta_2 173 } 174 { 175 \alpha_2 176 } 177 } 178 \right) 179 } 180 { 181 \vlder{\Phi_1}{} 182 { 183 \beta_1 184 } 185 { 186 \alpha_1 187 } 188 } 189$ 0b6498c Minor fixes teg authored Jun 29, 2009 190 to be equal, and we denote them both by 2133672 Remarked associativity of vertical composition of derivations teg authored Jun 21, 2009 191 $192 \vlderivation 193 { 194 \vlde{\Phi_3}{} 195 { 196 \beta_3 197 } 198 { 199 \vlin{\rho_2}{} 200 { 201 \alpha_3 202 } 203 { 204 \vlde{\Phi_2}{} 205 { 206 \beta_2 207 } 208 { 209 \vlin{\rho_1}{} 210 { 211 \alpha_2 212 } 213 { 214 \vlde{\Phi_1}{} 215 { 216 \beta_1 217 } 218 { 219 \vlhy 220 { 221 \alpha_1 222 } 223 } 224 } 225 } 226 } 227 } 228 } 229 \quad. 230$ d846ecd Started using Notation and Convention macros teg authored Jul 19, 2009 231 \end{convention} 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 232 %--------------- ebcb22a Added TODO's teg authored May 17, 2009 233 cc7c8e8 Why not automatic normal form of derivation? teg authored Dec 16, 2009 234 %---------------------------------------------------- 235 \begin{remark}\label{remark:NoNeedAssocOfComposition} 236 If desireable, Convention~\vref{convention:DerAssociativeComposition} could be made redundant by forcing associativity of horizontal composition in Definition~\vref{definition:Derivation}. The only reason we did not do this was for the sake of brevity of the following results. 237 \end{remark} 238 %----------- 239 240 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 241 %-------------------------------------- f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 242 \begin{lemma}\label{lemma:DerInContext} 0b6498c Minor fixes teg authored Jun 29, 2009 243 Given a derivation $\vlder{\Phi}{}{\beta}{\alpha}$ and a context $\xi\vlhole$, a derivation $\vlder{\Psi}{}{\xi\{\beta\}}{\xi\{\alpha\}}$, with size $\size{\Phi}+\size{\xi\vlhole}$, can be constructed. f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 244 \end{lemma} 245 246 \begin{proof} 247 We proceed by structural induction on $\xi\vlhole$. The base case, $\xi\vlhole\equiv\vlhole$, is trivial. 248 For the inductive case, let 249 $a6481b2 Fixed proof of context closure teg authored Jul 19, 2009 250 \xi\vlhole\equiv\vls(\xi'\vlhole.\gamma)\quad,\qquad\xi\vlhole\equiv\vls(\gamma.\xi'\vlhole)\quad, f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 251$ a6481b2 Fixed proof of context closure teg authored Jul 19, 2009 252 $253 \xi\vlhole\equiv\vls[\xi'\vlhole.\gamma]\qquad\mbox{or}\qquad\xi\vlhole\equiv\vls[\gamma.\xi'\vlhole]\quad. 254$ 255 for some formula $\gamma$ and a context $\xi'\vlhole$. By the inductive hypothesis we can construct the derivation $\vlder{\Psi'}{}{\xi'\{\beta\}}{\xi'\{\alpha\}}$, so the result follows by case (\ref{definition:Derivation:item:Horizontal}) of Definition~\vref{definition:Derivation}. f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 256 \end{proof} 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 257 %---------- f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 258 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 259 %-------------------------------------------- d846ecd Started using Notation and Convention macros teg authored Jul 19, 2009 260 \begin{notation}\label{notation:DerInContext} 0b6498c Minor fixes teg authored Jun 29, 2009 261 Given a derivation $\vlder{\Phi}{}{\beta}{\alpha}$ and a context $\xi\vlhole$, the derivation $\vlder{}{}{\xi\{\beta\}}{\xi\{\alpha\}}$ constructed in the proof of Lemma~\vref{lemma:DerInContext} is denoted $\xi\{\Phi\}$. d846ecd Started using Notation and Convention macros teg authored Jul 19, 2009 262 \end{notation} 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 263 %------------- f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 264 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 265 %---------------------------------------- 5c798ba Use varioref and fix some references teg authored Jun 14, 2009 266 \begin{lemma}\label{lemma:DerComposition} f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 267 Given two derivations $\vlder{\Phi_1}{}{\beta}{\alpha}$ and $\vlder{\Phi_2}{}{\gamma}{\beta}$, a derivation $\vlder{\Psi}{}{\gamma}{\alpha}$, with size $\size{\Phi_1}+\size{\Phi_2}-\size{\beta}$, can be constructed. beb7e3e Defined a formalism teg authored Apr 20, 2009 268 \end{lemma} 269 8cf5447 Changed names of derivations and started sketch of proof of composition teg authored Apr 20, 2009 270 \begin{proof} dd1ccae Merged Formalism and Classical Logic chapters teg authored Jun 30, 2009 271 We argue by structural induction on $\Phi_1$ 8cf5447 Changed names of derivations and started sketch of proof of composition teg authored Apr 20, 2009 272 \begin{enumerate} 7d910ed Defined inference rule and changed notation of composition of derivat… teg authored Apr 21, 2009 273 dd1ccae Merged Formalism and Classical Logic chapters teg authored Jun 30, 2009 274 \item\label{proof:DerComposition:item:Formula} if $\Phi_1=\beta$ then $\Psi=\Phi_2$, with size $\size{\Phi_1}+\size{\Phi_2}-\size{\beta}$; 7d910ed Defined inference rule and changed notation of composition of derivat… teg authored Apr 21, 2009 275 dd1ccae Merged Formalism and Classical Logic chapters teg authored Jun 30, 2009 276 \item\label{proof:DerComposition:item:Vertical} if f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 277 $278 \Phi_1\;=\; d8f02e0 Defined size of derivations and minor fixes teg authored Jun 22, 2009 279 \vlderivation 280 { 281 \vlde{\Phi''_1}{} 282 { 283 \beta 284 } 285 { 286 \vlin{\rho}{} 287 { 288 \alpha' 289 } 290 { 291 \vlde{\Phi'_1}{} 292 { 293 \beta' 294 } 295 { 296 \vlhy 297 { 298 \alpha 299 } 300 } 301 } 302 } 303 }\quad, f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 304$ 305 then, by the inductive hypothesis, we can construct $\vlder{\Psi'}{}{\gamma}{\alpha'}$, with size $\size{\Phi''_1}+\size{\Phi_2}-\size{\beta}$, we can then build 306 $307 \Psi\;=\; d8f02e0 Defined size of derivations and minor fixes teg authored Jun 22, 2009 308 \vlderivation 309 { 310 \vlde{\Psi'}{} 311 { 312 \gamma 313 } 314 { 315 \vlin{\rho}{} 316 { 317 \alpha' 318 } 319 { 320 \vlde{\Phi'_1}{} 321 { 322 \beta' 323 } 324 { 325 \vlhy 326 { 327 \alpha 328 } 329 } 330 } 331 } 332 }\quad, f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 333$ 334 with size $\size{\Phi'_1}+\size{\Psi'}=\size{\Phi'_1}+\size{\Phi''_1}+\size{\Phi_2}-\size{\beta}=\size{\Phi_1}+\size{\Phi_2}-\size{\beta}$; 7d910ed Defined inference rule and changed notation of composition of derivat… teg authored Apr 21, 2009 335 b7b6849 Trailing whitespace teg authored Dec 10, 2009 336 \item if f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 337 $338 \Phi_1\;=\; dd1ccae Merged Formalism and Classical Logic chapters teg authored Jun 30, 2009 339 \vls[\vlder{\Phi_{1,1}}{}{\beta_1}{\alpha_1}\;\;.\;\;\vlder{\Phi_{1,2}}{}{\beta_2}{\alpha_2}] 340 \qquad\mbox{or}\qquad 341 \Phi_1\;=\; 342 \vls(\vlder{\Phi_{1,1}}{}{\beta_1}{\alpha_1}\;\;.\;\;\vlder{\Phi_{1,2}}{}{\beta_2}{\alpha_2}) f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 343$ dd1ccae Merged Formalism and Classical Logic chapters teg authored Jun 30, 2009 344 we argue by structural induction on $\Phi_2$: 345 \begin{enumerate} 346 \item if $\Phi_2$ is a formula (resp., a vertical composition), the result follow by a symmetric argument to case \ref{proof:DerComposition:item:Formula} (resp., \ref{proof:DerComposition:item:Vertical}) above. 347 \item if 348 $349 \Phi_2\;=\; 350 \vls[\vlder{\Phi_{2,1}}{}{\gamma_1}{\beta_1}\;\;.\;\;\vlder{\Phi_{2,2}}{}{\gamma_2}{\beta_2}] 351 \qquad\mbox{or}\qquad 352 \Phi_2\;=\; 353 \vls(\vlder{\Phi_{2,1}}{}{\gamma_1}{\beta_1}\;\;.\;\;\vlder{\Phi_{2,2}}{}{\gamma_2}{\beta_2}) 354$ 355 then, by the first inductive hypothesis, we can construct 356 $357 \vlder{\Psi_1}{}{\gamma_1}{\alpha_1} 358 \qquad\mbox{and}\qquad 359 \vlder{\Psi_2}{}{\gamma_2}{\alpha_2}\quad, 360$ 361 with size $\size{\Phi_{1,1}}+\size{\Phi_{2,1}}-\size{\beta_1}$ and $\size{\Phi_{1,2}}+\size{\Phi_{2,2}}-\size{\beta_2}$, respectively, we can then build 362 $363 \Psi\;=\; 364 \vls[\vlder{\Psi_1}{}{\gamma_1}{\alpha_1}\;\;.\;\;\vlder{\Psi_2}{}{\gamma_2}{\alpha_2}] 365 \qquad\mbox{or}\qquad 366 \Psi\;=\; 367 \vls(\vlder{\Psi_1}{}{\gamma_1}{\alpha_1}\;\;.\;\;\vlder{\Psi_2}{}{\gamma_2}{\alpha_2}) 368$ 369 with size $\size{\Psi_1}+\size{\Psi_2}=\size{\Phi_{1,1}}+\size{\Phi_{1,2}}+\size{\Phi_{2,1}}+\size{\Phi_{2,2}}-(\size{\beta_1}+\size{\beta_2})=\size{\Phi_1}+\size{\Phi_2}-\size{\beta}$. 370 \end{enumerate} 8cf5447 Changed names of derivations and started sketch of proof of composition teg authored Apr 20, 2009 371 \end{enumerate} 372 \end{proof} 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 373 %---------- 8cf5447 Changed names of derivations and started sketch of proof of composition teg authored Apr 20, 2009 374 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 375 %---------------------------------------------- d846ecd Started using Notation and Convention macros teg authored Jul 19, 2009 376 \begin{notation}\label{notation:DerComposition} f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 377 Given derivations $\vlder{\Phi_1}{}{\beta}{\alpha}$ and $\vlder{\Phi_2}{}{\gamma}{\beta}$, the derivation $\vlder{\Psi}{}{\gamma}{\alpha}$ constructed in the proof of Lemma~\vref{lemma:DerComposition} is denoted: beb7e3e Defined a formalism teg authored Apr 20, 2009 378 $379 \vlderivation 380 { 8cf5447 Changed names of derivations and started sketch of proof of composition teg authored Apr 20, 2009 381 \vlde{\Phi_2}{}{\gamma} beb7e3e Defined a formalism teg authored Apr 20, 2009 382 { 8cf5447 Changed names of derivations and started sketch of proof of composition teg authored Apr 20, 2009 383 \vlde{\Phi_1}{}{\beta} beb7e3e Defined a formalism teg authored Apr 20, 2009 384 { 385 \vlhy{\alpha} 386 } 387 } 388 }\quad. 389$ d846ecd Started using Notation and Convention macros teg authored Jul 19, 2009 390 \end{notation} 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 391 %------------- beb7e3e Defined a formalism teg authored Apr 20, 2009 392 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 393 %======================================================================= dd1ccae Merged Formalism and Classical Logic chapters teg authored Jun 30, 2009 394 \section{The Calculus of Structures}\label{section:CalculusOfStructures} beb7e3e Defined a formalism teg authored Apr 20, 2009 395 b6d3376 Major search/cond-replace teg authored Nov 30, 2009 396 We now present the calculus of structures and in Theorem~\vref{theorem:CoSToFunc} and Theorem~\vref{theorem:FuncToCoS} we show that the functorial calculus and the calculus of structures polynomially simulate each other. 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 397 398 The intuition behind derivations in the calculus of structures is that we rewrite formulae by applying inference rules inside a context. be3798e Informal comments teg authored Jul 19, 2009 399 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 400 %--------------------------------------- eadb5e0 Defined CoS teg authored Jun 21, 2009 401 \begin{definition}\label{definition:CoS} 8c3033c Added index teg authored Jul 19, 2009 402 Given a deductive system $\mathcal S$, a set of formulae, $\mathcal F$, and $\alpha$ and $\beta$ from $\mathcal F$; a \emph{calculus of structures derivation $\Psi$ in $\mathcal S$ from $\alpha$ to $\beta$}\index{derivation!calculus of structures}, denoted $\vlder{\Psi}{\mathcal{S}}{\beta}{\alpha}$, is defined to be eadb5e0 Defined CoS teg authored Jun 21, 2009 403 \begin{enumerate} 0b6498c Minor fixes teg authored Jun 29, 2009 404 \item\label{definition:CoS:item:Formula} a formula: $\Psi\;=\;\alpha\equiv\beta$; or eadb5e0 Defined CoS teg authored Jun 21, 2009 405 8c3033c Added index teg authored Jul 19, 2009 406 \item\label{definition:CoS:item:Vertical} a \emph{vertical composition}\index{derivation!calculus of structures!vertical composition}: eadb5e0 Defined CoS teg authored Jun 21, 2009 407 $0b6498c Minor fixes teg authored Jun 29, 2009 408 \Psi\;=\; 409 \vlderivation eadb5e0 Defined CoS teg authored Jun 21, 2009 410 { 0b6498c Minor fixes teg authored Jun 29, 2009 411 \vlde{\Phi_2}{} eadb5e0 Defined CoS teg authored Jun 21, 2009 412 { d8f02e0 Defined size of derivations and minor fixes teg authored Jun 22, 2009 413 \beta eadb5e0 Defined CoS teg authored Jun 21, 2009 414 } 415 { 0b6498c Minor fixes teg authored Jun 29, 2009 416 \vlin{\rho}{} 417 { 418 \xi\{\alpha'\} 419 } 420 { 421 \vlde{\Phi_1}{} 422 { 423 \xi\{\beta'\} 424 } 425 { 426 \vlhy 427 { 428 \alpha 429 } 430 } 431 } eadb5e0 Defined CoS teg authored Jun 21, 2009 432 } 433 } 434 \quad, 435$ 0b6498c Minor fixes teg authored Jun 29, 2009 436 where $\vlinf{\rho}{}{\alpha'}{\beta'}$ is an instance of an inference rule from $\mathcal{S}$, and $\vlder{\Phi_1}{\mathcal S}{\xi\{\beta'\}}{\alpha}$ and $\vlder{\Phi_2}{\mathcal S}{\beta}{\xi\{\alpha'\}}$ are calculus of structures derivations. eadb5e0 Defined CoS teg authored Jun 21, 2009 437 \end{enumerate} 0b6498c Minor fixes teg authored Jun 29, 2009 438 The size of a calculus of structures derivation $\Psi$, denoted $\size{\Psi}$, is defined to be the sum of the size of the formulae appearing in $\Psi$. ebcb22a Added TODO's teg authored May 17, 2009 439 \end{definition} 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 440 %--------------- c7a7e30 Made the section on threshold formulae compile teg authored May 15, 2009 441 8e3c317 Added informal text and minor cleanups teg authored Jul 20, 2009 442 %--------------------------------------- 443 \begin{theorem}\label{theorem:CoSToFunc} f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 444 A calculus of structures derivation $\vlder{\Phi}{}{\beta}{\alpha}$ can be transformed into a functorial calculus derivation $\vlder{\Psi}{}{\beta}{\alpha}$ such that $\size{\Psi}\le\size{\Phi}$. 9e79774 Added Theorems comparing Formalism A to CoS teg authored Apr 21, 2009 445 \end{theorem} 446 e3fd71c Started proof of equality between CoS and FC teg authored Jun 21, 2009 447 \begin{proof} f68726f Finished comparison with CoS and finished definition of FuC teg authored Jun 22, 2009 448 We argue by structural induction on $\Phi$. The base case is trivial; $\Phi=\alpha\equiv\beta=\Psi$. For the inductive case, consider the following calculus of structures derivation: 449 $450 \Phi\;=\; 451 \vlinf{\rho}{} 452 { 453 \vlder{\Phi_2}{} 454 { 455 \beta 456 } 457 { 458 \xi\{\alpha'\} 459 } 460 } 461 { 462 \vlder{\Phi_1}{} 463 { 464 \xi\{\beta'\} 465 } 466 { 467 \alpha 468 } 469 } 470 \quad. 471$ 0b6498c Minor fixes teg authored Jun 29, 2009 472 By the inductive hypothesis, there are functorial calculus derivations $\vlder{\Psi_1}{}{\xi\{\beta'\}}{\alpha}$ and $\vlder{\Psi_2}{}{\beta}{\xi\{\alpha'\}}$, such that $\size{\Psi_1}\le\size{\Phi_1}$ and $\size{\Psi_2}\le\size{\Phi_2}$. By Lemma~\vref{lemma:DerInContext}, there is a functorial calculus derivation $\xi\left\{\vlinf{\rho}{}{\alpha'}{\beta'}\right\}$, with size $\size{\xi\vlhole}+\size{\alpha'}+\size{\beta'}$. By Lemma~\vref{lemma:DerComposition}, we can combine the three functorial calculus derivations to create $\vlder{\Psi}{}{\beta}{\alpha}$, with size $\size{\Psi_1}+\size{\Psi_2}+\size{\xi\vlhole}+\size{\beta'}+\size{\alpha'}-\size{\xi\vlhole}-\size{\beta'}-\size{\xi\vlhole}-\size{\alpha'}=\size{\Psi_1}+\size{\Psi_2}-\size{\xi\vlhole}\le\size{\Phi_1}+\size{\Phi_2}=\size{\Phi}$. e3fd71c Started proof of equality between CoS and FC teg authored Jun 21, 2009 473 \end{proof} dcc67dd Proved translation from FuC to CoS teg authored Jul 21, 2009 474 %---------- 475 932e7b3 Added example of flows and derivations teg authored Jul 25, 2009 476 %-------------- 477 \begin{example} 478 Figure~\vref{figure:ExampleAtomicFlows} has three examples of calculus of structures derivations transformed into functorial calculus derivations. 479 \end{example} 480 %------------ 481 dcc67dd Proved translation from FuC to CoS teg authored Jul 20, 2009 482 %-------------------------------------- 483 \begin{lemma}\label{lemma:CoSDerInContext} 484 Given a calculus of structures derivation $\vlder{\Phi}{}{\beta}{\alpha}$ and a context $\xi\vlhole$, a calculus of structures derivation $\vlder{\Psi}{}{\xi\{\beta\}}{\xi\{\alpha\}}$ can be constructed, such that the number of inference rule instances in $\Psi$ is the same as the number of inference rule instances in $\Phi$, and the size of the largest formula in $\Psi$ is the sum of the largest formula in $\Phi$ and $\size{\xi\vlhole}$. 485 \end{lemma} 486 487 \begin{proof} 488 The statements follows by structural induction on $\Phi$. 489 \end{proof} 490 %---------- 491 492 %---------------------------------------- 493 \begin{lemma}\label{lemma:CoSDerComposition} 494 Given two calculus of structures derivations $\vlder{\Phi_1}{}{\beta}{\alpha}$ and $\vlder{\Phi_2}{}{\gamma}{\beta}$, a calculus of structures derivation $\vlupsmash{\vlder{\Psi}{}{\gamma}{\alpha}}$ can be constructed, such that the number of inference rule instances in $\Psi$ is the sum of the number of inference rule instances in $\Phi_1$ and $\Phi_2$ combined, and the largest formula in $\Psi$ is the largest formula of $\Phi_1$ or the largest formula of $\Phi_2$. 495 \end{lemma} 496 497 \begin{proof} 498 The statement follows by structural induction on $\Phi_1$. 499 \end{proof} 500 %---------- 501 502 %--------------------------------------- 503 \begin{theorem}\label{theorem:FuncToCoS} 504 A functorial calculus derivation $\vlder{\Phi}{}{\beta}{\alpha}$ can be transformed into a calculus of structures derivation $\vlder{\Psi}{}{\beta}{\alpha}$ such that the size of $\Psi$ depends at most quadratically on the size of $\Phi$. 505 \end{theorem} 506 507 \begin{proof} 508 We first show how to construct $\Psi$: The base cases, when $\Phi$ is a formula or a vertical composition, are trivial. For the inductive case, consider a conjunction of functorial calculus derivations (the argument for the disjunction is similar): 509 $510 \Phi\;=\; 511 \vls 512 ( 513 \vlder{\Phi_1}{}{\beta_1}{\alpha_1} 514 \;\;.\;\; 515 \vlder{\Phi_2}{}{\beta_2}{\alpha_2} 516 )\quad. 517$ b6d3376 Major search/cond-replace teg authored Nov 30, 2009 518 By the inductive hypothesis and Lemma~\vref{lemma:CoSDerInContext} there are calculus of structures derivations dcc67dd Proved translation from FuC to CoS teg authored Jul 20, 2009 519 $520 \vlder{\Psi_1}{}{\vls(\beta_1.\alpha_1)}{\vls(\alpha_1.\alpha_1)} 521 \qquad\mbox{and}\qquad 522 \vlder{\Psi_2}{}{\vls(\beta_1.\beta_2)}{\vls(\beta_1.\alpha_2)} 523 \quad, 524$ 525 and by Lemma~\ref{lemma:CoSDerComposition} there exists a calculus of structures derivation $\vlder{\Psi}{}{\vls(\beta_1.\beta_2)}{\vls(\alpha_1.\alpha_2)}$. 526 527 To find an upper bound on the size of $\Psi$, we observe that it depends at most linearly on the number of inference rule instances in $\Psi$ multiplied by the size of the largest formula in $\Psi$. Furthermore, by the above Lemmata, the number of inference rules in $\Psi$ is the same as the number of inference rules in $\Phi$ and the size of the largest inference rule depends at most linearly on the size of $\Phi$, so the size of $\Psi$ depends at most quadratically on the size of $\Phi$. 528 \end{proof} 529 %---------- 6e9a9e6 Moved summary of results about CoS teg authored Jul 28, 2009 530 531 The calculus of structures is now well developed for classical \cite{Brun:03:Atomic-C:oz,Brun:06:Cut-Elim:cq,Brun:06:Locality:zh,BrunTiu:01:A-Local-:mz,Brun:06:Deep-Inf:qy}, intuitionistic \cite{Tiu:06:A-Local-:gf}, linear \cite{Stra:02:A-Local-:ul,Stra:03:MELL-in-:oy}, modal \cite{Brun::Deep-Seq:ay,GoreTiu:06:Classica:uq,Stou:06:A-Deep-I:rt} and commutative/non-commutative logics \cite{Gugl:06:A-System:kl,Tiu:06:A-System:ai,Stra:03:Linear-L:lp,Brus:02:A-Purely:wd,Di-G:04:Structur:wy,GuglStra:01:Non-comm:rp,GuglStra:02:A-Non-co:lq,GuglStra:02:A-Non-co:dq,Kahr:06:Reducing:hc,Kahr:07:System-B:fk}. The basic proof complexity properties of the calculus of structures are known \cite{BrusGugl:07:On-the-P:fk}. The calculus of structures promoted the discovery of a new class of proof nets for classical and linear logic \cite{LamaStra:05:Construc:qq,LamaStra:05:Naming-P:ov,LamaStra:06:From-Pro:et,StraLama:04:On-Proof:ec} (see also \cite{Guir:06:The-Thre:qt}). There exist implementations in Maude of deep-inference proof systems \cite{Kahr:07:Maude-as:lr}.