How to handle undecidable properties?

[ScriptRaccoon]

ykawase5048 mentioned the following (in #59):

There is a very interesting issue: It is independent of our foundation, ZFC with two Grothendieck universes, whether the category of free abelian groups is accessible; see [Makkai-Pare, Section5.5] or MathStackExchange. So, we would need to add the third option "undecidable" for properties.

Let's discuss about this here and then come up with a decision.

Some random thoughts at this moment:

1. How often does this happen? When it is rare, I am not up for changing the whole database model and the application logic.
2. On the other hand, there are also other properties that are not boolean valued. For example, what is the center of a category? It is a (large) monoid. The center is not true or false.
3. What about keeping these properties as unknown but leave a comment (database/data/001_categories/200_comments.sql) about its undecidability on the category detail page? Advantage: the infra is already there. Disadvantage: no formal distinction between unknown and undecidable properties. Also: the user needs to scroll down to see if something is undecidable. Maybe they don't even know that there is a comment section.
4. If there are models where it is false, mark the property as false, but in the proof mention that this depends on the model of ZFC. Or .... If there are models where it is true, mark the property as true, but in the proof mention that this depends on the model of ZFC.
5. It is now useful that I have refactored the category property assignments before into one table (these were two tables before), where basically each pair (category, property) gets a value is_satisfied of type boolean. We could add a new column called value which has a more generic type, rewrite the whole application (...), and then remove the is_satisfied column.

[ykawase5048]

Whenever we know that a property is independent of our foundation, we typically also know both a model in which it is true and a model in which it is false. So, the option 4 does not applicable, does it?

[ScriptRaccoon]

The idea of 4 is to have a bias what "satisfied" or "unsatisfied" means. Personally, I think it makes sense to define "satisfied" as "true in every model". If we then define "unsatisfied" as "not true in every model", undecidable properties will go there - accompanied with a comment as mentioned.

PS: I am not saying that 4 is the best solution. I was "thinking out loud".

[diracdeltafunk]

My personal take is that this situation is rare, and it's fine to use option 3.

As for properties of categories that are not propositions, I think it makes more sense for this to be a separate thing, the same way "special morphisms" are handled.