Romero (2005): Concealed Questions and Specificational Subjects

@cite{romero-2005}

Concealed Questions and Specificational Subjects. Linguistics and Philosophy 28(6):687–737.

Core Claims

1. Epistemic know is intensional w.r.t. its object position. The semantic argument of know is an intensional object obtained from either the extension (Reading A) or the intension (Reading B) of the complement NP.

2. Specificational be is intensional w.r.t. its subject position. The same extension/intension choice applies to the subject NP of specificational copular sentences, yielding the same A/B ambiguity.

3. Three purely extensional accounts (evaluation world, trace type ambiguity, pragmatic) are refuted for both concealed questions and specificational subjects.

The A/B Ambiguity (@cite{heim-1979})

"John knows the price that Fred knows."

• Reading A: John knows the same price question Fred knows — e.g., both know how much the milk costs.
• Reading B: John knows which price question Fred knows — e.g., John knows that the question Fred knows the answer to is "How much does the milk cost?", but John need not know the answer himself.

Lexical Entries

Two crosscategorial variants of know (Romero (29b,c)):

• know₁ : ⟨⟨s,e⟩, ⟨e, ⟨s,t⟩⟩⟩ — for ⟨s,e⟩ (individual concept) arguments
• know₂ : ⟨⟨s,⟨s,e⟩⟩, ⟨e, ⟨s,t⟩⟩⟩ — for ⟨s,⟨s,e⟩⟩ (concept of concepts) arguments

Parallel entries for specificational be (Romero (67a,b)):

• be₁_spec : ⟨e, ⟨⟨s,e⟩, ⟨s,t⟩⟩⟩ — Reading A (extension of SS NP)
• be₂_spec : ⟨⟨s,e⟩, ⟨⟨s,⟨s,e⟩⟩, ⟨s,t⟩⟩⟩ — Reading B (intension of SS NP)

Relation to Modern Frameworks

@cite{uegaki-2019} argues for a question-oriented semantics where all complement-taking predicates select for propositional concepts ⟨s,⟨s,t⟩⟩. Under that view, know₁/know₂ are subcases of a single entry taking a question meaning. Romero's A/B data remains the key empirical test for any such unification. See also @cite{ciardelli-groenendijk-roelofsen-2018} for an inquisitive-semantics approach to the same unification.

World and Entity Setup

@[reducible, inline]

abbrev Phenomena.Copulas.Studies.Romero2005.W : Type

Equations

• Phenomena.Copulas.Studies.Romero2005.W = Core.Proposition.World4

@[reducible, inline]

abbrev Phenomena.Copulas.Studies.Romero2005.E : Type

Equations

• Phenomena.Copulas.Studies.Romero2005.E = Fin 4

def Phenomena.Copulas.Studies.Romero2005.worlds : List W

All worlds in the model.

Equations

• Phenomena.Copulas.Studies.Romero2005.worlds = [Core.Proposition.World4.w0, Core.Proposition.World4.w1, Core.Proposition.World4.w2, Core.Proposition.World4.w3]

def Phenomena.Copulas.Studies.Romero2005.entities : List E

All entities in the model (prices / question-answers).

Equations

• Phenomena.Copulas.Studies.Romero2005.entities = [0, 1, 2, 3]

theorem Phenomena.Copulas.Studies.Romero2005.worlds_complete (w : W) : w ∈ worlds

worlds covers all of World4. Needed for soundness of List.all as universal quantification.

theorem Phenomena.Copulas.Studies.Romero2005.entities_complete (e : E) : e ∈ entities

entities covers all of Fin 4.

Doxastic Accessibility

Accessibility relations for two agents (John = 0, Fred = 1).

@[reducible, inline]

abbrev Phenomena.Copulas.Studies.Romero2005.john : E

Agent identifiers.

Equations

• Phenomena.Copulas.Studies.Romero2005.john = 0

@[reducible, inline]

abbrev Phenomena.Copulas.Studies.Romero2005.fred : E

Equations

• Phenomena.Copulas.Studies.Romero2005.fred = 1

def Phenomena.Copulas.Studies.Romero2005.Dox : E → W → W → Bool

Doxastic accessibility: Dox agent w w' means w' is compatible with what agent believes/knows in w.

Equations

