Add "undecidable" truth value

packages/compile/src/validations.ts

@@ -262,7 +262,7 @@ export function trait(input: File) {
       uid: String(uid).trim(),
       space: String(space).trim(),
       property: String(property).trim(),
-      value: Boolean(value),
+      value: value === 'undecidable' ? 'undecidable' : Boolean(value),
       counterexamples_id,
       refs,
       description: String(description).trim(),
@@ -275,7 +275,7 @@ export function trait(input: File) {
     required(trait, 'space', error)
     required(trait, 'property', error)
     required(trait, 'value', error)
-    required(trait, 'description', error)
+    // description is optional for traits
     noExtras(rest, error)
 
     return trait

packages/core/src/Formula.ts

@@ -3,16 +3,18 @@ import { parse as _parse } from './Formula/Grammar.js'
 
 import { union } from './Util.js'
 
+export type TruthValue = boolean | 'undecidable'
+
 type F<P> =
-  | { kind: 'atom'; property: P; value: boolean }
+  | { kind: 'atom'; property: P; value: TruthValue }
   | { kind: 'or'; subs: F<P>[] }
   | { kind: 'and'; subs: F<P>[] }
 
 function atomSchema<P>(p: z.ZodSchema<P>): z.ZodSchema<F<P>> {
   return z.object({
     kind: z.literal('atom'),
     property: p,
-    value: z.boolean(),
+    value: z.union([z.boolean(), z.literal('undecidable')]),
   }) as any
 }
 
@@ -34,7 +36,7 @@ export const formulaSchema = <P>(p: z.ZodSchema<P>): z.ZodSchema<F<P>> =>
 export interface Atom<P, X = never> {
   kind: 'atom'
   property: P
-  value: boolean | X
+  value: TruthValue | X
 }
 
 export interface And<P, X = never> {
@@ -59,7 +61,7 @@ export function or<P, X = never>(...subs: Formula<P, X>[]): Or<P, X> {
 
 export function atom<P, X = never>(
   property: P,
-  value: boolean | X = true,
+  value: TruthValue | X = true,
 ): Atom<P, X> {
   return { kind: 'atom', property, value }
 }
@@ -78,6 +80,7 @@ export function render<T>(f: Formula<T>, term: (t: T) => string): string {
     case 'atom':
       // eslint-disable-next-line no-case-declarations
       const name = term(f.property)
+      if (f.value === 'undecidable') return '⊬' + name
       return f.value ? name : '¬' + name
     case 'and':
       return '(' + f.subs.map(sf => render(sf, term)).join(' ∧ ') + ')'
@@ -86,9 +89,21 @@ export function render<T>(f: Formula<T>, term: (t: T) => string): string {
   }
 }
 
+export function hasUndecidable<P, X = never>(f: Formula<P, X>): boolean {
+  switch (f.kind) {
+    case 'atom':
+      return f.value === 'undecidable'
+    default:
+      return f.subs.some(hasUndecidable)
+  }
+}
+
 export function negate<P>(formula: Formula<P>): Formula<P> {
   switch (formula.kind) {
     case 'atom':
+      if (formula.value === 'undecidable') {
+        throw new Error('Cannot negate an undecidable atom')
+      }
       return atom(formula.property, !formula.value)
     case 'and':
       return or(...formula.subs.map(negate))
@@ -130,7 +145,7 @@ export function compact<P, X>(
 
 export function evaluate<T, V extends boolean | null = boolean>(
   f: Formula<T, V>,
-  traits: Map<T, boolean>,
+  traits: Map<T, TruthValue>,
 ): boolean | undefined {
   let result: boolean | undefined
 
@@ -192,8 +207,8 @@ type Serialized<X = never> =
   | { and: Serialized[] }
   | { or: Serialized[] }
   | { inner: Serialized }
-  | { property: string; value: boolean | X }
-  | Record<string, boolean | X>
+  | { property: string; value: TruthValue | X }
+  | Record<string, TruthValue | X>
 
 export function fromJSON(json: Serialized): Formula<string, null> {
   if ('and' in json && typeof json.and === 'object') {
@@ -211,7 +226,7 @@ export function fromJSON(json: Serialized): Formula<string, null> {
     throw `cannot cast object with ${entries.length} keys to atom`
   }
 
-  if (typeof entries[0][1] !== 'boolean') {
+  if (typeof entries[0][1] !== 'boolean' && entries[0][1] !== 'undecidable') {
     throw `cannot cast object with non-boolean value`
   }
 

packages/core/src/Logic/Derivations.ts

@@ -1,10 +1,11 @@
+import { type TruthValue } from '../Formula.js'
 import { Id } from './Types.js'
 
 type Evidence<TheoremId = Id, PropertyId = Id> = [TheoremId, PropertyId[]]
 
 export type Derivation<TheoremId = Id, PropertyId = Id> = {
   property: PropertyId
-  value: boolean
+  value: TruthValue
   proof: Proof<TheoremId, PropertyId>
 }
 
@@ -16,28 +17,32 @@ export type Proof<TheoremId = Id, PropertyId = Id> = {
 export class Derivations<TheoremId = Id, PropertyId = Id> {
   private evidence: Map<PropertyId, Evidence<TheoremId, PropertyId>>
   private given: Set<PropertyId>
-  private traits: Map<PropertyId, boolean>
+  private traits: Map<PropertyId, TruthValue>
 
   constructor(assumptions: PropertyId[] = []) {
     this.given = new Set(assumptions)
     this.evidence = new Map<PropertyId, Evidence<TheoremId, PropertyId>>()
-    this.traits = new Map<PropertyId, boolean>()
+    this.traits = new Map<PropertyId, TruthValue>()
   }
 
   addEvidence(
     property: PropertyId,
-    value: boolean,
+    value: TruthValue,
     theorem: TheoremId,
     support: PropertyId[],
   ): void {
     this.evidence.set(property, [theorem, support])
     this.traits.set(property, value)
   }
 
+  overrideGiven(property: PropertyId): void {
+    this.given.delete(property)
+  }
+
   all(): Derivation<TheoremId, PropertyId>[] {
     const result: Derivation<TheoremId, PropertyId>[] = []
 
-    this.traits.forEach((value: boolean, property: PropertyId) => {
+    this.traits.forEach((value: TruthValue, property: PropertyId) => {
       const proof = this.proof(property)
       if (!proof || proof === 'given') {
         return

packages/core/src/Logic/Prover.ts

@@ -1,9 +1,11 @@
 import {
+  type TruthValue,
   And,
   Atom,
   Formula,
   Or,
   evaluate,
+  hasUndecidable,
   negate,
   properties,
 } from '../Formula.js'
@@ -35,24 +37,28 @@ export default class Prover<
     PropertyId
   >,
 > {
-  private traits: Map<PropertyId, boolean>
+  private traits: Map<PropertyId, TruthValue>
   private derivations: Derivations<TheoremId, PropertyId>
 
   private queue: Queue<TheoremId, PropertyId, Theorem>
 
   constructor(
     implications: ImplicationIndex<TheoremId, PropertyId, Theorem>,
-    traits = new Map<PropertyId, boolean>(),
+    traits = new Map<PropertyId, TruthValue>(),
   ) {
     this.traits = traits
     this.derivations = new Derivations([...traits.keys()])
     this.queue = new Queue(implications)
 
-    traits.forEach((_: boolean, id: PropertyId) => {
+    traits.forEach((_: TruthValue, id: PropertyId) => {
       this.queue.mark(id)
     })
   }
 
+  enqueue(theorems: Theorem[]): void {
+    this.queue.addAll(theorems)
+  }
+
   run(): Result<TheoremId, PropertyId> {
     let theorem
     while ((theorem = this.queue.shift())) {
@@ -88,14 +94,14 @@ export default class Prover<
     const av = evaluate(a, this.traits)
     const cv = evaluate(c, this.traits)
 
-    if (av === true && cv === false) {
+    if (av === true && cv === false && !hasUndecidable(c)) {
       return this.contradiction(implication.id, [
         ...properties(a),
         ...properties(c),
       ])
     } else if (av === true) {
       return this.force(implication.id, c, [...properties(a)])
-    } else if (cv === false) {
+    } else if (cv === false && !hasUndecidable(a) && !hasUndecidable(c)) {
       return this.force(implication.id, negate(a), [...properties(c)])
     }
   }
@@ -114,16 +120,39 @@ export default class Prover<
   ): Contradiction<TheoremId, PropertyId> | undefined {
     const property = formula.property
 
-    if (this.traits.has(property)) {
-      if (this.traits.get(property) !== formula.value) {
-        return this.contradiction(theorem, [...support, property])
-      } else {
+    const existing = this.traits.get(property)
+
+    if (existing !== undefined) {
+      if (existing === formula.value) {
+        return
+      }
+      // undecidable has lower priority: true/false overrides it
+      if (existing === 'undecidable' && formula.value !== 'undecidable') {
+        this.traits.set(property, formula.value as TruthValue)
+        this.derivations.overrideGiven(property)
+        this.derivations.addEvidence(
+          property,
+          formula.value as TruthValue,
+          theorem,
+          support,
+        )
+        this.queue.mark(property)
+        return
+      }
+      // don't let undecidable override a definite value
+      if (formula.value === 'undecidable') {
         return
       }
+      return this.contradiction(theorem, [...support, property])
     }
 
-    this.traits.set(property, formula.value)
-    this.derivations.addEvidence(property, formula.value, theorem, support)
+    this.traits.set(property, formula.value as TruthValue)
+    this.derivations.addEvidence(
+      property,
+      formula.value as TruthValue,
+      theorem,
+      support,
+    )
     this.queue.mark(property)
   }
 

packages/core/src/Logic/Queue.ts

@@ -18,6 +18,12 @@ export default class Queue<
     this.index.withProperty(property).forEach(i => this.queue.add(i))
   }
 
+  addAll(theorems: Theorem[]): void {
+    for (const t of theorems) {
+      this.queue.add(t)
+    }
+  }
+
   shift(): Theorem | undefined {
     const result = this.queue.values().next()
     if (result.done) {

packages/core/src/Logic/index.ts

@@ -2,18 +2,35 @@ export { default as ImplicationIndex } from './ImplicationIndex.js'
 export { Derivations } from './Derivations.js'
 export { Contradiction, Proof } from './Prover.js'
 
-import { Formula, negate } from '../Formula.js'
+import { type TruthValue, Formula, hasUndecidable, negate } from '../Formula.js'
 import ImplicationIndex from './ImplicationIndex.js'
 import Prover, { Contradiction, Proof, Result } from './Prover.js'
 import { Id } from './Types.js'
 
 // Given a collection of implications and a collection of traits for an object,
-// find either the collection of derivable traits, or a contradiction
+// find either the collection of derivable traits, or a contradiction.
+// Undecidable theorems are deferred to a second phase so they don't interfere
+// with normal deduction performance.
 export function deduceTraits<TheoremId = Id, PropertyId = Id>(
   implications: ImplicationIndex<TheoremId, PropertyId>,
-  traits: Map<PropertyId, boolean>,
+  traits: Map<PropertyId, TruthValue>,
 ): Result<TheoremId, PropertyId> {
-  return new Prover(implications, traits).run()
+  const normal = implications.all.filter(
+    t => !hasUndecidable(t.when) && !hasUndecidable(t.then),
+  )
+  const undecidable = implications.all.filter(
+    t => hasUndecidable(t.when) || hasUndecidable(t.then),
+  )
+
+  const normalIndex = new ImplicationIndex<TheoremId, PropertyId>(normal)
+  const prover = new Prover<TheoremId, PropertyId>(normalIndex, traits)
+  const result = prover.run()
+  if (result.kind === 'contradiction' || undecidable.length === 0) {
+    return result
+  }
+
+  prover.enqueue(undecidable)
+  return prover.run()
 }
 
 // Given a collection of implications and a candidate formula,
@@ -71,14 +88,16 @@ export function proveTheorem<TheoremId = Id, PropertyId = Id>(
     return formatProof(result.contradiction)
   }
 
-  contradiction = prover.force('given', negate(then))
-  if (contradiction) {
-    return formatProof(contradiction)
-  }
+  if (!hasUndecidable(then)) {
+    contradiction = prover.force('given', negate(then))
+    if (contradiction) {
+      return formatProof(contradiction)
+    }
 
-  result = prover.run()
-  if (result.kind === 'contradiction') {
-    return formatProof(result.contradiction)
+    result = prover.run()
+    if (result.kind === 'contradiction') {
+      return formatProof(result.contradiction)
+    }
   }
 }
 

packages/core/src/Trait.ts

@@ -1,5 +1,6 @@
 import { z } from 'zod'
 import { Id as BaseId } from './Id.js'
+import { type TruthValue } from './Formula.js'
 import { Record, recordSchema } from './Record.js'
 
 export const proofSchema = <Id>(id: z.ZodSchema<Id>): z.ZodSchema<Proof<Id>> =>
@@ -18,7 +19,7 @@ export const traitSchema = <Id>(id: z.ZodSchema<Id>): z.ZodSchema<Trait<Id>> =>
     z.object({
       space: id,
       property: id,
-      value: z.boolean(),
+      value: z.union([z.boolean(), z.literal('undecidable')]),
       proof: proofSchema(id).optional(),
     }),
     recordSchema,
@@ -27,6 +28,6 @@ export const traitSchema = <Id>(id: z.ZodSchema<Id>): z.ZodSchema<Trait<Id>> =>
 export type Trait<Id = BaseId> = Record & {
   space: Id
   property: Id
-  value: boolean
+  value: TruthValue
   proof?: Proof<Id>
 }

packages/core/src/index.ts

@@ -5,7 +5,13 @@ import { theoremSchema } from './Theorem.js'
 import { traitSchema } from './Trait.js'
 
 export { type Bundle } from './Bundle.js'
-export { type Formula, type And, type Atom, type Or } from './Formula.js'
+export {
+  type Formula,
+  type And,
+  type Atom,
+  type Or,
+  type TruthValue,
+} from './Formula.js'
 export { parser } from './Parser.js'
 export { type Property, PropertyPage } from './Property.js'
 export {