# 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.

Basis

• Definitions:
• [Any appropriate definition of > in terms of &, +, and ~]
• Rules (The first rule of each set was given explicitly in the paper. -JH)
• Rule set 1
• R1.1: from (x & y) & z infer x & (y & z)
• R1.2: from ((x & y) & z) + a infer (x & (y & z)) + a
• R1.3: from ((x & y) & z) & b infer (x & (y & z)) & b
• R1.4: from (((x & y) & z) & b) + a infer ( (x & (y & z)) & b) + a
• R1.5: from x & (y & z) infer (x & y) & z
• R1.6: from ( x & (y & z)) + a infer ((x & y) & z) + a
• R1.7: from ( x & (y & z)) & a infer ((x & y) & z) & a
• R1.8: from (( x & (y & z)) & a) + b infer (((x & y) & z) & a) + b
• Rule set 2
• R2.1: from (x & (y & z)) & u infer (x & y) & (z & u)
• R2.2: from ((x & (y & z) ) & u) + a infer ((x & y) & (z & u)) + a
• R2.3: from ((x & (y & z)) & u) & b infer ((x & y) & (z & u)) & b
• R2.4: from (((x & (y & z)) & u) & b) + a infer (((x & y) & (z & u)) & b) + a
• R2.5: from ((x & y) & (z & u)) infer ( x & (y & z)) & u
• R2.6: from ((x & y) & (z & u)) + a infer ((x & (y & z)) & u) + a
• R2.7: from ((x & y) & (z & u)) & b infer ((x & (y & z)) & u) & b
• R2.8: from (((x & y) & (z & u)) & b) + a infer (((x & (y & z)) & u) & b) + a
• Rule set 3
• R3.1: from (x + y) + z infer x + (y + z)
• R3.2: from ((x + y) + z) + a infer (x + (y + z)) + a
• R3.3: from ((x + y) + z) & b infer (x + (y + z)) & b
• R3.4: from (((x + y) + z) & b) + a infer ((x + (y + z)) & b) + a
• R3.5: from x + (y + z) infer (x + y) + z
• R3.6: from (x + (y + z)) + a infer ((x + y) + z) + a
• R3.7: from (x + (y + z)) & b infer ((x + y) + z) & b
• R3.8: from ((x + (y + z)) & b) + a infer (((x + y) + z) & b) + a
• Rule set 4
• R4.1: from (x + (y + z)) + u infer (x + y) + (z + u)
• R4.2: from ((x + (y + z)) + u) + a infer ((x + y) + (z + u)) + a
• R4.3: from ((x + (y + z)) + u) & b infer ((x + y) + (z + u)) & b
• R4.4: from (((x + (y + z)) + u) & b) + a infer (((x + y) + (z + u)) & b) + a
• R4.5: from (x + y) + (z + u) infer (x + (y + z)) + u
• R4.6: from ((x + y) + (z + u)) + a infer ((x + (y + z)) + u) + a
• R4.7: from ((x + y) + (z + u)) & b infer ((x + (y + z)) + u) & b
• R4.8: from (((x + y) + (z + u)) & b) + a infer (((x + (y + z)) + u) & b) + a
• Rule set 5
• R5.1: from x & y infer y & x
• R5.2: from (x & y) + a infer (y & x) + a
• R5.3: from (x & y) & b infer (y & x) & b
• R5.4: from ((x & y) & b) + a infer ((y & x) & b) + a
• R5.5: from y & x infer x & y
• R5.6: from (y & x) + a infer (x & y) + a
• R5.7: from (y & x) & b infer (x & y) & b
• R5.8: from ((y & x) & b) + a infer ((x & y) & b) + a
• Rule set 6
• R6.1: from x + y infer y + x
• R6.2: from (x + y) + a infer (y + x) + a
• R6.3: from (x + y) & b infer (y + x) & b
• R6.4: from ((x + y) & b) + a infer ((y + x) & b) + a
• R6.5: from y + x infer x + y
• R6.6: from (y + x) + a infer (x + y) + a
• R6.7: from (y + x) & b infer (x + y) & b
• R6.8: from ((y + x) & b) + a infer ((x + y) & b) + a
• Rule set 7
• R7.1: from x & (y + z) infer (x & y) + (x & z)
• R7.2: from (x & (y + z)) + a infer ((x & y) + (x & z)) + a
• R7.3: from (x & (y + z)) & b infer ((x & y) + (x & z)) & b
• R7.4: from ((x & (y + z)) & b) + a infer (((x & y) + (x & z)) & b) + a
• R7.5: from ((x & y) + (x & z)) infer (x & (y + z))
• R7.6: from ((x & y) + (x & z)) + a infer (x & (y + z)) + a
• R7.7: from ((x & y) + (x & z)) & b infer (x & (y + z)) & b
• R7.8: from (((x & y) + (x & z)) & b) + a infer ((x & (y + z)) & b) + a
• Rule set 8
• R81: from ~(x + y) infer ~x & ~y
• R8.2: from ~ (x + y) + a infer (~x & ~y) + a
• R8.3: from ~ (x + y) & b infer (~x & ~y) & b
• R8.4: from (~ (x + y) & b) + a infer ((~x & ~y) & b) + a
• R8.5: from ~x & ~y infer ~ (x + y)
• R8.6: from (~x & ~y) + a infer ~ (x + y) + a
• R8.7: from (~x & ~y) & b infer ~ (x + y) & b
• R8.8: from ((~x & ~y) & b) + a infer (~ (x + y) & b) + a
• Rule set 9
• R9.1: from ~(x & y) infer ~x + ~y
• R9.2: from ~ (x & y) + a infer (~x + ~y) + a
• R9.3: from ~ (x & y) & b infer (~x + ~y) & b
• R9.4: from (~ (x & y) & b) + a infer ((~x + ~y) & b) + a
• R9.5: from (~x + ~y) infer ~ (x & y)
• R9.6: from (~x + ~y) + a infer ~ (x & y) + a
• R9.7: from (~x + ~y) & b infer ~ (x & y) & b
• R9.8: from ((~x + ~y) & b) + a infer (~ (x & y) & b) + a
• Rule set 10 [This is the rule set explictly expanded in the paper -JH]
• R10.1: from ~ ~ x infer x
• R10.2: from ~ ~ x + a infer x + a
• R10.3: from ~ ~ x & b infer x & b
• R10.4: from (~ ~ x & b) + a infer (x & b) + a
• R10.5: From x infer ~ ~ x
• R10.6: From x + a infer ~ ~ x + a
• R10.7: From x & b infer ~ ~ x & b
• R10.8: From (x & b) + a infer (~ ~ x & b) + a
• Rule set 11
• R11.1: From x & ~x infer x
• R11.2: from (x & ~x) + a infer x + a
• R11.3: from (x & ~x) & b infer x & b
• R11.4: from ((x & ~x) & b) + a infer (x & b) + a
• R11.5: from x infer x & ~x
• R11.6: from x + a infer (x & ~x) + a
• R11.7: from x & b infer (x & ~x) & b
• R11.8: from (x & b) + a infer ((x & ~x) & b) + a
• Rule set 12
• R12.1: from x + x infer x
• R12.2: from (x + x) + a infer x + a
• R12.3: from (x + x) & b infer x & b
• R12.4: from ((x + x) & b) + a infer (x & b) + a
• R12.5: from x infer x + x
• R12.6: from x + a infer (x + x) + a
• R12.7: from x & b infer (x + x) & b
• R12.8: from (x & b) + a infer ((x + x) & b) + a
• Rule set 13
• R13.1: From (x & ~x) + x infer x
• R13.2: from ((x & ~x) + x) + a infer x + a
• R13.3: from ((x & ~x) + x) & b infer x & b
• R13.4: from (((x & ~x) + x) & b) + a infer (x & b) + a
• R13.5: from x infer (x & ~x) + x
• R13.6: from x + a infer ((x & ~x) + x) + a
• R13.7: from x & b infer ((x & ~x) + x) & b
• R13.8: from (x & b) + a infer (((x & ~x) + x) & b) + a
• Rule set 14
• R14.1: from x + (y & z) infer (x & (y + ~y)) + (y & z)
• R14.2: from (x + (y & z)) + a infer ((x & (y + ~y)) + (y & z)) + a
• R14.3: from (x + (y & z)) & b infer ((x & (y + ~y)) + (y & z)) & b
• R14.4: from ((x + (y & z)) & b) + a infer (((x & (y + ~y)) + (y & z)) & b) + a
• R14.5: from (x & (y + ~y)) + (y & z) infer x + (y & z)
• R14.6: from ((x & (y + ~y)) + (y & z)) + a infer (x + (y & z)) + a
• R14.7: from ((x & (y + ~y)) + (y & z)) & b infer (x + (y & z)) & b
• R14.8: from (((x & (y + ~y)) + (y & z)) & b) + a infer ((x + (y & z)) & b) + a
• Rule set 15
• R15.1: from x + y infer (x & (y + ~y))+ y
• R15.2: from (x + y) + a infer ((x & (y + ~y)) + y) + a
• R15.3: from (x + y) & b infer ((x & (y + ~y)) + y) & b
• R15.4: from ((x + y) & b) + a infer (((x & (y + ~y)) + y) & b) + a
• R15.5: from (x & (y + ~y)) + y infer x + y
• R15.6: from ((x & (y + ~y)) + y) + a infer (x + y) + a
• R15.7: from ((x & (y + ~y)) + y) & b infer (x + y) & b
• R15.8: from (((x & (y + ~y)) + y) & b) + a infer ((x + y) & b) + a
• Rule set 16
• R16.1: from (x & ~x) & y infer (x & ~x) & (y & ~y)
• R16.2: from ((x & ~x) & y) + a infer ((x & ~x) & (y & ~y)) + a
• R16.3: from ((x & ~x) & y) & b infer ((x & ~x) & (y & ~y)) & b
• R16.4: from (((x & ~x) & y) & b) + a infer (((x & ~x) & (y & ~y)) & b) + a
• R16.5: from (x & ~x) & (y & ~y) infer (x & ~x) & y
• R16.6: from ((x & ~x) & (y & ~y)) + a infer ((x & ~x) & y) + a
• R16.7: from ((x & ~x) & (y & ~y)) & b infer ((x & ~x) & y) & b
• R16.8: from (((x & ~x) & (y & ~y)) & b) + a infer (((x & ~x) & y) & b) + a
• Rule set 17
• R17.1: from (x & ~x) & ~y infer (x & ~x) & y
• R17.2: from ((x & ~x) & ~y) + a infer ((x & ~x) & y) + a
• R17.3: from ((x & ~x) & ~y) & b infer ((x & ~x) & y) & b
• R17.4: from (((x & ~x) & ~y) & b) + a infer (((x & ~x) & y) & b) + a
• R17.5: from (x & ~x) & y infer (x & ~x) & ~y
• R17.6: from ((x & ~x) & y) + a infer ((x & ~x) & ~y) + a
• R17.7: from ((x & ~x) & y) & b infer ((x & ~x) & ~y) & b
• R17.8: from (((x & ~x) & y) & b) + a infer (((x & ~x) & ~y) & b) + a
• Axioms
• x + ~x

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:

• Rx.1: From p infer q
• Rx.2: From p + a infer q + a
• Rx.3: From p & b infer q & b
• Rx.4: From (p & b) + a infer (q & b) + a

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