I was re-reading Noah Schweber's answer to a question I wrote a bit over a year and a half ago. One part of this answer uses Kőnig's lemma to prove (countable?) compactness of classical propositional logic. I think Noah's argument could use either the simple graph or directed graph version of the lemma.
I read a little about Kőnig's lemma because I'm curious exactly what axioms/background assumptions we need to prove it. I get the impression that Kőnig's lemma is equivalent to the axiom of countable choice given ZF in the background based on the short entry in the Wikipedia article, but I'm really not sure. I might be misinterpreting the article and there's more I have to read about Kőnig's lemma. I suspect there's a lot written on axiom-like use on Kőnig's lemma because I've heard about it (and weak versions of it) in math talks before. My question about axiom-like use of the compactness theorem.
For the sake of concreteness, I'm specifically wondering what set theory you get when you take $\mathrm{ZF}$ and add the compactness theorem (suitably paraphrased into the language of set theory) as an axiom.
I'm also curious what set theories you get if you start with other weak theories like Kripke-Platek set theory and add compactness of propositional logic as an axiom.
Compactness of propositional logic for countable sets of formulas is a theorem of ZF. The proof you refer to uses Kőnig's lemma, but this particular use of Kőnig's lemma does not require any use of AC. In general, proving Kőnig's lemma uses AC to pick each step of the path you're building down the tree. But if the tree itself can be well-ordered (or even just totally ordered since in each step you are choosing from only finitely many options), you can just use that well-ordering to make the choices in each step. In the application you refer to, the tree consists of certain finite binary sequences, which form a countable set and so can be well-ordered.
Compactness of propositional logic in full generality (for arbitrary sets of formulas over an arbitrary set of propositional variables) is one of the many well-known equivalent forms of the the Boolean principal ideal theorem (BPI), which is a very well-studied weak form of AC. Other equivalent statements include that every proper filter on a set can be extended to an ultrafilter, Tychonoff's theorem for Hausdorff spaces, and compactness of first-order logic.