Slide #1.

Episode 15 Cirquent calculus • About cirquent calculus in general • The language of CL5 • Cirquents • Cirquents as circuits • Formulas as cirquents • Operations on cirquents • The rules of inference of CL5 • The soundness and completeness of CL5 • A cirquent calculus system for classical logic • CL5 versus affine logic 0
More slides like this


Slide #2.

15.1 About cirquent calculus in general irquent calculus is a new proof-theoretic approach, introduced ently in “Introduction to cirquent calculus and abstract resourc antics”. Its invention was motivated by the needs of computability c, which had stubbornly resisted any axiomatization attempts within framework of the traditional proof-theoretic approaches such as uent calculus or Hilbert-style systems. The main distinguishing feature of cirquent calculus from the known approaches is sharing: it allows us to account for the possibility of shared resources (say, formulas) between different parts of a proof tree. The version of cirquent calculus presented here can be called shallow as it limits cirquents to depth 2. Deep versions of cirquent calculus, with no such limits, are being currently developed.
More slides like this


Slide #3.

15.2 The language of CL5 The cirquent calculus system that we consider here is called CL5. CL5 axiomatizes the fragment of computability logic where all letters are general and 0-ary. And the only logical operators are ,  and . Furthermore, as in systems G1, G2 and G3 (Episodes 4 and 5),  is only allowed on atoms (if this condition is not satisfied, the formula should be rewritten into an equivalent one using the double negation and DeMorgan’s principles). And FG is understood as an abbreviation of EF. We agree that, throughout this episode, “formula” exclusively means a formula of the above fragment of the language of computability logic. L5 has 7 rules of inference: Identity, Mix, Exchange, Weakening, ication, -Introduction and -Introduction. We present those rules, ell as the concept of a cirquent, very informally through examples llustrations. More formal definitions, if needed, can be found in roduction to cirquent calculus and abstract resource semanti
More slides like this


Slide #4.

15.3 Cirquents F G H F Formulas Arcs Groups Every formula should be in (= connected with an arc to) at least one group.
More slides like this


Slide #5.

15.4 Formulas as Cirquents F = F
More slides like this


Slide #6.

15.4 Cirquents as Circuits F Circuit Sequent G H F
More slides like this


Slide #7.

15.4 Cirquents as Circuits F Cir quent G H F
More slides like this


Slide #8.

15.4 Cirquents as Circuits F Cir quent G H F
More slides like this


Slide #9.

15.4 Cirquents as Circuits F G H F Cir quent sequent Circuit F sequent G  sequent H   F 
More slides like this


Slide #10.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F
More slides like this


Slide #11.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F
More slides like this


Slide #12.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F
More slides like this


Slide #13.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F
More slides like this


Slide #14.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F
More slides like this


Slide #15.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F
More slides like this


Slide #16.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F
More slides like this


Slide #17.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F Merging formulas (merging G and H into E): F G H F
More slides like this


Slide #18.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F Merging formulas (merging G and H into E): F G H F
More slides like this


Slide #19.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F Merging formulas (merging G and H into E): F G H F
More slides like this


Slide #20.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F Merging formulas (merging G and H into E): F G H F
More slides like this


Slide #21.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F Merging formulas (merging G and H into E): F G H F
More slides like this


Slide #22.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F Merging formulas (merging G and H into E): F G H F
More slides like this


Slide #23.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F Merging formulas (merging G and H into E): F GH F
More slides like this


Slide #24.

