- 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.