Philosophical Propositional Calculus (1)

Subderivaton Rules

Each subderivation begins with an auxiliary assumption.

Conditional Introduction (⇒I) If P is an assumption that leads to Q, then P implies Q.

Negation Introduction (¬I) If an assumption P leads to both Q and not Q, then not P must be true.

Negation Elimination (¬E) If an auxiliary assumption P leads to Q and not Q, then P.

Disjunction Elimination (∨E) If P ∨ Q, and P leads to R and Q leads to R, then R.

Biconditional Introduction (⇔I) If P leads to Q and Q leads to P, then Q ⇔ P.