15.5 Operations on Cirquents F G H F Merging groups (merging groups #1 and #2): F G H F Merging formulas (merging G and H into E): F E F
More slides like this


Slide #25.

15.6 Identity F F I
More slides like this


Slide #26.

15.7 Mix F F Put one cirquent next to the other G G
More slides like this


Slide #27.

15.7 Mix F F G G M F F Put one cirquent next to the other G G
More slides like this


Slide #28.

15.7 Mix F F G G M F F Put one cirquent next to the other G G
More slides like this


Slide #29.

15.7 Mix F F G G M F F Put one cirquent next to the other G G
More slides like this


Slide #30.

15.7 Mix F F G G M F Put one cirquent next to the other F G G
More slides like this


Slide #31.

15.7 Mix F F G G M F Put one cirquent next to the other F G G
More slides like this


Slide #32.

15.8 Exchange F F Swap two adjacent formulas or groups G G
More slides like this


Slide #33.

15.8 Exchange F F G G E F F Swap two adjacent formulas or groups G G
More slides like this


Slide #34.

15.8 Exchange F F G G E F F Swap two adjacent formulas or groups G G
More slides like this


Slide #35.

15.8 Exchange F F G G E F F Swap two adjacent formulas or groups GG
More slides like this


Slide #36.

15.8 Exchange F F G G E F F Swap two adjacent formulas or groups G G
More slides like this


Slide #37.

15.8 Exchange F F G G E F F G G E F F Swap two adjacent formulas or groups G G
More slides like this


Slide #38.

15.8 Exchange F F G G E F F G G E F Swap two adjacent formulas or groups F G G
More slides like this


Slide #39.

15.8 Exchange F F G G E F F G G E F Swap two adjacent formulas or groups GF G
More slides like this


Slide #40.

15.8 Exchange F F G G E F F G G E F G Swap two adjacent formulas or groups F G
More slides like this


Slide #41.

15.8 Exchange F F G G E F F G G E F G F G E F G Swap two adjacent formulas or groups F G
More slides like this


Slide #42.

15.8 Exchange F F G G E F F G G E F G F G E F G Swap two adjacent formulas or groups F G
More slides like this


Slide #43.

15.8 Exchange F F G G E F F G G E F G F G E F G Swap two adjacent formulas or groups F G
More slides like this


Slide #44.

15.8 Exchange F F G G E F F G G E F G F G E F G Swap two adjacent formulas or groups F G
More slides like this


Slide #45.

15.8 Exchange F F G G E F F G G E F G F G E F G Swap two adjacent formulas or groups F G
More slides like this


Slide #46.

15.9 Weakening E F G H W E F G H Delete any arc in any group of the conclusion; if this leaves some formula “homeless”, delete that formula as well
More slides like this


Slide #47.

15.9 Weakening E F G H W E F G H W E F G H Delete any arc in any group of the conclusion; if this leaves some formula “homeless”, delete that formula as well
More slides like this


Slide #48.

15.9 Weakening E F G H W E F G H W E F G H Delete any arc in any group of the conclusion; if this leaves some formula “homeless”, delete that formula as well
More slides like this


Slide #49.

15.10 Duplication E F Replace a group with two identical copies G H
More slides like this


Slide #50.

15.10 Duplication E F G H D E F Replace a group with two identical copies G H
More slides like this


Slide #51.

15.10 Duplication E F G H D E F Replace a group with two identical copies G H
More slides like this


Slide #52.

15.10 Duplication E F G H D E F Replace a group with two identical copies G H
More slides like this


Slide #53.

15.10 Duplication E F G H D E F Replace a group with two identical copies G H
More slides like this


Slide #54.

15.11 -Introduction E F G Merge two adjacent formulas F and G into FG H
More slides like this


Slide #55.

15.11 -Introduction E F G H  E F G Merge two adjacent formulas F and G into FG H
More slides like this


Slide #56.

15.11 -Introduction E F G H  E F G Merge two adjacent formulas F and G into FG H
More slides like this


Slide #57.

15.11 -Introduction E F G H  E F G Merge two adjacent formulas F and G into FG H
More slides like this


Slide #58.

15.11 -Introduction E F G H  E F G Merge two adjacent formulas F and G into FG H
More slides like this


Slide #59.

15.12 -Introduction E F G H  E F G H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #60.

15.12 -Introduction E F G H  E F G H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #61.

15.12 -Introduction E F G H  E F G H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #62.

15.12 -Introduction E F G H  E F G H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #63.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #64.

15.12 -Introduction E FG H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #65.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #66.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #67.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #68.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #69.

15.12 -Introduction E FG H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #70.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #71.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #72.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #73.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #74.

15.12 -Introduction E FG H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #75.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #76.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #77.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #78.

15.12 -Introduction E F G H  E FG H In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #79.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #80.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #81.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #82.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #83.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #84.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #85.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #86.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #87.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #88.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #89.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #90.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #91.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #92.

-Introduction 15.12 E F G H K  E F G H K In the premise: • F and G are adjacent formulas, and no group contains both of them together; • Every group containing F is immediately followed by a group containing G, and vice versa: every group containing G is immediately preceded by a group containing F. To obtain the conclusion: • Merge each group that contains F with its right neighbor (that contains G); • Then merge F and G into FG.
More slides like this


Slide #93.

15.13 Proof of Blass’s Principle ( ( P  Q )  ( R  S ))  ( (P  R )  (Q  S ))
More slides like this


Slide #94.

15.13 Proof of Blass’s Principle ( ( P  Q )  ( R  S ))  ( (P  R )  (Q  S )) 
More slides like this


Slide #95.

15.13 Proof of Blass’s Principle ( ( P  Q )  ( R  S ))  ( (P  R )  (Q  S )) 
More slides like this


Slide #96.

15.13 Proof of Blass’s Principle ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) (P  R )  (Q  S )  ( (P  R )  (Q  S )) 
More slides like this


