Monads as a Solution for Generalized Opacity

Gianluca Giorgolo & Ash Asudeh

April 27, 2014 - TTNLS 2014

Denotations vs. senses

1 + 1 = 2

Denotations vs. senses

Similarly in natural language

  1. Hesperus is Phosphorus

is not necessarily a tautology:

  1. Reza doesn’t believe Hesperus is Phosphorus

Denotations vs. senses

Standard analysis:


In certain contexts an expression like (3)

  1. Sandy is Sandy

is also not a tautology…

Capgras syndrome

From Wikipedia:

“[Capgras syndrome] is a disorder in which a person holds a delusion that a friend, spouse, parent, or other close family member has been replaced by an identical-looking impostor.”

  1. Kim doesn’t believe Sandy is Sandy

Capgras syndrome

Capgras syndrome

  1. Kim doesn’t believe Sandy is Sandy
  1. Kim doesn’t believe ImpostorSandyKim = Sandyσ

Indiana Pi Bill

In 1897 Dr. Edwin J. Goodwin presented a bill to the Indiana General Assembly for

“[…] introducing a new mathematical truth and offered as a contribution to education to be used only by the State of Indiana free of cost”

He had copyrighted that

  1. π = 3.2


  1. Edwin doesn’t believe π = π

Our approach in a nutshell

Other opaque contexts

  1. Reza doesn’t believe Hesperus is Phosphorus
  1. Mary Jane loves Peter Parker but she doesn’t love Spiderman

but not in cases like (11)

  1. Dr. Octopus killed Spiderman but he didn’t kill Peter Parker” (compare with “murder”)

Outline of the talk

Naive implementation:
New types

Naive implementation:
Contentious expressions

Naive implementation:
Index switching expressions

Grammatical infrastructure

Problem 1:
Only contradictory reading

  1. Kim doesn’t believe Sandy is Sandy
  1. Kim doesn’t believe ImpostorSandyKim = ImpostorSandyKim

Problem 2:
Implication linearity

τ → δ → ρ,  τ,  δ  ⊢  ρ
τ → δ → ρ,  i → τ,  δ,   ⊢  i → ρ
τ → δ → ρ,  i → τ,  i → δ,   ⊢  i → i → ρ

Problem 3:
Linearity again

What if the object of a verb like “love” is non contentious?

  1. e → (i → e) → t, e, e ⊢ ?

α ⊢ i → α not a valid inference in linear logic




Technical detail:
 ⋆  (“bind”) rather than μ

 ⋆  =  λm.λk.λi.k(m(i))(i) : 
  (i → τ) → (τ → (i → δ)) → (i → δ)

Monads in the logic

Online theorem prover

Monads, intuitively

Capgras example

  1. Kim doesn’t believe Sandy is Sandy
Kim Kim e
not λpp t → t
believe λs.λc.λi.believe(s)(c(s)) e → ◊t → ◊t
Sandy {Kim ↦ ImpostorKim, σ ↦ Sandyσ} e
is λx.λy.x = y e → e → t


Satisfiable reading

Sandy ⋆ λx.believe(Kim)(Sandy ⋆ λy.η(x = y)) ⋆ λz.ηz)

¬believe(Kim)(ImpostorKim = Sandyσ)

Unsatisfiable readings

believe(Kim)(Sandy ⋆ λx.Sandy ⋆ λy.η(x = y)) ⋆ λz.ηz)

¬believe(Kim)(ImpostorKim = ImpostorKim)

Sandy ⋆ λx.Sandy ⋆ λy.believe(Kim)(η(x = y)) ⋆ λz.ηz)

¬believe(Kim)(Sandyσ = Sandyσ)

love” example

  1. Mary Jane loves Peter Parker but she doesn’t love Spiderman
Mary Jane MJ e
love λs.λo.λ e → ◊e → ◊t
Peter Parker PP e
not λpp t → t
Spiderman {MJ ↦ SMMJ, σ ↦ PP} e


Satisfiable reading

love(MJ)(η(PP)) ⋆ λ ⋆ λq.η(p ∧ ¬q)

love(MJ)(PP) ∧ ¬love(MJ)(SMMJ)

Unsatisfiable reading

love(MJ)(η(PP)) ⋆ λp.Spiderman ⋆ λη(x)) ⋆ λq.η(p ∧ ¬q)

love(MJ)(PP) ∧ ¬love(MJ)(PP)

Beyond names

  1. Tina believes Bob is a woodchuck but she doesn’t believe he is a groundhog
  1. Tina thinks Flipper is a dolphin but she doesn’t think he is a marine mammal

Beyond names

dolphin {Flipper, Oscar, ...} e → t
{σ ↦ {Flipper, Oscar, MobyDick, ...}, 
 Tina ↦ {MobyDick, ...}}
◊(e → t)

To sum up


Supported by:
Marie Curie Intra-European Fellowship #327811 (Giorgolo)
Early Researcher Award, Province of Ontario (Asudeh)
NSERC Discovery Grant #371969 (Asudeh)