Errata to "On the logical structure of choice and bar induction principles", N. Brede, H. Herbelin
--------------------------------------------------------------------------------------------------
(January 2025 update)

Added June 2021:
While the definition of sequential alignment in Table XII is enough
for Theorem 4 to hold, the definitions of alignment in Table XV misses
stability by downwards (resp. upwards) inclusion for Theorem 7 to
work. They have to be changed into:
positive alignment of R (R⊤) : λu. ∀(a, b) ∈ u (R(a, b))
negative alignment of R (R⊥) : λu. ∃(a, b) ∈ u (R(a, b))

Added July 2023:
Page 3, column 2, definition of u ≺ₛ α: "is an initial prefix of f"
should be "is an initial prefix of α" (thanks to Jad Koleilat).

Added July 2023:
Proof of Proposition 6: the given more general lemma needed in the
proof is not general enough. It should state: "for u∈↓⁻T, T is
productive from u iff T has unbounded paths from u" (thanks to Étienne
Miquey).

Added January 2025:
Errors in the "bar-induction" side of Propositions 11, 12 and 13:
- First, the definition of \hat{T} should be broken down into two variants
  \hat+{T} and \hat-{T}:
  - v∈\hat+{T} iff ∃u(v=ord(u)∧u∈T), which corresponds to the original \hat{T},
  - v∈\hat-{T} iff ∀u(v=ord(u)→u∈T), which is symmetric to \hat+{T} and new.
- Then, in Proposition 11:
  - the first item should be reformulated into:
    if T is closed under restriction, u∈T iff u∈||↑⁻ \hat+{T}||
    which was correct;
  - to be proved, the second item should be changed to:
    if T is closed under extension, u∈T iff u∈||↓⁺ \hat-{T}||.
- Similarly, in Proposition 12:
  - the first item is correct (reformulating \hat{T} into \hat+{T});
  - the second item is provable when the second part is changed into:
    ↓⁺ \hat-{T} is inductively N-B-barred iff T is inductively barred.
- Similarly, in Proposition 13, the second part of the second item
  should be: ↓⁺ \hat-{T} is N-B-barred iff T is barred.
In particular, these are the needed symmetrisations so that the
argument "by duality" works in the proofs of Propositions 12 and 13
(thanks to Martin Baillon, April 2024)

Added January 2025:
Interestingly, the "GDC implies DC^prod" part of Theorem 5 is
essentially intuitionistic, in the sense of requiring using an
hypothesis several times in the proof.
By duality, the "GBI implies BI^ind" part of Theorem 5 then requires
classical logic (many thanks to Martin Baillon, March 2024, who
additionally observed that either decidability of T or monotony of T
is enough to obtain "GBI implies BI^ind" intuitionistically).

Added January 2025:
Proposition 14 requires classical logic. More precisely, the GDC case
would be intuitionistically provable by replacing Bool with Prop
(thanks to the impredicativity of Prop) while the GBI case seems
intrinsically classical (observations from Yannick Forster, April
2024).