Speaking of logic, here's a problem for you gamemaster77:
Consider the following system:
Primitive symbols: infinitely many propositional symbols P, Q, R, S, T, with and without subscripts, parenthesis (or dots), and the single operator symbol "|". The rules for wffs in N may be stated as:
1. Any single letter of N is a wff.
2. If P and Q are wffs, then (P)|(Q) is a wff.
(No formula of N will be regarded as being a wff unless its being so follows from this definition)
Single axiom (in metalanguage... its a pattern for infinite axioms in the object language):
Ax. P.|.Q|R:|::T.|.T|T:.|:.S|Q:|

|S.|.P|S
Single rule of inference:
Rule. From P and P.|.R|Q to infer Q.
Now:
Prove: Q:.|:.Q|P.|.P:|:Q|P.|.P