Paraconsistent Animals

When the facts disagree, say so, instead of pretending they don’t.

paraconsistent-animals.js · output · proof · check · try it in the playground

The question

Birds fly. Penguins don’t. Tweety is a bird and a penguin. Does Tweety fly?

Real data is often like this: two rules, or a rule and an observation, point in opposite directions. Ordinary logic breaks down here: from a contradiction it lets you conclude anything at all.

Paraconsistent reasoning is reasoning that keeps working when the data contains contradictions. It keeps the conflict contained and visible.

What we tell eyecode: animals and rules

fact(bird('tweety'))
fact(penguin('tweety'))
fact(bird('falco'))
fact(penguin('opus'))
fact(mammal('batsy'))
fact(bat('batsy'))
fact(fish('nemo'))
fact(bird('mythic'))
// An explicit observation that contradicts the rule for birds.
fact(observed('mythic', 'flies', 'false'))
implies(bird(X), flies(X, 'true'))
implies(bird(X), wings(X, 'true'))
implies(penguin(X), flies(X, 'false'))
implies(mammal(X), wings(X, 'false'))
implies(bat(X), [flies(X, 'true'), wings(X, 'true')])
// …

Conclusions are written as flies(X, 'true') or flies(X, 'false'), so both can be recorded side by side without the program falling over.

What we tell eyecode: summaries

Each property gets a local summary: true only, false only, or both.

// Local summaries. These inspect the rule conclusions, so they run only after
// the stratum above has reached its fixpoint.
implies([flies(X, 'true'), flies(X, 'false')], flight_status(X, 'both'))
implies([flies(X, 'true'), not(flies(X, 'false'))], flight_status(X, 'true_only'))
// …
implies(flight_status(X, 'true_only'), flies_safely(X, 'true'))
implies(flight_status(X, 'both'), flies_safely(X, 'undecided'))

not(...) means “not found”: nothing eyecode knows says otherwise. Because the summaries look at what the animal rules concluded, eyecode runs them only after those rules have finished (this is called stratified negation), so a “not found” is never premature. Decisions read only the summary, so a conflict leads to undecided, never to both answers.

What eyecode concludes

50 conclusions in all. The interesting ones:

inconsistent('tweety', 'flies')
needs_review('tweety', 'flies')
inconsistent('mythic', 'flies')
inconsistent('batsy', 'wings')
flies_safely('tweety', 'undecided')
flies_safely('falco', 'true')
flies_safely('opus', 'false')
moves_by('opus', 'walking')

Tweety (bird and penguin) and Mythic (a bird seen not flying) are flagged for review. Batsy the bat has wings by one rule and none by the mammal rule. Falco and Batsy move by flying, Opus walks, and Nemo has no wings. Nothing is concluded about properties with no evidence: no rule says whether Nemo flies, so Nemo gets no flight decision at all.

Why: the proof in plain words

For Tweety:

  1. Tweety flies — birds fly, because bird('tweety').
  2. Tweety does not fly — penguins don’t, because penguin('tweety').
  3. So Tweety’s flight status is both, and Tweety needs review.

For Falco:

  1. Falco flies — birds fly.
  2. Nothing says Falco does not fly (a search that found nothing).
  3. So Falco’s status is true only, and Falco flies safely.

Checked, not just claimed

The proof has 66 steps: 59 were verified against the program, and the other 7 are the “not found” steps described below. Verdict: checked_with_obligations.

The 7 obligations are all of the kind called absent, one for each “not found” the decisions rely on, such as:

obligation('absent', 'theory_scoped', not(flies('falco', 'false')))

eyecode concluded that nothing says Falco cannot fly because it searched everything it knows and found nothing. The checker records each such absence rather than proving it, and confirmed that no step in the proof contradicts any of them.

Try it

eyecode examples/paraconsistent-animals.js            # the answers
eyecode --proof examples/paraconsistent-animals.js    # answers with their proof

Or open it in the playground. Delete the line fact(observed('mythic', 'flies', 'false')) and run again: the conflict disappears, and you get flies_safely('mythic', 'true') and moves_by('mythic', 'flying').

Takeaway

Contradictions in data are not a reason to give up or to guess. Kept local and labelled, they become a to-do list for a human, while everything that is clear-cut still gets decided.