Propositional Calculus 0

RULES:

(Ax) Axiom:

Every axiom is a theorem.

(MP) Modus Ponens:

For all wff's P and Q, if P is a theorem and P ⇒ Q is a theorem, then Q is a theorem.

(Sub) Substitution:

For each K, R , and L, if R is a theorem, K is a component of R, and L is a wff, then the propositional form obtained by replacing in R every occurrence of K by L is a theorem.

DEFINITIONS:

A wff is a theorem iff it is obtained using rules Ax, MP, and Sub.


For all wff's P and Q, F1 through F5 are also wff's. Only strings of symbols built from variables using F1 through F5 can be wff's.

F1: ¬P 

F2: P ⇒ Q

F3: P ∧ Q
F4: P ∨ Q     
F5: P ⇔ Q