Handle undecidable properties as assignments

DATABASE.md

@@ -33,7 +33,6 @@ Further tables are:
 - `special_morphisms`
 - `related_category_properties`
 - `category_comments`
-- `category_property_comments`
 
 For functors there are similar tables, such as:
 

databases/catdat/data/categories/FreeAb.yaml

@@ -57,9 +57,9 @@ unsatisfied_properties:
   - property: ℵ₁-filtered colimits
     reason: It is shown in <a href="https://mathoverflow.net/questions/511426" target="_blank">MO/511426</a> that the $\aleph_1$-filtered diagram of countable subgroups of $\IZ^{\IN}$ does not have a colimit in $\FreeAb$.
 
-category_property_comments:
+undecidable_properties:
   - property: accessible
-    comment: The question if this category is accessible is undecidable in ZFC. See <a href="https://math.stackexchange.com/questions/720885" target="_blank">MSE/720885</a>.
+    reason: The question if this category is accessible is undecidable in ZFC. See <a href="https://math.stackexchange.com/questions/720885" target="_blank">MSE/720885</a>.
 
 special_objects:
   initial object:

databases/catdat/data/categories/M-Set.yaml

@@ -31,9 +31,9 @@ unsatisfied_properties:
   - property: trivial
     reason: This is trivial.
 
-category_property_comments:
+undecidable_properties:
   - property: semi-strongly connected
-    comment: If this category is semi-strongly connected depends on the choice of $M$. For $M = 1$ it is, for $M = \IZ$ it is not. In general, if $G$ is a group, then $G{-}\Set$ is semi-strongly connected if and only if for all subgroups $H,K \subseteq G$, $H$ is subconjugated to $K$ or $K$ is subconjugated to $H$. If $G$ is abelian, this means that the poset of subgroups is linear, in which case $G$ is either isomorphic to $\IZ/p^n$ or to $\IZ/p^{\infty}$ for a prime $p$. See also <a href="https://math.stackexchange.com/questions/5129804" target="_blank">MSE/5129804</a>.
+    reason: If this category is semi-strongly connected depends on the choice of $M$. For $M = 1$ it is, for $M = \IZ$ it is not. In general, if $G$ is a group, then $G{-}\Set$ is semi-strongly connected if and only if for all subgroups $H,K \subseteq G$, $H$ is subconjugated to $K$ or $K$ is subconjugated to $H$. If $G$ is abelian, this means that the poset of subgroups is linear, in which case $G$ is either isomorphic to $\IZ/p^n$ or to $\IZ/p^{\infty}$ for a prime $p$. See also <a href="https://math.stackexchange.com/questions/5129804" target="_blank">MSE/5129804</a>.
 
 special_objects:
   initial object:

databases/catdat/schema/004_category-properties.sql

