diff --git a/packages/compile/src/validations.ts b/packages/compile/src/validations.ts
index a21f77d8..ce9cf5e8 100644
--- a/packages/compile/src/validations.ts
+++ b/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
diff --git a/packages/core/src/Formula.ts b/packages/core/src/Formula.ts
index dd9c3aec..29fb8a8c 100644
--- a/packages/core/src/Formula.ts
+++ b/packages/core/src/Formula.ts
@@ -3,8 +3,10 @@ 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>[] }
 
@@ -12,7 +14,7 @@ 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`
   }
 
diff --git a/packages/core/src/Logic/Derivations.ts b/packages/core/src/Logic/Derivations.ts
index ef072910..893802c6 100644
--- a/packages/core/src/Logic/Derivations.ts
+++ b/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,17 +17,17 @@ 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 {
@@ -34,10 +35,14 @@ export class Derivations<TheoremId = Id, PropertyId = Id> {
     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
diff --git a/packages/core/src/Logic/Prover.ts b/packages/core/src/Logic/Prover.ts
index b09e38d4..c90e6f98 100644
--- a/packages/core/src/Logic/Prover.ts
+++ b/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)
   }
 
diff --git a/packages/core/src/Logic/Queue.ts b/packages/core/src/Logic/Queue.ts
index 40b8885c..28cc84dd 100644
--- a/packages/core/src/Logic/Queue.ts
+++ b/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) {
diff --git a/packages/core/src/Logic/index.ts b/packages/core/src/Logic/index.ts
index 88d2d015..a69a405c 100644
--- a/packages/core/src/Logic/index.ts
+++ b/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)
+    }
   }
 }
 
diff --git a/packages/core/src/Trait.ts b/packages/core/src/Trait.ts
index a9188ed9..12a68f28 100644
--- a/packages/core/src/Trait.ts
+++ b/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>
 }
diff --git a/packages/core/src/index.ts b/packages/core/src/index.ts
index bb346fae..7be8f716 100644
--- a/packages/core/src/index.ts
+++ b/packages/core/src/index.ts
@@ -5,7 +5,14 @@ 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,
+  hasUndecidable,
+} from './Formula.js'
 export { parser } from './Parser.js'
 export { type Property, PropertyPage } from './Property.js'
 export {
diff --git a/packages/viewer/src/components/Shared/Formula/Atom.svelte b/packages/viewer/src/components/Shared/Formula/Atom.svelte
index ff37fe10..e9fd64de 100644
--- a/packages/viewer/src/components/Shared/Formula/Atom.svelte
+++ b/packages/viewer/src/components/Shared/Formula/Atom.svelte
@@ -8,6 +8,12 @@
   export let link: boolean = true
 </script>
 
-{value.value === null ? '?' : value.value ? '' : '¬'}{#if link}<Link.Property
-    property={value.property}
-  />{:else}<Typeset body={value.property.name} />{/if}
+{value.value === null
+  ? '?'
+  : value.value === 'undecidable'
+  ? '⊬'
+  : value.value
+  ? ''
+  : '¬'}{#if link}<Link.Property property={value.property} />{:else}<Typeset
+    body={value.property.name}
+  />{/if}
diff --git a/packages/viewer/src/components/Theorems/Show.svelte b/packages/viewer/src/components/Theorems/Show.svelte
index 8f469ca8..6e6d6c9b 100644
--- a/packages/viewer/src/components/Theorems/Show.svelte
+++ b/packages/viewer/src/components/Theorems/Show.svelte
@@ -3,12 +3,13 @@
   import { Link, References, Tabs, Source, Typeset } from '../Shared'
   import Name from './Name.svelte'
   import Converse from './Converse.svelte'
+  import hasUndecidable from '@pibase/core' // FIXME not sure where to import this from but I doubt core is best
 
   export let theorem: Theorem
   export let tab: 'converse' | 'references'
   export let rel: string | undefined = undefined
 
-  const tabs = ['converse', 'references'] as const
+  const tabs: readonly ['converse', 'references'] | readonly ['references'] = (hasUndecidable(theorem.when) || hasUndecidable(theorem.then)) ? ['references'] : ['converse', 'references']
 </script>
 
 <h3>Theorem <Link.Theorem {theorem} content="idLong" /></h3>
diff --git a/packages/viewer/src/components/Traits/FilterButtons.svelte b/packages/viewer/src/components/Traits/FilterButtons.svelte
index a3531b1e..c571ca80 100644
--- a/packages/viewer/src/components/Traits/FilterButtons.svelte
+++ b/packages/viewer/src/components/Traits/FilterButtons.svelte
@@ -46,6 +46,17 @@
 >
   <Icons.X />
 </button>
+<button
+  class="btn {filterMode === 'undecidable'
+    ? 'btn-secondary'
+    : 'btn-outline-secondary'}"
+  type="button"
+  on:click={() => {
+    filterMode = 'undecidable'
+  }}
+>
+  —
+</button>
 <button
   class="btn {filterMode === 'asserted'
     ? 'btn-secondary'
diff --git a/packages/viewer/src/components/Traits/Related.svelte b/packages/viewer/src/components/Traits/Related.svelte
index f1c09c40..d3ce09f5 100644
--- a/packages/viewer/src/components/Traits/Related.svelte
+++ b/packages/viewer/src/components/Traits/Related.svelte
@@ -16,7 +16,14 @@
   const filter = writable('')
   urlSearchParam('filter', filter)
 
-  let filterMode: 'all' | 'known' | 'asserted' | 'true' | 'false' | 'missing'
+  let filterMode:
+    | 'all'
+    | 'known'
+    | 'asserted'
+    | 'true'
+    | 'false'
+    | 'undecidable'
+    | 'missing'
   filterMode = 'known'
 
   $: all = related($traits)
@@ -34,9 +41,11 @@
       case 'asserted':
         return t?.asserted
       case 'true':
-        return t?.value
+        return t?.value === true
       case 'false':
-        return t && !t.value
+        return t?.value === false
+      case 'undecidable':
+        return t?.value === 'undecidable'
       case 'missing':
         return !t
     }
diff --git a/packages/viewer/src/components/Traits/Show.svelte b/packages/viewer/src/components/Traits/Show.svelte
index e6dfd6db..23a3fc2c 100644
--- a/packages/viewer/src/components/Traits/Show.svelte
+++ b/packages/viewer/src/components/Traits/Show.svelte
@@ -51,10 +51,15 @@
     <Icons.Question />
   {/if}
   {#if trait}
-    <Link.Space {space} />
-    is
-    {trait.value ? '' : 'not'}
-    <Link.Property {property} />
+    {#if trait.value === 'undecidable'}
+      "<Link.Space {space} />
+      is <Link.Property {property} />" is logically independent
+    {:else}
+      <Link.Space {space} />
+      is
+      {trait.value ? '' : 'not'}
+      <Link.Property {property} />
+    {/if}
   {:else}
     We have insufficient information to determine whether or not
     <Link.Space {space} />
diff --git a/packages/viewer/src/components/Traits/Value.svelte b/packages/viewer/src/components/Traits/Value.svelte
index 660b90ae..ad450653 100644
--- a/packages/viewer/src/components/Traits/Value.svelte
+++ b/packages/viewer/src/components/Traits/Value.svelte
@@ -1,5 +1,5 @@
 <script lang="ts">
-  export let value: boolean | undefined
+  export let value: boolean | 'undecidable' | undefined
   export let icon: 'check' | 'user' = 'check'
 
   import { Icons } from '../Shared'
@@ -10,6 +10,8 @@
     <Icons.User />
   {:else if value === false}
     <Icons.Robot />
+  {:else if value === 'undecidable'}
+    <span title="Undecidable">—</span>
   {:else}<!-- value === undefined -->
     <Icons.Question />
   {/if}
@@ -18,6 +20,8 @@
     <Icons.Check />
   {:else if value === false}
     <Icons.X />
+  {:else if value === 'undecidable'}
+    <span title="Undecidable">—</span>
   {:else}<!-- value === undefined -->
     <Icons.Question />
   {/if}
diff --git a/packages/viewer/src/models/Traits.ts b/packages/viewer/src/models/Traits.ts
index 92f51c9f..a3ba7fe8 100644
--- a/packages/viewer/src/models/Traits.ts
+++ b/packages/viewer/src/models/Traits.ts
@@ -141,6 +141,9 @@ export default class Traits {
     { when, then }: { when: Formula<Property>; then: Formula<Property> },
     space: Space,
   ): boolean {
+    if (F.hasUndecidable(when) || F.hasUndecidable(then)) {
+      return false
+    }
     return (
       this.evaluate({
         formula: F.and(when, F.negate(then)),
diff --git a/packages/viewer/src/parser/internalLinks.ts b/packages/viewer/src/parser/internalLinks.ts
index 73bcb092..b5a838c9 100644
--- a/packages/viewer/src/parser/internalLinks.ts
+++ b/packages/viewer/src/parser/internalLinks.ts
@@ -17,17 +17,25 @@ export function internal(
           const space = spaces.find(Number(sid))
           const property = properties.find(Number(pid))
           const trait = space && property && traits.find(space, property)
-          const connector =
-            trait?.value === true
-              ? 'is'
-              : trait?.value === false
-              ? 'is not'
-              : '?'
+          let title = undefined
+          if (trait?.value === 'undecidable') {
+            title = `"${space ? space.name : 'S' + sid} is ${
+              property ? property.name : 'P' + pid
+            }" is logically independent`
+          } else {
+            const connector =
+              trait?.value === true
+                ? 'is'
+                : trait?.value === false
+                ? 'is not'
+                : '?'
+            title = `${space ? space.name : 'S' + sid} ${connector} ${
+              property ? property.name : 'P' + pid
+            }`
+          }
           return {
             href: `/spaces/S${sid}/properties/P${pid}`,
-            title: `${space ? space.name : 'S' + sid} ${connector} ${
-              property ? property.name : 'P' + pid
-            }`,
+            title,
           }
         }
 
