Project topics and materials
Get Complete Project Material File(s) Now! »
Propositional Classical Logic
The traditional formalism in deep inference is the calculus of structures [Gug07].
The idea of a new formalism, named formalism A based on the calculus of structures, but where derivations contain less bureaucracy, was proposed by Guglielmi in [Gug04], and later Brünnler and Lengrand developed a term calculus around these ideas [BL05].
In this chapter I define a formalism based on the ideas of formalism A and call it (as suggested by François Lamarche) the functorial calculus. The reason to introduce a new for-malism is that it greatly simplifies the presentation of some of the more technical results in this thesis (in particular Section 6.4.1 on page 65).
After presenting the functorial calculus we compare it briefly with the calculus of struc-tures before we introduce the standard deductive system for classical logic in deep inference and show some preliminary results.
We now define ‘formulae’ and ‘inference rules’, which are in common between both the functorial calculus and the calculus of structures. Definitions 2.0.1 to 2.0.4 on pages 6–7 are based on definitions given in [BG09]. 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.
Definition 2.0.1. We define a set of formulae, denoted by , , , to be: atoms, denoted by a, b , c, d and a, b , c, d ; formula variables, denoted by A, B, C , D; units f (false) and t (true); and the disjunction and conjunction of formulae and , denoted by [ _ ] and ( ^ ), respectively.
A formula is ground if it contains no variables. We usually omit external brackets of formulae, and sometimes we omit dispensable brackets under associativity. We use to denote literal equality of formulae. The size j j of a formula is the number of unit, atom and variable occurrences appearing in it. On the set of atoms there is an involution ¯, called negation (i.e., ¯ is a bijection from the set of atoms to itself such that a¯ a); we require that a¯ 6 a for every a; when both a and a¯ appear in a formula, we mean that atom a is mapped to by a¯ by ¯. A context is a formula where one hole f g appears in the place of a subformula; for example, a _ (b ^ f g) is a context; the generic context is denoted by f g. The hole can be filled with formulae; for example, if f g b ^ [f g _ c], then fag b ^ [a _ c], fb g b ^ [b _ c] and fa ^ b g b ^ [(a ^ b ) _ c]. The size of f g is defined as j f gj = j fagj 1.
Definition 2.0.2. A renaming is a map from the set of atoms to itself, and it is denoted by fa1=b1,* a2=b2, . . . g. A renaming of by fa1=b1, a2=b2, . . . g is indicated by fa1=b1, a2=b2, . . . g and is obtained by simultaneously substituting every occurrence of ai in by bi and ev- ¯ ; for example, if a ^ [b _ (a ^ [a¯_ c])] then ¯ ¯ =c ery occurrence of a¯i by bi f a=b , b g ¯ ¯ fA1= 1 A2= 2 g instance fA1 = 1 g of b ^ [b _ c] A2= 2 b ^ c¯ _ . A substitution is a map from the set of formula variables to the set formulae, denoted by , , . . . . An of by , ,… is indicated by fA1= 1, A2= 2 , . . . g and is obtained by simultaneously substituting every occur- c ^ b¯ _ (b ^ c). Ai i A _ (b ^ c) fA= c ¯ g in by formula ; for example if then ^ b rence of variable
Convention 2.0.3. By the above definition, formula variables will only be used to define inference rules, and will never appear in derivations. However, when we perform normalisa-tion we will sometimes single out atom occurrences (by decorating them) and substitute on them as if they were formula variables.
Definition 2.0.4. An inference rule is an expression , where the formulae and are called premiss and conclusion, respectively. A (deductive) system is a finite set of inference rules. An inference rule instance of is such that and are ground, and fa1=b1, a2=b2, . . . gfA1= 1, A2= 2, . . . g and fa1=b1, a2=b2, . . . gfA1= 1, A2= 2, . . . g, for some renaming fa1=b1, a2=b2, . . . g and substiution fA1= 1, A2= 2, . . . g.
The Functorial Calculus
We now present the functorial calculus in the context of classical propositional logic and give some basic results.
The intuition behind derivations in the functorial calculus is that we can compose deriva-tions by the same connectives we can compose formulae.
Remark 2.1.3. If desireable, Convention 2.1.2 on the preceding page could be made redun-dant by forcing associativity of horizontal composition in Definition 2.1.1 on page 7. The only reason we did not do this was for the sake of brevity of the following results.
The Calculus of Structures
We now present the calculus of structures and in Theorem 2.2.2 and Theorem 2.2.6 on page 13 we show that the functorial calculus and the calculus of structures polynomially simulate each other.
The intuition behind derivations in the calculus of structures is that we rewrite formulae by applying inference rules inside a context.
Definition 2.2.1. Given a deductive system S , a set of formulae, F, and and from F; a calculus of structures derivation in S from to , denoted S To find an upper bound on the size of , we observe that it depends at most linearly on the number of inference rule instances in multiplied by the size of the largest formula in . Furthermore, by the above Lemmata, the number of inference rules in is the same as the number of inference rules in and the size of the largest inference rule depends at most linearly on the size of , so the size of depends at most quadratically on the size of . The calculus of structures is now well developed for classical [Brü03a, Brü06a, Brü06d, BT01, Brü06b], intuitionistic [Tiu06a], linear [Str02, Str03b], modal [Brü06c, GT07, Sto07] and commutative/non-commutative logics [Gug07, Tiu06b, Str03a, Bru02, DG04, GS01, GS02, GS09, Kah06, Kah07]. The basic proof complexity properties of the calculus of struc-tures are known [BG09]. The calculus of structures promoted the discovery of a new class of proof nets for classical and linear logic [LS05a, LS05b, LS06, SL04] (see also [Gui06]). There exist implementations in Maude of deep-inference proof systems [Kah08].
System SKS
We now define the standard deductive system SKS for classical propositional logic in deep inference [Brü03a, Brü06a, Brü06d, BT01]. For an excellent reference to previous work on normalisation in SKS, see [Brü04]. Subsystems of SKS are used throughout this thesis.
The results presented in this section, with the exception of Theorem 2.3.14 on page 18, are standard results which can be found in the literature. We include the proofs for complete-ness and as means for giving examples of the functorial calculus.
The calculus of structures and system SKS were originally defined in terms of equiva-lence classes of formulae, called ‘structures’, and without the above invertible logical rules. However, we find it more convenient to use formulae instead, since it makes it simpler to ‘trace atom occurrences’, which we will see in Section 4.1 on page 28. We now show that the two approaches are morally the same.
Remark 2.3.4. By Notation 2.3.3 on the facing page and Lemma 2.1.4 on page 9, for any formulae and and context f g we have that = implies f g = f g.
Proposition 2.3.5. The relation = defined in Definition 2.3.2 on the facing page is an equiva-lence relation.
It turns out that the equivalence class induced by = is the same as the structures used in [Brü04].
Remark 2.3.6. If = , then (as remarked in [BG09]) there exists a derivation f= ,= ,= #,= « ,= #,= #,= « ,= « ,= #,= #,= « ,= « g _c ^c a a f t f t f^ t_ f^ t_ whose size depends at most quadratically on the sum of the sizes
Notation 2.3.7. When we work in (subsystems of) SKS, we often omit mentioning the invertible rules. Given S be a subsystem of SKS, then, unless specified otherwise, when we write S we mean S [ f=_c, =^c, =a #, =a « , =f #, =t#, =f « , =t », =f^#, =t_#, =f^ », =t_ »g. Furthermore, if 2 SKS, and there is a derivation
Proof. We show how to construct the first derivation, the second one can be done sym-metrically. The result follows by induction on the number of occurrences of a in , and Lemma 2.3.8 on the preceding page.
Table of contents :
1 Introduction
I Derivations
2 Propositional Classical Logic
2.1 The Functorial Calculus
2.2 The Calculus of Structures
2.3 System SKS
II Atomic Flows
3 Atomic Flows
3.1 Paths and Cycles
3.2 Subflows
4 Atomic Flows and Derivations
4.1 Extracting Flows from Derivations
4.2 A Normal Form of Derivation
5 Normal Forms
III Normalisation
6 Global Reductions
6.1 Simplifier
6.2 Isolated Subflow Removal
6.3 Path Breaker
6.4 Multiple Isolated Subflows Removal
6.4.1 Threshold Formulae
7 Local Reductions
7.1 Soundness
7.2 Termination and Confluence
7.3 Complexity
8 Main Result
Index
Bibliography
