[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[lojban] Difficult logical questions



coi

I apologize somewhat in advance. The following questions have driven folks mad (mostly on IRC, but also sometimes IRL), so don't worry if you're not interested in them. However, they all seem extremely pertinent to continued formalization efforts, and I'd like to think that they've come up before. I also have rigged the game somewhat by having an answer for each question, which I'll provide; however, I'm very interested in what answers other folks have, and I am only committed to my answers inasmuch as I have researched them in order to have a well-read opinion.

Relations are, generally, sets. In particular they are subsets of products. Even more particularly, nullary relations are truth values and unary relations are sets. However, ckaji2 ranges over all unary relations and ckini3 ranges over all binary relations; kampu2, cmima2, and steci3 range over (almost) all sets. This leads to immediate size issues; how do we avoid Russell's paradox?

My answer is to declare an inaccessible cardinal, which is like a cornerstone that can be used to build a "small" set theory. This cardinal can be big enough to give us enough room for not just ZF set theory, but any small category or similar structure. The downside is that we are immediately cut off from some large objects; however, we weren't using them anyway. However, we are given a very flexible universe of things; we are free to accept the Axiom of Choice, or not; we can also choose whether to accept the Law of Excluded Middle.

CLL Lojban allows quantification ranging over two orders of variables; {da} range over things, while {bu'a} range over relations between things. This is syntax for second-order logic (SOL). However, many speakers, including myself, infer an informal type system which constrains each {da} to range only over some set of things which isn't the set of all things in the universe. (To clarify this sentence, solve our size issues.) When all things are constrained in this way, then it happens that second-order logic becomes many-sorted first-order logic; every "set of things" becomes its own type in a sort of types of sets. Is Lojban second-order, or many-sorted first-order?

My answer is to embrace full SOL. The main tradeoff to consider is that full second-order semantics often give categoricity, which means that things can be specified up to isomorphism, but are Gödel-incomplete; while first-order semantics can be Gödel-complete, but usually admits non-standard models of any infinite thing. For example, the natural numbers are categorical, which means that there is a second-order theory (known as Z₂) which uniquely identifies them. In modern category-theoretic language, we say that a natural numbers object, or NNO, is unique when it exists. In both cases, the uniqueness is up to the bounding rules of the universe of sets. We can, of course, recover fragments of first-order reasoning at any time by simply putting extra {poi} onto our {da}, and we can mechanically send SOL to FOL with some choice of type-inference algorithm.

Also, like, "the cat is red," is it a cat or a red? SOL lets us just say that it's a thing which is both among the set of cats and also among the set of reds, while FOL requires us to informally infer types and say that it's a cat.

CLL gives full-throated support for the Law of Excluded Middle (LEM), with a rule which sends {na na broda} => {broda}. This happens to be equivalent to a complete buy-in to the world of Boolean reasoning, and there are examples of this embrace throughout Lojban. {nagi'a} is mistaken for implication, for example, despite merely having the same truth table in the Booleans; {steci} manifests the Axiom of Choice in one direction with steci1 empty, or LEM with steci2 empty. To be fair, it's reasonable to imagine that, since a unary relation is a set, surely a thing either is or is not an element of a unary relation. But, over the past century, we've found that LEM is not realizeable/computable. {le du'u nei jitfa} (or whatever equivalent one (in)formally desires to work with) doesn't have a consistent truth value. So do we keep LEM?

My answer is kind of biased, isn't it? I'm a constructivist of sorts, so I'm going to prefer it if LEM is optional. It can always be added in on a per-proof basis in order to tighten up some reasoning. But this also requires trading in De Morgan's laws and negation-raising through the prenex for weaker constructive versions.

Oh, also, the inaccessible-cardinal construction I used earlier gives us a topos, but not necessarily a Boolean topos; if we have a set of things, we can't form the set of all things in the universe which are't in our original set, because we can't see from inside the topos that the universe's things might all fit into a set.

To be a bit more clear, we could still have {na na na broda} <=> {na broda}. There would still only be two truth values. We simply would be a bit more honest about when we can't tell which of the two truth values we're supposed to assign.

I hope that this was useful food for thought for the multiple folks working on different formalizations, since I think that everybody will need to answer these questions one way or another.

And finally, I should include preliminary feedback from IRC. Folks were generally supportive of the first two points, but preferred not giving up LEM. There were strong and serious concerns about contextuality vs. modal possibility and the domain of discourse vs. the universe of things; folks don't want Lojban to be artificially limited. In general, I'm finding that that one quote from a decade ago is true, about how formalization is a political process even when the maths is well-settled.

.i mi'e la korvo .i di'ai

--
You received this message because you are subscribed to the Google Groups "lojban" group.
To unsubscribe from this group and stop receiving emails from it, send an email to lojban+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/lojban/676db32f-fdd7-479f-825e-4571293b08a1o%40googlegroups.com.