Logic and formal reasoning are essential skills for programming and computer science. Still, they are challenging to teach due to their abstract nature. This paper explores how Game-Based Learning (GBL) can simplify logic concepts, making them interactive and engaging for young learners. We introduce LogiCraft, an educational framework for co-designing board games that teach propositional logic. The framework includes three illustrative tile-based board games: ¬SCR∧BL, Tautoblocks, and Deducto. These games teach propositional logic by merging computational thinking with hands-on gameplay. By integrating syntax and semantics in new ways, ¬SCR∧BL focuses on logic formulas construction and truth tables visualization, Tautoblocks introduces more advanced concepts of negation, tautology, and contradiction, and Deducto highlights translation and model-based reasoning. Playtesting sessions with students and teachers suggest that our games can enhance logic skills and promote cooperative learning. Our initial classroom results show potential for broader applications in game-based learning.

We introduce a realisability semantics for infinitary intuitionistic set theory that is based on Ordinal Turing Machines (OTMs). We show that our notion of OTM-realisability is sound with respect to certain systems of infinitary intuitionistic logic, and that all axioms of infinitary Kripke-Platek set theory are realised. Finally, we use a variant of our notion of realisability to show that the propositional admissible rules of (finitary) intuitionistic Kripke-Platek set theory are exactly the admissible rules of intuitionistic propositional logic.