Kirst, DominikShillito, Ian2025-05-232025-05-2397839597736211868-8969http://www.scopus.com/inward/record.url?scp=85217438656&partnerID=8YFLogxKhttps://hdl.handle.net/1885/733752858We provide a succinct and verified completeness proof for first-order bi-intuitionistic logic, relative to constant domain Kripke semantics. By doing so, we make up for the almost-50-year-old substantial mistakes in Rauszer's foundational work, detected but unresolved by Shillito two years ago. Moreover, an even earlier but historically neglected proof by Klemke has been found to contain at least local errors by Olkhovikov and Badia, that remained unfixed due to the technical complexity of Klemke's argument. To resolve this unclear situation once and for all, we give a succinct completeness proof, based on and dualising a standard proof for constant domain intuitionistic logic, and verify our constructions using the Coq proof assistant to guarantee correctness.Received funding from the European Union's Horizon research and innovation programme under the Marie Sk\u0142odowska-Curie grant agreement No. 101152583 and a Minerva Fellowship of the Minerva Stiftung Gesellschaft f\u00FCr die Forschung mbH.19en© Dominik Kirst and Ian Shillito.bi-intuitionistic logiccompletenessCoq proof assistantfirst-order logic2025-02-0310.4230/LIPIcs.CSL.2025.4085217438656