882:
if it admits a proof of the absurd. If the system has a cut elimination theorem, then if it has a proof of the absurd, or of the empty sequent, it should also have a proof of the absurd (or the empty sequent), without cuts. It is typically very easy to check that there are no such proofs. Thus,
189:
490:, whereas in LJ the RHS may only have one formula or none: here we see that allowing more than one formula in the RHS is equivalent, in the presence of the right contraction rule, to the admissibility of the
498:'s logic LC it is easy to obtain a rather natural formalisation of classical logic where the RHS contains at most one formula; it is the interplay of the logical and structural rules that is the key here.
624:
313:
252:
542:
580:
763:
494:. However, the sequent calculus is a fairly expressive framework, and there have been sequent calculi for intuitionistic logic proposed that allow many formulae in the RHS. From
1221:
687:
725:
871:
demonstrated that there was a derivation that could be completed in a page using cut, but whose analytic proof could not be completed in the lifespan of the universe.
477:
450:
423:
396:
369:
342:
849:
829:
806:
786:
647:
867:
are those proofs that do not use Cut. Typically such a proof will be longer, of course, and not necessarily trivially so. In his essay "Don't
Eliminate Cut!"
922:
90:
1144:
1122:
657:
The cut-elimination theorem states that (for a given system) any sequent provable using the rule Cut can be proved without use of this rule.
1043:
65:
respectively. The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the
1088:
943:
1205:
918:
591:
926:
914:
479:…)." Note that the left-hand side (LHS) is a conjunction (and) and the right-hand side (RHS) is a disjunction (or).
1200:
491:
891:
883:
once a system is shown to have a cut elimination theorem, it is normally immediate that the system is consistent.
259:
198:
515:
553:
903:
736:
1226:
991:
1195:
666:
58:
698:
1132:
899:
887:
809:
1140:
1118:
947:
938:
879:
483:
969:, pp. 208–213, gives a 5-page proof of the elimination theorem. See also pages 188, 250.
1077:
1032:
502:
495:
317:, and (as glossed by Gentzen) should be understood as equivalent to the truth-function "If (
42:
1179:
455:
428:
401:
374:
347:
320:
1065:
1020:
852:
62:
46:
910:
programming language, depends upon the admissibility of Cut in the appropriate system.
864:
834:
814:
791:
771:
660:
For sequent calculi that have only one formula in the RHS, the "Cut" rule reads, given
632:
482:
The LHS may have arbitrarily many or few formulae; when the LHS is empty, the RHS is a
17:
1215:
1154:
1110:
868:
487:
486:. In LK, the RHS may also have any number of formulae—if it has none, the LHS is a
506:
808:
used to prove this theorem can be inlined. Whenever the theorem's proof mentions
49:
in his landmark 1934 paper "Investigations in
Logical Deduction" for the systems
1184:
54:
50:
788:
as a theorem, then cut-elimination in this case simply says that a lemma
184:{\displaystyle A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots }
981:, pp. 453, gives a very brief proof of the cut-elimination theorem.
1081:
1036:
82:
907:
994:(university lecture notes about cut-elimination, German, 2002-2003)
1095:
Gentzen, Gerhard (1965). "Investigations into logical deduction".
1050:
Gentzen, Gerhard (1964). "Investigations into logical deduction".
886:
Normally also the system has, at least in first order logic, the
85:
is a logical expression relating multiple formulas, in the form
898:
Cut elimination is one of the most powerful tools for proving
925:(every proof term reduces in a finite number of steps into a
41:) is the central result establishing the significance of the
73:, that is, a proof that does not make use of the cut rule.
1068:(1935). "Untersuchungen über das logische Schließen. II".
1023:(1935). "Untersuchungen über das logische Schließen. I.".
902:. The possibility of carrying out proof search based on
837:
831:, we can substitute the occurrences for the proof of
817:
794:
774:
739:
701:
669:
635:
594:
556:
518:
458:
431:
404:
377:
350:
323:
262:
201:
93:
619:{\displaystyle \Gamma ,\Pi \vdash \Delta ,\Lambda }
843:
823:
800:
780:
757:
719:
681:
641:
629:That is, it "cuts" the occurrences of the formula
618:
574:
536:
471:
444:
417:
390:
363:
336:
307:
246:
183:
890:, an important property in several approaches to
863:For systems formulated in the sequent calculus,
505:, and equivalent to a variety of rules in other
921:, cut elimination algorithms correspond to the
501:"Cut" is a rule in the normal statement of the
1089:Untersuchungen über das logische Schließen II
8:
1044:Untersuchungen über das logische Schließen I
1222:Theorems in the foundations of mathematics
874:The theorem has many, rich consequences:
836:
816:
793:
773:
738:
700:
668:
634:
593:
555:
517:
463:
457:
436:
430:
409:
403:
382:
376:
355:
349:
328:
322:
308:{\displaystyle B_{1},B_{2},B_{3},\ldots }
293:
280:
267:
261:
247:{\displaystyle A_{1},A_{2},A_{3},\ldots }
232:
219:
206:
200:
169:
156:
143:
124:
111:
98:
92:
959:
906:, the essential insight leading to the
537:{\displaystyle \Gamma \vdash A,\Delta }
1003:
978:
966:
575:{\displaystyle \Pi ,A\vdash \Lambda }
7:
1117:. New York: Dover Publications Inc.
758:{\displaystyle \Gamma ,\Pi \vdash B}
915:higher-order typed lambda calculus
746:
740:
702:
670:
649:out of the inferential relation.
613:
607:
601:
595:
569:
557:
531:
519:
25:
1115:Foundations of mathematical logic
1097:American Philosophical Quarterly
1052:American Philosophical Quarterly
851:. Consequently, the cut rule is
1157:(1984). "Don't eliminate cut".
1137:Introduction to metamathematics
682:{\displaystyle \Gamma \vdash A}
45:. It was originally proved by
1159:Journal of Philosophical Logic
919:Curry–Howard isomorphism
720:{\displaystyle \Pi ,A\vdash B}
1:
923:strong normalization property
1139:. Ishi Press International.
913:For proof systems based on
1201:Encyclopedia of Mathematics
944:Gentzen's consistency proof
859:Consequences of the theorem
1243:
492:law of the excluded middle
1180:"Cut Elimination Theorem"
1070:Mathematische Zeitschrift
1025:Mathematische Zeitschrift
892:proof-theoretic semantics
193:, which is to be read as
1194:Dragalin, A.G. (2001) ,
732:
694:
587:
549:
32:cut-elimination theorem
27:Theorem in formal logic
18:Cut elimination theorem
900:interpolation theorems
845:
825:
802:
782:
759:
721:
683:
643:
620:
576:
538:
473:
446:
419:
392:
365:
338:
309:
248:
185:
1111:Curry, Haskell Brooks
846:
826:
803:
783:
760:
722:
684:
644:
621:
577:
539:
474:
472:{\displaystyle B_{3}}
447:
445:{\displaystyle B_{2}}
420:
418:{\displaystyle B_{1}}
393:
391:{\displaystyle A_{3}}
366:
364:{\displaystyle A_{2}}
339:
337:{\displaystyle A_{1}}
310:
249:
186:
1133:Kleene, Stephen Cole
835:
815:
792:
772:
737:
730:allows one to infer
699:
667:
633:
592:
585:allows one to infer
554:
516:
456:
429:
402:
375:
348:
321:
260:
199:
91:
990:Wilfried Buchholz,
888:subformula property
1196:"Sequent calculus"
1082:10.1007/BF01201363
1037:10.1007/BF01201353
1006:, pp. 373–378
841:
821:
798:
778:
755:
717:
679:
639:
616:
572:
534:
469:
442:
415:
388:
361:
334:
305:
244:
181:
1146:978-0-923891-57-2
1124:978-0-486-63462-3
939:Deduction theorem
844:{\displaystyle A}
824:{\displaystyle A}
801:{\displaystyle A}
781:{\displaystyle B}
642:{\displaystyle A}
69:also possesses a
16:(Redirected from
1234:
1208:
1190:
1189:
1166:
1150:
1128:
1104:
1085:
1066:Gentzen, Gerhard
1059:
1040:
1021:Gentzen, Gerhard
1007:
1001:
995:
988:
982:
976:
970:
964:
850:
848:
847:
842:
830:
828:
827:
822:
807:
805:
804:
799:
787:
785:
784:
779:
764:
762:
761:
756:
726:
724:
723:
718:
688:
686:
685:
680:
648:
646:
645:
640:
625:
623:
622:
617:
581:
579:
578:
573:
543:
541:
540:
535:
503:sequent calculus
496:Jean-Yves Girard
478:
476:
475:
470:
468:
467:
451:
449:
448:
443:
441:
440:
424:
422:
421:
416:
414:
413:
397:
395:
394:
389:
387:
386:
370:
368:
367:
362:
360:
359:
343:
341:
340:
335:
333:
332:
316:
314:
312:
311:
306:
298:
297:
285:
284:
272:
271:
254:
253:
251:
250:
245:
237:
236:
224:
223:
211:
210:
192:
190:
188:
187:
182:
174:
173:
161:
160:
148:
147:
129:
128:
116:
115:
103:
102:
43:sequent calculus
21:
1242:
1241:
1237:
1236:
1235:
1233:
1232:
1231:
1212:
1211:
1193:
1178:Alex Sakharov.
1177:
1176:
1173:
1153:
1147:
1131:
1125:
1109:
1094:
1064:
1049:
1019:
1016:
1011:
1010:
1002:
998:
989:
985:
977:
973:
965:
961:
956:
935:
865:analytic proofs
861:
833:
832:
813:
812:
790:
789:
770:
769:
768:If we think of
735:
734:
697:
696:
665:
664:
655:
653:Cut elimination
631:
630:
590:
589:
552:
551:
514:
513:
509:, which, given
459:
454:
453:
432:
427:
426:
405:
400:
399:
378:
373:
372:
351:
346:
345:
324:
319:
318:
289:
276:
263:
258:
257:
256:
228:
215:
202:
197:
196:
194:
165:
152:
139:
120:
107:
94:
89:
88:
86:
79:
63:classical logic
47:Gerhard Gentzen
28:
23:
22:
15:
12:
11:
5:
1240:
1238:
1230:
1229:
1224:
1214:
1213:
1210:
1209:
1191:
1172:
1171:External links
1169:
1168:
1167:
1155:Boolos, George
1151:
1145:
1129:
1123:
1107:
1106:
1105:
1092:
1062:
1061:
1060:
1047:
1015:
1012:
1009:
1008:
996:
983:
971:
958:
957:
955:
952:
951:
950:
948:Peano's axioms
941:
934:
931:
896:
895:
884:
860:
857:
840:
820:
797:
777:
766:
765:
754:
751:
748:
745:
742:
728:
727:
716:
713:
710:
707:
704:
690:
689:
678:
675:
672:
654:
651:
638:
627:
626:
615:
612:
609:
606:
603:
600:
597:
583:
582:
571:
568:
565:
562:
559:
545:
544:
533:
530:
527:
524:
521:
507:proof theories
466:
462:
439:
435:
412:
408:
385:
381:
358:
354:
331:
327:
304:
301:
296:
292:
288:
283:
279:
275:
270:
266:
243:
240:
235:
231:
227:
222:
218:
214:
209:
205:
180:
177:
172:
168:
164:
159:
155:
151:
146:
142:
138:
135:
132:
127:
123:
119:
114:
110:
106:
101:
97:
78:
75:
71:cut-free proof
59:intuitionistic
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
1239:
1228:
1225:
1223:
1220:
1219:
1217:
1207:
1203:
1202:
1197:
1192:
1187:
1186:
1181:
1175:
1174:
1170:
1165:(4): 373–378.
1164:
1160:
1156:
1152:
1148:
1142:
1138:
1134:
1130:
1126:
1120:
1116:
1112:
1108:
1103:(3): 204–218.
1102:
1098:
1093:
1091:(Archive.org)
1090:
1087:
1086:
1083:
1079:
1075:
1071:
1067:
1063:
1058:(4): 249–287.
1057:
1053:
1048:
1046:(Archive.org)
1045:
1042:
1041:
1038:
1034:
1030:
1026:
1022:
1018:
1017:
1013:
1005:
1000:
997:
993:
992:Beweistheorie
987:
984:
980:
975:
972:
968:
963:
960:
953:
949:
945:
942:
940:
937:
936:
932:
930:
928:
924:
920:
916:
911:
909:
905:
901:
893:
889:
885:
881:
877:
876:
875:
872:
870:
869:George Boolos
866:
858:
856:
854:
838:
818:
811:
795:
775:
752:
749:
743:
733:
731:
714:
711:
708:
705:
695:
693:
676:
673:
663:
662:
661:
658:
652:
650:
636:
610:
604:
598:
588:
586:
566:
563:
560:
550:
548:
528:
525:
522:
512:
511:
510:
508:
504:
499:
497:
493:
489:
488:contradiction
485:
480:
464:
460:
437:
433:
410:
406:
383:
379:
356:
352:
329:
325:
302:
299:
294:
290:
286:
281:
277:
273:
268:
264:
241:
238:
233:
229:
225:
220:
216:
212:
207:
203:
178:
175:
170:
166:
162:
157:
153:
149:
144:
140:
136:
133:
130:
125:
121:
117:
112:
108:
104:
99:
95:
84:
76:
74:
72:
68:
64:
60:
56:
52:
48:
44:
40:
39:
33:
19:
1227:Proof theory
1199:
1183:
1162:
1158:
1136:
1114:
1100:
1096:
1073:
1069:
1055:
1051:
1028:
1024:
999:
986:
974:
962:
912:
897:
880:inconsistent
878:A system is
873:
862:
767:
729:
691:
659:
656:
628:
584:
546:
500:
481:
80:
77:The cut rule
70:
66:
57:formalising
37:
35:
31:
29:
1076:: 405–431.
1031:: 176–210.
1004:Boolos 1984
979:Kleene 2009
927:normal form
1216:Categories
1014:References
967:Curry 1977
917:through a
904:resolution
853:admissible
36:Gentzen's
1206:EMS Press
1185:MathWorld
1135:(2009) .
1113:(1977) .
750:⊢
747:Π
741:Γ
712:⊢
703:Π
674:⊢
671:Γ
614:Λ
608:Δ
605:⊢
602:Π
596:Γ
570:Λ
567:⊢
558:Π
532:Δ
523:⊢
520:Γ
484:tautology
398:…) then (
303:…
242:…
179:…
137:⊢
134:…
38:Hauptsatz
933:See also
67:cut rule
255:proves
83:sequent
1143:
1121:
908:Prolog
954:Notes
810:lemma
692:and
547:and
1141:ISBN
1119:ISBN
946:for
371:and
344:and
61:and
53:and
34:(or
30:The
1078:doi
1033:doi
929:).
452:or
425:or
1218::
1204:,
1198:,
1182:.
1163:13
1161:.
1099:.
1074:39
1072:.
1054:.
1029:39
1027:.
855:.
81:A
55:LK
51:LJ
1188:.
1149:.
1127:.
1101:2
1084:.
1080::
1056:1
1039:.
1035::
894:.
839:A
819:A
796:A
776:B
753:B
744:,
715:B
709:A
706:,
677:A
637:A
611:,
599:,
564:A
561:,
529:,
526:A
465:3
461:B
438:2
434:B
411:1
407:B
384:3
380:A
357:2
353:A
330:1
326:A
315:"
300:,
295:3
291:B
287:,
282:2
278:B
274:,
269:1
265:B
239:,
234:3
230:A
226:,
221:2
217:A
213:,
208:1
204:A
195:"
191:"
176:,
171:3
167:B
163:,
158:2
154:B
150:,
145:1
141:B
131:,
126:3
122:A
118:,
113:2
109:A
105:,
100:1
96:A
87:"
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.