Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  ax-nat-ind

Axiom ax-nat-ind 594
Description: The induction axiom for second-order arithmetic. To accomodate higher-order relations, the selbri parameter is generalized to a brirebla.
Assertion
Ref Expression
ax-nat-indganai ge li no bo'a gi ro da poi ke'a bo'a ku'o zo'u su'o de zo'u ge da kacli'e de gi de bo'a gi ro da poi ke'a kacna'u ku'o zo'u da bo'a
Distinct variable group:   da , de

This axiom is referenced by:  nat-indi  595  nat-ind-cur  597
  Copyright terms: Public domain W3C validator