ax-nat-ind - brismu bridi

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

Axiom ax-nat-ind 490

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-ind	⊢ ganai ge li 0 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 491 nat-ind-cur 493

W3C validator