ECE 208: Discrete Math 2

Hilbert system rules

Axioms:

\(\vdash (A\implies (B\implies A))\)
\(\vdash (A\implies (B\implies C))\implies ((A\implies B)\implies (A\implies C))\)
\(\vdash (\neg B\implies\neg A)\implies (A\implies B))\)

Inference (MP):

Derived rules:

Deduction: \(\frac{U\cup \{A\}\vdash B}{U\vdash A\implies B}\)
Contrapositive: \(\frac{U\vdash \neg B\implies\neg A}{U\vdash A\implies B}\) (and vice versa)
Transitivity: \(\frac{u\vdash A\implies B, U\vdash B\implies C}{U\vdash A\implies C}\)
Exchange of antecedent: \(\frac{U\vdash A\implies (B\implies C)}{U\vdash B\implies (A\implies C)}\)
Double negation: \(\frac{U\vdash \neg\neg A}{U\vdash A}\) (and vice versa)
Reductio ad absurdum: \(\frac{U\vdash\neg A\implies false}{U\vdash A}\)