1 (Naturau Deduction System, N-system) 11,,,,, n- R t 1,, t n Rt 1 t n atomic formula : x, y, z, u, v, w, : f, g, h, : c, d, : t, s, r, : P, Q, : R, : A, B, C, D, 12 A A A A N-system 1 1 N-system N-system Hilbert-style system Gentzen-system 1
(Introduction rules) A B ( I) A B (Elimination rules) A B A ( E r) A B B ( E l) [A] B A B ( I) A A B ( I r) ϕ(x) xϕ(x) ϕ(t) xϕ(x) ( I) ( I) B A B ( I l) A B B A B xϕ(x) ϕ[t/x] xϕ(x) ψ A [A] C C ( E) ( E) [A] C ( E) [ϕ(x)] ψ ( E) 10 A A ( E) [A] ( I) A (minimal logic) P (P Q) P Q, P Q A ( ) ( ) ex falso sequitur quodlibet 2 A A A A ( E) 10 ( ) 11 2 material implication 2
13 N-system N-system Ni 1 [A (B C)] 1 [A] 3 E [A B]2 [A] 3 E B C B E C A C I 3 (A B) (A C) I 2 (A (B C)) ((A B) (A C)) I 1 (A (B C)) ((A B) (A C)) deduction derivation I [A] B A B ( I) (A (B C)) ((A B) (A C)) (A (B C)) ((A B) (A C)) ((A B) (A C)) A B A C A C A C 1 (1) (A B) (B A) (2) (A (B C)) ((A B) C) (3) A A (4) (A B) C (A C) (B C) (5) (A C) (B C) (A B) C (4) (5) (A B) C (A C) (B C) 3
[(A C) (B C)] D (A B) C [(A B) C] D (A C) (B C) (A B) C (A C) (B C) 2( cancellation [A] 1 A A I 1 N-system N-system N-system (scheme) A, B A B A B A A B A, B active A, B Γ D A D B A B D -I 3 Γ A B Γ A B -I Γ B Γ {A} A B 3 Γ 4
A Γ Γ {A} Γ A 2 A A A A [A] A A Γ = {A} Γ A 4 3 [A] B A I 1 A (B A) I 1 -I A A A B A I A (B A) I A B A B vacuous discharge 2 4 (1) -E sequent calculus style (2) 3 B A [A (A B)] 2 [A] 1 E A B [A] 1 E B A B I 1 (A (A B)) (A B) I 2 -I 1 discharge -I sequent style 4 {A} A 5
A (A B)) A (A B) A A A (A B), A A B A A A (A B), A B (A (A B)) (A B) I (A (A B)) (A B) I E 14 1 constant 2 3 t 1,, t n n- f n f n (t 1 t n ) t free variable F V (t) 1 t = a F V (a) = φ, 2 t = x F V (x) = {x}, 3 t = f n (t 1,, t n ) F V (f n (t 1,, t n )) = F V (t 1 ) F V (t n ) A F V (A) 1 F V ( ) = φ, 2 F V (P (t 1 t n )) = F V (t 1 ) F V (t n ), 3 F V (A B) = F V (A B) = F V (A B) = F V (A) F V (B), 4 F V ( xa) = F V ( xa) = F V (A) {x} x t x t [t /x] t x t t[t /x] [t/x] 1 a[t/x] = a, 2 y x y[t/x] = y, y = x y[t/x] = t, 6
3 f n (t 1,, t n )[t/x] = f n (t 1 [t/x],, t n [t/x]) [t/x] 1 [t/x] =, 2 (P n (t 1,, t n ))[t/x] = P n (t 1 [t/x],, t n [t/x]), 3 =,, (A B)[t/x] = A[t/x] B[t/x], 4 y x ( ya)[t/x] = ya(t/x), y = x ( ya)[t/x] = ya 5 y x ( ya)[t/x] = ya(t/x), y = x ( ya)[t/x] = ya [ ] t A x A x t t A y x(y < x) y x y x x(x < x) 5 1z xp (y, x) y 2f(x 0, x 1 ) x 1 P (x 0, x 3 ) x 0 3z P (x, y) xq(x, w) x 1 xa y A[y/x] 2 xa a A[a/x] A(y/x) A(t/x) xa I xa I ( I t 6 ) I 5 x(y < x) y x rename z(y < z) 6 t A x 7
y A(y/x) xa [A(y/x)] xa I A(y/x) A(y/x) A(y/x) [ x ya(x, y)] 1 E ya(x, y) E A(x, y) xa(x, y) I y xa(x, y) I x ya(x, y) y xa(x, y) I 1 I A(x, y) [ x ya(x, y)] x E xa A(t/x) E t 7 E [A(y/x)] n xa C D C E n y C xa [A(y/x)] C [A(y/x)] 7 t xa x x y(x = y) y(y = y) 8
x F V (A) x(a B(x)) (A xb(x)) [ x(a B(x))] 1 E A B(x) [A] 2 E B(x) xb(x) I A xb(x) I 2 x(a B(x)) (A xb(x)) I 1 x F V (B) x(a(x) B) ( xa(x) B) [ x(a(x) B)] 3 E A(x) B [A(x)] 1 [ xa(x)] 2 B E B 1 xa(x) B I 2 x(a(x) B) ( xa(x) B) I 3 E 3 (1) x(a(x) B(x)) xa(x) xb(x), (2) x(a(x) B(x)) ( xa(x) xb(x)), (3) xa(x) A(x), (4) x(a(x) B) xa(x) B, x F V (B) x(x = x) x = x E y(x = y) I occurrences 15 10 (RAA) 9
[ A] A (RAA) ( I) (RAA) ( I) P P (RAA) P P P P [A] 1 A A I [ (A A)] 2 E A I 1 A A I [ (A A)] 2 E A A RAA 2 (A B) (B A) [B] 1 A B I 1 (A B) (B A) I [ ((A B) (B A))] 2 E B A B I 1 (A B) (B A) I [ ((A B) (B A))] 2 E (A B) (B A) RAA 2 x A(x) xa(x) 4 [A(x)] 3 [ xa(x)] 2 xa(x) I E A(x) I 3 [ x A(x)] 1 x A(x) I E xa(x) RAA 2 x A(x) xa(x) I 1 10
(1) xa(x) x A(x), (2) A A, (3) A B ( A B), (4) A ( A B), (5) ((A B) (A B)) A 11
G-system, Sequent Calculus) G-system cancellation -I explicit Γ D A D B A B Γ A B Γ A B G-system Γ A B Γ A B G right rules 8 Γ A B Γ, A B R A, Γ B Γ A B R Γ A Γ A B R 1 Γ B Γ A B R 2 G N-system -E A, Γ C B, C A B, Γ, C 8 R Γ A B Γ, A B R L G1 R Γ, A Γ, B Γ, A B p17 (3) 12
[A] A B C C [B] C ( E) G A, B, Γ C A B, Γ C L Γ A B, C A B, Γ, C A B A E r A B B E l A B B A E A B C A B C C A B resouce A B D 1 D 2 A B A B A B C [A, B] C E C A B L A B A B A B I C [A, B] C E 13
A B A, B C C A B C convert ( A B) Inversion principle A B - A, B A, B C A B C - A B A B C C B C A B A A B A C [B] C E A B [A] B A B I C A [B] C E 14
Ạ Ḅ C L G1 G1 Ax A A (structural rule) LW Γ A, Γ RW Γ Γ, A LC A, A, Γ A, Γ RC Γ, A, A Γ, A LEx Γ, A, B, Λ Γ, B, A, Λ REx Γ, A A, Λ Θ Γ, Λ, Θ Γ, A, B, Λ Γ, B, A, Λ Γ, A Γ, B R Γ, A B L A, B, Γ A B, Γ R A, Γ, B Γ, A B L Γ, A B, Γ A B, Γ, R Γ, A Γ, A B Γ, B Γ, A B L A, Γ B, Γ A B, Γ 15
R A, Γ Γ, A L Γ, A A, Γ LK 9 (1) G- A A A A A A (2) G- (A (A B)) (A B) (A (A B)) (A B) sequent A A B, A B A A A B, A B A (A B), A B A (A B) A B R (A (A B)) (A B) R sequent A A B B B, A B LW LW weakning( Thinning vacuous discharge 5 A A A, B A LW A B A R A (B A) R 9 16
(3) G G1 G1 G1 G1 G1 G1 G1c G1i 10 R Γ A B Γ, A B R Γ Θ, A Ξ, B Γ, Θ, Ξ, A B Γ Delta shared context A Γ B Γ Γ, A Γ, B Γ, A B (4) G1i Γ Γ ϕ Γ Γ - Γ Γ ϕ weakening 10 LK,LJ 17
ϕ, Γ Γ ϕ R -I Γ ϕ ϕ, Γ L -E Γ sequent Γ sequent Γ sequent falsifiable A, Γ Γ, A sequent Γ A A G1c ϕ(t), Γ xϕ, Γ L Γ, xϕ(x) Γ, ϕ(a) R L t R a Γ, a eigenvaliable ϕ(a), Γ xϕ(x), Γ L Γ, ϕ(t) Γ, xϕ(x) R 18
L a Γ, a eigenvariable R t G1c A A A, A L A, A A R A A, A REx A A, A A R RC A A G1c F (a) F (a) F (a) xf (x) R xf (x), F (a) R xf (x), y G(y) R y F (y) xf (x) L y F (y) xf (x) R 1 F (a) F (a) F (a), G(a) F (a) LW G(a) G(a) F (a), G(a) G(a) LW R F (a), G(a) F (a) G(a) F (a), G(a) x(f (x) G(x)) R F (a), xg(x) x(f (x) G(x)) L xf (x), xg(x) x(f (x) G(x)) L xf (x) xg(x) x(f (x) G(x)) L xf (x) xg(x) x(f (x) G(x)) R 2 (1) A B ( A B) (2) ( A B) A B (3) (A B) A B (4) (A B) A B (5) ( A B) ( B A) (6) ( A B) (B A) (7) xf (x) y F (y) (8) yf (y) x F (x) (9) x(a B(x)) (A xb(x)) (10) (A xb(x)) x(a B(x)) (11) x(a(x) B(x)) ( xa(x) xb(x)) 19
G1i G1c sequent Γ G1i A A A A A L A, A A L A A, A A L LC A A (A A) R G1i (1) A B A B (2) A B A (3) A A B (4) A B (A B) (5) (A B) A B (6) A B (A B) (7) (A C) (B C) (A B) C (8) A B B A (9) xf (x) y F (y) (10) x F (x) xf (x) (11) x(f (x) G(x)) xf (x) xg(x) (12) (A B), A B (13) B B, (A B) A B (14) A A (15) A A G3ip( ) G3 P, Γ P ( P ) A, B, Γ C A B, Γ C L Γ A Γ B Γ A B R A, Γ C B, Γ C A B, Γ C L Γ A Γ A B R 1 Γ B Γ A B R 2 20
A B, Γ A B, Γ C A B, Γ C A, Γ B Γ A B R, Γ C L the root first proof search G1 (1) weakning A A P, Γ P P (2) Γ multiset Γ {A, B, C} {A, C, B} multiset {A, B, C} {A, A, B, C} Γ (3) R Γ A B Γ, A B Γ R Γ A Γ B Γ A B Shared context A, B A A, B B R A, B A B A B A B R A (B A B) R 5 (1) (A B) (B A) (2) (A (B C)) ((A B) C) 21
(3) A A (4) (A B) C (A C) (B C) (5) (A C) (B C) (A B) C 5 G3ip A A (3) A ((A ) ) A, A A, A L A, A A (A ) R A ((A ) ) R 6 (1) (A (B C)) ((A B) (A C)) (2) (A B C) ((A C) (B C)) (3) ( A B) (A B) (4) (P P ) (5) (A (A B)) (A B) admissibility G3ip Γ D D, C Γ, C -free system G3ip cut-free G3ip cut cut cut G3ip cut admissible G3ip+cut G3ip cut G3ip conservative extension 22
cut admissibility weight 1 A w(a) 1 w( ) = 0 2 P w(p ) = 1 3 w(a B) = w(a) + w(b) + 1,, w( A) = w(a ) = w(a) + w( ) + 1 = w(a) + 1 2 height L 0 1 C contextγ sequent C, Γ C [ ] C w(c) 1 C = P C = P C = 11 C, Γ C L C = P C =,, Γ L, Γ R w(c) n C C, Γ C w(d) n + 1 D D, Γ D D = A B w(a) n w(b) n A B, Γ A B A, B, Γ A A B, Γ A L A B, Γ A B A, B, Γ B A B, Γ B L R A, B, Γ A A, B, Γ B B, Γ = Γ A, Γ = Γ A, Γ A B, Γ B context 11 23
D = A B w(a) n w(b) n A, Γ A A, Γ A B R B, Γ B 1 B, Γ A B R 2 L A B, Γ A B D = A B A, A B, Γ A B, A, Γ B A, A B, Γ B A B, Γ A B R sequent QED n Γ C sequent Γ C G3ip n 4 Height-preserving weakening D n D, Γ C n Γ C [ ] Base case: n = 0 Γ C L C Γ Γ D, Γ C L Induction base: n height-preserving weakening n Induction step: L Γ = A B, Γ A, B, Γ C A B, Γ C L A, B, Γ C n D, A, B, Γ C n L n + 1 D, A B, Γ C QED 24
5: Inversion lemma (i) (ii) (iii) n A B, Γ C n A, B, Γ C, n A B, Γ C n A, Γ C n B, Γ C, n A B, Γ C n B, Γ C [ ] n (i) A B, Γ C L A B A B context A B, Γ C C C, A B, Γ C A B, Γ context A, B, Γ C L n (i) n+1 A B, Γ C A B A B L A, B, Γ C n A B A B, Γ C A B, Γ C n n A, B, Γ C n A, BΓ C A, B, Γ C n + 1 (ii) (i) A B, Γ C A, Γ C B, Γ C A B L A, Γ C B, Γ C n A B A B, Γ C A B, Γ C n (1) n A, Γ C (2) n B, Γ C (3) n A, Γ C (4) n B, Γ C (1) (3) A, Γ C (2) (4) B, Γ C n + 1 (iii) A B, Γ C A B B, Γ C n A B A B, Γ C A B, Γ C n 25
n B, Γ C n B, Γ C B, Γ C n + 1 QED A B, Γ A B, Γ C A B, Γ C inversion (*) n A B, Γ C n A B, Γ A Inversion lemma (i) n A B, Γ C n A, B, Γ C A B, Γ C ( A, B, Γ C n (*) A B, Γ C A B, Γ A (*) L R cut 12 G3ip inconsistent, L R Contraction contraction 6 Height-preserving contraction n D, Γ C n D, D, Γ C 12 cut 26
[ ] n = 0 D, D, Γ C L C D, Γ C L n contraction contraction formula (1) contraction formula D contraction D, D, Γ C D, D, Γ C n n D, Γ C n+1 D, Γ C (2) D D D = A B L n A, B, A B, Γ C 5 n A, B, A, B, A B, Γ C n A, B, Γ C L n+1 A B, Γ C D = A B D = A B n A B, A B, Γ A n B, A B, Γ C sequent n A B, Γ A 5 sequent n B, B, Γ C n B, Γ C n+1 A B, Γ C QED D = A B cut L cut cut cut L L cut L cut, Γ C P, Γ P P, C 27
P, C C = P C L cut P, Γ, C L cut formula 7: -Height cut cut-height cut 8 cut Γ D D, C Γ, C G3ip (1) cut L (2) cut cut formula (3) cut cut formula (4) cut cut formula cut L 1 Γ D L 11 cut formula D Γ cut Γ, C D, C weakening cut 12 Γ Γ, C L 2 D, C L 21 C Γ, C 22 C = D Γ C weakening cut Γ, C (cut ) 23 Γ, C L 24 D = cut Γ, C Γ, C 28
Γ 1 L Γ 13 cut-height 31 33 cut 3 cut formula D D (R- sequent n, m, k, 31 L Γ = A B, Γ cut-height n + 1 + m cut A, B, Γ D A B, Γ D L D, C A B, Γ, C L, L A, B, Γ D D, C A, B, Γ, C A B, Γ, C L cut-height n + m 32 L Γ = A B, Γ cut-height max(n, m) + 1 + k A, Γ D B, Γ D A B, Γ L D D, C A B, Γ, C n + k m + k cut A, Γ D D, C B, Γ D D, C A, Γ, C B, Γ, C A B, Γ L, C 13 sequent 29
33 Γ = A B, Γ cut-height max(n, m)+1+k A B, Γ A B, Γ D A B, Γ D D, C A B, Γ, C m + k cut A B, Γ A A B, Γ, A W k B, Γ D D, C B, Γ, C A B, Γ, C cut-height 4 cut formula D cut-height cut 41 L = A B, D, A, B, C Γ D D, A B, C L Γ, A B, C cut-height n + m + 1 n + m Γ D D, A, B, C Γ, A, B, C Γ, A B, C L 42 L = A B, cut-height n + max(m, k) + 1 D, A, C D, B, C Γ D D, A B, C Γ, A B, C L n + m n + k cut Γ D D, A, C Γ D D, B, C Γ, A, C Γ, B, C Γ, A B, L C 43 cut-height n + max(m, k) + 1 30
Γ D D, A B, A D, B, C D, A B, C Γ, A B, C n + m n + k cut Γ D D, A B, A Γ D D, B, C Γ, A B, A Γ, B, C Γ, A B, C 44 R C = A B cut-height n+max(m, k)+ 1 D, A D, B R Γ D D, A B Γ, A B n + m n + k cut Γ D D, A Γ D D, B Γ, A Γ, B R Γ, A B 45 R C = A B cut-height n + m + 1 n + k + 1 cut D, A Γ D D, A B R 1 Γ, A B D, B Γ D D, A B R 2 Γ, A B cut-height n + m n + k Γ D D, A Γ, A Γ, A B R 1 Γ D D, B Γ, B Γ, A B R 2 46 R C = A B cut-height n + m + 1 D, A, B Γ D D, A B R Γ, A B cut-height n + m cut 31
Γ D D, A, B Γ, A, B Γ, A B R cut-height 5 cut formula 51 D = A B cut-height max(n, m) + 1 + k + 1 cut Γ A Γ B A, B, C R Γ A B A B, C L Γ, C height n + k m + max(n, k) + 1 cut Γ A A, B, C Γ B Γ, B, C Γ, Γ, C Γ, C Ctr contraction cut-height cut-height cut-formula cut cut-height 52 D = A B cut-height n + 1 + max(m, k) + 1 Γ A Γ A B R A, C B, C 1 L A B, C Γ, C cut-height Γ B Γ A B R A, C B, C 2 L A B, C Γ, C cut-height n + m n + k 32
Γ A A, C Γ, C Γ B B, C Γ, C cut-height cut 53 D = A B n + 1 + max(m, k) + 1 A, Γ B Γ A B R A B A B, C A B, C Γ, C A, Γ B Γ A B R A B, A Γ, A Γ, C A, Γ B B, C A, Γ, C cut n+1+m, n + k, max(n + 1, m) + 1 + max(n, k) + 1 cut cut cut cut cut QED cut cut cut (a) (subformula property) 9 Γ C G3ip Γ, C G3ip cut 9 G3ip consistency 33
10 G3ip A B A B [ ] sequent R QED (b) 10 disjunction property Underivability results:g3ip sequent A A P P sequent sequent A A A P 11 sequent G3ip (i) P P (ii) (iii) (iv) P P ((P Q) P ) P (P Q R) ((P Q) (P R)) [ ] (i) P P disjunction property P P P P P R inversion P (ii): P P P P (i) root P P P L P P P (P ) R root P P 34
(iii): ((P Q) P ) P (Peirce s Law) 2 (P Q) P P Q P P (P Q) P P ((P Q) P ) P R sequent R P, (P Q) P P Q P, P Q P, (P Q) P Q (P Q) P P Q R P, P Q (P Q) P P Q P P Q R (P Q) P P Q ((P Q) P ) P (iv): (P Q R) ((P Q) (P R)) sequent R (P Q R) ((P Q) (P R)) sequent R 1 (P Q R) (P Q) (P Q R) ((P Q) (P R)) R 1 R R P, Q Q P, R Q L P, P Q R P P, Q R Q P, P Q R Q P Q R P Q R P Q R (P Q) (P R) R 1 P, R Q R P Q R P Q R P P Q R P Q R P Q P Q R P Q P Q R (P Q) (P R) R 1 35
R 2 sequent QED (c) A B ( A B) sequent (i) (ii) (iii) ( A B) A B A B A B (A B) A B (d) G3ip cut contraction 12 G3ip sequent Γ C [ ] sequent sequent sequent sequent L sequent sequent L endsequent G3cp: (1) A A (3) A A (4)RAA 36
Ạ A G-system sequent (multi succedent ) sequent A, Γ, B Γ, A B A, Γ B Γ A B A A, A, A multisuccedent R A (A G3cp Logical axioms: P, Γ, P Logical rules: G3cp A, B, Γ A B, Γ L Γ, A Γ, B Γ, A B R 37
A, Γ B, Γ A B, Γ L Γ, A, B Γ, A B R Γ, A B, Γ A B, Γ A, Γ, B Γ, A B R, Γ L G3cp G3cp invertible inversion 13 G3cp invertible invertible sequent R Γ, A Γ, B R Γ, A B n Γ, A B n Γ, A n Γ, B R invertible G3cp L, L invertible G3ip sequent C R R Γ, A B L A B Γ, A Γ, B L n inversion n+1 Γ, A B A B Γ, A B Γ, A B n n Γ, A n Γ, B n Γ, A n Γ, B 38
Γ, A Γ, B n + 1 A B R Γ, A Γ, B n QED G3cp weakning contraction Γ A, Γ LW Γ Γ, A RW A, A, Γ A, Γ LC Γ, A, A Γ, A RC G3cp cut rule, Γ, D D, Γ Γ, Γ, admissible G3ip 14 Height-preserving contraction: n C, C, Γ n C, Γ n Γ, C, C n Γ, C [ ] n = 0 L contraction L n contraction (1)contract contraction rule (2)contract 6 L L 6 R n Γ, A B, A n Γ, A B, B 13 invertibility Γ, A, A n Γ, B, B n contraction n Γ, A n Γ, B R n+1 Γ, A B n R R R vdash n A, Γ, A B, B height-preserving invertibility n A, A, Γ, B, B 39
n A, Γ, B R contraction A B, Γ, A B, A B, Γ A B, A B, Γ inversion n Γ, A, A n B, B, Γ n Γ, A n B, Γ A B, Γ n + 1 QED G3cp cut G3ip 15 cut Γ, D D, Γ Γ, Γ, G3cp cut G3cp 16 G3cp sequent Γ Γ, G3i G3c G3i A(t/x), xa, Γ C xa, Γ C L Γ A(y/x) Γ xa R A(y/x), Γ C Γ A(t/x) xa, Γ C L Γ A R R y Γ xa L y xa, Γ, C G3c 40
A(t/x), xa, Γ xa, Γ L Γ, A(y/x) Γ, xa R A(y/x), Γ Γ, A, A(t/x) xa, Γ L Γ, A R y Γ, xa L y xa, Γ, G3i G3c 16 t A(t/x) xa xa G3i G3c 17 G3i Γ C G3c Γ Γ, C (Γ, sequent G3i G3c G3i G3i xa cut R 18 G3i xa t A(t/x) existence property G3i x A xa 19 sequent x A xa G3i [ ] root R x A x A xa x A xa x A xa R x A x A A(t/x) x A A(t/x) x A xa R x A xa R R 41
R x A, A(y/x), A(z/x) x A, A(y/x) A(z/x) R x A, A(y/x) x A R, A(y/x) x A, A(y/x) x A A(y/x) R x A x A R xa x A xa x A xa R R x A, A(y/x), A(z/x), sequents G3ip sequent Γ sequent G3ip topsequent,, P 1,, P m Q 1,, Q n,,, G3ip Γ sequent 0 m, n 0 20 G3ip sequent Γ topsequent G3ip root-first C C (1)sequent C G3ip (2) tree topsequents L (3) sequent C sequent 42
21 regular sequence P 1,, P m Q 1,, Q n,,, sequent P i Q j sequent regular sequent trace formula 1 P 1 P m Q 1 Q n, m, n > 0 2 Q 1 Q n, m = 0, n > 0 3 (P 1 P m ), m > 0, n = 0 4, m, n = 0 regular sequence P i, Q j C L topsequent regular sequent tree trace formula trace formula C 1,, C n C (C 1 C n ) C 1 C n C C 1 C n C i P 1 P m Q 1 Q n trace formula P 1 P m Q 1 Q n C 1 C n 22 C regular sequence trace formulas C (C 1 C n ) sequent 23 valuation 0, 1 v(p ) = 0 v(p ) = 1 43
v( ) = 0 v(a B) = min(v(a), v(b)) v(a B) = max(v(a), v(b)) v(a B) = max(1 v(a), v(b)) v(a B) = 1 iff v(a) v(b) multiset Γ (Γ), (Γ) C Γ v (Γ) = min(v(c)), v (Γ) = max(v(c)) 24 sequent Γ v (Γ) > v ( ) v sequent Γ Γ v v (Γ) v ( ) 25 v min(v(a), v(b)) v(c) iff v(a) v(b C) 26 min(v(a B), v(a)) v(b) G3cp 27 Soundness sequent Γ G3cp Γ sequent L v (P, Γ) v (, P ) v (, Γ) v ( ) A, B, Γ A B, Γ L v (A, B, Γ) v( ) v (A B, Γ) = v (A, B, Γ) v (A B, Γ) v( ) 25,26 R QED 44
28 Completeness Γ G3cp Γ G3cp root first L regular sequent Γ regular sequents regular sequents Γ 1 1, Γ n n n > 0) regular sequent trace formula C i 22 C C 1 C n C (Γ) ( ) Γ v(c) = 1 C C 1 C n v(c) v(c 1 C n ) C i v v(c i ) = 1 C i 1 C i (P 1 P m ) P j 1 C i P 1 P m Q i Q r Q i Q r P j 1 Q k 0 C i 0 regular sequent QED 45