Skip to content

Commit 0770b41

Browse files
rzachrzach
committed
First two chapters of a Proof Theory part; experimental
1 parent f1e8339 commit 0770b41

22 files changed

Lines changed: 4284 additions & 0 deletions

‎content/proof-theory/cut-elimination/ce-largest.tex‎

Lines changed: 340 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,340 @@
1+
% Part: proof-theory
2+
% Chapter: cut-elimination
3+
% Section: ce-largest
4+
5+
\documentclass[../../../include/open-logic-section]{subfiles}
6+
7+
\begin{document}
8+
9+
\olfileid{pt}{cut}{inv}
10+
11+
\olsection{Removing Largest Cuts}
12+
13+
The proof of \olref[seq][inv]{lem:G3c-invert} shown that if \Log{G3c}
14+
!!{prove}s the conclusion of a logical rule (other than
15+
\RightR{\lexists} and \LeftR{\lforall}), it also !!{prove}s each of
16+
the premises of the rule without increasing the !!{height} of the
17+
proof. We can do better and show that this holds also for $\Log{G3c} +
18+
\CutCS$.
19+
20+
As before, we take the \emph{cut rank} of a \CutCS{} inference to be
21+
the depth of its cut !!{formula}.
22+
23+
\begin{lem}\ollabel{lem:inv-G3c-cut}
24+
If $\Log{G3c} + \CutCS$ !!{prove}s the conclusion of a logical
25+
rule~$R$ other than \RightR{\lexists} or \LeftR{\lforall} using !!a{proof}~$\pi$ then it also !!{prove}s each premise
26+
with !!{proof}~$\pi'$ (or !!{proof}s~$\pi'$, $\pi''$ depending on
27+
whether the rule has one or two premises). Moreover,
28+
(a)~$\pheight{\pi'}\le\pheight{\pi}$ (and
29+
$\pheight{\pi''}\le\pheight{\pi}$) and (b)~the number of \CutCS{}
30+
inferences as well as their ranks is the same in~$\pi'$ (and $\pi''$)
31+
as in~$\pi$.
32+
\end{lem}
33+
34+
\begin{proof}
35+
By inspection of the proofs of
36+
\cref{pt:seq:inv:lem:G3c-invert,pt:seq:inv:lem:invert-quant}. That
37+
proof was by induction on~$\pheight{\pi}$. In the base case, we
38+
replaced an axiom by another axiom. So conditions (a) and~(b) are
39+
trivially satisfied. If the last rule of~$\pi$ was~$R$, its immediate
40+
sub-!!{proof}s are the !!{proof}s~$\pi_i$ we want, and (a) and~(b) are
41+
both satisfied. In all other cases, we applied the inductive
42+
hypothesis to the immediate sub-!!{proof}s of~$\pi$, i.e., those
43+
leading to the premise(s) of the last inference~$R$, and then applied
44+
that same rule $R$ to the results. The conditions (a) and~(b) hold for
45+
the immediate sub-!!{proof}s of the new proof, and so (a) and~(b) hold
46+
for the entire proof. It remains to verify the case where the last
47+
inference is~\CutCS. We do this again for one example only: suppose
48+
$\pi$ is !!a{proof} of the conclusion $!B \land !C, \Gamma \Sequent
49+
\Delta$ of \LeftR{\land}, and ends in~\CutCS:
50+
\[
51+
\AxiomC{}
52+
\RightLabel{$\pi_1$}
53+
\Deduce$!B \land !C, \Gamma \fCenter \Delta, !A$
54+
\AxiomC{}
55+
\RightLabel{$\pi_2$}
56+
\Deduce$!A, !B \land !C, \Gamma \fCenter \Delta$
57+
\RightLabel{\CutCS}
58+
\BinaryInf$!B \land !C, \Gamma \fCenter \Delta$
59+
\DisplayProof
60+
\]
61+
The induction hypothesis applies to $\pi_1$ and~$\pi_2$ (which are
62+
also !!{proof}s of instances of the conclusion of $\LeftR{\land}$) and
63+
yields !!{proof}s $\pi_1'$ and~$\pi_2'$ of $!B, !C, \Gamma \fCenter
64+
\Delta, !A$ and $!A, !B, !C, \Gamma \fCenter \Delta$,
65+
respectively. We combine these using \CutCS{} to obtain~$\pi'$:
66+
\[
67+
\AxiomC{}
68+
\RightLabel{$\pi_1'$}
69+
\Deduce$!B, !C, \Gamma \fCenter \Delta, !A$
70+
\AxiomC{}
71+
\RightLabel{$\pi_2'$}
72+
\Deduce$!A, !B, !C, \Gamma \fCenter \Delta$
73+
\RightLabel{\CutCS}
74+
\BinaryInf$!B, !C, \Gamma \fCenter \Delta$
75+
\DisplayProof
76+
\]
77+
Clearly, (a) and~(b) are satisfied.
78+
\end{proof}
79+
80+
Note that this would not work if we used \Cut{} instead of \CutCS, as
81+
then the conclusion of the last !!{proof} would have two copies of
82+
$!B, !C, \Gamma$ in the antecedent and two copies of $\Delta$ in the
83+
succedent. We would have to appeal to the admissibility of
84+
contraction, but the proof of \olref[seq][inv]{prop:G3c-cont-adm} uses
85+
the invertibility lemma. We'd thus be arguing in a circle.
86+
87+
We can use \cref{pt:cut:inv:lem:inv-G3c-cut} to give an alternative
88+
proof of cut elimination. In this proof we do not successively remove
89+
topmost occurrences of \CutCS{} inferences, but occurrences of \CutCS{}
90+
inferences of maximal rank. That is, we start with !!a{proof}~$\pi$ in
91+
$\Log{G3c} + \CutCS$ and remove a cut anywhere in it (possibly
92+
replacing it with cuts of smaller rank)---and then keep doing that
93+
until no cuts remain. The only condition is that above the cut we deal
94+
with, no cuts of the same or higher rank occur.
95+
96+
\begin{lem}\ollabel{lem:max-cut-red-G3c} If $\pi$ is !!a{proof} in
97+
$\Log{G3c}+\CutCS$ ending in a~\CutCS{} inference of rank~$n$ and
98+
otherwise using only rules of~$\Log{G3c}$ and \CutCS{} inferences of
99+
rank $<n$, then there is a proof~$\pi'$ of the same end-sequent
100+
in~$\Log{G3c} + \CutCS$ where every \CutCS{} inference has rank~$<n$.
101+
\end{lem}
102+
103+
\begin{proof}
104+
The !!{proof}~$\pi$ ends in:
105+
\[
106+
\AxiomC{}
107+
\RightLabel{$\pi_1$}
108+
\Deduce$\Gamma \fCenter \Delta, !A$
109+
\AxiomC{}
110+
\RightLabel{$\pi_2$}
111+
\Deduce$!A, \Gamma \fCenter \Delta$
112+
\RightLabel{\CutCS}
113+
\BinaryInf$\Gamma \fCenter \Delta$
114+
\DisplayProof
115+
\]
116+
We distinguish cases according to the form of~$!A$.
117+
118+
Suppose $!A$ is atomic. Observe that by the condition that all
119+
\CutCS{} inferences in~$\pi_1$ and $\pi_2$ must have rank $<
120+
\depth{!A} = 0$, there can be no \CutCS{} inferences in~$\pi_1$
121+
or~$\pi_2$. We show that $\Gamma \Sequent \Delta$ has a cut-free proof
122+
by induction on $\pheight{\pi_2}$. If $\pheight{\pi_2} = 0$, then $!A,
123+
\Gamma \Sequent \Delta$ is an axiom. If $!A$ is not principal, some
124+
atomic $!C$ is !!a{element} of both~$\Gamma$ and $\Delta$, and $\Gamma
125+
\Sequent \Delta$ itself is an axiom. If $!A$ is principal, then
126+
$\Delta = \Delta, !A$. In this case, $\pi_1$ ends in $\Gamma \Sequent
127+
\Delta', !A, !A$. We obtain a cut-free proof of $\Gamma \Sequent
128+
\Delta', !A$ by applying \olref[seq][inv]{prop:G3c-cont-adm}
129+
(admissibility of contraction). If $\pheight{\pi_2} > 0$ it ends in a
130+
rule~$R$. Take a premise of that rule: it has the form $!A, \Gamma',
131+
\Pi \Sequent \Delta', \Lambda$, where $\Pi$ and $\Lambda$ are the
132+
active !!{formula}s of~$R$. \olref[seq][adm]{prop:weak-G3c-adm}
133+
applied to~$\pi_1$ and $\pi_2$ yields !!{proof}s of $\Gamma, \Gamma',
134+
\Pi \Sequent \Delta, \Delta', \Lambda, !A$ and $!A, \Gamma, \Gamma',
135+
\Pi \Sequent \Delta, \Delta', \Lambda$, to which the induction
136+
hypothesis applies. This gives us !!a{proof} of $\Gamma, \Gamma', \Pi
137+
\Sequent \Delta, \Delta', \Lambda$, for each premise of~$R$. Applying
138+
$R$ yields $\Gamma, \Gamma \Sequent \Delta, \Delta$, and
139+
\olref[seq][inv]{prop:G3c-cont-adm} provides the cut-free proof of
140+
$\Gamma \Sequent \Delta$.
141+
142+
If $!A$ is not atomic, we distinguish cases according to the !!{main
143+
operator} of~$!A$. In each case, we apply \olref{lem:inv-G3c-cut} to
144+
obtain !!{proof}s of the premises of the left- and right-rules with
145+
$!A$ as principal formula. We then proceed as in case~E of the proof
146+
of \olref[top]{lem:cut-adm-G3c}.
147+
\begin{enumerate}
148+
\item $!A \ident \lnot !B$. The !!{proof}s $\pi_1$ and $\pi_2$ end
149+
in $\Gamma \Sequent \Delta, \lnot !B$ and $\lnot !B, \Gamma \Sequent
150+
\Delta$. By \olref{lem:inv-G3c-cut}, there are !!{proof}s $\pi_1'$
151+
and $\pi_2'$ of $!B, \Gamma \Sequent
152+
\Delta$ and $\Gamma \Sequent \Delta, !B$. The !!{proof}~$\pi'$ is:
153+
\[
154+
\AxiomC{}
155+
\RightLabel{$\pi_2'$}
156+
\Deduce$\Gamma \fCenter \Delta, !B$
157+
\AxiomC{}
158+
\RightLabel{$\pi_1'$}
159+
\Deduce$!B, \Gamma \fCenter \Delta$
160+
\RightLabel{\CutCS}
161+
\BinaryInf$\Gamma \fCenter \Delta$
162+
\DisplayProof
163+
\]
164+
\item $!A \ident (!B \lor !C)$. The !!{proof}s $\pi_1$ and $\pi_2$
165+
end in $\Gamma \Sequent \Delta, !B \lor !C$ and $!B \lor !C, \Gamma
166+
\Sequent \Delta$. By \olref{lem:inv-G3c-cut} (inversion for for
167+
\RightR{\lor} applied to~$\pi_1$), there is !!a{proof} $\pi_1'$ of
168+
$\Gamma \Sequent \Delta, !B, !C$. By \olref{lem:inv-G3c-cut}
169+
(inversion for \LeftR{\lor} applied to~$\pi_2$), there is !!a{proof}
170+
$\pi_2'$ of $!B, \Gamma \Sequent \Delta$ and !!a{proof} $\pi_2''$ of
171+
$!C, \Gamma \Sequent \Delta$. By applying
172+
\olref[seq][adm]{prop:weak-G3c-adm} to $\pi_2''$ we also get
173+
!!a{proof}~$\pi_2'''$ of $!C, \Gamma \Sequent \Delta, !B$. The
174+
!!{proof}~$\pi'$ is:
175+
\[
176+
\AxiomC{}
177+
\RightLabel{$\pi_1'$}
178+
\Deduce$\Gamma \fCenter \Delta, !B, !C$
179+
\AxiomC{}
180+
\RightLabel{$\pi_2'''$}
181+
\Deduce$!C, \Gamma \fCenter \Delta, !B$
182+
\RightLabel{\CutCS}
183+
\BinaryInf$\Gamma \fCenter \Delta, !B$
184+
\AxiomC{}
185+
\RightLabel{$\pi_2'$}
186+
\Deduce$!B, \Gamma \fCenter \Delta$
187+
\RightLabel{\CutCS}
188+
\BinaryInf$\Gamma \fCenter \Delta$
189+
\DisplayProof
190+
\]
191+
\item $!A \ident (!B \land !C)$. Exercise.
192+
\item $!A \ident (!B \lif !C)$. The !!{proof}s $\pi_1$ and $\pi_2$
193+
end in $\Gamma \Sequent \Delta, !B \lif !C$ and $!B \lif !C, \Gamma
194+
\Sequent \Delta$. By \olref{lem:inv-G3c-cut} (inversion for
195+
\RightR{\lif} applied to~$\pi_1$), there is !!a{proof} $\pi_1'$ of
196+
$!B, \Gamma \Sequent \Delta, !C$. By \olref{lem:inv-G3c-cut}
197+
(inversion for \LeftR{\lif} applied to~$\pi_2$), there is
198+
!!a{proof} $\pi_2'$ of $\Gamma \Sequent \Delta, !B$ and !!a{proof}
199+
$\pi_2''$ of $!C, \Gamma \Sequent \Delta$. By applying
200+
\olref[seq][adm]{prop:weak-G3c-adm} to $\pi_2''$ we also get
201+
!!a{proof}~$\pi_2'''$ of $!C, !B, \Gamma \Sequent \Delta$. The
202+
!!{proof}~$\pi'$ is:
203+
\[
204+
\AxiomC{}
205+
\RightLabel{$\pi_2'$}
206+
\Deduce$\Gamma \fCenter \Delta, !B$
207+
\AxiomC{}
208+
\RightLabel{$\pi_1'$}
209+
\Deduce$!B, \Gamma \fCenter \Delta, !C$
210+
\AxiomC{}
211+
\RightLabel{$\pi_2'''$}
212+
\Deduce$!C, !B, \Gamma \fCenter \Delta$
213+
\RightLabel{\CutCS}
214+
\BinaryInf$!B, \Gamma \fCenter \Delta$
215+
\RightLabel{\CutCS}
216+
\BinaryInf$\Gamma \fCenter \Delta$
217+
\DisplayProof
218+
\]
219+
\item $!A \ident \lforall[x][!B(x)]$. The !!{proof}s $\pi_1$ and
220+
$\pi_2$ end in $\Gamma \Sequent \Delta, \lforall[x][!B(x)]$ and
221+
$\lforall[x][!B(x)], \Gamma \Sequent \Delta$. By
222+
\olref{lem:inv-G3c-cut}, there is !!a{proof}~$\pi_1'$ of $\Gamma
223+
\Sequent \Delta, !B(c)$.
224+
225+
Now consider the !!{proof}~$\pi_2$. It ends in $\lforall[x][!B(x)],
226+
\Gamma \Sequent \Delta$. Moving upward from the end-sequent
227+
of~$\pi_2$, mark every occurrence of $\lforall[x][!B(x)]$ on the
228+
left of a sequent that ``leads to'' the occurrence of
229+
$\lforall[x][!B(x)]$ in the end-sequent of~$\pi_2$, that is:
230+
(a)~Mark $\lforall[x][!B(x)]$ in the end-sequent of~$\pi_2$. (b)~If
231+
$\lforall[x][!B(x)]$ occurs in the context of the conclusion of a
232+
rule and is marked, mark a corresponding occurrence in the
233+
premise(s) of the rule. (c)~If $\lforall[x][!B(x)]$ is principal in
234+
the conclusion of a \LeftR{\lforall} rule and is marked, mark the
235+
corresponding active occurrences of $\lforall[x][!B(x)]$ and $!B(t)$
236+
in the premise.
237+
238+
Now consider all these marked occurrences of $\lforall[x][!B(x)]$.
239+
None of them are active in a rule other than \LeftR{\lforall} (only
240+
active !!{formula}s of \LeftR{\lforall} get marked). Delete all
241+
marked occurrences of $\lforall[x][!B(x)]$ in $\pi_2$.
242+
If this is a correct !!{proof}, the marked occurrences of
243+
$\lforall[x][!B(x)]$ were never active; they all came directly from
244+
axioms. The !!{proof} ends in~$\Gamma \Sequent \Delta$ and we can
245+
replace $\pi$ by it. We have a removed a cut of maximal rank.
246+
247+
Otherwise, what we have is not a correct proof because we have
248+
deleted !!{formula}s $\lforall[x][!B(x)]$ which were active in some
249+
\LeftR{\lforall} inferences. We have turned these into
250+
``inferences'' of the form
251+
\[
252+
\AxiomC{}
253+
\RightLabel{$\pi_t$}
254+
\Deduce$!B(t), \Pi \fCenter \Lambda$
255+
\RightLabel{\LeftR{\lforall}}
256+
\UnaryInf$\Pi \fCenter \Lambda$
257+
\DisplayProof
258+
\]
259+
Replace each topmost such ``inference'' by
260+
\[
261+
\AxiomC{}
262+
\RightLabel{$\Subst{\pi_1'}{t}{c}[\Pi \Sequent \Lambda]$}
263+
\Deduce$\Gamma, \Pi \fCenter \Delta, \Lambda, !B(t)$
264+
\AxiomC{}
265+
\RightLabel{$\pi_t[\Gamma \Sequent \Delta]$}
266+
\Deduce$!B(t), \Gamma, \Pi \fCenter \Delta, \Lambda$
267+
\RightLabel{\CutCS}
268+
\BinaryInf$\Gamma, \Pi \fCenter \Delta, \Lambda$
269+
\DisplayProof
270+
\]
271+
and add $\Gamma$ to the left and $\Delta$ to the right of every
272+
sequent below it. Repeat until all \LeftR{\lforall} ``inferences''
273+
with a marked $!B(t)$ in the premise have been replaced by a
274+
\CutCS{} inference on some~$!B(t)$. The end-sequent of the resulting
275+
!!{proof} (and it now is a correct !!{proof}) is of the form
276+
$\Gamma, \dots, \Gamma \Sequent \Delta, \dots, \Delta$. Apply
277+
admissibility of contraction to turn it into !!a{proof} of~$\Gamma
278+
\Sequent \Delta$ and replace $\pi$ with it. We have replaced one cut
279+
on $\lforall[x][!B(x)]$ with (possibly many) cuts on $!B(t)$, but
280+
these are all of lower rank. Any cuts already occurring in $\pi_1$ or
281+
$\pi_2$ remain present, but they are also all of lower rank.
282+
\end{enumerate}
283+
\end{proof}
284+
285+
\begin{prob}
286+
Verify the case where $!A \ident (!B \land !C)$ in the proof of
287+
\olref{lem:inv-G3c-cut}. That is, show that if there is
288+
!!a{proof}~$\pi$ ending in
289+
\[
290+
\AxiomC{}
291+
\RightLabel{$\pi_1$}
292+
\Deduce$\Gamma \fCenter \Delta, !B \land !C$
293+
\AxiomC{}
294+
\RightLabel{$\pi_2$}
295+
\Deduce$!B \land !C, \Gamma \fCenter \Delta$
296+
\RightLabel{\CutCS}
297+
\BinaryInf$\Gamma \fCenter \Delta$
298+
\DisplayProof
299+
\]
300+
with $\pi_1$ and $\pi_2$ containing only cuts of rank $<\depth{!B
301+
\land !C}$ then there is !!a{proof}~$\pi'$ of $\Gamma \Sequent \Delta$
302+
containing only cuts of rank $<\depth{!B \land !C}$.
303+
\end{prob}
304+
305+
% \begin{prob}
306+
% Verify the case where $!A \ident \lexists[x][!B(x)]$ in the proof of
307+
% \olref{lem:inv-G3c-cut}.
308+
% \end{prob}
309+
310+
311+
\olref[top]{lem:cut-adm-G3c} establishes that we can replace a \CutCS{}
312+
inference of highest rank in !!a{proof} by \CutCS{} inferences of
313+
lower rank. We can again use this lemma to show that we can eliminate
314+
any number of \CutCS{} inferences from !!a{proof} by successively
315+
applying it to the topmost sub-!!{proof}s ending in maximal~\CutCS.
316+
317+
\begin{thm}\ollabel{thm:cut-elim-G3c-largest}
318+
Any !!{proof} $\pi$ in $\Log{G3c} + \CutCS$ can be transformed into a proof in~\Log{G3c}.
319+
\end{thm}
320+
321+
\begin{proof}
322+
First we prove that all cuts of maximal rank in~$\pi$ can be
323+
removed. Let $d$ be the maximal rank of cuts occuring in~$\pi$, and
324+
let $n$ be the number of cuts of rank~$d$. The proof is by induction
325+
on~$n$. If $n=0$ there is nothing to prove. If $n>0$, pick a topmost
326+
cut of rank~$d$, and let $\pi_1$ be the sub-!!{proof} ending in it.
327+
By \olref{lem:max-cut-red-G3c}, there is !!a{proof}~$\pi_1'$ of the
328+
same end-sequent with all cuts of rank $<d$. Replace $\pi_1$ by
329+
$\pi_1'$ in~$\pi$. This results in !!a{proof} containing $n-1$ cuts
330+
of rank~$d$, and the induction hypothesis applies.
331+
332+
Now the result follows by induction on~$d$. If $d=0$, all cuts are
333+
atomic, and by the previous result can all be removed. If $d>0$,
334+
the previous result yields a proof in which all cuts of rank $d$
335+
have been replaced by cuts of rank~$<d$. Since $d$ was the maximum
336+
rank of cuts in~$\pi$, we have proof in which the maximal rank of
337+
cuts is $<d$, and the induction hypothesis applies.
338+
\end{proof}
339+
340+
\end{document}

0 commit comments

Comments
 (0)