summaryrefslogtreecommitdiffstats
path: root/content/zettel/4c2a.md
blob: b9b6be652afdaf37ab1d201ee97a837a1c52689b (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
+++
title = "Cut elimination"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["4c2"]
forwardlinks = ["4c2b"]
zettelid = "4c2a"
+++

Cut elimination is a rule that is present in Gentzen's sequent calculus
(LK).

$$ \frac{\Gamma \vdash \Delta, A \quad A, \Sigma \vdash \Lambda}{\Gamma, \Sigma\vdash \Delta, \Lambda} $$