ucwm/specialists/logic.md

# Logic Specialist

**specialist_id:** `logic`  
**trigger_gates:** `has_logical_negation`, `has_comparison`, `has_constraint`

---

## Responsibility

The logic specialist handles negation, implication, contradiction, quantifiers, and truth status. It attaches LogicalFacets to propositions and claims, and emits logical constraints that the resolver uses to detect contradictions and propagate truth values.

---

## Manifest

```
declared_facet_kinds:
  - logical

declared_constraint_types:
  - truth_value
  - implies
  - negates
  - contradicts
  - requires
  - exclusive_or
  - universally_quantified
  - existentially_quantified

budget_caps:
  max_objects_proposed:     4
  max_facets_emitted:       8
  max_constraints_emitted: 10
  max_merges:               0
  max_splits:               0
```

---

## Output: LogicalFacet

Attach to objects of kind `proposition`, `claim`, or `event` with a truth dimension.

```
LogicalFacet fields used:
  - truth_status:   "true" | "false" | "unknown" | "hypothetical" | "negated" | "asserted"
  - quantifier:     "universal" | "existential" | "none"
  - implies_refs:   [proposition_ids this implies]
  - negates_refs:   [proposition_ids this negates]
  - contradicts_refs: [proposition_ids this contradicts]
```

---

## Output: Constraints

### `truth_value(P, status)`

Sets the explicit truth status of a proposition.

```
{
  "constraint_type": "truth_value",
  "argument_refs": ["P1"],
  "polarity": "positive",
  "strength": "hard",
  "expression": "truth(P1) = false"
}
```

### `negates(P1, P2)`

P1 is the logical negation of P2. If P1 is true, P2 is false, and vice versa.

### `implies(P1, P2)`

If P1 is true, P2 must be true. Defeasible by default unless marked hard.

### `contradicts(P1, P2)`

P1 and P2 cannot both be true. Strength is always hard.

### `requires(A, B)`

A requires B to hold. Equivalent to `implies(A, B)` but semantically marks a dependency rather than a logical implication.

### `exclusive_or(P1, P2)`

Exactly one of P1 or P2 is true.

---

## Negation handling

Negation is the most error-prone logical operation. Rules:

1. Surface negation (e.g., `not`, `isn't`) does not always mean logical negation of a proposition — it may be just semantic modification.
2. When `has_logical_negation` fires, the logic specialist inspects whether the negation applies to:
   - A predicate (`Alice is NOT happy` → LogicalFacet truth_status = negated)
   - A quantifier (`NOT all → some are not`)
   - A condition (`unless X` → implies(NOT X, consequence))
3. Emit `truth_value` constraints conservatively — only when confident the scope of negation is correctly identified.

---

## Contradiction detection support

The logic specialist does not resolve contradictions. It emits `contradicts` constraints when it detects that two propositions in WorldState logically oppose each other. The resolver handles contradiction resolution.

```
if P1 has truth_status = true AND P2 = negation_of(P1):
  emit contradicts(P1, P2) with strength = hard
```

---

## Contract test requirements

- Given `Alice is not happy`, must emit a LogicalFacet on `P_alice_happy` with `truth_status: negated`
- Given `If it rains, the ground is wet`, must emit `implies(E_rain, S_ground_wet)`
- Must not emit temporal or quantity constraints
- Contradiction constraints must reference two objects that exist in WorldState
- All emitted constraints must have `source_module: logic`