In the same manner that Intuitionist PC and can be mapped onto S4 standard PC and S5 are related. [Zeman, 1973, p231] [Hughes and Cresswell, 1996, p225]

There is one alternative formulation for PC that I've given its own page. That is Jean Porte's 1962 basis for PC While is has EXACTLY THE SAME theorems as standard PC (no more, no less), but isn't actually the SAME system since it doesn't have Modus Ponens and the 136 rules it does have are strictly weaker than Modus Ponens, so the rule of Modus Ponens is not provable within the system. (Although the axiom of Modus Ponens is.) More recently Lloyd Humberstone in ["Replacing Modus Ponens with One-Premiss Rules", Logic Journal of the IGPL, Volume16, issue5 (2008), pp431-45] has given a theory of such systems, and a way of generating them.

PC from Principia Mathematica: ~ and + primitive, the rest added by definition.

- Definitions
- *1.01: p>q ==def ~p+q
- *3.01: p&q ==def ~(~p+~q)
- *4.01: p==q ==def ((p>q)&(q>p))

- Rules
- Uniform Substitution
- Modus Ponens: from |- p and |- p>q infer |- q

- Axioms
- *1.2: (p+p) > p
- *1.3: q > (p+q)
- *1.4: (p+q) > (q+p)
- *1.6: (q>r) > ((p+q)>(p+r))

[Whitehead and Russell, 1910, Volume 1, p100 (First edition), (p96 second edition)] The axiom numbers are Whitehead and Russell's. Almost nobody else ever used them. It is more usual to see the four axioms referred to as A1-A4, although some authors use A1-A5, with *1.5 below being A4.

Note that the original also has

- *1.5: (p + (q + r)) > (q + (p + r))

But this was shown redundant by Paul Bernays, "*Axiomatische
Untersuchungen des Aussagenkalküls der Principia Mathematica*",
Mathematiche Zeitschrift, Vol 25, 1926, pp 305-320,
Bernay's states that Haskel Curry also had a proof, using ideas from one
originally due to Peirce. [Paul Bernays, in his review of Peter Nidditch's
article "*A Note on the Redundant Axiom of Principia Mathematica*".
His review appeared in The Journal of Symbolic Logic, Vol. 36, No. 2
(Jun., 1971), pp. 332-333]

The second edition of Principia changed from being "+" and "~" based, to being Sheffer stroke ("|") based, with the definitions:

- ~p =def p|p
- p+q =def (p|p)|(q|q)

These were added to Chapter 1, and fully explained in the preface to the second addition.

PC is the Positive Propositional Logic plus

- PC1 [(~p>~q)>(q>p)]

PC is the Positive Propositional Logic plus

- ~~p > p
- p > ((q>~p) > ~q)

PC is the Positive Propositional Logic plus

- p + ~p
- ~p > (p>q)
- (p>~p) > ~p

PC is the Positive Propositional Logic plus

- p + ~p
- ~p > (p>q)
- (p>~p) > ~p

The axioms of Łukasiewicz:

- Rules
- Uniform Substitution
- Modus Ponens: from |- p and |- p>q infer |- q

- Definitions
- + : a+b =def ~(~a & ~b)
- > : a >b =def ~ (a & ~b)
- p==q =def ((p>q)&(q>p))

- Axioms
- CN1: (p>q)>((q>r)>(p>r))
- CN2: p>(~p>q)
- CN3: (~p>p)>p

Rosser's Axioms

- Rules
- Uniform Substitution
- Modus Ponens: from |- p and |- p>q infer |- q

- Definitions
- p+q =def ~(~p&~q)
- p>q =def ~(p&~q)
- p==q =def ((p>q)&(q>p))

- Axioms:
- KN1: p>(p&p)
- KN2: (p&q)>p
- KN3: (p>q)>(~(q&r)>~(r&p))

[Zeman 1973, p 26]
**[Rosser,
1953, Page 55]**

Tarski, Bernays, and Wajsberg basis 1 (F primitive):

- Rules
- Uniform Substitution
- Modus Ponens: from |- p and |- p>q infer |- q

- Constants
- F

- Definitions
- ~p = p>F
- Any of the standard definitions for "+", "&", and "==" in terms
of ">", and "~".
Such as:
- p+q =def ~p>q
- p&q =def ~(p>~q)
- p==q =def ((p>q)&(q>p))

- Axioms
- Syllogism: (p>q) > ((q>r) > (p>r)
- Peirce: ((p>q)>p) > p
- p > (q > p)
- F > p

Wajsberg himself credits these to Tarski and Bernays.
**[Wajsberg,
1937, pages 154-157]**
(Page 285 of the English translation:
[McCall,
1967])
I belive that Quine adds Wajsberg to the list because Wajsberg proved
a lot of the results for this axiomatic basis. -JH

The Peirce axiom can be replaced by the rule: From |- (p>q) > p infer p. [Wajsberg, 1937] (Page 285 of the English translation: [McCall, 1967])

Tarski, Bernays, and Wajsberg basis 2 (~ primitive):

- Rules
- Uniform Substitution
- Modus Ponens: from |- p and |- p>q infer |- q

- Definitions
- F = ~(p>p)
- Any standard definitions for "+", "&" in terms of ">", and "~"

- Axioms [Same axioms as prior base -JH]
- 1: (p>q) > ((q>r) > (p>r)
- 2: ((p>q)>p) > p
- 3: p > (q > p)
- 4: F > p

Wajsberg himself credits these to Tarski and Bernays. [Wajsberg, 1937, pages 154-157] (Page 285 of the English translation by S. McCall and P.Woodruff appearing in: [McCall, 1967], pages ) I belive that Quine adds Wajsberg to the list because Wajsberg proved a lot of the results for this axiomatic basis. -JH

Wajsberg basis 1 (~ primitive):

- Rules
- Uniform Substitution
- Modus Ponens: from |- p and |- p>q infer |- q

- Definitions
- F = ~(p>p)
- Any standard definitions for "+", "&" in terms of ">", and "~"

- Axioms
- (p>q) > ( (q>r) > (p>r))
- ((p>q)>p) > p
- p > ((p>q) > q)

**[Wajsberg,
1937]**
(Page 319 of the English translation
S. McCall and P.Woodruff appearing in:
[McCall,
1967])

Wajsberg basis 2 (~ primitive):

- Rules
- Uniform Substitution
- Modus Ponens: from |- p and |- p>q infer |- q

- Definitions
- F = ~(p>p)
- Any standard definitions for "+", "&" in terms of ">", and "~"

- Axioms
- r > ( ((p>q) > p) > p )
- (p>q) > ((q>r) > (p>r)

**[Wajsberg,
1939]**
(Page 319 of the English translation by S. McCall appearing in
[McCall,
1967])

(: Almost everything... :)

Standard PC has some alternatives...

Editorial comment:

[I personally don't see why any these alternatives shouldn't
be a basis for many of the modal logic systems instead
of PC. Of course, if the systems were build on this framework
they wouldn't be the same systems.
But I think that they would still be interesting systems.
In fact, the intuitionist versions of S4 and S5
*have* actually been investigated in the literature. -JH

© Copyright 2007, by John Halleck, All Rights Reserved.

This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/pc.html

This page was last modified on July 9th, 2011