• Phenomena.Copulas.Studies.Romero2005.Dox 0 Core.Proposition.World4.w0 Core.Proposition.World4.w0 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 0 Core.Proposition.World4.w0 x✝ = false
• Phenomena.Copulas.Studies.Romero2005.Dox 0 Core.Proposition.World4.w1 Core.Proposition.World4.w1 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 0 Core.Proposition.World4.w1 x✝ = false
• Phenomena.Copulas.Studies.Romero2005.Dox 0 Core.Proposition.World4.w2 Core.Proposition.World4.w2 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 0 Core.Proposition.World4.w2 Core.Proposition.World4.w3 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 0 Core.Proposition.World4.w2 x✝ = false
• Phenomena.Copulas.Studies.Romero2005.Dox 0 Core.Proposition.World4.w3 Core.Proposition.World4.w2 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 0 Core.Proposition.World4.w3 Core.Proposition.World4.w3 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 0 Core.Proposition.World4.w3 x✝ = false
• Phenomena.Copulas.Studies.Romero2005.Dox 1 Core.Proposition.World4.w0 Core.Proposition.World4.w0 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 1 Core.Proposition.World4.w0 Core.Proposition.World4.w2 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 1 Core.Proposition.World4.w0 x✝ = false
• Phenomena.Copulas.Studies.Romero2005.Dox 1 Core.Proposition.World4.w1 Core.Proposition.World4.w1 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 1 Core.Proposition.World4.w1 x✝ = false
• Phenomena.Copulas.Studies.Romero2005.Dox 1 Core.Proposition.World4.w2 Core.Proposition.World4.w0 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 1 Core.Proposition.World4.w2 Core.Proposition.World4.w2 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 1 Core.Proposition.World4.w2 x✝ = false
• Phenomena.Copulas.Studies.Romero2005.Dox 1 Core.Proposition.World4.w3 Core.Proposition.World4.w3 = true
• Phenomena.Copulas.Studies.Romero2005.Dox 1 Core.Proposition.World4.w3 x✝ = false
• Phenomena.Copulas.Studies.Romero2005.Dox x✝² x✝¹ x✝ = (x✝¹ == x✝)

@[reducible, inline]

abbrev Phenomena.Copulas.Studies.Romero2005.DoxRel : Semantics.Attitudes.Doxastic.AccessRel W E

Dox is an AccessRel — connecting to the theory-layer doxastic infrastructure in Semantics.Attitudes.Doxastic.

Equations

• Phenomena.Copulas.Studies.Romero2005.DoxRel = Phenomena.Copulas.Studies.Romero2005.Dox

Individual Concepts (Price Functions)

A "price" is an individual concept: a function from worlds to entities. "The price of milk" maps each world to the price of milk in that world. "The price of oil" maps each world to the price of oil in that world.

def Phenomena.Copulas.Studies.Romero2005.priceMilk : Core.Intension W E

Price of milk: varies across worlds.

Equations

• Phenomena.Copulas.Studies.Romero2005.priceMilk Core.Proposition.World4.w0 = 0
• Phenomena.Copulas.Studies.Romero2005.priceMilk Core.Proposition.World4.w1 = 1
• Phenomena.Copulas.Studies.Romero2005.priceMilk Core.Proposition.World4.w2 = 0
• Phenomena.Copulas.Studies.Romero2005.priceMilk Core.Proposition.World4.w3 = 2

def Phenomena.Copulas.Studies.Romero2005.priceOil : Core.Intension W E

Price of oil: constant across all worlds.

Equations

• Phenomena.Copulas.Studies.Romero2005.priceOil x✝ = 3

def Phenomena.Copulas.Studies.Romero2005.rigidZero : W → E

A rigid IC with value 0 at all worlds. Used to demonstrate that extensional mechanisms (Account 3, extensional verbs) cannot distinguish ICs that agree at the evaluation world.

Equations

• Phenomena.Copulas.Studies.Romero2005.rigidZero x✝ = 0

def Phenomena.Copulas.Studies.Romero2005.instBEqIntensionWE : BEq (Core.Intension W E)

Equations

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

Romero's Lexical Entries

know₁ and know₂ (Romero (29b,c))

These are crosscategorial variants: they perform the same doxastic-universal operation but differ in the type of their first argument.

• know₁ takes an individual concept y : ⟨s,e⟩ and checks that its value is correctly identified across all doxastic alternatives.
• know₂ takes a concept of individual concepts y : ⟨s,⟨s,e⟩⟩ and checks that the meta-question answer is correctly identified.

def Phenomena.Copulas.Studies.Romero2005.know₁ (y : W → E) (x : E) (w : W) : Bool

⟦know₁⟧(y_{⟨s,e⟩})(x_e)(w_s) = 1 iff ∀w' ∈ Dox_x(w). y(w') = y(w)