diff --git a/packages/viewer/src/stores/deduction.ts b/packages/viewer/src/stores/deduction.ts
index 0bc1cdcb..799a21ed 100644
--- a/packages/viewer/src/stores/deduction.ts
+++ b/packages/viewer/src/stores/deduction.ts
@@ -199,7 +199,7 @@ export function checkIfRedundant(
   const assertedTraits = traits.forSpace(space).filter(([_, t]) => t.asserted)
   const map = new Map(
     assertedTraits.map(([p, t]) => {
-      if (p === property) {
+      if (p === property && t.value !== 'undecidable') {
         return [p.id, !t.value]
       } else {
         return [p.id, t.value]
diff --git a/packages/viewer/src/types/index.ts b/packages/viewer/src/types/index.ts
index d60a0123..6b6acc2a 100644
--- a/packages/viewer/src/types/index.ts
+++ b/packages/viewer/src/types/index.ts
@@ -1,5 +1,5 @@
-export type { Formula } from '@pi-base/core'
-import type { Formula, Ref as R } from '@pi-base/core'
+export type { Formula, TruthValue } from '@pi-base/core'
+import type { Formula, Ref as R, TruthValue } from '@pi-base/core'
 
 export type Ref = R.Ref
 
@@ -23,7 +23,7 @@ export type AssertedTrait = {
   asserted: true
   space: number
   property: number
-  value: boolean
+  value: TruthValue
   description: string
   refs: Ref[]
 }
@@ -32,7 +32,7 @@ export type DeducedTrait = {
   asserted: false
   space: number
   property: number
-  value: boolean
+  value: TruthValue
   proof: {
     properties: number[]
     theorems: number[]