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.
Identity
As a classic and powerful first example, we can give a redefinition of {du}
in NFOL terms.
ro da ro de zo'u:
da du de
========================== (id-def)
ro bu'a zo'u da .o de bu'a
This rule is a second-order definition; such rules are not possible within
first-order logic. There are many reasons to justify this sort of explanation
as a definition, but the primary reason is that they could be entered into
Lojban dictionaries. For example, we could define {du}
as:
ro bu'a zo'u x₁ .o x₂ bu'a
And give any tautology, like (id-refl)
, as an example:
ro da zo'u da du da
Once so defined, {du}
is technically not in terms of any particular
selbri; rather, it is a global property of all selbri!
Natural numbers
We can give the induction principle for natural numbers with SO quantifiers.
ro bu'a zo'u:
ge li no bu'a gi ro da su'o de zo'u da na.a de bu'a .ije da kacli'e de
---------------------------------------------------------------------- (kacna'u-ind)
ro da zo'u da kacna'u nagi'a bu'a