System ICI (Intuitionist Calculus of Implication)

[Zeman, 1973, p8]
[Hilbert and Ackermann, 1950] (Not this system per say, but includes it. -jh)

Notes

Also called the "Positive Implicational Calculus" [Zeeman, 1973, p8]

This system is the pure implicational part of the Intuitionist logic.

A decision procedure for this system (Under the name PIC) is given in [Resnik, 1962,]

Based on (Frege)

IPC is:

Operators
- Implication
Definitions
Rules
- Uniform Substitution
- Modus Ponens (Detachment for implication)
Axioms
- PL1: p>(q>p)
- PL2: (p>(q>r))>((p>q)>(p>r))
- C: ((p>(q>r)) > (q>(p>r)))

As part of a larger system (I pealed off the implicational fragment -jh), with history: [Hilbert and Ackermann, 1950, p29] (quoting G. Frege: "Begriffsschrift; eine der arithmetischen nachgebildeten Formelsprache des reinen Denkens. Halle 1879")

Based on (Łukasiewicz)

IPC is:

Operators
- Implication
Definitions
Rules
- Uniform Substitution
- Modus Ponens (Detachment for implication)
Axioms
- PL1: p>(q>p)
- PL2: (p>(q>r))>((p>q)>(p>r))

As part of a larger system, with history: [Hilbert and Ackermann, 1950, p29] (quoting J. Łukasiewicz and A. Tarski, "Untersuchungen über den Aussagenkalkül" ( C.R. Soc Sci., Varsovie, Bd. 23, Klasse III, Warschau 1930]")

As just the implicational part: [Zeman, 1973, p8, top]

Based on (Hilbert)

Definitions (none)
Rules
- Uniform Substitution
- Modus Ponens
Axioms
- PL1: p>(q>p)
- ((p>(p>q)) > (p>q)
- (p>q) > ((q>r) > (p>r))

[Hilbert und Bernays, 1934, p68]

Based on (Hilbert II)

Definitions (none)
Rules
- Uniform Substitution
- Modus Ponens
Axioms

[Hilbert und Ackermann, 1959, p39]

Basis for

PCI = ICI + Peirce: ((p>q)>p)>p [CCCpqpp] [Zeman, 1973, p14, top]