ProV Logo
0
Schematic Cut elimination and the Ordere...
Cerna, David...

Free

Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version] by Cerna, David ( Author )
Lemonjar Open Access
N.A
25-01-2016
In previous work, an attempt was made to apply the schematic CERES method [8] to a formal proof with an arbitrary number of {\Pi} 2 cuts (a recursive proof encapsulating the infinitary pigeonhole principle) [5]. However the derived schematic refutation for the characteristic clause set of the proof could not be expressed in the formal language provided in [8]. Without this formalization a Herbrand system cannot be algorithmically extracted. In this work, we provide a restriction of the proof found in [5], the ECA-schema (Eventually Constant Assertion), or ordered infinitary pigeonhole principle, whose analysis can be completely carried out in the framework of [8], this is the first time the framework is used for proof analysis. From the refutation of the clause set and a substitution schema we construct a Herbrand system.
-
Article
pdf
36.88 KB
English
-
MYR 0.01
-
https://arxiv.org/abs/1601.06548
Share this eBook