Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Tue, 02 Apr 2024 19:04:01 -0700
Sender: lojban@googlegroups.com
Date: Tue, 2 Apr 2024 19:03:54 -0700 (PDT)
From: Corbin Simpson <mostawesomedude@gmail.com>
To: lojban <lojban@googlegroups.com>
Message-Id: <e4027bb2-42da-4745-aea1-ce412bea587fn@googlegroups.com>
Subject: [lojban] Baseline Lojban is 3% defined, 12% ontologized
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_199092_1533033137.1712109834882"
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -4.9
X-Spam_score_int: -48
X-Spam_bar: ----

------=_Part_199092_1533033137.1712109834882
Content-Type: multipart/alternative; 
	boundary="----=_Part_199093_2017294838.1712109834882"

------=_Part_199093_2017294838.1712109834882
Content-Type: text/plain; charset="UTF-8"

coi lo se kansa,

Here -- *after* April 1st -- is my annual status update.

I have continued to sporadically work towards formalizing Lojban. My 
project now includes *ontology*, the structuring of relations relative to 
each other. To make this manageable at scale, I have used my poset editor 
tool [0] to generate several diagrams, included those diagrams into the 
book when small or illustrative, and also compiled the data in the diagrams 
into Metamath axioms. For a taste of the result, see [1]. As a result, we 
are now 15% formalized, with 3% as dictionary-ready definitions and 12% 
belonging to an ontological class; for a breakdown by selma'o, see [4].

The main highlight since my last update is the inclusion of {pagbu} as the 
*mereology* relation. I am hoping that we can have a pluralist multiverse 
of axioms when it comes to mereology and set theory; in the future, we may 
give an optional bridge which allows mereologists to translate their 
theorems to sets for free. If any mereologists find this interesting, 
please read the axioms and definitions at [4] and let me know whether 
they're strong enough for you.

Instead of mathboxes or multiple-file databases, I've started directly 
encoding assorted baseline claims about various selbri. I hope that this 
will eventually be a third source of formal claims. For example, {mintu} 
has a symmetry from its definition [5] and {dunli} has one from its modal 
{du'i} definition [6]. This lets me get around the problem that these two 
example selbri have been impossible to convincingly define; their 
properties can be prior to {go} logical expansions or {ganai} extensions.

[0] https://github.com/MostAwesomeDude/zaha/
[1] https://mostawesomedude.github.io/brismu/mmtheorems5.html
[2] https://en.wikipedia.org/wiki/Olog
[3] https://mostawesomedude.github.io/brismu/foreword.html
[4] https://mostawesomedude.github.io/brismu/mmtheorems4.html#mm336b
[5] https://mostawesomedude.github.io/brismu/ax-mintu-sym.html
[6] https://mostawesomedude.github.io/brismu/ax-dunli-sym.html

To the LFK:
* Please meet annually.
* I wish to propose some definitions for a future dictionary project. To 
that end, I would like to discuss up to 75 currently-formalized valsi at a 
venue of your choice.
* Oh, unless it's Discord. Nothing personal, but I can't participate there.
* We actually need to talk about what a definition *is*. Does it have to 
start with {go}? Can we do {ge} or {ganai}?
* I have *so many* tiny notes that I'd love to discuss, if you're 
interested. Turns out second-order logic is *really* powerful, and there 
are lots of nuances that I'm taking lots of time to ponder. Your judgement 
could speed things up.
* Also, I'd like some feedback on the project and how it's informing your 
plans. In particular, I want better metavariables and also to bless my 
lujvo. I also want to know if you'd like to adopt a standard/recommended 
format for these sorts of "ontology logs" [2] to store ontological data.

di'ai,
~ C.

-- 
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/e4027bb2-42da-4745-aea1-ce412bea587fn%40googlegroups.com.

------=_Part_199093_2017294838.1712109834882
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

coi lo se kansa,<br /><br />Here -- *after* April 1st -- is my annual statu=
s update.<br /><br />I have continued to sporadically work towards formaliz=
ing Lojban. My project now includes *ontology*, the structuring of relation=
s relative to each other. To make this manageable at scale, I have used my =
poset editor tool [0] to generate several diagrams, included those diagrams=
 into the book when small or illustrative, and also compiled the data in th=
e diagrams into Metamath axioms. For a taste of the result, see [1]. As a r=
esult, we are now 15% formalized, with 3% as dictionary-ready definitions a=
nd 12% belonging to an ontological class; for a breakdown by selma'o, see [=
4].<br /><br />The main highlight since my last update is the inclusion of =
{pagbu} as the *mereology* relation. I am hoping that we can have a plurali=
st multiverse of axioms when it comes to mereology and set theory; in the f=
uture, we may give an optional bridge which allows mereologists to translat=
e their theorems to sets for free. If any mereologists find this interestin=
g, please read the axioms and definitions at [4] and let me know whether th=
ey're strong enough for you.<br /><br />Instead of mathboxes or multiple-fi=
le databases, I've started directly encoding assorted baseline claims about=
 various selbri. I hope that this will eventually be a third source of form=
al claims. For example, {mintu} has a symmetry from its definition [5] and =
{dunli} has one from its modal {du'i} definition [6]. This lets me get arou=
nd the problem that these two example selbri have been impossible to convin=
cingly define; their properties can be prior to {go} logical expansions or =
{ganai} extensions.<br /><br />[0] https://github.com/MostAwesomeDude/zaha/=
<br />[1] https://mostawesomedude.github.io/brismu/mmtheorems5.html<br />[2=
] https://en.wikipedia.org/wiki/Olog<br /><div>[3] https://mostawesomedude.=
github.io/brismu/foreword.html</div><div>[4] https://mostawesomedude.github=
.io/brismu/mmtheorems4.html#mm336b<br />[5] https://mostawesomedude.github.=
io/brismu/ax-mintu-sym.html<br />[6] https://mostawesomedude.github.io/bris=
mu/ax-dunli-sym.html</div><br />To the LFK:<br />* Please meet annually.<br=
 />* I wish to propose some definitions for a future dictionary project. To=
 that end, I would like to discuss up to 75 currently-formalized valsi at a=
 venue of your choice.<br />* Oh, unless it's Discord. Nothing personal, bu=
t I can't participate there.<br />* We actually need to talk about what a d=
efinition *is*. Does it have to start with {go}? Can we do {ge} or {ganai}?=
<br />* I have *so many* tiny notes that I'd love to discuss, if you're int=
erested. Turns out second-order logic is *really* powerful, and there are l=
ots of nuances that I'm taking lots of time to ponder. Your judgement could=
 speed things up.<br />* Also, I'd like some feedback on the project and ho=
w it's informing your plans. In particular, I want better metavariables and=
 also to bless my lujvo. I also want to know if you'd like to adopt a stand=
ard/recommended format for these sorts of "ontology logs" [2] to store onto=
logical data.<br /><br />di'ai,<br />~ C.<br />

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;lojban&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:lojban+unsubscribe@googlegroups.com">lojban+unsub=
scribe@googlegroups.com</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/d/msgid/lojban/e4027bb2-42da-4745-aea1-ce412bea587fn%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/e4027bb2-42da-4745-aea1-ce412bea587fn%40googlegroups.com</a>.<br />

------=_Part_199093_2017294838.1712109834882--

------=_Part_199092_1533033137.1712109834882--