@@ -23,8 +23,9 @@ CREATE TABLE category_property_assignments (
     id INTEGER PRIMARY KEY,
     category_id TEXT NOT NULL,
     property_id TEXT NOT NULL,
-    is_satisfied INTEGER NOT NULL
-        CHECK (is_satisfied in (TRUE, FALSE)),
+    is_satisfied INTEGER
+        -- we use NULL for undecidable properties
+        CHECK (is_satisfied in (TRUE, FALSE, NULL)),
     reason TEXT NOT NULL CHECK (length(reason) > 0),
     is_deduced INTEGER NOT NULL DEFAULT FALSE
         CHECK (is_deduced in (TRUE, FALSE)),

databases/catdat/schema/010_functor-properties.sql

@@ -15,8 +15,9 @@ CREATE TABLE functor_property_assignments (
     id INTEGER PRIMARY KEY,
     functor_id TEXT NOT NULL,
     property_id TEXT NOT NULL,
-    is_satisfied INTEGER NOT NULL
-        CHECK (is_satisfied IN (TRUE, FALSE)),
+    is_satisfied INTEGER
+        -- we use NULL for undecidable properties
+        CHECK (is_satisfied in (TRUE, FALSE, NULL)),
     reason TEXT NOT NULL CHECK (length(reason) > 0),
     is_deduced INTEGER NOT NULL DEFAULT FALSE
         CHECK (is_deduced in (TRUE, FALSE)),

databases/catdat/scripts/deduce-entity-properties.ts

@@ -299,15 +299,17 @@ function deduce_unsatisfied_properties(
 /**
  * Assign dual properties to dual entities:
  * If C has property P, then C^op has property P^op (if defined).
- * Warning: This mutates the sets of satisfied and unsatisfied properties.
+ * Warning: This mutates the sets of assigned properties.
  */
 function deduce_dual_properties(
 	db: Database,
 	entity: EntityMeta & { dual: string },
 	satisfied: Set<string>,
 	unsatisfied: Set<string>,
+	undecidable: Set<string>,
 	dual_satisfied: Set<string>,
 	dual_unsatisfied: Set<string>,
+	dual_undecidable: Set<string>,
 	properties_dict: Record<string, PropertyMeta>,
 	type: 'category',
 ) {
@@ -329,14 +331,24 @@ function deduce_dual_properties(
 		unsatisfied.add(p_dual)
 	}
 
+	const new_undecidable = new Set<string>()
+
+	for (const p of dual_undecidable) {
+		const p_dual = properties_dict[p].dual
+		if (!p_dual || undecidable.has(p_dual)) continue
+		new_undecidable.add(p_dual)
+		undecidable.add(p_dual)
+	}
+
 	const property_insert = db.prepare(`
 		INSERT INTO ${type}_property_assignments
 			(${type}_id, property_id, is_satisfied, reason, is_deduced)
 		VALUES (?, ?, ?, ?, TRUE)
 	`)
 
-	const reason_satisfied = 'Its dual ${type} satisfies the dual property.'
-	const reason_unsatisfied = 'Its dual ${type} does not satisfy the dual property.'
+	const reason_satisfied = `Its dual ${type} satisfies the dual property.`
+	const reason_unsatisfied = `Its dual ${type} does not satisfy the dual property.`
+	const reason_undecidable = `The dual property is undecidable for its dual ${type}.`
 
 	for (const p of new_satisfied) {
 		property_insert.run(entity.id, p, 1, reason_satisfied)
@@ -353,6 +365,14 @@ function deduce_dual_properties(
 	console.info(
 		`Deduced ${new_unsatisfied.size} unsatisfied properties by duality for ${entity.id}`,
 	)
+
+	for (const q of new_undecidable) {
+		property_insert.run(entity.id, q, null, reason_undecidable)
+	}
+
+	console.info(
+		`Deduced ${new_undecidable.size} undecidable properties by duality for ${entity.id}`,
+	)
 }
 
 /**
@@ -375,19 +395,19 @@ export function deduce_properties_for_entities(type: 'category' | 'functor') {
 	const implications = get_normalized_implications(db, type)
 	const entities = get_entities(db, type)
 	const properties_dict = get_properties_dict(db, type)
-	const all_decided_properties = get_property_assignments(db, entities, type)
+	const get_assigned_properties = get_property_assignments(db, entities, type)
 
 	const deduction = db.transaction(() => {
 		delete_deduced_properties(db, type)
 
 		for (const entity of entities) {
-			const decided = all_decided_properties[entity.id]
+			const assigned = get_assigned_properties[entity.id]
 
 			deduce_satisfied_properties(
 				db,
 				entity,
 				implications,
-				decided.satisfied,
+				assigned.satisfied,
 				properties_dict,
 				type,
 			)
@@ -396,8 +416,8 @@ export function deduce_properties_for_entities(type: 'category' | 'functor') {
 				db,
 				entity,
 				implications,
-				decided.satisfied,
-				decided.unsatisfied,
+				assigned.satisfied,
+				assigned.unsatisfied,
 				properties_dict,
 				type,
 			)
@@ -413,16 +433,18 @@ export function deduce_properties_for_entities(type: 'category' | 'functor') {
 		for (const entity of entities) {
 			if (!is_dual_entity(entity)) continue
 
-			const decided = all_decided_properties[entity.id]
-			const dual_decided = all_decided_properties[entity.dual]
+			const assigned = get_assigned_properties[entity.id]
+			const dual_assigned = get_assigned_properties[entity.dual]
 
 			deduce_dual_properties(
 				db,
 				entity,
-				decided.satisfied,
-				decided.unsatisfied,
-				dual_decided.satisfied,
-				dual_decided.unsatisfied,
+				assigned.satisfied,
+				assigned.unsatisfied,
+				assigned.undecidable,
+				dual_assigned.satisfied,
+				dual_assigned.unsatisfied,
+				dual_assigned.undecidable,
 				properties_dict,
 				type,
 			)
@@ -431,7 +453,7 @@ export function deduce_properties_for_entities(type: 'category' | 'functor') {
 				db,
 				entity,
 				implications,
-				decided.satisfied,
+				assigned.satisfied,
 				properties_dict,
 				type,
 			)
@@ -440,8 +462,8 @@ export function deduce_properties_for_entities(type: 'category' | 'functor') {
 				db,
 				entity,
 				implications,
-				decided.satisfied,
-				decided.unsatisfied,
+				assigned.satisfied,
+				assigned.unsatisfied,
 				properties_dict,
 				type,
 			)

databases/catdat/scripts/seed.ts

@@ -73,7 +73,6 @@ function clear_all_data() {
 			db.prepare(`DELETE FROM special_objects`).run()
 			db.prepare(`DELETE FROM special_object_types`).run()
 
-			db.prepare(`DELETE FROM category_property_comments`).run()
 			db.prepare(`DELETE FROM category_property_assignments`).run()
 
 			db.prepare(`DELETE FROM category_comments`).run()
@@ -187,11 +186,6 @@ function seed_categories() {
 		) VALUES (?, ?, ?, ?, ?)`,
 	)
 
-	const property_comment_insert = db.prepare(`
-		INSERT INTO category_property_comments (
-			category_id, property_id, comment
-		) VALUES (?, ?, ?)`)
-
 	function insert_category(category: CategoryYaml) {
 		category_insert.run(
 			category.id,
@@ -251,11 +245,13 @@ function seed_categories() {
 			)
 		}
 
-		for (const comment_obj of category.category_property_comments ?? []) {
-			property_comment_insert.run(
+		for (const entry of category.undecidable_properties ?? []) {
+			property_assignment_insert.run(
 				category.id,
-				comment_obj.property,
-				comment_obj.comment,
+				entry.property,
+				null,
+				entry.reason,
+				entry.check_redundancy === false ? 0 : 1,
 			)
 		}
 	}

databases/catdat/scripts/seed.types.ts

@@ -28,13 +28,10 @@ export type CategoryYaml = {
 	related_categories: string[]
 	satisfied_properties: PropertyEntry[]
 	unsatisfied_properties: PropertyEntry[]
+	undecidable_properties?: PropertyEntry[]
 	special_objects: Record<string, ObjectEntry | undefined>
 	special_morphisms: Record<string, MorphismEntry | undefined>
 	comments?: string[]
-	category_property_comments?: {
-		property: string
-		comment: string
-	}[]
 }
 
 type PropertyEntry = {

databases/catdat/scripts/test.ts

@@ -150,14 +150,15 @@ function test_decided_entities(entities: string[], type: 'category' | 'functor')
  * Tests if selected categories or functors behave as expected:
  * All of their properties in the database have to match those in the
  * respective JSON files in the subfolder "expected-data".
+ * We exclude undecidable properties here.
  */
 function test_properties_of_selected_entities(
 	expected: Record<string, Record<string, boolean>>,
 	type: 'category' | 'functor',
 ) {
 	const property_query = db.prepare(
 		`SELECT property_id, is_satisfied FROM ${type}_property_assignments
-		WHERE ${type}_id = ?`,
+		WHERE ${type}_id = ? AND is_satisfied IS NOT NULL`,
 	)
 
 	for (const entity_id in expected) {

databases/catdat/scripts/utils/deduction.ts

@@ -74,7 +74,8 @@ export function get_properties_dict(db: Database, type: 'category' | 'functor')
 
 /**
  * Returns a dictionary with all assigned properties of a list of entities
- * (categories or functors), grouped by id and value (satisfied / unsatisfied).
+ * (categories or functors), grouped by id and
+ * value (satisfied / unsatisfied / undecidable).
  */
 export function get_property_assignments(
 	db: Database,
@@ -86,18 +87,32 @@ export function get_property_assignments(
 			`SELECT property_id, ${type}_id as entity_id, is_satisfied
 			FROM ${type}_property_assignments`,
 		)
-		.all() as { property_id: string; entity_id: string; is_satisfied: 0 | 1 }[]
+		.all() as { property_id: string; entity_id: string; is_satisfied: 0 | 1 | null }[]
 
-	const grouped: Record<string, { satisfied: Set<string>; unsatisfied: Set<string> }> =
-		{}
+	const grouped: Record<
+		string,
+		{ satisfied: Set<string>; unsatisfied: Set<string>; undecidable: Set<string> }
+	> = {}
 
 	for (const entity of entities) {
-		grouped[entity.id] = { satisfied: new Set(), unsatisfied: new Set() }
+		grouped[entity.id] = {
+			satisfied: new Set(),
+			unsatisfied: new Set(),
+			undecidable: new Set(),
+		}
 	}
 
 	for (const row of rows) {
 		const { property_id, entity_id, is_satisfied } = row
-		grouped[entity_id][is_satisfied ? 'satisfied' : 'unsatisfied'].add(property_id)
+		let group_key: 'satisfied' | 'unsatisfied' | 'undecidable'
+		if (is_satisfied === 1) {
+			group_key = 'satisfied'
+		} else if (is_satisfied === 0) {
+			group_key = 'unsatisfied'
+		} else {
+			group_key = 'undecidable'
+		}
+		grouped[entity_id][group_key].add(property_id)
 	}
 
 	return grouped
@@ -106,6 +121,7 @@ export function get_property_assignments(
 /**
  * Returns a dictionary with all assigned properties of entities,
  * grouped by entity, value (satisfied / unsatisfied), and deduced status.
+ * We exclude undecidable properties here.
  */
 export function get_property_assignments_by_deduction(
 	db: Database,
@@ -115,7 +131,7 @@ export function get_property_assignments_by_deduction(
 	const rows = db
 		.prepare(
 			`SELECT property_id, ${type}_id as entity_id, is_satisfied, is_deduced
-			FROM ${type}_property_assignments`,
+			FROM ${type}_property_assignments WHERE is_satisfied IS NOT NULL`,
 		)
 		.all() as {
 		property_id: string

src/components/PropertyList.svelte

@@ -9,17 +9,16 @@
 			reason?: string | null
 		}[]
 		type: 'category' | 'functor'
-		reason_heading?: string
 	}
 
-	let { properties, type, reason_heading }: Props = $props()
+	let { properties, type }: Props = $props()
 </script>
 
 {#if properties.length}
 	<ul>
 		{#each properties as { id, relation, reason }}
 			<li>
-				<TextWithReason {reason} heading={reason_heading}>
+				<TextWithReason {reason}>
 					{relation}
 					<a href={get_property_url(id, type)}>{id}</a>
 				</TextWithReason>

src/components/TextWithReason.svelte

@@ -7,18 +7,17 @@
 	type Props = {
 		children: Snippet
 		reason?: string | null
-		heading?: string
 	}
 
-	let { children, reason, heading = 'Reason' }: Props = $props()
+	let { children, reason }: Props = $props()
 
 	const id = $props.id()
 
 	function show_reason(e: MouseEvent) {
 		e.stopPropagation()
 		show_popup({
 			id,
-			heading,
+			heading: 'Reason',
 			text: reason!,
 		})
 	}