Byungwoong Yoo

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

We construct an explicit infinite model showing that Ulrich's remaining 15-symbol candidate u4 is not a single axiom for positive implicational logic under substitution and modus ponens. The model satisfies every substitution instance of u4 and is closed under modus ponens, while...