Self-implications in BCI
Tomasz Kowalski · Notre Dame Journal of Formal Logic · 2008
Humberstone asks whether every theorem of BCI provably implies φ → φ for some formula φ . Meyer conjectures that the axiom B does not imply any such "self-implication." We prove a slightly stronger result, thereby confirming Meyer's conjecture.