History: Axiom of stratified comprehension--Mekso example

Source of version: 14 (current)

The below is a translation, possibly with some errors, of the axiom schema of stratified comprehension, a core axiom of New Foundations, an axiomatic set theory. The axiom reads as follows: A predicate P is said to be ''stratified'' if and only if there exists a function f from the arguments of P to the natural numbers such that for all sets S1 and S2, if S1 is a member of S2, then f(S2) = f(S1)+1, and if S1=S2, then f(S1)=f(S2). For all stratified predicates P, the set {x : P(x)} exists. In mekso, this reads: .i ca'e ro da poi ke'a selbri zo'u go da cmaci multersenta gi ge de fancu lo'i terbri be da le'i zmamulna'u gi ro di ro da xi re zo'u ge va'o lo du'u di cmima da xi re kei li na'u me de mo'e da xi re du li na'u me de mo'e di su'i pa gi va'o lo du'u di du da xi re kei li na'u me de mo'e di du li na'u me de mo'e da xi re .i ca'e ro bu'a zo'u lo'i bu'a cu zasti va'o lo du'u la'e zo bu'a cu multersenta The below is the same passage in bridi math. fancrnaplai is a placeholder defined as .i ko'a fancrnaplai ko'e ko'i ko'o ... .ijo ko'a = ko'e(ko'i,ko'o,...) .i ca'e ro da poi ke'a selbri zo'u go da cmaci multersenta gi ge de fancu lo'i terbri be da le'i zmamulna'u gi ro di ro da xi re zo'u ge va'o lo du'u di cmima da xi re kei lo ni'ai fancrnaplai de da xi re cu sumji li pa lo ni'ai fancrnaplai de di gi va'o lo du'u di du da xi re kei lo ni'ai fancrnaplai de di cu du lo ni'ai fancrnaplai de da xi re .i ca'e ro bu'a zo'u lo'i bu'a cu zasti va'o lo du'u la'e zo bu'a cu multersenta In bridi math with [http://www.lojban.org/tiki/BPFK+Section%3A+Pro-bridi|{me'au} and {me'ei}]: .i ca'e ro me'ei bu'a zo'u go me'ei bu'a cu cmaci multersenta gi ge me'ei bu'e cu fancu lo'i terbri be me'ei bu'a le'i zmamulna'u gi ro da ro de zo'u ge va'o gi da cmima de gi lo bu'e be de cu sumji li pa lo bu'e be da gi va'o gi da du de gi lo bu'e be da cu du lo bu'e be de .i ca'e ro me'ei bu'a poi ke'a multersenta zo'u lo'i bu'a cu zasti (In the last example, we adopt the convention, by analogy to sumji etc., x1 = f(x2,x3,...), so that {lo broda be ko'a bei ko'e} is f(ko'a,ko'e))