System PC - Jean Porte's basis

This is Jean Porte's basis for Standard Propositional calculus. It is given its own page because it is HUGH, and while it has exactly the same theorems as standard PC, it has rules that are strictly weaker since they can't prove the rule of Modus Ponens, but are provable rules of standards PC with Modus Ponens.

This basis originally appeared in "Un systèm logistique très faible pour le calcul propositionannel classique." in Comptes rendus hebdomadaires des séances de l' Académie des Sciences (Paris), vol. 254 (1962), pp 2500-2502. (This paper is in French. If anyone knows of an official translation into English I would be interested in seeing it -JH)

Overview of the paper

This system has ONE axiom, and 136 single premiss inference rules.

The paper lays the rules out as 17 sets of eight rules. It explicitly gives one rule for each set of 17, and then expands out a single rule set (R10) as an example of how you expand them out. It then states that the other sets are expanded out in the same manner.

At the end of the paper is some discussion of independence of the rules (Jean Porte suspects they are not independent). There is also a discussion of admissible rules in the system.


For those trying to follow this, the pattern for each ruleset is that if we have a rule of the form:

From p infer q

then the generated rules are:

and Rx.5 - Rx.6 are the same as Rx.1 - Rx.4 with the premiss and consequent swapped

Go to ...

© Copyright 2009, by John Halleck, All Rights Reserved.
This page is
This page was last modified on July 9th, 20R11