The agent x knows the value of individual concept y: in all doxastic alternatives, y yields the same value as in actuality. Romero (29b); also (100) know_{CQ,STR} (strongly exhaustive CQ know).

Equations

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

def Phenomena.Copulas.Studies.Romero2005.know₂ (y : W → W → E) (x : E) (w : W) : Bool

⟦know₂⟧(y_{⟨s,⟨s,e⟩⟩})(x_e)(w_s) = 1 iff ∀w' ∈ Dox_x(w). y(w') = y(w)

The agent x knows the value of a concept of individual concepts y: in all doxastic alternatives, the meta-question y yields the same individual concept as in actuality. Same operation, higher type.

Equations

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

Connection to Doxastic Theory Layer

know₁ is a specialization of Doxastic.boxAt: universal quantification over doxastic alternatives with a specific proposition y(w') = y(w).

theorem Phenomena.Copulas.Studies.Romero2005.know₁_eq_boxAt (y : W → E) (x : E) (w : W) : know₁ y x w = Semantics.Attitudes.Doxastic.boxAt DoxRel x w worlds fun (w' : W) => y w' == y w

know₁ is boxAt applied to the identity proposition y(w') = y(w).

be₁_spec and be₂_spec (Romero (67a,b))

Specificational be is an intensional verb w.r.t. its subject position.

• be₁_spec takes the NP's extension (an individual concept) and a post-copular entity, and checks identity at the evaluation world.
• be₂_spec takes the NP's intension (a concept of concepts) and a post-copular individual concept, and checks identity at the evaluation world.

def Phenomena.Copulas.Studies.Romero2005.be₁_spec (x : E) (y : W → E) (w : W) : Bool

⟦be₁_spec⟧(x_e)(y_{⟨s,e⟩})(w_s) = 1 iff y(w) = x

Reading A: the individual concept y (extension of the SS NP) has value x at the actual world w. Romero (67a); also (104) be_{SS,STR}.

Equations

• Phenomena.Copulas.Studies.Romero2005.be₁_spec x y w = (y w == x)

def Phenomena.Copulas.Studies.Romero2005.be₂_spec (x : W → E) (y : W → W → E) (w : W) : Bool

⟦be₂_spec⟧(x_{⟨s,e⟩})(y_{⟨s,⟨s,e⟩⟩})(w_s) = 1 iff y(w) = x

Reading B: the concept-of-concepts y (intension of the SS NP) has value x (an individual concept) at the actual world w.

Equations

• Phenomena.Copulas.Studies.Romero2005.be₂_spec x y w = (y w == x)

The A/B Ambiguity: "John knows the price that Fred knows"

The CQ NP "the price that Fred knows" has:

• Extension at w: the unique price concept whose value Fred knows at w.
• Intension: the function mapping each world to that extension.

In our model, Fred knows priceMilk (his Dox-alternatives all agree on milk prices). So the NP's extension is priceMilk at every world.

def Phenomena.Copulas.Studies.Romero2005.thePriceFredKnows (_w : W) : W → E

Extension of "the price that Fred knows" at world w: the unique price individual concept y such that Fred knows y at w. In our model, Fred knows priceMilk at every world (fred_knows_milk), so this is constant.

Equations

• Phenomena.Copulas.Studies.Romero2005.thePriceFredKnows _w = Phenomena.Copulas.Studies.Romero2005.priceMilk

theorem Phenomena.Copulas.Studies.Romero2005.fred_knows_milk (w : W) : know₁ priceMilk fred w = true

Fred knows the price of milk at all worlds.

theorem Phenomena.Copulas.Studies.Romero2005.readingA_w0 : know₁ (thePriceFredKnows Core.Proposition.World4.w0) john Core.Proposition.World4.w0 = true

Reading A: ⟦know₁⟧ + extension of NP.

"John knows the same price as Fred" — both know how much the milk costs. At w0, John's Dox = {w0}, and priceMilk w0 = 0 = priceMilk w0.

theorem Phenomena.Copulas.Studies.Romero2005.readingA_w2 : know₁ (thePriceFredKnows Core.Proposition.World4.w2) john Core.Proposition.World4.w2 = false

Reading A fails at w2: John doesn't know the milk price (his Dox alternatives w2 and w3 assign different milk prices).

def Phenomena.Copulas.Studies.Romero2005.thePriceFredKnows_intension : W → W → E

The intension of "the price that Fred knows": maps each world to the individual concept that Fred knows at that world. In our model this is constant (Fred always knows priceMilk).

Equations

• Phenomena.Copulas.Studies.Romero2005.thePriceFredKnows_intension x✝ = Phenomena.Copulas.Studies.Romero2005.priceMilk

theorem Phenomena.Copulas.Studies.Romero2005.readingB_w2 : know₂ thePriceFredKnows_intension john Core.Proposition.World4.w2 = true

Reading B: ⟦know₂⟧ + intension of NP.

"John knows which price question Fred knows the answer to." At w2, John's Dox = {w2, w3}. The intension maps both to priceMilk. So know₂ checks: ∀w' ∈ Dox(john, w2). thePriceFredKnows_intension w' = thePriceFredKnows_intension w2. Both map to priceMilk.

Note: Reading B is true at w2 even though Reading A is false — John knows which question Fred knows (the milk price question) without knowing the actual milk price. This is the key empirical difference.

theorem Phenomena.Copulas.Studies.Romero2005.readings_differ : know₁ (thePriceFredKnows Core.Proposition.World4.w2) john Core.Proposition.World4.w2 = false ∧ know₂ thePriceFredKnows_intension john Core.Proposition.World4.w2 = true

The two readings genuinely differ: A is false but B is true at w2.

Refutation of Account 1: Evaluation World

Romero §2.4.1: Can the A/B ambiguity be derived by evaluating the NP's extension at different world variables? The answer is no.

The formula has only two possible world binders: λw (top) and ∀w' (from know). Binding by λw gives Reading A. Binding by ∀w' gives a formula that is NOT Reading B — it requires John to also know the answer to the price question, which Reading B does not require.

def Phenomena.Copulas.Studies.Romero2005.account1_readingB (w : W) : Bool

Account 1's "Reading B" candidate (Romero (37)): evaluate the NP at the bound doxastic variable w' instead of the matrix w.

∀w' ∈ Dox(john, w). the price Fred knows at w' = the price Fred knows at w'

The NP extension is computed at w', yielding a single IC, which is then compared at worlds w' and w. But this is NOT Reading B because it still requires John to track the actual price.

Note: in our model, thePriceFredKnows is constant, so the second argument (thePriceFredKnows w') w equals priceMilk w regardless. For non-constant NP extensions, this formula and the paper's (37) would further diverge.

Equations

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

theorem Phenomena.Copulas.Studies.Romero2005.account1_equals_readingA (w : W) : account1_readingB w = know₁ (thePriceFredKnows w) john w

Account 1 collapses: its "Reading B" candidate equals Reading A.

Because thePriceFredKnows is constant (priceMilk at every world), both (thePriceFredKnows w') w' and (thePriceFredKnows w') w reduce to priceMilk w' and priceMilk w respectively. The formula reduces to ∀w' ∈ Dox(john, w). priceMilk w' = priceMilk w — which is exactly know₁ priceMilk john w. The evaluation world trick doesn't help.

Specificational Subjects: Parallel Ambiguity

"The price that Fred thought was $1.29 was (actually) $1.79."

Reading A: The question whose answer Fred thought was $1.29 has actual answer $1.79 (e.g., Fred thought milk costs $1.29; it actually costs $1.79).

Reading B: The question Fred thought had answer $1.29 was the milk-price question (and milk actually costs $1.79).

The same extension/intension mechanism applies to be.

theorem Phenomena.Copulas.Studies.Romero2005.spec_readingA : be₁_spec (priceMilk Core.Proposition.World4.w0) priceMilk Core.Proposition.World4.w0 = true

Specificational be Reading A: extension of SS NP + be₁_spec.

theorem Phenomena.Copulas.Studies.Romero2005.spec_readingB : be₂_spec priceMilk thePriceFredKnows_intension Core.Proposition.World4.w0 = true

Specificational be Reading B: intension of SS NP + be₂_spec.

Crosscategorial Uniformity

know₁ and know₂ perform the same operation — doxastic universal quantification with identity check — at different types. They are crosscategorial variants in the sense of @cite{partee-rooth-1983}.

def Phenomena.Copulas.Studies.Romero2005.knowGeneric {α : Type} [BEq α] (y : W → α) (x : E) (w : W) : Bool

Generic doxastic knowledge template: ∀w' ∈ Dox(x,w). y(w') = y(w). Both know₁ (at type E) and know₂ (at type W → E) instantiate this template — same operation, different type parameter.

Equations

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

theorem Phenomena.Copulas.Studies.Romero2005.know₁_is_knowGeneric (y : W → E) (x : E) (w : W) : know₁ y x w = knowGeneric y x w

know₁ is knowGeneric at type E.

theorem Phenomena.Copulas.Studies.Romero2005.know₂_is_knowGeneric (y : W → W → E) (x : E) (w : W) : know₂ y x w = knowGeneric y x w

know₂ is knowGeneric at type W → E.

def Phenomena.Copulas.Studies.Romero2005.beGeneric {α : Type} [BEq α] (x : α) (y : W → α) (w : W) : Bool

Similarly, be₁_spec and be₂_spec share a template at different types.

Equations

• Phenomena.Copulas.Studies.Romero2005.beGeneric x y w = (y w == x)

theorem Phenomena.Copulas.Studies.Romero2005.be₁_is_beGeneric (x : E) (y : W → E) (w : W) : be₁_spec x y w = beGeneric x y w

theorem Phenomena.Copulas.Studies.Romero2005.be₂_is_beGeneric (x : W → E) (y : W → W → E) (w : W) : be₂_spec x y w = beGeneric x y w

Individual Concepts Are Not Rigid

The A/B ambiguity only arises when the individual concept is non-rigid (varies across worlds). For rigid designators (proper names), extension = intension (up to type), so the two readings collapse.

theorem Phenomena.Copulas.Studies.Romero2005.oil_rigid : priceOil.IsRigid

Oil price is rigid — the two readings of "John knows the price of oil" would be equivalent.

theorem Phenomena.Copulas.Studies.Romero2005.milk_not_rigid : ¬priceMilk.IsRigid

Milk price is NOT rigid — the two readings genuinely differ.

Predicational vs Specificational be

@cite{partee-1987} analyzes the predicational copula as an extensional type-shift BE : ⟨⟨e,t⟩,t⟩ → ⟨e,t⟩. This applies to sentences like "The number of planets is large" (predicational: a property is predicated of the subject).

Romero's be₁_spec/be₂_spec are for specificational copular sentences like "The number of planets is nine" — the subject determines a question and the post-copular phrase gives the answer. The key difference:

• Partee's BE is extensional: both arguments are evaluated at the same world. No intensional mechanism.
• Romero's specificational be is intensional w.r.t. its subject: the subject NP contributes an intensional object (an individual concept or a concept of concepts), not a simple entity.

This is Romero's novel contribution: specificational be is an intensional verb, paralleling know and look for, not a variant of the predicational copula.

See Phenomena.Copulas.Studies.Partee1987 for the predicational analysis.

Refutation of Account 2: Trace Type Ambiguity (§2.4.2)

Account 2 varies the type τ of the trace in [NP the price that Fred knows t_τ]:

• τ = ⟨s,e⟩ → Reading A (using know₁ throughout)
• τ = ⟨s,⟨s,e⟩⟩ → Reading B (using know₂ for matrix, know₃ for embedded)

This requires a third lexical entry know₃ (Romero (43c)), which evaluates the concept-of-concepts at the matrix world before checking doxastic identity.

The problem: once know₂ and know₃ are both in the lexicon, nothing prevents them from swapping positions (know₃ for matrix, know₂ for embedded), generating the unavailable Reading B' — the inverse of B.

def Phenomena.Copulas.Studies.Romero2005.know₃ (y : W → W → E) (x : E) (w : W) : Bool

⟦know₃⟧(y_{⟨s,⟨s,e⟩⟩})(x_e)(w_s) = 1 iff ∀w' ∈ Dox_x(w). y(w)(w') = y(w)(w)

Account 2's additional lexical entry (Romero (43c)). Takes a concept-of-concepts y but evaluates it at the matrix world w first, then checks that the resulting IC's value is stable across dox-alternatives. Unlike know₂, this is NOT a crosscategorial variant — it introduces an extra layer of world evaluation.

Equations

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

theorem Phenomena.Copulas.Studies.Romero2005.know₃_reduces_to_know₁ (y : W → W → E) (x : E) (w : W) : know₃ y x w = know₁ (y w) x w

know₃ structurally collapses to know₁: evaluating the concept-of-concepts at w yields an individual concept, which is then processed identically to know₁. The extra intension layer is absorbed by evaluation.

def Phenomena.Copulas.Studies.Romero2005.readingBprime (w : W) : Bool

Reading B': the unavailable inverse reading overgenerated by Account 2. Uses know₃ for the matrix verb (John) — meaning John knows the actual value of the IC that Fred meta-knows — rather than know₂.

Since know₃ reduces to know₁, B' = know₁ priceMilk john w = Reading A.

Equations

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

theorem Phenomena.Copulas.Studies.Romero2005.readingBprime_eq_readingA (w : W) : readingBprime w = know₁ (thePriceFredKnows w) john w

B' reduces to Reading A (since thePriceFredKnows_intension is constant at priceMilk).

theorem Phenomena.Copulas.Studies.Romero2005.account2_overgenerates : readingBprime Core.Proposition.World4.w2 = false ∧ know₂ thePriceFredKnows_intension john Core.Proposition.World4.w2 = true

Account 2 overgenerates: B' ≠ B at w2 (B' is false, B is true). The spurious Reading B' is predicted to be available but isn't.

theorem Phenomena.Copulas.Studies.Romero2005.know₃_not_crosscategorial : ∃ (y : W → W → E) (x : E) (w : W), know₃ y x w ≠ knowGeneric y x w

know₃ breaks crosscategorial uniformity: unlike know₁ and know₂, it is NOT an instance of knowGeneric. It pre-evaluates the concept-of-concepts y at w before applying the generic schema, so know₃ y x w = knowGeneric (y w) x w rather than knowGeneric y x w.

This is the structural economy argument (§2.5): the proposed analysis uses only know₁/know₂ (both crosscategorial), while Account 2 requires the non-uniform know₃ which breaks the pattern.

Refutation of Account 3: Pragmatic Account (§2.4.3)

@cite{heim-1979}'s pragmatic account: know takes two internal arguments:

• an entity x_e provided by the NP's extension
• a free property P_{⟨e,⟨s,t⟩⟩} contextually supplied

Formula: know(agent, ιx_e[price(x,w) ∧ know(f,x,Q,w)], P, w)

The argument is type e (an entity), NOT ⟨s,e⟩ (an individual concept). Since the NP's extension and the trace co-refer (same variable x), the formula can only track entity-level knowledge. Reading B requires question-level knowledge (which IC Fred knows), which cannot be encoded as a property P of an entity.

def Phenomena.Copulas.Studies.Romero2005.knowPragmatic (agent x : E) (P : E → W → Bool) (w : W) : Bool

Account 3's pragmatic know: the agent knows entity x under property P. ∀w' ∈ Dox(agent, w). P(x)(w')

Equations

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

def Phenomena.Copulas.Studies.Romero2005.priceMilkProperty : E → W → Bool

The most natural property P for "the price that Fred knows": being the price of milk. Under @cite{heim-1979}'s pragmatic bias, the property mentioned in the NP is the most salient one.

Equations

• Phenomena.Copulas.Studies.Romero2005.priceMilkProperty x w = (x == Phenomena.Copulas.Studies.Romero2005.priceMilk w)

theorem Phenomena.Copulas.Studies.Romero2005.account3_entity_frozen (P : E → W → Bool) (w : W) : knowPragmatic john (priceMilk w) P w = worlds.all fun (w' : W) => !Dox john w w' || P (priceMilk w) w'

The structural limitation of Account 3: the entity argument is evaluated and frozen at the matrix world w. Across dox-alternatives w', P is always applied to the SAME entity priceMilk w, never to different entities. This is why the formula can only track whether John knows the entity-level value, not which IC Fred knows.

theorem Phenomena.Copulas.Studies.Romero2005.account3_gives_readingA (w : W) : knowPragmatic john (priceMilk w) priceMilkProperty w = know₁ priceMilk john w

With the salient P, Account 3 gives Reading A (not B). The formula checks whether John knows the entity-level value of priceMilk, which is exactly what Reading A checks.

theorem Phenomena.Copulas.Studies.Romero2005.account3_fails_at_w2 : knowPragmatic john (priceMilk Core.Proposition.World4.w2) priceMilkProperty Core.Proposition.World4.w2 = false ∧ know₂ thePriceFredKnows_intension john Core.Proposition.World4.w2 = true

Account 3 cannot derive Reading B: the salient-P formula is false at w2 (= Reading A), but Reading B is true. Since the argument is type e, no property P can capture question-level knowledge.

theorem Phenomena.Copulas.Studies.Romero2005.account3_extensional_in_ic (y y' : W → E) (agent : E) (P : E → W → Bool) (w : W) (h : y w = y' w) : knowPragmatic agent (y w) P w = knowPragmatic agent (y' w) P w

Type-level expressiveness limitation: Account 3's entity-type argument makes knowPragmatic extensional in the IC — it depends on y only through y w, discarding cross-world behavior. For ANY property P, two ICs that agree at w produce identical results.

theorem Phenomena.Copulas.Studies.Romero2005.account3_type_limitation : priceMilk Core.Proposition.World4.w2 = rigidZero Core.Proposition.World4.w2 ∧ (∀ (P : E → W → Bool), knowPragmatic john (priceMilk Core.Proposition.World4.w2) P Core.Proposition.World4.w2 = knowPragmatic john (rigidZero Core.Proposition.World4.w2) P Core.Proposition.World4.w2) ∧ know₁ priceMilk john Core.Proposition.World4.w2 ≠ know₁ rigidZero john Core.Proposition.World4.w2

The structural refutation: Account 3 cannot distinguish ICs that agree at the evaluation world, for ANY choice of P. But know₁ can, because it checks the IC's values across doxastic alternatives.

priceMilk and rigidZero both yield 0 at w2. No property P makes knowPragmatic tell them apart. Yet know₁ gives different results (false vs true) because milk prices vary at w3 but rigidZero doesn't.

SS Account Refutations (§3.3)

Parallel to §2.4 for CQs. Account 2 requires be₃_spec which collapses to be₁_spec.

def Phenomena.Copulas.Studies.Romero2005.be₃_spec (x : E) (y : W → W → E) (w : W) : Bool

Account 2's be entry (Romero (71c)). Evaluates concept-of-concepts at w twice, collapsing to entity comparison. Parallel to know₃.

Equations

• Phenomena.Copulas.Studies.Romero2005.be₃_spec x y w = (y w w == x)

theorem Phenomena.Copulas.Studies.Romero2005.be₃_reduces_to_be₁ (x : E) (y : W → W → E) (w : W) : be₃_spec x y w = be₁_spec x (y w) w

be₃_spec collapses to be₁_spec.

CQ Knowledge as Partition-Cell Inclusion

@cite{groenendijk-stokhof-1984} partition semantics: a question denotes an equivalence relation on worlds. know₁ y x w checks that all doxastic alternatives of x at w fall within the same partition cell as w — the cell induced by the individual concept y.

def Phenomena.Copulas.Studies.Romero2005.cqQuestion (y : W → E) : QUD W

The CQ question induced by individual concept y: "what is y's value?" Two worlds are equivalent iff y assigns them the same entity.

Equations

• Phenomena.Copulas.Studies.Romero2005.cqQuestion y = QUD.ofProject y

theorem Phenomena.Copulas.Studies.Romero2005.know₁_eq_doxInCell (y : W → E) (x : E) (w : W) : know₁ y x w = worlds.all fun (w' : W) => !Dox x w w' || (cqQuestion y).sameAnswer w w'

know₁ y x w = all dox-alternatives of x at w lie in the same partition cell as w under the CQ question induced by y.

This is the formal bridge between Romero's individual-concept semantics and @cite{groenendijk-stokhof-1984}'s partition semantics for questions: knowing a CQ IS having one's epistemic state contained in a single partition cell.

theorem Phenomena.Copulas.Studies.Romero2005.rigid_trivial_question (y : W → E) (hrig : Core.Intension.IsRigid y) (x : E) (w : W) : know₁ y x w = true

Rigid IC → trivially known by all agents.

When an IC is rigid (constant), the induced CQ partition is trivial — the question has only one possible answer. Every agent's doxastic state is vacuously contained in the single cell. This is why the A/B distinction only matters for non-rigid ICs like priceMilk.

Mention-Some Readings (§4.1)

def Phenomena.Copulas.Studies.Romero2005.know_CQ_SOME (leq : E → E → Bool) (y : W → E) (x : E) (w : W) : Bool

Mention-some know (Romero (101)): ∃z. z ≤ y(w) ∧ ∀w' ∈ Dox(x,w). z ≤ y(w'). Parametric over leq (@cite{link-1983}'s ≤).

Equations

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

def Phenomena.Copulas.Studies.Romero2005.be_SS_SOME (leq : E → E → Bool) (x : E) (y : W → E) (w : W) : Bool

Mention-some be (Romero (105)): x ≤ y(w).

Equations

• Phenomena.Copulas.Studies.Romero2005.be_SS_SOME leq x y w = leq x (y w)

theorem Phenomena.Copulas.Studies.Romero2005.mentionSome_atomic_entails_str (y : W → E) (x : E) (w : W) (h : know_CQ_SOME (fun (x1 x2 : E) => x1 == x2) y x w = true) : know₁ y x w = true

For atomic ≤ (= equality), mention-some entails strongly exhaustive. With no proper parts, any witness z with z = y(w) yields know₁. This is the converse of @cite{groenendijk-stokhof-1984}'s mentionAll_implies_mentionSome.

Connection to G&S Mention-Some Framework

Romero's know_CQ_SOME is an instance of @cite{groenendijk-stokhof-1984}'s knowMentionSome: the CQ under leq induces a mention-some interrogative where abstract(w, z) = leq(z, y(w)), and doxastic universal quantification supplies the knowledge operator.

def Phenomena.Copulas.Studies.Romero2005.cqMSI (leq : E → E → Bool) (y : W → E) : Semantics.Questions.MentionSome.MentionSomeInterrogative W E

The mention-some interrogative induced by a CQ under part-of ≤. "Which part z of y's value holds?"

Equations

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

def Phenomena.Copulas.Studies.Romero2005.doxKnows (agent : E) (w : W) (prop : W → Bool) : Bool

Doxastic universal quantification as a knowledge operator.

Equations

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

theorem Phenomena.Copulas.Studies.Romero2005.know_CQ_SOME_eq_knowMentionSome (leq : E → E → Bool) (y : W → E) (x : E) (w : W) : know_CQ_SOME leq y x w = Semantics.Questions.MentionSome.knowMentionSome (cqMSI leq y) (fun (w : W) (agent : E) (prop : W → Bool) => doxKnows agent w prop) x w

Romero's know_CQ_SOME IS @cite{groenendijk-stokhof-1984}'s knowMentionSome applied to the CQ-induced mention-some interrogative with doxastic knowledge. Definitional equality (rfl).

Extensional Verb Limitation (Appendix)

Romero's Appendix argues that the freedom to combine with extension or intension is a property of intensional verbs (know, look for, spec. be) only. Extensional verbs like kill take type-e arguments, so the NP's contribution is always evaluated at the local world — no room for IC-level interpretation. This is why CQ/SS readings don't arise with extensional verbs.

We formalize this by defining an extensional verb template and proving that it collapses the A/B distinction: it can only access the entity y(w), not the IC y itself, making it impossible to distinguish worlds where y varies.

def Phenomena.Copulas.Studies.Romero2005.extensionalVerb (verb : E → E → W → Bool) (y : W → E) (x : E) (w : W) : Bool

An extensional verb takes an entity argument (type e) and checks a world-relative property. The IC y is always evaluated at w before being passed to the verb.

Equations

• Phenomena.Copulas.Studies.Romero2005.extensionalVerb verb y x w = verb (y w) x w

theorem Phenomena.Copulas.Studies.Romero2005.extensional_collapses (verb : E → E → W → Bool) (y y' : W → E) (x : E) (w : W) (h : y w = y' w) : extensionalVerb verb y x w = extensionalVerb verb y' x w

For extensional verbs, the IC y and any IC y' that agrees at w produce identical results. The verb cannot "see" the IC's behavior at other worlds. This is why CQ readings (which require cross-world IC comparison) are unavailable with extensional verbs.

theorem Phenomena.Copulas.Studies.Romero2005.extensional_vs_intensional : priceMilk Core.Proposition.World4.w2 = rigidZero Core.Proposition.World4.w2 ∧ (∀ (verb : E → E → W → Bool), extensionalVerb verb priceMilk john Core.Proposition.World4.w2 = extensionalVerb verb rigidZero john Core.Proposition.World4.w2) ∧ know₁ priceMilk john Core.Proposition.World4.w2 ≠ know₁ rigidZero john Core.Proposition.World4.w2

The key contrast: priceMilk and rigidZero agree at w2 (both yield 0). An extensional verb CANNOT distinguish them (it only sees the entity at w), but intensional know₁ CAN (it checks doxastic alternatives where they diverge). This is why CQ readings require intensional verbs.

CQ/SS Unification

The paper's main contribution: CQs (with know) and SSs (with be) share the same semantic mechanism — the complement/subject NP contributes either its extension (Reading A) or its intension (Reading B) as an intensional object. The A/B ambiguity is derived from the two interpretive dimensions of the NP, NOT from lexical ambiguity of the verb.

The crosscategorial templates knowGeneric and beGeneric witness this unification: both are parameterized by the same type variable α, with α = E for Reading A and α = (W → E) for Reading B.

theorem Phenomena.Copulas.Studies.Romero2005.cq_ss_unified : (∀ (y : W → E) (x : E) (w : W), know₁ y x w = knowGeneric y x w) ∧ (∀ (y : W → W → E) (x : E) (w : W), know₂ y x w = knowGeneric y x w) ∧ (∀ (x : E) (y : W → E) (w : W), be₁_spec x y w = beGeneric x y w) ∧ ∀ (x : W → E) (y : W → W → E) (w : W), be₂_spec x y w = beGeneric x y w

CQ/SS unification: know₁/be₁_spec (Reading A) and know₂/be₂_spec (Reading B) are instances of the SAME crosscategorial templates at different types. The A/B ambiguity is type-driven, not lexicon-driven.