These are the rules I use for the programs at https://github.com/wslooney/Symbolic-Logic. They roughly work the same in Polish notation.
| Reiteration i. | P ⊢ | P Ri | &Introduction i. | P j. | Q ⊢ | P&Q &Ii,j | &Elimination i. | P&Q ⊢ | P &Ei ⊢ | Q &Ei | Assumption i. | P j. || Q Assume |
| vIntroduction i. | P ⊢ | PvQ vIi ⊢ | QvP vIi | vElimination i. | PvQ j. || P Assume k. || R l. || Q Assume m.|| R ⊢ | R vEi,j-k,l-m | >Introduction i. || P Assume j. || Q ⊢ | Q >Ii-j | >Elimination i. | P>Q j. | P ⊢ | Q >Ii,j |
| ~Introduction i. || P Assume || Q j. || ~Q ⊢ | ~P ~Ii-j | ~Elimination i. || ~P Assume || Q j. || Q ⊢ | P ~Ei-j | <>Introduction i. || P Assume j. || Q k. || Q Assume l. || P ⊢ | P<>Q <>Ii-j,k-l | <>Elimination i. | P<>Q j. | P ⊢ | Q <>Ei,j i. | P<>Q j. | Q ⊢ | P <>Ei,j |
| 4Introduction* (universal) i. | P(a/x) ⊢ | (4x)P 4I1 1. a does not occur in any undischarged assumption or any premise. 2. a does not occur in (4x)P. | 4Elimination* i. | (4x)P ⊢ | P(a/x) 4E1 | 3Introduction* (existential) i. | P(a/x) ⊢ | (3x)P 3Ei | 3Elimination* i. | (3x)P j. || P(a/x) Assume k. || Q ⊢ || Q 1. a does not occur in any undischarged assumption or any premise. 2. a does not occur in (3x)P. 3. a does not occur in Q. |