Slide #97.

15.13 Proof of Blass’s Principle ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) (P  R )  (Q  S )  ( (P  R )  (Q  S ))  
More slides like this


Slide #98.

15.13 Proof of Blass’s Principle P  Q (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) (P  R )  (Q  S )  ( (P  R )  (Q  S ))  
More slides like this


Slide #99.

15.13 Proof of Blass’s Principle P  Q (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) (P  R )  (Q  S )  ( (P  R )  (Q  S ))  
More slides like this


Slide #100.

15.13 Proof of Blass’s Principle P  Q (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) (P  R )  (Q  S )  ( (P  R )  (Q  S ))  
More slides like this


Slide #101.

15.13 Proof of Blass’s Principle P  Q (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) (P  R )  (Q  S )  ( (P  R )  (Q  S ))  
More slides like this


Slide #102.

15.13 Proof of Blass’s Principle P  Q (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #103.

15.13 Proof of Blass’s Principle P  Q P  Q PR R  S (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) Q  S (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #104.

15.13 Proof of Blass’s Principle P  Q P  Q PR R  S (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) Q  S (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #105.

15.13 Proof of Blass’s Principle P  Q P  Q PR R  S (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) Q  S (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #106.

15.13 Proof of Blass’s Principle P  Q P  Q PR R  S (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) Q  S (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #107.

15.13 Proof of Blass’s Principle P  Q P  Q PR R  S (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) Q  S  (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #108.

15.13 Proof of Blass’s Principle P  Q P  Q PR R  S (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) Q  S  (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #109.

15.13 Proof of Blass’s Principle P Q P  Q P  Q PR R  S PR R  S Q  S  (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) Q  S (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #110.

15.13 Proof of Blass’s Principle P Q P  Q P  Q PR R  S PR R  S Q  S   (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) Q  S (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #111.

15.13 Proof of Blass’s Principle P Q P  Q P  Q PR R S PR R  S Q  S    (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) Q  S (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #112.

15.13 Proof of Blass’s Principle P Q P  Q P  Q P R R S PR R  S Q  S     (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) Q  S (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #113.

15.13 Proof of Blass’s Principle P Q P  Q P  Q P R R S PR R  S S Q  S     (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) Q (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #114.

15.13 Proof of Blass’s Principle P P P P I P Q P  Q P  Q Q Q Q I Q R R R P R R S PR R  S S S Q S I S S Q  S M…M E…E     (P  R )  (Q  S ) R  S ( P  Q )  ( R  S ) ( ( P  Q )  ( R  S )) R I (P  R )  (Q  S )  ( (P  R )  (Q  S ))   
More slides like this


Slide #115.

15.14 Soundness and completeness Theorem 15.1. For any formula F, the following statements are equivalent: (i) F is provable in CL5. (ii) F is valid. (iii) F is uniformly valid. Furthermore, there is an effective procedure that takes a CL5-proof of any formula F and constructs a uniform solution for F. We call this property of CL5 (and the same property of any other deductive system) uniform-constructive soundness.
More slides like this


Slide #116.

15.15 CL5 versus classical logic Remember that we see the atoms of classical logic as 0-ary elementary letters, while, on the other hand, the atoms of CL5 are 0-ary general letters. Let us for now disregard this difference and see no distinction between the two sorts of atoms. That is, let us see the formulas of CL5 as formulas of propositional classical logic. An interesting question to ask then is how CL5 compares with classical logic. Here is an answer: Fact 15.2. Every formula provable in CL5 is a tautology of classical logic, but not vice versa: some tautologies are not provable in CL5 (and hence not valid in computability logic when their atoms are seen as general atoms). The simplest example of a tautology not provable in CL5 is P(PP). Indeed, this formula (cirquent) could only be derived by -Introduction from the premise  P PP With a little thought one can see that the above cirquent, in turn, cannot be derived.
More slides like this


Slide #117.

15.16 A cirquent-calculus system for classical logic The next question to ask is how to strengthen CL5 so that it proves all tautologies (and only tautologies). The answer turns out to be very simple. All it takes to extend CL5 to a sound and complete system for classical logic is to add to it the contraction rule: Contraction E F F H Merge two adjacent and identical formulas F and F into F
More slides like this


Slide #118.

15.16 A cirquent-calculus system for classical logic The next question to ask is how to strengthen CL5 so that it proves all tautologies (and only tautologies). The answer turns out to be very simple. All it takes to extend CL5 to a sound and complete system for classical logic is to add to it the contraction rule: Contraction E F F H C E F F H Merge two adjacent and identical formulas F and F into F
More slides like this


Slide #119.

15.16 A cirquent-calculus system for classical logic The next question to ask is how to strengthen CL5 so that it proves all tautologies (and only tautologies). The answer turns out to be very simple. All it takes to extend CL5 to a sound and complete system for classical logic is to add to it the contraction rule: Contraction E F F H C E F F H Merge two adjacent and identical formulas F and F into F
More slides like this


Slide #120.

15.16 A cirquent-calculus system for classical logic The next question to ask is how to strengthen CL5 so that it proves all tautologies (and only tautologies). The answer turns out to be very simple. All it takes to extend CL5 to a sound and complete system for classical logic is to add to it the contraction rule: Contraction E F F H C E FF H Merge two adjacent and identical formulas F and F into F
More slides like this


Slide #121.

15.16 A cirquent-calculus system for classical logic The next question to ask is how to strengthen CL5 so that it proves all tautologies (and only tautologies). The answer turns out to be very simple. All it takes to extend CL5 to a sound and complete system for classical logic is to add to it the contraction rule: Contraction E F F H C E F H Merge two adjacent and identical formulas F and F into F
More slides like this


Slide #122.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P I
More slides like this


Slide #123.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P P P I P P P P I M
More slides like this


Slide #124.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P P I P P P P P I M
More slides like this


Slide #125.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P I M
More slides like this


Slide #126.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P M P P P I E
More slides like this


Slide #127.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P M P P P I E
More slides like this


Slide #128.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P M P P P I E
More slides like this


Slide #129.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P M P P P I E
More slides like this


Slide #130.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P P P P M P P P P I E C
More slides like this


Slide #131.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P PP P P P M P P P P I E C
More slides like this


Slide #132.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P P P M P P P P I E C
More slides like this


Slide #133.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P P P P P M P P P P P I E C 
More slides like this


Slide #134.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P P P P P M P P P P P I E C 
More slides like this


Slide #135.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P P P P P M P P P P P I E C 
More slides like this


Slide #136.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P P P P P M P P P P P I E C 
More slides like this


Slide #137.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P P P P M P P P P  P P I E C 
More slides like this


Slide #138.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P P P P P M P E P C P  P  P P  P P I 
More slides like this


Slide #139.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P P P P P M P E P C P  P  P P  P P I 
More slides like this


Slide #140.

15.17 Example Now P(PP) becomes provable, and so do any other classical tautologies: P P I P P P P P P P P P P M P E P C P  P  P P  ( P  P) P I 
More slides like this


Slide #141.

15.18 CL5 versus multiplicative affine logic Affine logic is a variation of the famous linear logic. Multiplicative affine logic is obtained from system G1 (see Episode 4) by deleting Contraction (as for linear logic, it further deletes Weakening as well). Our CL5 is also obtained by deleting Contraction from a deductive system for classical logic, and it is natural to ask how the two compare. Here is the answer: Fact 15.3. Every formula provable in multiplicative affine logic is also provable in CL5, but not vice versa: some formulas provable in CL5 are not provable in affine logic. Blass’s principle ( ( P  Q )  ( R  S ))  ( (P  R )  (Q  S )) proven on slide 15.13 is an example of a formula provable in CL5 but not in affine logic. In fact, one can show that any proof of Blass’s principle in G1 would require using not only Contraction, but also Weakening. On the other hand, our CL5-proof of it used neither Weakening nor Contraction (nor Duplication).
More slides like this