Minimal implicational calculus, or intuitionistic implicational calculus, or positive implicational calculus, is the implicational fragment of minimal calculus (which is also the implicational fragment of intuitionistic calculus and of positive calculus). It is sometimes called "C-pure intuitionism" since the letter C is used to denote implication in Polish prefix notation. It can be axiomatized by the inference rule of modus ponens ax-mp together with the axioms { ax-1, ax-2 } (sometimes written KS), or with { imim1, ax-1, pm2.43 } (written B'KW), or with { imim2, pm2.04, ax-1, pm2.43 } (written BCKW), or with the single axiom adh-minim, or with the single axiom adh-minimp. This section proves first adh-minim from { ax-1, ax-2 }, followed by the converse, due to Ivo Thomas; and then it proves adh-minimp from { ax-1, ax-2 }, also followed by the converse, also due to Ivo Thomas.
Sources for this section are * Carew Arthur Meredith, A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170; * Ivo Thomas, On Meredith's sole positive axiom, Notre Dame Journal of Formal Logic, volume XV, number 3, July 1974, page 477, in which the derivations of { ax-1, ax-2 } from adh-minim are shortened (compared to Meredith's derivations in the aforementioned paper); * Carew Arthur Meredith and Arthur Norman Prior, Notes on the axiomatics of the propositional calculus, Notre Dame Journal of Formal Logic, volume IV, number 3, July 1963, pages 171--187; and * the webpage https://web.ics.purdue.edu/~dulrich/C-pure-intuitionism-page.htm on Dolph Edward "Ted" Ulrich's website, where these and other single axioms for the minimal implicational calculus are listed.
This entire section also holds intuitionistically.
Users of the Polish prefix notation also often use a compact notation for proof derivations known as the D-notation where "D" stands for "condensed Detachment". For instance, "D21" means detaching ax-1 from ax-2, that is, using modus ponens ax-mp with ax-1 as minor premise and ax-2 as major premise. When the numbered lemmas surpass 10, dots are added between the numbers. D-strings are accepted by the grammar Dundotted := digit | "D" Dundotted Dundotted ; Ddotted := digit + | "D" Ddotted "." Ddotted ; Dstr := Dundotted | Ddotted .
(Contributed by BJ, 11-Apr-2021.) (Revised by ADH, 10-Nov-2023.)