Corrections and typos in my 2019
Proof Complexity book, and
further remarks
- p.14, Thm.1.1.3: the monotone version should assume that
atoms p occur only positively in \alpha or only *positively*
in \beta.
The condition that is there (positive in \alpha or negative in \beta)
is good under the assumption that \alpha \wedge \beta is unsatisfiable.
- p.17, proof of Spira's lemma (Lemma 1.1.4):
for the first subtree T_a with size
|T_a| \le (k/(k+1))|T| the previous subtree must have size
at most s \le k|T_a| + 1 (+1 is missing); the rest of the proof
follows as before.
- p.34, line -4: the quantities s_P and s_Q ought to be switched
to s_P(\tau) \le s_Q(\tau)^c.
- p.43, Thm.2.2.1: the estimates to the number of steps and the size
of the constructed tree-like proofs use
implicitly that modus ponens is present or,
more generally, that it can be simulated using each premise just once.
Jerabek gave a counter-example for a general case: there is no fixed
polynomial slow-down that would hold for all Frege systems F (the degree
may depend on F).
He also (cf. ArXiv: 2303.15090) improved a bit bounds to k_{F^*} and s_{F^*}
when modus ponens is present in terms of his notion
of "inferential size" (of an F-proof) instead of ordinary s_F.
- p.77, L.3.4.5: the proof as given is wrongly organized.
An alternative stand-alone argument using the Buss-Pudlak game
(Sec.2.2) and DNF-R (Sec.5.7) is in
the attached 2-page note. It gives
only a quasi-polynomial bound but that suffices in all
uses of the lemma.
-
p.79, definition of the Sigma-depth: in item 3 should be inequality dp(A)\le d+1.
In the definition of LK_{d+1/2} in the 2nd paragraph: allow also Pi^{S,t}_d
formulas in \pi.
-
p.191: the notation X \le x ought to be introduced before
the bounded CA axiom and the 2nd order existential quantifier
\exists X in it ought to be bounded: \exists X \le x.
Without it we can prove that for each [0,x] there is X having
an empty intersection with the interval but not the existence of
the empty set (the former suffices for many purposes but it
is unintuitive).
-
p.206, L.10.5.1: the upper bound to the lengths of propositional
simulations of theories T^i_1(\alpha) (in this lemma and others
in Sec.10.5) is quasi-polynomial as it uses L.3.4.7 and hence implicitly
L.3.4.5 - see the remark about that lemma above.
There is an additional quasi-poly blow-up when translating
sharply bounded formulas into DNF/CNF formulas; this can be remedied,
however, posing a restriction on sharply bounded kernels of induction
formulas analogous to DNF_1 formulas.
Polynomial upper bounds hold for the theory defined before L.10.5.2
by the model-theoretic proof in [288]. Analogous theories
can be defined for higher i > 1.
But most natural is to use
the quasi-polynomial proof size and theories T^i_2 because all uses
of these simulations use theories with the smash function (including the
original paper [276]).
-
p.240, Cor.12.2.4: the proof is not well-presented (e.g. that h
does not occur in T and that axioms of equality are not needed to derive (12.2.9) from (12.2.8) and hence h does not occur in axioms of equality
is not stated).
It is much clearer to base the proof on "propositional" Cor.12.2.2:
(12.2.6) is a tautology and after replacing everywhere h(t'_k) by z_k
same atoms (= atomic formulas) remain same and hence (12.2.6) remains
a tautology.
(See references in the book for further alternative proofs.)
-
p.288, Cor.13.5.4: constant c is redundant
- p.300, Thm.14.3.1:
using the lower bound for R-refutations of \neg WPHP^{n^2}_n
instead of lower bounds for R^*(\log) we can strengthen a bit
the base case of Thm.14.3.1 to the separation of LK_{1/2}
from LK_0 and hence from LK^*_1 (by L.3.4.4). This then implies
a separation of LK_{d + 1/2} vs. LK_d or equivalently vs.
LK^*_{d+1}.
I do not know if this improvement
has some immediate bounded arithmetic
relevance.
-
p.375, Subsec.17.6.2: the bound to CC and MCC is (2 \log n)
rather than just log n as in 17.6.1 (both players need to send
their partial sums in the binary search).
-
p.433/ definition of s(n)-iterability before Thm.19.5.3: this definition using
g_n-circuits is not the right one (the thm is still correct but useless).
Use instead the
original definition from Sec.3 of [291] (= J.K., "Dual weak ...") using
the notion of an "iteration protocol".
-
p.468, Problem 21.5.3: for a fixed P there is such time-optimal
(A,P), with A constructed as in universal search (for i = 1,2,...
try first i algorithms for i steps until you find a P-proof of
the formula). Here set E can be empty.
Further: it can be proved that some (A,P) is time-optimal iff
P is p-optimal, for P containing R and satisfying the technical
condition in Lemma 21.1.1.
An augmented definition of the quasi-ordering of proof search algorithms
was proposed: see extended abstract
and slides from
my Oberwolfach 2020 talk. However, I now look at it a bit differently:
see paper
Information in propositional proofs and algorithmic proof search.
-
p.468 bottom (remarks for Sec.21.1): the results of [353,269,64] mentioned
relate to the existence of an optimal proof system, not p-optimal.
- p.470: the weak set theory I write about in the second paragraph
is called "adjunctive set theory" and was discussed already in 1950s
by W.Szmielew, A.Tarski and others.
Michal Garlik wrote a
3-page list of minor errors and misprints he noted while using the book
in his St.Petersburg course in Fall 2020.
If you noticed some other errors please
let me know.
Acknowledgements
I am indebted to
Sam Buss (San Diego),
Pietro Galliani (Bolzano),
Michal Garlik (St.Petersburg),
Raheleh Jalali (Amsterdam),
Emil Jerabek (Prague) and
Emre Yolcu (CMU)
for pointing out some of these errors.