A Toy Windmill
Junior Member
Here's a fairly famous axiom system for propositional logic:
For any propositional formulas φ, ψ and χ, declare the following to be tautologies
1) φ → (ψ → φ)
2) [φ → (ψ → χ)] → [(φ → ψ) → (φ → χ)]
3) (¬φ → ¬ψ) → (ψ → φ)
Now declare that, for any tautology φ, and any tautology of the form φ → ψ, we can take ψ to be a tautology. This rule is sometimes called modus ponens, and sometimes detachment. It is taken as the only inference rule for the system.
It turns out that the set of tautologies arising from (1-3) and the one inference rule are just those formulas that always come out true in a truth-table check.
The appealing fact about this system is that arguments are not given by premises and conclusion, and so we don't have to muck about with rules concerning assumptions in force, conditional proofs or discharging. Proofs are left much simpler.
For instance, we can prove that ¬p → (p → q) as follows:
Substitute (¬q → ¬p) → (p → q) for φ and ¬p for ψ in 1, and substitute q for φ and p for ψ in 3. Apply modus ponens to the pair to give the tautology:
4) ¬p → [(¬q → ¬p) → (p → q)]
Substitute ¬p for φ and ¬q for ψ in 1 to obtain
5) ¬p → (¬q → ¬p)
Substitute ¬p for φ, ¬q → ¬p for ψ and p → q for χ in 2, to obtain
6) [¬p → [(¬q → ¬p) → (p → q)]] → [¬p → (¬q → ¬p)] → [¬p → (p → q)]
Apply modus ponens to 4 and 6 to obtain
7) [¬p → (¬q → ¬p)] → [¬p → (p → q)]
Apply modus ponens to 5 and 7 to obtain
¬p → p → q.
So ¬p → p → q is a tautology. Contradictions imply anything.
If you add in a few axioms for dealing with universal quantifiers, and then add in the axioms of ZFC set theory, then you can find any theorem of classical mathematics just by repeatedly using modus ponens to the resulting formulas. No assumptions or premises are needed in any mathematical argument anywhere.
For any propositional formulas φ, ψ and χ, declare the following to be tautologies
1) φ → (ψ → φ)
2) [φ → (ψ → χ)] → [(φ → ψ) → (φ → χ)]
3) (¬φ → ¬ψ) → (ψ → φ)
Now declare that, for any tautology φ, and any tautology of the form φ → ψ, we can take ψ to be a tautology. This rule is sometimes called modus ponens, and sometimes detachment. It is taken as the only inference rule for the system.
It turns out that the set of tautologies arising from (1-3) and the one inference rule are just those formulas that always come out true in a truth-table check.
The appealing fact about this system is that arguments are not given by premises and conclusion, and so we don't have to muck about with rules concerning assumptions in force, conditional proofs or discharging. Proofs are left much simpler.
For instance, we can prove that ¬p → (p → q) as follows:
Substitute (¬q → ¬p) → (p → q) for φ and ¬p for ψ in 1, and substitute q for φ and p for ψ in 3. Apply modus ponens to the pair to give the tautology:
4) ¬p → [(¬q → ¬p) → (p → q)]
Substitute ¬p for φ and ¬q for ψ in 1 to obtain
5) ¬p → (¬q → ¬p)
Substitute ¬p for φ, ¬q → ¬p for ψ and p → q for χ in 2, to obtain
6) [¬p → [(¬q → ¬p) → (p → q)]] → [¬p → (¬q → ¬p)] → [¬p → (p → q)]
Apply modus ponens to 4 and 6 to obtain
7) [¬p → (¬q → ¬p)] → [¬p → (p → q)]
Apply modus ponens to 5 and 7 to obtain
¬p → p → q.
So ¬p → p → q is a tautology. Contradictions imply anything.
If you add in a few axioms for dealing with universal quantifiers, and then add in the axioms of ZFC set theory, then you can find any theorem of classical mathematics just by repeatedly using modus ponens to the resulting formulas. No assumptions or premises are needed in any mathematical argument anywhere.