Byungwoong Yoo

An Explicit Infinite Model Refuting Ulrich's u4 as a Single Axiom for Positive Implication

Corrected and strengthened v2. This release supplies a complete preprint and a Lean 4.33.0 formalization of an explicit substitution-closed infinite countermodel showing that Ulrich's u4 is not a single axiom for positive implicational logic under uniform substitution and modus p...