The comment for [vgn-1] is a bit more inadequate

[wceusters]

  (cl:comment "Entity is either universal or particular, so not all are instantiated. Instead make a predicate 'entity' analogous to particular universal [vgn-1]"
    (forall (x)
     (if
      (exists (t)
       (or (instance-of x continuant t) (instance-of x occurrent t)))
      (entity x))))

This comment seems either to confuse the use of 'entity' in the BFO2020 ISO standard with 'thing' or 'entity' as top class in an OWL rendering of BFO, or doesn't do what it is supposed to do.

From the ISO standard:
3.2
universal
type
entity (3.1) that has indefinitely many instances (3.6)

3.6
instance
particular that instantiates some universal (3.2)

So I have honestly no idea what the axiom is supposed to be, but as written currently, the comment would better be phrased as: "All occurrents and continuants are entities".

[alanruttenberg]

That's a confusing one, I admit. A late fix to accommodate the definitions in the ISO standard and Barry's view of what entity means, which is not the same as the OWL entity. OWL entity means a particular and there's an issue proposing changing its name to that. Entity in BFO is either a universal or a particular.

3.1
entity
object
item that is perceivable or conceivable
Note 1 to entry: The terms ‘entity’ and ‘object’ are catch-all terms analogous to ‘something’. In terminology circles ‘object’ is commonly used in this way. In ontology circles, ‘entity’ and ‘thing’ are commonly used. See B.3.3.
[SOURCE: ISO 1087-1:2000]

3.2
class
general entity (3.1)
Note 1 to entry: In some ontology communities, all general entities are referred to as classes. In other ontology communities, a distinction is drawn between classes as the extensions of general entities (for example, as sets of instances) and the general entities themselves, sometimes referred to as ‘types’, ‘kinds’, or ‘universals’.

3.3
particular individual entity (3.1)
Note 1 to entry: In contrast to classes or types, particulars are not exemplified or instantiated by further entities.

Entities are divided into general and individual entities.

This make trouble for the verifying the OWL translation, and the comment reflects that. All of the OWL classes are universals in BFO (and hence instantiated) except entity, which needs to be translated to ____?

The solution, and I'm not sure I caught all the loose ends, was to translate entity to a predicate in terms that could be used in conjunction with other terms the domain of discourse of OWL, which doesn't include universals or the terms particular or universal. The axiom referred to is a necessary condition, and sufficient for the translation from OWL.

Apparently I didn't add universal x -> entity x, which would be true.

I didn't add that entity is covered by universal and particular. Because I was leaving open a future in which entity meant portion of reality. As you can see from one of our recent conversations, I have no idea how Barry decides one thing is an entity and another not. Seems to me that all portions of reality are "conceivable" in the sense of definition 3.1. It's not clear to me whether universals fall under the "conceivable" or "perceivable" categories.

There's a proposal in one of the issues that entity be changed to particular in the OWL, but even that is weird since it also instantiated. A better solution might be for there to be no entity "superclass" in OWL, so OWL classes are all either universal or defined classes, or to simply ignore (and document) that the two OWL axioms that involve entity are meaningless and remove them from the set of axioms I try to prove to validate the OWL.

Bleh.

[wceusters]

I'm glad you agree that the vegan axiom is inadequate.