In August 2026, I examined whether a single formula, Ulrich’s u4, could generate all the theorems of its intended logic. The countermodel I constructed and formalized showed that u4 could not even derive P → P. After publishing the verification package, I learned that the same principal conclusion and a Lean formalization had been public for several months. I closed the journal path on 2 September.
P → P means “if P, then P.” Positive implicational logic studies theorems built around implication, without adding connectives such as conjunction or negation. A single-axiom question asks whether one starting formula, together with the permitted inference rules, can generate everything required. One theorem that cannot be derived is enough to disqualify a candidate.
From a failed search to a proof of impossibility
Failing to find a proof after a long search does not establish impossibility. I instead built an infinite countermodel over finite formulas. It designates a collection of formulas as true, includes every substitution instance of u4, and preserves membership under the rule that obtains Q from P and P → Q.
No formula of the form P → P belongs to that collection. Starting from u4 and following the permitted rules therefore cannot reach it. The formalization explicitly includes uniform substitution: consistently replacing each variable with the same formula throughout an expression. The strengthened version also derives P → P from a standard K/S basis in the same Lean environment, making the separation between the two systems explicit.
What changed in the verification package
The initial record used Lean 4.30.0. The corrected and strengthened v2, published on 21 August, moved to Lean 4.33.0 and made substitution, derivability and soundness explicit. Soundness ensures that every formula obtained through the rules remains in the countermodel’s designated collection. I also restored the recursive definitions that had been omitted from the earlier public PDF.
The package retained direct Lean compilation, an environment check, the separately implemented Rust checker nanoda, an axiom-dependency audit and Python symbolic checks. Direct compilation exited with code 0, and the nanoda log reported no typechecker errors. The axiom audit names the standard axioms used; the proof was not passed by leaving holes with sorry or admit, or by introducing a custom axiom for the conclusion.
The Python checks covered 100 recursive schemes and all 58,786 binary application-tree shapes with 12 leaves. A leaf represents one copy of the starting formula; an internal branch represents an application. These finite checks help compare the recurrence with its implementation. The all-stage conclusion rests on induction and formalization, not on reaching a large enough finite search depth. The separate checkers were run within the project to compare different implementations.
After the priority check
My first public search missed an equivalent proof. A follow-up on 29 August supplied a fixed release published on 12 March, establishing that the principal result and Lean verification predated mine. I disclosed the structural overlap and priority issue to the journal that day. On 2 September, the manuscript was rejected for insufficient originality of the principal result, and I closed that submission lineage.
The public verification package remains available. Its DOI records an archived release, not a journal’s recognition of novelty. On 5 September I prepared a bundle for theorem-by-theorem comparison of the earlier fixed release with my strengthened version. At that preparatory stage, a viable continuation depended on identifying a proposition beyond the earlier result. That is the question I would need to resolve before taking the work further.