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:

But…

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

Thus

  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

Problems

Solution

Monads

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

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

Monads in the logic


Online theorem prover

http://llilab.carleton.ca/~giorgolo/tp.html

Monads, intuitively

Capgras example

  1. “Kim doesn’t believe Sandy is Sandy”
Kim Kim e
not λp.¬p 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

Readings

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.λi.love(s)(o(s)) e → ◊e → ◊t
Peter Parker PP e
not λp.¬p t → t
Spiderman {MJ ↦ SMMJ, σ ↦ PP} ◊e

Readings

Satisfiable reading

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

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

Unsatisfiable reading

⟦love⟧(MJ)(η(PP)) ⋆ λp.⟦Spiderman⟧ ⋆ λx.⟦love⟧(MJ)(η(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
marine
mammal
{σ ↦ {Flipper, Oscar, MobyDick, ...}, 
 Tina ↦ {MobyDick, ...}}
◊(e → t)

To sum up




Thanks!

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