Prof. Gregory Chaitin [1,2] (ministrado em português)
Abstract: We add a new (valid) strong propositional substitution rule
(SUB) : $\frac{\Gamma}{\theta(\Gamma)}$ for any $\theta \in
\mbox{Hom}(V~AR \to F0R)$ and consider dag-like cut-free sequent calculus
SEQ$_{sub}$ with (SUB) (for brevity classical, but also keep
intuitionistic one in mind). We formulate for SEQ$_{sub}$ the Hauptsatz
with Compression. We ask if SEQ$_{sub}$ admits better/faster speed-up of
proof compression than analogous calculus with weaker substitution for
$\theta \in \mbox{Hom}(V~AR \to LIT)$?
[1] http://en.wikipedia.org/wiki/Gregory_Chaitin
[2] https://ufrj.academia.edu/GregoryChaitin
[3] http://www.informatik.uni-trier.de/~ley/pers/hd/g/Gordeev:Lew