In debugging why the Right thalamus isn't inferred to be (always) part
of some Brain in my setup, I realize there might be some ambiguity in
the FMA about the thalamus.
Specifically, I think the answer is that there are two fma:Thalamus,
the left and right, which are subclasses of Thalamus. Most of their
parts that are asserted as part of the thalamus (which inherit to the
right and left) are bilateralized as one would expect.
The only exception is the second partition into allothalamus and
isothalamus. If I understand things correctly those they could be bilaterally
differentiated as well, but are not at the moment.
The thalamus is asserted to be regional part of the diencephalon.
The Thalamic complex has parts Left thalamus, Right Thalamus, and the
Interthalamic adhesion. This looks like an exhaustive partition. It
isn't part of anything, leaving the Interthalamic adhesion an orphan.
I think it might be clearer to have the Thalamic complex be part of
the diencephalon. Then it would be clear that next level of component
below diencephalon is the thalamic complex. Not asserting diencephalon
having part thalamus might also cause less possibility for confusion
between thalamus and thalamic complex. The left and right would be
inferred to be part of the diencephalon because the they are part of
the thalamic complex.
There is a general issue when one has the pattern
<non-bilateral> (e.g. diencephalon)
has_part <superclass of bilateral> (e.g. thalamus)
<left> (e.g. left thalamus)
<right> (e.g. right thalamus)
which is that we don't know (from the axioms) whether the
<non-bilateral> has both or only one of the <left> and <right>.
The all-some axiom is: ALL <non-bilateral> has_part some SOME
This is satisfied by it having either a <left> or a <right>. (think of
tool that is manufactered in left and right hand versions - some parts
are in common to both, and some are specialized to right and left, but
there would be only one of left or right).
Even if we have the inverses - that ALL <left> is part of SOME
<non-bilateral>, and ALL <right> is part of SOME <non-bilateral> we
still have a situation in which having a single <left> or <right> would
satisfy the axioms.
I am thinking that what I should do is just recognize the pattern and add axioms