Non-first-order-izability (NFO)
One of the curious phenomena of second-order logic is that some sentences cannot be translated from second-order to first-order logic, even when both logics agree about set theory. In a certain sense, second-order logic is more expressive than first-order logic, and also more abstractive. Specifically, it is more Felleisen-expressive and Shutt-abstractive.
Examples
| Metamath statement | Lojban bridi | Description |
|---|---|---|
| df-du | {go ko'a du ko'e gi ro bu'a zo'u ko'a .o ko'e bu'a} | definition of identity |
| ax-nat-ind | {ganai 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} | induction for natural numbers |