Default Reasoning: Classic Examples

Theory-neutral data for two classic default reasoning examples:

1. Tweety Triangle: Birds normally fly. Tweety is a bird. Tweety is a penguin. Penguins are birds. Penguins normally don't fly. Conclusion: Tweety presumably doesn't fly (the more specific default wins).

2. Nixon Diamond (multiple attributions): Quakers are normally pacifist. Republicans are normally not pacifist. Nixon is both a Quaker and a Republican. Conclusion: agnosticism — neither "presumably pacifist" nor "presumably not pacifist" follows.

These examples test specificity (Tweety) and conflicting defaults (Nixon). Both require conditional defaults ("if φ then normally ψ") to formalize properly — unconditional defaults can only express the degenerate case.

inductive Phenomena.DefaultReasoning.TweetyWorld : Type

The Tweety world: 4 possible states of an entity.

• birdFlies : TweetyWorld
• birdNoFly : TweetyWorld
• penguinFlies : TweetyWorld
• penguinNoFly : TweetyWorld

instance Phenomena.DefaultReasoning.instDecidableEqTweetyWorld : DecidableEq TweetyWorld

Equations

• Phenomena.DefaultReasoning.instDecidableEqTweetyWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.DefaultReasoning.instReprTweetyWorld.repr : TweetyWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Phenomena.DefaultReasoning.instReprTweetyWorld : Repr TweetyWorld

Equations

• Phenomena.DefaultReasoning.instReprTweetyWorld = { reprPrec := Phenomena.DefaultReasoning.instReprTweetyWorld.repr }

def Phenomena.DefaultReasoning.instBEqTweetyWorld.beq : TweetyWorld → TweetyWorld → Bool

Equations

• Phenomena.DefaultReasoning.instBEqTweetyWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.DefaultReasoning.instBEqTweetyWorld : BEq TweetyWorld

Equations

• Phenomena.DefaultReasoning.instBEqTweetyWorld = { beq := Phenomena.DefaultReasoning.instBEqTweetyWorld.beq }

instance Phenomena.DefaultReasoning.instFintypeTweetyWorld : Fintype TweetyWorld

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.DefaultReasoning.isBird : TweetyWorld → Prop

Equations

• Phenomena.DefaultReasoning.isBird Phenomena.DefaultReasoning.TweetyWorld.birdFlies = True
• Phenomena.DefaultReasoning.isBird Phenomena.DefaultReasoning.TweetyWorld.birdNoFly = True
• Phenomena.DefaultReasoning.isBird Phenomena.DefaultReasoning.TweetyWorld.penguinFlies = True
• Phenomena.DefaultReasoning.isBird Phenomena.DefaultReasoning.TweetyWorld.penguinNoFly = True

def Phenomena.DefaultReasoning.isPenguin : TweetyWorld → Prop

Equations

• Phenomena.DefaultReasoning.isPenguin Phenomena.DefaultReasoning.TweetyWorld.penguinFlies = True
• Phenomena.DefaultReasoning.isPenguin Phenomena.DefaultReasoning.TweetyWorld.penguinNoFly = True
• Phenomena.DefaultReasoning.isPenguin x✝ = False

def Phenomena.DefaultReasoning.flies : TweetyWorld → Prop

Equations

• Phenomena.DefaultReasoning.flies Phenomena.DefaultReasoning.TweetyWorld.birdFlies = True
• Phenomena.DefaultReasoning.flies Phenomena.DefaultReasoning.TweetyWorld.penguinFlies = True
• Phenomena.DefaultReasoning.flies x✝ = False

theorem Phenomena.DefaultReasoning.penguin_is_bird (w : TweetyWorld) : isPenguin w → isBird w

Every penguin is a bird.

def Phenomena.DefaultReasoning.tweety_doesnt_fly : Bool

Empirical judgment: given "birds normally fly" and "penguins normally don't fly", Tweety (a penguin) presumably doesn't fly. The more specific default (penguins) overrides the general one (birds).

Equations

• Phenomena.DefaultReasoning.tweety_doesnt_fly = true

def Phenomena.DefaultReasoning.robin_flies : Bool

Empirical judgment: non-penguin birds presumably do fly.

Equations

• Phenomena.DefaultReasoning.robin_flies = true

inductive Phenomena.DefaultReasoning.NixonWorld : Type

The Nixon world: 4 possible states.

• quakerPacifist : NixonWorld
• quakerNotPacifist : NixonWorld
• repPacifist : NixonWorld
• repNotPacifist : NixonWorld

instance Phenomena.DefaultReasoning.instDecidableEqNixonWorld : DecidableEq NixonWorld

Equations

• Phenomena.DefaultReasoning.instDecidableEqNixonWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.DefaultReasoning.instReprNixonWorld.repr : NixonWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Phenomena.DefaultReasoning.instReprNixonWorld : Repr NixonWorld

Equations

• Phenomena.DefaultReasoning.instReprNixonWorld = { reprPrec := Phenomena.DefaultReasoning.instReprNixonWorld.repr }

def Phenomena.DefaultReasoning.isQuaker : NixonWorld → Prop

Equations

• Phenomena.DefaultReasoning.isQuaker Phenomena.DefaultReasoning.NixonWorld.quakerPacifist = True
• Phenomena.DefaultReasoning.isQuaker Phenomena.DefaultReasoning.NixonWorld.quakerNotPacifist = True
• Phenomena.DefaultReasoning.isQuaker x✝ = False

def Phenomena.DefaultReasoning.isRepublican : NixonWorld → Prop

Equations

• Phenomena.DefaultReasoning.isRepublican Phenomena.DefaultReasoning.NixonWorld.repPacifist = True
• Phenomena.DefaultReasoning.isRepublican Phenomena.DefaultReasoning.NixonWorld.repNotPacifist = True
• Phenomena.DefaultReasoning.isRepublican x✝ = False

def Phenomena.DefaultReasoning.isPacifist : NixonWorld → Prop

Equations

• Phenomena.DefaultReasoning.isPacifist Phenomena.DefaultReasoning.NixonWorld.quakerPacifist = True
• Phenomena.DefaultReasoning.isPacifist Phenomena.DefaultReasoning.NixonWorld.repPacifist = True
• Phenomena.DefaultReasoning.isPacifist x✝ = False

def Phenomena.DefaultReasoning.nixon_agnostic : Bool

Empirical judgment: given conflicting defaults ("Quakers normally pacifist", "Republicans normally not pacifist"), a Quaker Republican is agnostic — neither "presumably pacifist" nor "presumably not pacifist" should follow.

Equations

• Phenomena.DefaultReasoning.nixon_agnostic = true