Documentation

Studies.Mirrazi2024

Mirrazi (2024): Indefinites in Negated Intensional Contexts #

Rodica does not think that Carl read some of the books has, in Farsi, a reading on which the indefinite scopes above the negation but below think: Rodica believes that there are books Carl did not read, without believing of any particular book that he did not read it. No syntactic position is at once above the negation and below the attitude, so Mirrazi derives the reading from a choice function closed above the negation whose world argument the attitude binds, (44), and likewise for a modal, (48). An intensional choice function, applied to the intension of its restrictor but not skolemized to a world, gives only the de re reading when the restrictor is the same set in every belief world, (41)–(42): the fixed-set problem.

Main results #

Implementation notes #

References #

source
theorem Mirrazi2024.skolemized_iff {W : Type u_1} {E : Type u_2} {R : SetRel W W} {w₀ : W} {VP : E → W → Prop} {N : W → E → Prop} (hN : ∀ (w : W), ∃ (x : E), N w x) :
(∃ (F : W → Reference.ChoiceFunction E), ModalLogic.Box R (fun (w : W) => ¬VP ((F w) (N w)) w) w₀) ↔ ModalLogic.Box R (fun (w : W) => Quantifier.GQ.some (N w) fun (x : E) => ¬VP x w) w₀

Closing a world-skolemized choice function above the negation, with its world argument bound by the operator, (44) and (48), makes the sentence true exactly when every accessible world has a member of the restrictor that fails the predicate there.

source
theorem Mirrazi2024.intensional_iff_of_fixed {W : Type u_1} {E : Type u_2} {R : SetRel W W} {w₀ : W} {VP : E → W → Prop} {N : W → E → Prop} {B : E → Prop} (hB : ∃ (x : E), B x) (hN : ∀ (w : W), (w₀, w) ∈ R → N w = B) :
(∃ (f : Reference.ChoiceFunction E), ModalLogic.Box R (fun (w : W) => ¬VP (f (N w)) w) w₀) ↔ Quantifier.GQ.some B fun (x : E) => ModalLogic.Box R (fun (x_1 : W) => ¬VP x x_1) w₀

An intensional choice function applied to a restrictor whose extension is one fixed set B in every accessible world, (41) with (42), makes the sentence true exactly when one member of B fails the predicate in every accessible world, the de re reading.

The context of (40) #

source
inductive Mirrazi2024.Scenario40.Book :
Type

The five books Carl has to read.

Instances For
    source
    @[instance_reducible]
    instance Mirrazi2024.Scenario40.instDecidableEqBook :
    DecidableEq Book
    Equations
    source
    @[instance_reducible]
    instance Mirrazi2024.Scenario40.instFintypeBook :
    Fintype Book
    Equations
    • One or more equations did not get rendered due to their size.
    source
    inductive Mirrazi2024.Scenario40.World :
    Type

    The actual world and three of Rodica's belief worlds.

    Instances For
      source
      @[instance_reducible]
      instance Mirrazi2024.Scenario40.instDecidableEqWorld :
      DecidableEq World
      Equations
      source
      @[instance_reducible]
      instance Mirrazi2024.Scenario40.instFintypeWorld :
      Fintype World
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Mirrazi2024.Scenario40.beliefs :
      SetRel World World

      Rodica's belief worlds are the three non-actual ones.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance Mirrazi2024.Scenario40.instDecidableRelWorldMemProdSetRelBeliefsMk :
        DecidableRel fun (x1 x2 : World) => (x1, x2) ∈ beliefs
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mirrazi2024.Scenario40.unread :
        World → Book → Prop

        The book Carl did not read in each belief world, as the function picks in (45).

        Equations
        Instances For
          source
          @[instance_reducible]
          instance Mirrazi2024.Scenario40.instDecidableRelWorldBookUnread :
          DecidableRel unread
          Equations
          source
          def Mirrazi2024.Scenario40.Read (x : Book) (w : World) :
          Prop

          Carl read the books other than the unread one.

          Equations
          Instances For
            source
            theorem Mirrazi2024.Scenario40.skolemized :
            ∃ (F : World → Reference.ChoiceFunction Book), ModalLogic.Box beliefs (fun (w : World) => ¬Read ((F w) fun (x : Book) => True) w) World.actual

            Some world-skolemized function makes (40) true in its context.

            source
            theorem Mirrazi2024.Scenario40.not_intensional :
            ¬∃ (f : Reference.ChoiceFunction Book), ModalLogic.Box beliefs (fun (w : World) => ¬Read (f fun (x : Book) => True) w) World.actual

            No intensional choice function makes (40) true in its context, since the books are the same in every belief world and no book went unread in all of them.

            source
            theorem Mirrazi2024.Scenario40.not_narrow :
            ¬ModalLogic.Box beliefs (fun (w : World) => ¬∃ (x : Book), Read x w) World.actual

            The reading with the indefinite below the negation, that Rodica thinks Carl read none of the books, is false in the context of (40).