Paul Rubin <no.email at nospam.invalid> writes: > FORALL P. [ P(0) and P(n) -> P(n+1) ] Sorry, that was supposed to say FORALL P. [ (P(0) and P(n) -> P(n+1)) -> forall n. P(n) ] FORALL quantifies over formulas and forall quantifies over numbers. Maybe something is still missing from the above ;-).