ax-succ-std - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > ax-succ-std

Axiom ax-succ-std 494

Description: There are no non-standard natural numbers. This axiom upgrades our arithmetic from BA, "baby arithmetic", to Robinson's Q. This is Robinson axiom 3.

**Assertion**
Ref	Expression
ax-succ-std	⊢ ro da poi ke'a kacna'u ku'o zo'u ga da du li 0 gi su'o de zo'u de kacli'e da

Distinct variable group: da ,de

This axiom is referenced by: (None)

W3C validator