Transparent quantification into hyperintensional objectual attitudes

Abstract

We demonstrate how to validly quantify into hyperintensional contexts involving non-propositional attitudes like seeking, solving, calculating, worshipping, and wanting to become. We describe and apply a typed extensional logic of hyperintensions that preserves compositionality of meaning, referential transparency and substitutivity of identicals also in hyperintensional attitude contexts. We specify and prove rules for quantifying into hyperintensional contexts. These rules presuppose a rigorous method for substituting variables into hyperintensional contexts, and the method will be described. We prove the following. First, it is always valid to quantify into hyperintensional attitude contexts and over hyperintensional entities. Second, factive empirical attitudes (e.g. finding the site of Troy) validate, furthermore, quantifying over intensions and extensions, and so do non-factive attitudes, both empirical and non-empirical (e.g. calculating the last decimal of the expansion of $\pi$), provided the entity to be quantified over exists. We focus mainly on mathematical attitudes, because they are uncontroversially hyperintensional.

1 Introduction

The topic of this paper is quantifying-in. Quantifying-in is existential quantification into modal or attitudinal contexts, mixing quantification with modalities or attitudes.¹ Technically, one or more existential quantifiers need to bind one or more occurrences of one or more variables inside the scope of one or more modal or attitudinal operators. The key problem which quantifying-in poses is whether, and if so just how, in full technical detail, the existential quantifier succeeds in reaching across any such operator in order to bind one or more variables occurring within the scope of the operator. The standard way of phrasing the problem of quantifying-in is that the same variable has occurrences in two different kinds of context. When bound by the quantifier, the occurrence is extensional; when inside the scope of the operator, the occurrence is non-extensional. So the worry is that the quantificational domain of the variable slides from extensional to non-extensional entities, such that the quantifier cannot get a grip on the non-extensional occurrence of the variable.²

A subsequent logical problem to the problem of variable-binding is to hone in on just those inferential schemas that are valid. A subsequent philosophical problem is to make good intuitive sense of those valid inferences.

Where Op is an arbitrary modal or attitudinal operator, $\varphi ^{n}$ an $n$-ary predicate, $a_{n}\; n$ number of constants, and $\alpha _{n}\;n$ number of variables, the validity of quantifying-in (QI) presupposes that the instances of this schema be valid:

$$\begin{aligned} \frac{{\ldots }Op\ldots (\ldots \varphi ^{n}\ldots a_n \ldots )}{\ldots \exists \alpha _n \ldots Op\ldots (\ldots \varphi ^{n}\ldots \alpha _n \ldots )\ldots }\quad \hbox {QI} \end{aligned}$$

The schema displays the phenomenon of exportation: whereas in the premise the reference to the semantic values of $a_{n}$ occurs inside the scope of Op, in the conclusion the reference, $\alpha _{n}$, occurs outside the scope of Op, thanks to existential quantification over $\alpha _{n}$.

Here are two examples, one modal, the other attitudinal, to make matters more concrete, where $a$ may be an entity of any sort (not just an individual):

• (modality) contingently, $a$ has property $F$; therefore, there is an $x$ such that, contingently, $x$ has property $F$

• (attitude) agent $b$ believes that $a$ has property $F$; therefore, there is an $x$ such that $b$ believes that $x$ has property $F$

We delimit our scope in this paper to attitudes, as opposed to modalities, that are hyperintensional, as opposed to intensional, and objectual, as opposed to propositional. A typical example of a hyperintensional objectual attitude would be:

$$\begin{aligned} a\;\hbox {calculates the square root of 125} \end{aligned}$$

First, the complement of $a$’s computational attitude cannot be an intensional entity, where an intensional entity is defined as per possible-world semantics, a mapping defined on a logical space of possible worlds.³ Intensions fall notoriously short of modelling mathematical attitudes; the lesson is that mathematical complements must be hyperintensionally individuated.

Second, the complement cannot be propositional. If $a$ calculates $X$, then $X$ is not the sort of entity that can be either true or false (the hallmark of the propositional). $a$’s attitude does not consist in, e.g., calculating whether the square root of 125 is an integer, which is a propositional attitude. When calculating the (principal) square root of 125, $a$ is involved in the appetitional, as opposed to contemplative, attitude of attempting to arrive at the outcome of a computational procedure, with no guarantee of obtaining it. The outcome is not a truth-value or a truth-condition, but an irrational number, and $a$ wishes to know which it is, with no guarantee that there even exists a number that is the square root of 125. For instance, if $a$ is calculating the square root of 125 divided by 0, then there is no number that will roll out as the result of the computational effort. Some may even consider the computation illegitimate, because they consider dividing by 0 an illegitimate application of the division function. Still, despite the possible illegitimacy of dividing by zero and despite the necessary absence of a result, it remains an option for $a$ to be engaged in the activity of calculating the result of an arithmetic operation.

In this paper we are going to show how variable-binding is technically compatible with quantifying-in; we are going to describe one particular semantic theory capable of sustaining it; and we will provide suitable domains of quantification. The fact that we are quantifying into hyperintensional contexts is importantly different from quantifying into intensional contexts, because it is just much more technically challenging to do so. Quantifying into the latter, as we show below, is straightforward. Quantifying into the former is problematic because a hyperintensional context, hence any of its constituents, is ‘sealed off’ from immediate logical manipulation. Therefore the challenge becomes how to ‘open up’ a hyperintensional context so as to manipulate one or more of its constituents. The so-called substitution method we describe below is our tool to do just that.

More specifically, we prove the following. First, it is always valid to quantify into hyperintensional attitude contexts and over hyperintensional entities. Any entity is hyperintensional as soon as it obeys a principle of individuation finer than logical equivalence. Any attitude context is hyperintensional as soon as the complement of the attitude is a hyperintensional entity. Second, factive empirical attitudes (e.g. finding the site of Troy) validate, furthermore, quantifying over intensions and extensions, and so do non-factive attitudes, both empirical and non-empirical (e.g. calculating the last decimal of the expansion of $\pi$), provided the entity to be quantified over exists. Thus, if per impossibile the expansion of $\uppi$ would have a unique last decimal then there is a number $x$ such that $x$ is the product of some computational procedure applied to $\uppi$. (Soundness, of course, is another matter.) Similarly for non-factive, empirical attitudes, like worshipping a particular deity, who exists at at least all the world/time couples at which someone worships the deity in question.⁴

The novelties this paper presents are the following. (1) We present an updated and improved definition of hyperintensional individuation, which amounts to a modification of Church’s Alternative (A1).⁵ (2) We present a detailed study of the mathematical attitude of calculating. (3) We present updated rules for quantifying into hyperintensional contexts de dicto, which are an adjustment and generalization of the rules presented in Duží et al. (2010). (4) We present an analysis of ostensibly logically impossible empirical attitudes like seeking a yeti without seeking an abominable snowman, which revolve around two different hyperintensions presenting one and the same intension. (5) We present, finally, rules for quantifying into hyperintensional attitudes de re that correct the rules presented in (Duží et al. (2010), § 5.3).

Arguably, valid rules for quantifying-in are indispensable also from a semi-practical point of view, for instance, in order to design the behaviour of software agents in a multi-agent system. Such a system is composed of autonomous and intelligent, but also resource-bounded agents. The agents act in order to achieve their individual as well as collective goals. There is no central dispatcher to control the behaviour of the system. Instead, the agents’ behaviour and reasoning is governed by messaging among the agents. The autonomous agents communicate with each other by exchanging messages formulated in a quasi-natural language. In order to behave in a reasonable and intelligent way, the agents must be equipped with an ontology and a knowledge base defined over that ontology. While the latter typically contains factual empirical knowledge, the former is a stable part of the system consisting of conceptual knowledge including inference rules. These rules enable the agents to derive or compute inferable knowledge from the basic pool of explicit knowledge. Here is a simple example, to make matters more concrete. Imagine agent $a$ receives the message that agents $b$ and $c$ are calculating the distance from their position to the gas station closest to $a$’s position. In such a situation $a$ cannot infer that there is a gas station close to his position. Instead, $a$ can only infer that $b$ and $c$ share a property, namely the property of being related to the hyperintensional activity of calculating a particular distance. In case $a$ also needs to fill up his car, it is reasonable to send a message to $b$ and $c$ asking to tell him whether they did succeed in calculating the distance. The situation is different if $a$ receives the message that, for instance, b has calculated the distance. For now $a$ can draw the conclusion that $b$ has identified a particular number as the distance measured in kilometres between two points; hence $a$ can also draw the conclusion that there is one gas station nearer to his position than any other gas station. $a$ can go on to, for instance, request the exact location of the station. This paper, however, is devoted to the theoretical aspects of quantifying-in.

The rest of this paper is organized as follows. Section 2 provides philosophical background to the logical problem of quantifying-in and motivates our choice of background theory. Section 3 sets out the philosophical foundations of our background theory. Section 4 sets out its logical foundations, leading up to the general rules of quantification into hyperintensional objectual attitudes. Section 5 presents the various rules of quantifying-in and proves their validity, exemplifying them by way of philosophical applications.

2 Background and overview

Quantifying-in would, naïvely, seem to pose no problem at all. The rule of existential generalization simply serves to make explicit an ontological commitment incurred in the premise. Thus nobody will bat an eyelid if somebody draws this inference:

$$\begin{aligned} \frac{\varphi ^{1}a_1}{\exists x_1 (\varphi ^{1}x_1)}\quad \end{aligned}$$

(EG)

For instance, if the individual Tilman lives in Tilburg then there is at least one element $x$ in the domain of individuals who lives in Tilburg. If the premise is true then the conclusion is the truth that the quantity of objects with a particular quality (in casu living in Tilburg) amounts to at least one.

However, things are not that simple once attitudes or modalities are thrown into the mix, as was mentioned in the Introduction. The main formal problem quantifying-in poses has a syntactic and a semantic, a logical and an ontological aspect. The syntactic aspect is whether the formalism in which quantifying-in is to be carried out sustains variable-binding across modal/attitudinal operators. The semantic aspect is what sort of semantics is required to validate such variable-binding. The logical aspect is which inferences bearing on quantifying-in are valid. The ontological or metaphysical aspect is what sorts of entities one’s theory is geared to quantify over. This ontological issue is, of course, well-known independently of quantifying-in. Where variable $f$ ranges over properties of individuals, this inference remains controversial:

$$\begin{aligned} \frac{\varphi ^{1}a_1}{\exists f^{1}\left( {f^{1}a_1}\right) } \end{aligned}$$

(EG′)

That is, if Tilman lives in Tilburg then there is at least one property $f$ that Tilman has. Those who oppose this instance of EG will agree that Tilman lives in Tilburg, but disagree that he has the property of living in Tilburg, or they will agree that he does have this property, but shy away from quantifying over intensional entities such as properties. We have no such ontological qualms, so we do not think twice about validating this second inference as well.

We investigate quantifying-in by investigating the logic of instances of two inferential schemas that share the same premise but have two different conclusions.

The first schema is this one:

$$\begin{aligned} \frac{a\;\hbox {has an objectual attitude}\; Att\; \hbox {whose complement is}\; X}{\exists x\;({a\;\hbox {has}\;Att\;\hbox {toward}\;x})} \end{aligned}$$

(1)

Schema (1) exemplifies quantification over X, the conclusion making explicit an ontological commitment implicit in the premise. If $X$ belonging to domain Dom occurs as the complement of $a$’s attitude then there is an element $x$ in Dom that occurs as the complement of $a$’s attitude.

But we need to be careful with Dom in order not to draw illicit inferences. For instance, if the premise is that $a$ is seeking an abominable snowman then the conclusion ought not be that there is an individual (an extensional entity) $x$ such that $a$ is seeking $x$. For if there are no abominable snowmen, the inference will have crossed the line from logic into magic, conjuring up an individual out of thin air. For a non-empirical example, if the premise is that $a$ is calculating the sum of seven and five the conclusion ought not to be that there is a number (an extensional entity) $y$ such that $a$ is calculating $y$. For it is nonsense to calculate a number, numbers themselves being computationally inert. To calculate is to apply an arithmetic operation to a suitable supply of numbers as operands with the purpose of obtaining a number as output value. There may be no output value, of course: five divided by zero has no quotient. Still $a$ may be calculating the quotient of five and zero; $a$’s computational effort is futile, for sure, but no less of an effort for it. Again we do not want the conclusion to conjure up a number (of any category) out of thin air by existential quantification over a domain of numbers (of any category).

Examples such as these suggest to us that the respective quantificational ranges of $x, y$ cannot in all cases be those of extensional entities such as individuals or numbers. But what would a suitable quantificational range be? The validity of (1) requires a reasoned answer. This answer will also spell out what ontological category a given instance of $X$ belongs to. Hence (1) turns out to be instrumental in putting out in the open the ontology underneath assorted objectual attitudes.

The second schema is this one:

$$\begin{aligned} \frac{a\;\hbox {has an objectual attitude}\; Att\;\hbox {whose complement is}\; X(b)}{\exists z\;({a\;\hbox {has}\;Att\;\hbox {toward}\;X(z/b)})} \end{aligned}$$

(2)

Schema (2) exemplifies quantification into X. The conclusion extracts a component $z$ from $X$ and quantifies over it. Again the inference appears straightforward. If we can quantify over $X$ then surely it must be equally possible to quantify into any position within $X$. For instance, if $a$ is seeking an abominable snowman then there is a $z$ such that $z$ is abominable and $a$ is seeking $z$ (i.e. $a$ is seeking something abominable). Or if $a$ is calculating the sum of seven and five then there is a $z^{\prime }$ such that $z^{\prime }$ is a number and $a$ is calculating the sum of $z^{\prime }$ and five. However, the same caveats we issued with respect to (1) apply to (2).

The framework within which we discuss and solve the problem of quantifying-in is Transparent Intensional Logic. Formally, TIL is a partial, typed, hyperintensional $\lambda$-calculus. Its $\lambda$-terms are interpreted by way of a procedural, as opposed to denotational, semantics. A procedural semantics construes linguistic meaning as a procedure for converting input objects into output objects; a denotational semantics construes meaning as an output object. For instance, the procedural meaning of ‘5!’ is the very procedure of applying the factorial function to 5, whereas the denotational meaning of ‘5!’ is the number 120. Furthermore, TIL is a partial logic in the specific sense that TIL embraces partially defined functions. Partiality is important in the case of such functors as ‘$\div$’ (division) and ‘the Archbishop of Rome’ when their respective denotation is applied to an argument that fails to return a value. Finally, TIL comes with a ramified type hierarchy, as known from Russell, encompassing a simple type theory, as known from Montague and Church. Pulling off quantifying-in is taxing for the expressive power of any semantic theory, and what recommends TIL for the task of validating quantifying-in is not least TIL’s impressive expressive power. The ramified types enable us to always go one up, as it were, as required by quantification that exceeds the sphere of first-order objects.

Another feature that makes TIL suitable as a background theory for quantifying-in is its top-down approach to logic and semantics. TIL is a context-invariant semantics that is generated by generalizing from the hardest case. The hardest case is a hyperintensional context, which is sensitive to hyperintensional distinctions that do not register in an intensional, let alone extensional context. TIL starts out by devising a semantic theory for hyperintensional contexts and goes on to generalize the same semantics to intensional and extensional contexts. Whichever sort of context a term or expression is embedded within, its meaning will remain the same across contextual embedding. Moreover, its denotational relation will also remain fixed. This is because the denotational relation is a function exclusively of the entity the procedural meaning is typed to produce, and not also of the embedding context. The only class of exceptions are indexical terms such as pronouns, whose meaning remains context-invariant, though. The overarching meta-semantic requirement TIL is designed to satisfy is that a logically manageable semantic theory must respect the laws of extensional logic, the compositionality of meaning, the substitutivity of identicals, and referential transparency (which outlaws reference shift).

The sweet fruit we reap from our top-down approach is that TIL is an extensional logic of hyperintensions and of intensions. Therefore, EG must apply also in hyperintensional and intensional contexts. In fact, from an instrumental point of view, testing whether EG comes out valid provides a clear method for testing various theories of non-extensional contexts.⁶ Does the theory validate quantifying-in in a transparent and principled manner; or does the theory validate quantifying-in by means of all sorts of adhockery, obscure opacity and contextualist epicycles; or does the theory fail to validate quantifying-in altogether? The second path is likely to be followed by those theories of hyperintensionality that work bottom-up, from extensional through intensional to hyperintensional contexts. This methodology is liable to treat non-extensional contexts as semantic and logical anomalies, rather than as what they are, contexts located smack in the heart of colloquial discourse. As language-users we routinely and confidently speak about what might be true, what ought to be true, what somebody hopes to be or become true, what they are searching for, are afraid of, etc. The third path marks either the deplorable failure of a theory to accommodate what its designers set out to accommodate, or it marks the intended failure to do so, on the ground that quantifying-in is considered illogical. Its adherents are not prepared to square off an extensional rule such as EG with non-extensional contexts. As adherents of the first path, we see no problem in principle with applying EG to non-extensional contexts. We do see a string of logical and semantic challenges that call for formally worked-out, principled solutions. This paper is devoted to providing the solutions required.

As it happens, this paper can be seen as a substantiation of a remark made by (Montague (2007), p. 517, n. 32). She hints at the fact that TIL is able to develop a theory of non-propositional attitudes:

An intensional logic based on objects called ‘constructions’ developed by Pavel Tichý (1988) can capture entailments involving propositional and non-propositional objects. If it can be shown that constructions are also involved in intentional attitudes, the theory of constructions would satisfy important motivations for propositionalism without committing to propositionalism.

Propositionalism is the thesis that, in the final analysis, all attitudes, without exception, take propositions as complements.⁷ The present paper is part three of a trilogy devoted to quantifying into hyperintensional contexts. The first two parts address hyperpropositional contexts de re and de dicto, respectively, presenting and proving logical rules for quantifying-in. The present paper does the same for objectual attitudes. Our trilogy on quantifying-in builds upon a handful of previous TIL studies on quantifying-in, namely: Tichý (1986), which quantifies into intensional contexts and over intensions; Materna (1997), which quantifies into hyperintensional contexts and over hyperintensions; and (Duží et al. (2010), § 5.3), which quantifies into intensional and hyperintensional contexts and over hyperintensions, intensions and extensions. Furthermore, (Tichý (1988), § 43) studies briefly hyperintensional (or constructional) attitudes; (Duží et al. (2010), Chap. 5) explores them in great length; (ibid., § 5.2) is devoted to objectual attitudes, and (ibid., § 5.3) is devoted in part to quantifying into objectual attitudes. The rules for quantifying-in have been revised over the years; the present trilogy contains their latest statement.

3 Philosophical foundations

3.1 Which attitudes, if any, are objectual?

The analysanda of this paper pose two problems their propositional brethren do not. First, we simply lack a good name for the non-propositional of the attitudes. Calling them ‘non-propositional’ offers only a negative description. Calling them ‘objectual’ seems also quite inclusive, for propositions are reasonably characterized as objects as well, as is pretty much everything else in a typed universe such as that of TIL. Nor will a linguistic-syntactic criterion do. It might be tempting to characterize, or even define, the analysanda as those attitudes that are denoted by intensional transitive verbs, like ‘to seek’. But doing so will ultimately hold a logical category hostage to a linguistic quirk that is not intrinsic to the analysanda.⁸ So what, if any, is the unifying feature of non-propositional attitudes? We have not come across one. Therefore, we settle for ‘objectual’ for the time being in keeping with the practice introduced by Forbes (2000).⁹

Second, if propositionalism is true there are ultimately no analysanda, for all non-propositional attitudes will reduce to propositional ones. For instance, to seek the fountain of youth will be to strive to make the proposition true that the seeker find the fountain of youth. But there are cogent reasons for resisting propositionalism, at the very least with respect to contemplative attitudes like admiring, considering and, well, contemplating.¹⁰ We continue to take objectual attitudes at face value, as irreducible attitudes in their own right, rather than attempting to provide synonymy-preserving translation rules from non-propositional to propositional attitudes.¹¹ Should a strong philosophical argument emerge to the effect that some attitudes are irreducibly non-propositional, we shall thus already have a detailed theory to account for them.

What we can do is describe by example the sort of attitudes whose behaviour when quantified into we are interested in studying:

• $a$ seeks an abominable snowman

• $a$ finds an abominable snowman

• $a$ admires kindness to strangers

• $a$ wants to become a millionaire

• $a$ wants a colourless green shirt

• $a$ attempts to sing notes beyond reach

• $a$ prevents an accident

• $a$ attempts to prevent an accident

• $a$ worships Baal

• $a$ wants to become the Archbishop of Rome

• $a$ wants to become the Archbishop of Rome, but not the Head of State of the Vatican

• $a$ calculates the square root of (5! + 5)

• $a$ calculates the probability of winning the Spanish state lottery

• $a$ proves Fermat’s Last Theorem (FLT)

• $a$ is puzzled by the proof of FLT

A propositional attitude, on our construal, takes invariably either a possible-world proposition (an intensional entity) or a structured hyperproposition as its complement. Thus propositional attitudes can be defined exhaustively by means of the logical type of their respective complements. Not so with objectual attitudes. The list above sports various complements, including properties (i.e. sets-in-intension), events (typed as possible-world propositions, i.e. truth-values-in-intension), individual offices (i.e. individuals-in-intension), mathematical operations, logical operations, etc. There is little to no reason to assume the above list of complements to be exhaustive. Excluded from our present analysis are cases like “Hitler admires Stalin” in case Stalin is typed as an individual, which in our typed universe is an atomic extensional entity. Relations-in-intension between individuals are not interesting with respect to existential quantification: from $R(a, b)$ it readily follows that there is an $x$ and there is a $y$ such that $R(x, y)$. To make the analysis of “Hitler admires Stalin” logically interesting, ‘Stalin’ needs to be construed as a name of an individual office, such that Hitler’s admiration is aimed at an intensional entity.¹² Only then will Hitler’s relation to Stalin qualify as an attitude.

What we do in Sect. 5 is to demonstrate, for various particular types of complement, how quantifying-in works with respect to factive and non-factive attitudes. These applications will be instances of the particular rules explained and justified in the first part of Sect. 5.

3.2 De re versus de dicto

Following in the footsteps of Frege’s semantic contextualism, Church (1956, p. 8, n. 20) says:

[I]n “Schliemann sought the site of Troy” the names ‘Troy’ and ‘the site of Troy’ occur obliquely. For to seek the site of some other city, determined by a different concept, is not the same as to seek the site of Troy, not even if the two cities should happen as a matter of fact (perhaps unknown to the seeker) to have had the same site.

According to this sort of contextualist semantics, in a context like “The site of Troy is located in Asia Minor” the definite description (or name, in Church’s permissive Fregean sense of ‘name’) ‘the site of Troy’ denotes a particular spot in Asia Minor, provided ‘the site of Troy’ has a unique descriptum, whereas in a context like Church’s above ‘the site of Troy’ denotes a concept of the site of Troy. Church argues that it is a concept of a location, not the location itself, that guides Schliemann’s and every other seeker’s search for the site of Troy.¹³ While we agree with Church’s view on what the object of Schliemann’s search is, we want no truck with his contextualism.

What might a context-invariant semantics for an empirical definite description like ‘the site of Troy’ look like? What TIL can offer is this. Let ‘the site of Troy’ be a functor denoting a function from empirical indices to at most one individual, modelling physical locations as logical individuals (i.e. particulars individuated solo numero).¹⁴ More specifically, let ‘the site of Troy’ denote a function from possible worlds to a partial function from times to individuals; we call such a possible-world intension an individual office. The functor denotes an empirical condition, namely the condition of being a world/time pair such that it has a unique location that is the site of Troy. The definite description nowhere and never denotes the satisfier, if any, of this condition at the world/time pair of evaluation, i.e. ‘the site of Troy’ nowhere and never names a particular location. Nor is the function the meaning of the definite description. Rather its meaning is a procedure whose product is the function. (This claim will be qualified below: the meaning is the privileged member of an equivalence class of procedures, a primus inter pares).

So what is the semantic status of the location, if any, that is the satisfier of the condition at the world/time pair of evaluation? None. It is semantically inconsequential which particular object, if any, happens to satisfy the condition. What does matter is whether there is a satisfier rather than none and whether the satisfier in question is also at the receiving end of other empirical conditions also requiring uniqueness, such that the $F$ is also the $G$.

‘The site of Troy’ always has, by way of semantic fiat, a denotation, namely the function that its meaning produces. ‘The site of Troy’ has sometimes also a reference, namely the value, whenever there is one, of the function the site of Troy at the world/time pair of evaluation. The bearer of a property such as being located in Asia Minor is a value of the function and not the function itself. Yet ‘the site of Troy’ is not linked semantically to its reference. This is the point where TIL’s distinction between de re and de dicto enters. We say that the meaning presenting a function occurs de re when the function descends to its value, if any, at the argument(s) chosen, and occurs de dicto when the function itself is the subject of predication. Hence in “The site of Troy is located in Asia Minor” the meaning of ‘the site of Troy’ occurs de re, whereas it occurs de dicto in “Schliemann seeks the site of Troy”. That is, ‘the site of Troy’ invariably denotes a function, and the logical form in which the meaning of ‘the site of Troy’ occurs determines whether its meaning occurs de re or de dicto. This implementation of the de re/de dicto distinction is what enables TIL to maintain that a definite description is a functor denoting a function without being stuck with the surreal view that a function may be located in Asia Minor.

3.3 Relational versus notional

Central to Quine (1956) is his distinction between notional and relational attitudes.¹⁵ If Quine wants a sloop then, if his attitude is notional, any sloop will do to relieve him of slooplessness, and if his attitude is relational then only a particular sloop will satisfy his wish. The latter is arguably ambiguous: Quine wants a particular object, which happens to be a sloop; or Quine has his mind set on one particular sloop, to the exclusion of all other sloops. Be that as it may, Quine phrases relational attitudes by means of existential locutions: “There is an $x$ such that $x$ is a sloop and Quine wants $x$”. It is this phrasing of relational attitudes that pushes quantifying-in to the fore. Relational attitudes have eluded philosophical conceptualization and logical formalization to a much higher degree than notional attitudes have. The two classical hermeneutic efforts are Kaplan (1968, 1986), followed by Crawford (2008).

Crawford (2008, p. 84) makes a point of distinguishing relational attitudes from de re attitudes, due to the strong conception of the latter he subscribes to:

The assumption is that triadic or de re belief implies that the believer knows who, or which object, his belief is about in the sense that he can in some salient sense identify or recognize it.

We do not share Crawford’s exclusive conception of de re attitudes.¹⁶ In fact, ours is a highly inclusive conception of de re attitudes, because an attribution of a de re attitude reflects the attributer’s perspective and not the attributee’s. This is not to say that we identify notional with de dicto attitudes and relational with de re attitudes. Rather we disregard Quine’s pair. The main reason is the murkiness of the notion of relational attitude, including the attempt to conceptualize and distinguish it from that of notional attitude in terms of quantifying-in. A relational attitude, if we have Quine and his commentators right, is all about having a particular object with a certain property in mind. Yet existential quantification abstracts from who or what has that property, merely recording the fact that the property has an instance. So it seems that relational attitudes are too strong, and quantification too weak, for them to match up.

Quine’s relational/notional pair is historically at the root of the problem of quantifying-in, but not necessarily conceptually at its root. Quantifying-in rears its head, as soon as an existential quantifier needs to reach across a modal or attitudinal operator. It is not intrinsically the case that the attitudinal variant of quantifying-in must be conceptualized philosophically in terms of relational attitudes. It may be that exportation of terms in subject position is valid only for relational attitudes, but since we allow exportation also of terms in predicate position, the very validity of quantifying-in cannot serve, for us, as a criterion of the specifically relational. Put crudely, we are not comfortable with the relational/notional pair and are not sure what exactly to make of it. Whatever relational attitudes may eventually turn out to be, the philosophical challenge quantifying-in poses is, strictly speaking, to make good sense of the notion that the quantity of entities $x_{i}$ that are such that somebody entertains a certain attitude toward $x_{i}$ amounts to at least one.

3.4 Three kinds of context: display versus execution

The dichotomy between de dicto and de re described in Sect. 3.2 is a special case of the three tiers TIL operates with. At the highest level of abstraction, the formal ontology of TIL operates with a fundamental dichotomy between hyperintensions (procedures) and their products, i.e. functions.¹⁷ This dichotomy corresponds to two basic ways in which a procedure (meaning) can occur, to wit, displayed or executed.¹⁸ If the procedure is displayed then the procedure itself is an object of predication; we say that it occurs hyperintensionally. If the procedure is executed, then it is a constituent of another procedure, and an additional distinction can be found at this level. The constituent presenting a function may occur either intensionally (de dicto) or extensionally (de re). If intensionally, then the whole function is an object of predication; if extensionally, then a functional value is an object of predication. Both distinctions are instrumental in selecting a procedure or else what the meaning produces, which is either a function or a functional value, as the functional argument of a function.

For an example of the contrast between displayed and executed procedures, consider the mathematical equation $sin(x)=0$. If $a$ is solving this equation then $a$ is related to the very meaning of “$sin(x)=0$” rather than the set of multiples of the number $\uppi$. $a$ wants to execute the procedure expressed by “$sin(x)=0$” in order to find out which set of real numbers matches the equation. Hence in “$a$ is solving the equation $sin(x)=0$” the meaning of “$sin(x)=0$” is displayed. On the other hand, if we claim that the solution of the equation $sin(x) = 0$ is the set $\{{\ldots }, -2{\uppi }, -{\uppi }, 0, \uppi , 2{\uppi }, \ldots \}$ the meaning of “$sin(x)=0$” is executed to produce the set which is claimed to be identical to $\{\ldots , -2{\uppi }, -{\uppi }, 0, \uppi , 2{\uppi }, \ldots \}$. Yet the constituent meaning of “$sin(x)=0$” occurs intensionally in the meaning of “The solution of the equation $sin(x) = 0$ is the set $\{\ldots , -2{\uppi }, -{\uppi }, 0, \uppi , 2{\uppi },\ldots \}$”. The whole set (a characteristic function) is the object of predication. An example of an extensional occurrence of the meaning of ‘sin’ would be provided by the meaning of the simple sentence “$sin(\uppi ) = 0$”. Here the value of the function sine at the argument $\uppi$ is the object of which it is predicated that it is equal to zero.

The same differentiation applies also to the meanings of terms stemming from empirical language. For an example of the contrast between intensional and extensional occurrence, consider predication. Predication, in TIL, is an instance of functional application: a characteristic function is applied to a suitable argument in order to obtain a truth-value, according as the argument is an element of the set. In the case of predication of empirical properties, the relevant set is obtained by extensionalizing a property. In the context “The site of Troy is located in Asia Minor” we want the functional value of the office the site of Troy to occur either as an argument for the set of entities located in Asia Minor or as an argument for the binary relation (-in-intension) located in whose second argument is Asia Minor. Hence the meaning of ‘the site of Troy’ occurs extensionally here. On the other hand, when Schliemann sought the site of Troy, he was not related to any value of the denoted function. Rather he was related to the whole office aiming to determine its value, if any. As a result, the meaning of ‘the site of Troy’ occurs intensionally in “Schliemann sought the site of Troy”. Similarly, the term ‘the temperature in Prague’ occurs extensionally in “The temperature in Prague is 13 $^{\circ }$C”, while in “The temperature in Prague is rising” the same meaning of this definite description occurs intensionally. To be rising is a property of the whole function rather than of any value. Finally, in “$a$ knows (hyperintensionally) that the temperature in Prague is 13 $^{\circ }$C” the same meaning occurs hyperintensionally. When knowing something hyperintensionally, we are related to the very meaning of the embedded clause rather than the produced function (a possible-world proposition in this case).

The two distinctions, between displayed/executed and intensional/extensional, allow us to distinguish between three sorts of context. This paper zooms in on hyperintensional contexts. What uniquely characterizes a hyperintensional context is the fact that in it a hyperintension occurs displayed rather than executed. The hyperintension is not executed in order to obtain an object beyond it, namely the object it is typed to present (either a lower-order hyperintension or a function). Instead the hyperintension itself occurs as a functional argument.

Here is a summary of the three kinds of context:

• hyperintensional context: one or more hyperintensions occur displayed (though one or more hyperintensions at least one order higher need to be executed in order to produce the displayed hyperintensions)

• intensional context: one or more hyperintensions are executed in order to produce one or more functions (moreover, the executed hyperintensions do not occur within another hyperintensional context)

• extensional context: one or more hyperintensions are executed in order to produce one or more particular values of one or more functions at one or more given arguments (moreover, the executed hyperintensions do not occur within another intensional or hyperintensional context).

The basic idea underlying the above trifurcation is that the same set of logical rules apply to all three kinds of context, but they operate on different complements: hyperintensions, functions, and functional values, respectively. Consider the rule of substitution of identicals. For a puzzle from the standard repertoire, consider how Partee’s puzzle is generated¹⁹:

$$\begin{aligned} \frac{{\begin{array}{l} \hbox {the temperature is}\;90^{\circ }\hbox {F}; \\ \hbox {the temperature is rising} \\ \end{array}}}{90^{\circ }\;\hbox {F is rising}} \end{aligned}$$

Where ‘the temperature’ is a functor denoting a function, the first premise predicates a property of a value of the function whereas the second premise predicates a property of the entire function. A necessary requirement of valid substitution in the position denoted by ‘the temperature’ inside the intensional context denoted by “The temperature is rising” requires swapping one intension (a function) for another; swapping an intension for a mere extension (a functional value) will not do. The morale is that the rule of substitution of identicals has been misapplied, because the substituend is of the wrong kind. The morale is not that the rule ‘breaks down’ when applied to non-extensional contexts.²⁰

Nor will swapping a hyperintension for an intension preserve validity in this argument:

$$\begin{aligned} \frac{{\begin{array}{l} \hbox {Tilman knows that the glass before him is half-full}; \\ \hbox {necessarily},\;\hbox {whatever is half-full is half-empty, and} \\ \hbox {whatever is half-empty is half-full} \\ \end{array}}}{\hbox {Tilman knows that the glass before him is half-empty}} \end{aligned}$$

The argument is valid if Tilman’s two epistemic attitudes take possible-world propositions as complements. It is not valid if, as we are assuming, Tilman’s complements are hyperpropositions, for then only hyperpropositions are the proper kind of substituends.

Needless to say, nor will swapping a hyperintension for an extension preserve validity:

$$\begin{aligned} \frac{{\begin{array}{l} \hbox {Tilman computes 5}! \\ \hbox {5}! = \hbox {120} \\ \end{array}}}{\hbox {Tilman computes 120}} \end{aligned}$$

The complements of Tilman’s hyperpropositional knowledge and his computational efforts are hyperintensional contexts, in which hyperintensions must be substituted for hyperintensions.

The technical ability to shift between executing and displaying hyperintensions is what helps TIL to a notion of hyperintensional attitudes in the first place. Displayed hyperintensions figure as the complements of hyperintensional attitudes by being the second argument of functions taking agents to the hyperintensions they take an attitude towards. Displayed hyperintensions pose far greater technical challenges than do executed hyperintensions, not least when quantifying into them. These technical challenges take centre stage in the remainder of this paper.

4 Logical foundations

4.1 Constructions as hyperintensions

Above we referred to hyperintensions interchangeably as ‘hyperintensions’, ‘procedures’ and ‘meanings’. These three labels capture three different aspects of one and the same underlying notion. The notion in question is that of construction; cf. Chap. 1. Constructions are the key entities of TIL. They are hyperintensionally individuated procedures, of one or multiple steps, and they serve both as linguistic meanings and as the complements of hyperintensional attitudes. When we talk about hyperintensional attitudes, we intend constructional attitudes. Just to be clear, constructions are not functions, nor are they formulae or otherwise linguistic entities. They are kindred to Platonic forms, Bolzano-style ideas-in-themselves (Vorstellungen an sich) and Frege-style Sinn. Their inductive definition below enumerates six different constructions.

Three remarks straightaway. The first is that variables are constructions. Technically, variables behave as defined by Tarski, in virtue of total functions assigning values to variables according to a valuation function $v$. But $x$ is not a piece of language; ‘$x$’ is: ‘$x$’ designates the construction $x$, which constructs its value in one step simply by having it as its $v$-assigned value. The second remark is that the construction Composition, which is the procedure of applying a function to an argument, is impervious to whether it is ever executed by an agent, and whether the procedure produces a product. The same Platonic traits are featured by Closure, which is the procedure of forming a function, except that a Closure always produces a product, to wit a function, however degenerate the function may be. The third remark is that Trivialization has the effect, when applied to an object, that the Trivialization displays that object. This is absolutely critical in helping us to a theory of hyperintensional attitudes. Thus, if ‘$X$’ denotes some construction, the notation ‘${}^{0}\!X$’ (read: ‘the Trivialization of the construction $X$’) means that we are to ‘look at’ $X$ itself, whereas the notation ‘$X$’ means that we are to ‘look at’ what $X$ constructs (if anything).

Tichý, in (1988, Chap. 5), introduces the logical core of TIL in the shape of two fundamental definitions. He first defines constructions and afterwards the ramified hierarchy of types. He then goes on to explain how the products of particular constructions are typed. In the interest of simplicity we first define simple types of order 1, then constructions together with the types of their products, and finally the ramified hierarchy of types.

Definition 1

(types of order 1) Let $B$ be a base, where a base is a collection of pair-wise disjoint, non-empty sets. Then:

• (i) Every member of $B$ is an elementary type of order 1 over B.

• (ii) Let ${\upalpha }, \upbeta _{1}, \ldots , \upbeta _{m}(m > 0)$ be types of order 1 over $B$. Then the collection ($\upalpha \upbeta _{1}\ldots \upbeta _{m})$ of all $m$-ary partial mappings from $\upbeta _{1} \times ..\times \upbeta _{m}$ into ${\upalpha }$ is a functional type of order 1 over B.

• (iii) Nothing else is a type of order 1 over B.$\square$

Remark 1

For the purposes of natural-language analysis, we are currently assuming the following base of elementary types, each of which is part of the ontological commitments of TIL:

$\hbox {o}$::

the set of truth-values {T, F};

$\upiota$::

the set of individuals (constant universe of discourse);

$\uptau$::

the set of real numbers (doubling as temporal continuum);

$\upomega$::

the set of logically possible worlds (logical space).

Definition 2

(construction)

• (i) (Variable) Let valuation $v$ assign object $o$ to variable $x$. Then $x$ is a construction that v-constructs $o$.

• (ii) (Trivialization) Let $X$ be any object whatsoever (i.e. an extension, an intension, or a construction). Then ${}^{0}\!X$ is the Trivialization of $X$, which constructs $X$ without any change of $X$.

• (iii) (Composition) Let $X v$-construct a function $f$ of type (${\upalpha }\upbeta _{1}\ldots \upbeta _{m})$, and let $Y_{1},\ldots ,Y_{m} v$-construct entities $B_{1},\ldots ,B_{m}$ of types $\upbeta _{1},\ldots ,\upbeta _{m}$, respectively. Then the Composition $[X Y_{1}\ldots Y_{m}$] v-constructs the value (an entity, if any, of type ${\upalpha }$) of $f$ on the tuple argument $\left\langle {B_1,\ldots ,B_m} \right\rangle$. Otherwise the Composition [$X Y_{1}\ldots Y_{m}$] does not v-construct anything and so is $v$-improper.

• (iv) (Closure) Let $x_{1},\ldots ,x_{m}$ be pair-wise distinct variables and $Y$ a construction. Then [$\lambda x_{1} \ldots x_{m} Y$] is the construction $\lambda$-Closure (or Closure). It $v$-constructs the following function $f$ of type (${\upalpha }\upbeta _{1} \ldots \upbeta _{m})$. Let variables $x_{1}, \ldots , x_{m}$ v-construct entities of types $\upbeta _{1},\ldots ,\upbeta _{m}$, and let Y v-construct an ${\upalpha }$-entity. Let $v(B_{1}/x_{1},\ldots ,B_{m}/x_{m})$ be a valuation identical with $v$ at least up to assigning objects $B_{1}/\upbeta _{1},\ldots ,B_{m}/\upbeta _{m}$ to variables $x_{1},\ldots , x_{m}$. If $Y$ is $v(B_{1}/x_{1},\ldots ,B_{m}/x_{m})$-improper (see iii), then $f$ is undefined on $\left\langle {B_1, \ldots ,B_m} \right\rangle$. Otherwise the value of $f$ on $\left\langle {B_1, \ldots ,B_m} \right\rangle$ is the $\upalpha$-entity $v(B_{1}/x_{1},\ldots ,B_{m}/x_{m})$-constructed by $Y$.

• (v) (Single Execution) Let $X\,v$-construct object $o$. Then the Single Execution ${}^{1}\!X v$-constructs $o$. Let $X$ be either a non-construction or a $v$-improper construction. Then ${}^{1}\!X$ is v-improper.

• (vi) (Double Execution) Let $X\,v$-construct a construction $Y$ and let $Y\,v$-construct object $Z$ (possibly itself a construction). Then the Double Execution ${}^{2}\!X\,v$-constructs $Z$. Let $X$ be a non-construction or a construction not constructing another construction, or a construction constructing a $v$-improper construction. Then ${}^{2}\!X$ is v-improper.

• (vii) Nothing else is a construction.

The overarching idea behind the notion of construction is that, given some input objects, we can apply operations or procedures or constructions to obtain some output objects (or none, in some instances of Composition, Single and Double Execution). As already mentioned, a variable constructs an object by having that object as its value dependent on a valuation function $v$ arranging variables and objects in a sequence. Trivialization is our objectual counterpart of a non-descriptive constant term, which simply harpoons a particular object. In programming jargon, Trivialization calls an object: no object can be operated on without first having been called, i.e. retrieved from a pool of objects. Composition is the procedure of functional application, rather than the functional value (if any) resulting from application.²¹ Closure is the procedure of functional abstraction, rather than the resulting function. The Single Execution ${}^{1}\!X$ is the same construction as $X$, provided $X$ is a construction at all: the default mode in which constructions occur is Single Execution. Single Execution serves basically to differentiate between $v$-proper constructions, which are the ‘successful’ constructions, and everything else, which are either $v$-improper (‘failing’) constructions or non-constructions, which cannot be executed at all. Double Execution encodes the transitivity of construction.²²

Variables and Trivializations, as well as those instances of Single Execution where $X$ is an atomic construction, are the one-step or primitive or atomic constructions of TIL, and none of them can be improper. In particular, what does not exist cannot be Trivialized. (Similarly, what does not exist cannot be named; but it can be described, as per ‘the largest prime’ or ‘is a winged unicorn’ or ‘the planet between Mercury and the Sun’.) Composition, Closure, and Double Execution, as well as those instances of Single Execution where $X$ is composite, are the multiple-step or composite procedures. An atomic construction is a structured whole with but one constituent part, namely the construction itself. Importantly, the constituent part of ${}^{0}\!X$ is ${}^{0}\!X$ and not $X$, which is located beyond ${}^{0}\!X$: the product of a procedure is no part of the procedure. A composite construction is a structured whole with more constituent parts than just itself.

${\upalpha }$-intensions are functions of type (${\upalpha }{\upomega })$, i.e. mappings with domain in possible worlds $\upomega$ and range in the arbitrary type ${\upalpha }$. The frequently occurring type of ${\upalpha }$-intensions is ((${\upalpha }{\uptau }){\upomega })$, i.e. mappings from possible worlds to chronologies of objects of type ${\upalpha }$, abbreviated as ‘${\upalpha }_{{\uptau }{\upomega }}$’, where a chronology is a mapping from times $\uptau$ to ${\upalpha }$.

Examples of frequently occurring intensions are:

• propositions (i.e. empirical truth-conditions) of type $\hbox {o}_{{\uptau }{\upomega }}$ (e.g. that the sky is blue)

• properties of individuals of type $(\hbox {o}{\upiota })_{{\uptau }{\upomega }}$ (e.g. being blue)

• individual roles/offices of type $\upiota _{{\uptau }{\upomega }}$ (e.g. the first dog in space)

• attributes of type $({\upiota }{\upiota })_{{\uptau }{\upomega }}$ (e.g. the king of)

• binary relations-in-intension between individuals of type ($\hbox {o}{\upiota }{\upiota })_{{\uptau }{\upomega }}$ (e.g. kicking)

• propositional attitudes of type $(\hbox {o}{\upiota }\hbox {o}_{{\uptau }{\upomega }})_{{\uptau }{\upomega }}$ (e.g. knowing that a certain proposition is true)

• hyperpropositional attitudes of type $(\hbox {o}{\upiota }{}{*}_{n})_{{\uptau }{\upomega }}$ (e.g. knowing* that a certain propositional construction constructs a proposition that is true).

The definition of the ramified hierarchy of types divides into three parts: firstly, simple types of order 1, which were already defined by Definition 1; secondly, constructions of order $n$; thirdly, types of order $n+1$.

Definition 3

(ramified hierarchy of types)

$\mathbf{T}_{\mathbf{1}}$ (types of order 1). See Definition 1.

$\mathbf{C}_{\varvec{n}}$ (constructions of order n)

• (i) Let $x$ be a variable ranging over a type of order $n$. Then $x$ is a construction of order n over B.

• (ii) Let $X$ be a member of a type of order $n$. Then ${}^{0}\!X, {}^{1}\!X, {}^{2}\!X$ are constructions of order n over B.

• (iii) Let $X, X_{1},\ldots , X_{m}(m\,{>}\,0)$ be constructions of order $n$ over $B$. Then $[X\,X_{1}\!\ldots \! X_{m}]$ is a construction of order n over B.

• (iv) Let $x_{1}, \ldots , x_{m}, X(m\,{>}\,0)$ be constructions of order $n$ over $B$. Then [$\lambda x_{1} \ldots x_{m} X]$ is a construction of order n over B.

• (v) Nothing is a construction of order n over $B$ unless it so follows from C $_{\varvec{n}}$ (i)–(iv).

$\mathbf{T}_{\varvec{n}+\mathbf{1}}$ (types of order n $+$ 1)

Let ${*}_{n}$ be the collection of all constructions of order $n$ over $B$. Then

• (i) ${*}_{n}$ and every type of order n are types of order n $+$1.

• (ii) If $m > 0$ and $\upalpha , \upbeta _{1},\ldots ,\upbeta _{m}$ are types of order $n+1$ over $B$, then ($\upalpha \upbeta _{1} \ldots \upbeta _{m})$ (see $\hbox {T}_{1}$ (ii)) is a type of order n $+$ 1 over B.

• (iii) Nothing else is a type of order n $+$ 1 over B.

Example 1

The number 1 and the function $+$ are objects belonging to types $\uptau$ and (${\uptau }{\uptau }{\uptau }$), respectively, which are types of order 1. The Trivializations ${}^{0}\!1$, ${}^{0}\!+$ are thus constructions of order 1 belonging to type $*_{1}$, the type of order 2. If a variable $x\;v$-constructs numbers then $x$ is a construction of order 1 belonging to $*_{1}$, the type of order 2. The Composition $[{}^{0}{+}\,x\,{}^{0}{1}] \, {v}$-constructs the successor of the number $v$-constructed by $x$. The Closure ${\lambda }x$ [${}^{0}\!{+}\,x \,{}^{0}\!{1}$] constructs the successor function of type (${\uptau }{\uptau }$), a type of order 1. Hence this Composition and this Closure are also constructions of order 1 belonging to ${*}_{1}$, the type of order 2. The Trivializations of these constructions, i.e. ${}^{0}\!{x}$, ${}^{0}[{}^{0}\!{+}\,x\,{}^{0}\!{1}]$, ${}^{0}[{\lambda }x\; [{}^{0}\!{+}\,x\,{}^{0}\!{1}]]$, are constructions of order 2 belonging to ${*}_{2}$, the type of order 3. The Trivialization ${}^{0}[{}^{0}[{\lambda }x\;[{}^{0}\!{+}\;x \;{}^{0}\!{1}]]]$, or ‘$^{00}[{\lambda }x\;[{}^{0}\!{+}\,x \,{}^{0}\!{1}]]$’ for short, is a construction of order 3, i.e. a member of ${*}_{3}$, the type of order 4. This Trivialization constructs a member of the type of order 3, namely the Trivialization ${}^{0}[{\lambda }x\;[{}^{0}\!{+}\;x\;{}^{0}\!{1}]]$. The Double Execution ${}^{2}[{}^{0}[{\lambda }x\,[{}^{0}{+}\,x\,{}^{0}\!{1}$]]], or ‘${}^{20}[{\lambda }x\,[{}^{0}\!{+}\,x\,{}^{0}\!{1}]]$’ for short, is also a construction of order 3, i.e. a member of ${}{*}_{3}$, which is the type of order 4. It constructs what is constructed by what is constructed by the Trivialization ${}^{0}[{\lambda }x\,[{}^{0}\!{+}\,x\,{}^{0}\!{1}$]], which is the successor function, a member of the type of order 1. In general, ${}^{20}\!{C}\,v$-constructs the same object as $C\,v$-constructs, if any; only that if $C$ is a construction of order $n$ then ${}^{0}\!{C}$ is a construction of order $n+1$ and ${}^{20}\!{C}$ is a construction of order $n+2$.

Definition 4

(quantifiers) The quantifiers $\forall ^{{\upalpha }}, \exists ^{{\upalpha }}$ are total, type-theoretically polymorphous functions of type $(\hbox {o}(\hbox {o}{\upalpha }))$, for an arbitrary type ${\upalpha }$, defined as follows. The universal quantifier $\forall ^{{\upalpha }}$ is the function that associates a class $S$ of ${\upalpha }$ elements with T if $S$ contains all the elements of type ${\upalpha }$, otherwise with F. The existential quantifier $\exists ^{{\upalpha }}$ is the function that associates a class $S$ of ${\upalpha }$ elements with T if $S$ is a non-empty class, otherwise with F. $\square$

Remark 2

Since the topic of this paper is existential quantification, we will examine below various arguments whose conclusion is an existentially quantified construction. One should keep in mind, though, that quantifiers are not ‘special symbols’ as in first-order predicate logic. Rather they are classes of classes of ${\upalpha }$-objects. Thus existential quantification translates into the procedure of applying the existential quantifier $\exists ^{{\upalpha }}$ to a class of ${\upalpha }$-objects. For instance, if Transcendental, of type ($\hbox {o}{\uptau }$), is the class of transcendental numbers, then to claim that there are transcendental numbers amounts to claiming that Transcendental is a non-empty class: [${}^{0}\exists {}^{\uptau }\;{}^{0}{ Transcendental}$]. Moreover, since we work with properly partial functions, before applying an existential quantifier we must first prove that the argument class is non-empty. For instance, if : is the division function of type (${\uptau }{\uptau }{\uptau })$, this would be an invalid derivation: $[{}^{0}{=}\;[{}^{0}{:}\;{}^{0}5 \;{}^{0}{0}]\;{}^{0}{0}] \vdash [{}^{0}\exists ^{\uptau }\;{\lambda }x\;[{}^{0}{=}\;[{}^{0}{:} \;{}^{0}5\;{}^{0}{0}]\;x]$, because the class constructed by the Closure ${\lambda }x\;[{}^{0}\!{=}\;[{}^{0}{:} \;{}^{0}{5} \;{}^{0}{0}]\;x]$ is not non-empty. It is a degenerate class whose characteristic function is undefined at all its arguments, because the Composition $[{}^{0}\!{:} \;{}^{0}\!{5}\;{}^{0}\!{0}]$ is $v$-improper, and so is the Composition $[{}^{0}\!{=}\,[{}^{0}{:} \;{}^{0}\!{5}\;{}^{0}\!{0}]\;x]$ for every valuation $v$.

Notational conventions Some logical objects, like truth-functions and quantifiers (cf. Definition 4), are extensional entities: $\wedge$ (conjunction), $\vee$ (disjunction) and $\supset$ (implication) are of type (ooo), and $\lnot$ (negation) of type (oo). When using constructions of truth-functions, we will omit Trivialization and use infix notation to conform to standard notation in the interest of better readability. Also when using constructions of identities of ${\upalpha }$-entities, $=_{{\upalpha } }/(\hbox {o}{\upalpha }{\upalpha })$, we omit Trivialization, the type subscript, and use infix notation when no confusion can arise. Instead of ‘[${}^{0}\exists {}{}^{{\upalpha }}\; {\lambda }x \ldots ]$’, ‘$[{}^{0}\forall {}^{{\upalpha }}\;{\lambda }x \ldots ]$’ we will write ‘${\exists } x \ldots$’, $`\forall x \ldots$’ when no confusion arises. Below all type indications will be provided outside the formulae in order not to clutter the notation. Furthermore, ‘$X/{\upalpha }$’ means that an object $X$ is (a member) of type ${\upalpha }$; $`X \rightarrow _{v}{\upalpha }$’ means that the type of the object valuation-constructed by $X$ is ${\upalpha }$. We write ‘$X \rightarrow {\upalpha }$’ if what is $v$-constructed does not depend on a valuation $v$. This holds throughout: the variables $w \rightarrow _{v} {\upomega }$ and $t \rightarrow _{v} {\uptau }$. If $C \rightarrow _{v}{\upalpha }_{{\uptau }{\upomega }}$ then the frequently used Composition $[[Cw] t]$, which is the intensional descent (a.k.a. extensionalization) of the ${\upalpha }$-intension $v$-constructed by $C$, will be encoded as ‘$C_{wt}$’.

Example 2

Let Cot, $Sin/({\uptau }{\uptau })$ be the trigonometric functions Cotangent, Sine, respectively, ${\uppi }/{\uptau }, Improper/(\hbox {o}{*}_{1})$ the class of constructions of order 1 that are $v$-improper for every valuation $v$. Then

$$\begin{aligned}&{}^{0}{Cot}/{*}_{1} \rightarrow ({\uptau }{\uptau }); {}^{0}{\uppi }/{*}_{1} \rightarrow \uptau ; \;[{}^{0}{Cot}\;{}^{0}{\uppi }]/{*}_{1} \rightarrow \uptau ;\;{}^{0}\!{Improper}/{*}_{2} \rightarrow (\hbox {o}{*}_{1});\\&{}^{0}[{}^{0}{Cot}\;{}^{0}{\uppi }]/{*}_{2} \rightarrow {*}_{1};\; [{}^{0}{Improper}\,{}^{0}[{}^{0}{Cot}\;{}^{0}{\uppi }]]/{*}_{2} \rightarrow \hbox {o}; \\&[{}^{0}{=}_{({\uptau }{\uptau })}\,[{}^{0}Sin\,{}^{0}{\uppi }]\,{}^{0}{0}]/{*}_{1} \rightarrow \hbox {o},\;\hbox {or}\;`[[{}^{0}{Sin}\,{}^{0}{\uppi }] = {}^{0}{0}]\text {'}\;\hbox {for short};\\&[{}^{0}{\wedge }\,[{}^{0}{Improper}\,{}^{0}[{}^{0}{Cot}\,{}^{0}{\uppi }]]\, [{}^{0}{=}_{({\uptau }{\uptau })}\,[{}^{0}{Sin}\,{}^{0}{\uppi }]\,{}^{0}{0}]]/{*}_{2} \rightarrow \hbox {o},\;\hbox {or}\\&`[[{}^{0}{Improper}\,{}^{0}[{}^{0}{Cot}\,{}^{0}{\uppi }]] \wedge [[{}^{0}{Sin}\,{}^{0}{\uppi }] = {}^{0}{0}]]\text {'},\;\hbox {for short} \end{aligned}$$

Example 3

Let $Happy/(\hbox {o}{\upiota })_{{\uptau }{\upomega }}$ be a property of individuals, $Tilman/\upiota$ an individual. Then $[[{}^{0} Happy\,w] t]/{*}_{1} \rightarrow (\hbox {o}{\upiota })$, or $`{}^{0}Happy_{wt}\text {'}$ for short, $v$-constructs the population of the property of being happy in a given $w$ and $t$; $[{}^{0}Happy_{wt}\;{}^{0}Tilman]/{*}_{1} \rightarrow \hbox {o}v$-constructs T or F according as Tilman is happy in a given world $w$ and time $t$ of evaluation, and ${\lambda }w{\lambda }t\;[{}^{0}Happy_{wt }\;{}^{0}Tilman]/{*}_{1}\rightarrow \hbox {o}_{{\uptau }{\upomega }}$ constructs the proposition that Tilman is happy. If $Know/(\hbox {o}{\upiota }{}{*}_{n})_{{\uptau }{\upomega }}$ is a hyperpropositional attitude, then the Closure ${\lambda }w{\lambda }t\;[{}^{0}\!{Know}_{wt} \;{}^{0}\!{Tom}\;{}^{0}[{\lambda }w{\lambda }t\;[{}^{0}\!{Happy}_{wt}\;{}^{0}\!{Tilman}]]]/{*}_{2} \rightarrow \hbox {o}_{{\uptau }{\upomega }}$ constructs the proposition that Tom (hyperintensionally, i.e. explicitly) knows that Tilman is happy.

4.2 Displayed versus executed constructions

In Sect. 3.4 we sketched the difference between the two modes in which a construction can occur, to wit, displayed and executed. The Trivialization ${}^{0}C$ of a construction $C$ displays the construction C and all the subconstructions of $C$. Hence $C$ is not executed, and so does not obtain an object beyond $C$. Instead $C$ occurs itself as a functional argument. Thus we have this contrast:

• (executed Composition) [${}^{0}\!{Cot}\;{}^{0}{\uppi }$]: its constituent parts are the Composition itself, ${}^{0}\!{Cot},\;{}^{0}{\uppi }$. Since the cotangent function is not defined at $\uppi$, the Composition is $v$-improper for any valuation $v$

• (displayed Composition) ${}^{0}[{}^{0}\!{Cot}\;{}^{0}{\uppi }$]: this time the only constituent part of this construction is the Trivialization itself, ${}^{0}[{}^{0}\!{Cot}\;{}^{0}\!{\uppi }$]. The Composition [${}^{0}\!{Cot}\;{}^{0}{\uppi }$] is not a constituent part. Instead it is displayed, in virtue of being constructed by its Trivialization. In [${}^{0}Improper\;{}^{0}[{}^{0}\!{Cot}\;{}^{0}\!{\uppi }$]] the Composition [${}^{0}\!{Cot}\;{}^{0}{\uppi }$] is also displayed rather than executed, and the Composition [${}^{0}Improper\;{}^{0}[{}^{0}\!{Cot}\;{}^{0}{\uppi }$]] constructs T, for it is true that the construction [${}^{0}\!{Cot}\;{}^{0}{\uppi }$] is $v$-improper for every valuation $v$. “[${}^{0}Improper\;[{}^{0}\!{Cot}\;{}^{0}\!{\uppi }$]]” would mean that what [${}^{0}\!{Cot}\;{}^{0}{\uppi }$] constructs is improper, which is literally nonsensical.

To further demonstrate the difference between displayed and executed constructions, consider this hyperintensional objectual attitude:

$$\begin{aligned} a\;\hbox {calculates the cotangent of}\;\uppi \end{aligned}$$

Types: $a \rightarrow _{v} \upiota$: a construction of an individual; $Cot/({\uptau }{\uptau })$: the trigonometric cotangent function; $Calculate/(\hbox {o}{\upiota }{*}_{n})_{{\uptau }{\upomega }}$: a relation-in-intension of an individual to a construction.

If an agent is related to what [${}^{0}\!{Cot}\;{}^{0}\!{\uppi }$] constructs then the agent will be related to nothing. But though the agent’s computational efforts are bound to be futile, the agent is still engaged in a computational activity in which the agent is related intentionally to something rather than nothing. By relating a mathematician to a construction, of type ${}{*}_{n}$, we are not relating the mathematician to a piece of mathematical syntax. For sure, apart from simple so-called mental maths, computational acts are aided by syntactic manipulation; but to calculate is not tantamount to manipulating syntax. As (Brown (1999), pp. 92–93) rightly says, ‘2’ and ‘two’ have the same sense; similarly ‘2 $+$ 5’ and ‘two plus five’ share the same sense. In TIL we say that the last two terms encode one and the same Composition: $[{}^{0}\!{+}\;{}^{0}\!{2}\;{}^{0}\!{5}]$. It is also irrelevant which name for an object is used when the object is Trivialized. Thus, for instance, ${}^{0}2$ and ${}^{0}$ Two are one and the same construction, and so are [${}^{0}{+}\;{}^{0}2\;{}^{0}5]$ and [${}^{0}{Plus}\;{}^{0}{Two}\;{}^{0}{Five}]$. Hence from our point of view, calculating 2 + 5 and calculating two plus five are one and the same attitude.²³ To calculate is, rather, tantamount to manipulating abstract, extra-mental, extra-notational procedures. Different (sorts of) agents may well manipulate those procedures in somewhat different ways. Humans, computers, and extraterrestrials (should they exist) encode the procedures in different ways, and already the history of human mathematics has seen many notational systems and different ways of encoding mathematical computations, but the mathematical procedures transcend these differences.²⁴

The analysis of the attitude mentioned above is this construction:

$$\begin{aligned} {\lambda }w{\lambda }t\;[{}^{0}Calculate_{wt}\;a\;{}^{0}[{}^{0}\!{Cot}\;{}^{0}{\uppi }]] \end{aligned}$$

(1)

In (1) the Composition $[{}^{0}\!{Cot}\;{}^{0}\!{\uppi }$] is displayed (by means of Trivialization) as the second argument of the extensionalized relation-in-intension Calculate; and so are all the sub-constructions within this Composition. They are not constituents of the Closure (1). The Closure (1) decomposes into these constituent parts:

• ${\lambda } w{\lambda }t\;[{}^{0}{Calculate}_{wt}\;a\;{}^{0}[{}^{0}\!{Cot}\;{}^{0}{\uppi }]]$

• ${\lambda }t\;[{}^{0}Calculate_{wt}\;a\;{}^{0}[{}^{0}\!{Cot}\;{}^{0}{\uppi }]]$

• $[{}^{0}{Calculate}_{wt}\;a \;{}^{0}[{}^{0}\!{Cot}\;{}^{0}{\uppi }]]$

• $[[{}^{0}{Calculate}\;w]\,t]$

• $[{}^{0}{Calculate}\;w]$

• ${}^{0}{Calculate}$

• $w$

• $t$

• $a$

• ${}^{0}[{}^{0}\!{Cot}\;{}^{0}{\uppi }$]

But not also:

• $[{}^{0}\!{Cot}\;{}^{0}{\uppi }$]

• ${}^{0}\!{Cot}$

• ${}^{0}{\uppi }$

At any $\langle w, t\rangle$, whoever evaluates whether the truth-condition constructed by (1) is satisfied at $\langle w, t\rangle$ is not ipso facto calculating the Composition [${}^{0}\!{Cot}\;{}^{0}\!{\uppi }$]. They are only checking whether $a$ is in the process of executing this Composition, assigning the truth-value T or F, according as $a$ is engaged in this futile activity. Hence (1) constructs a proposition that returns T or F at $\langle w,t\rangle$, regardless of the fact that [${}^{0}\!{Cot}\;{}^{0}\!{\uppi }$] constructs nothing.

Recall the three kinds of context in which a construction can occur, namely hyperintensional, intensional and extensional. (1) is an example of a construction in which the Composition [${}^{0}\!{Cot}\;{}^{0}\!{\uppi }$] occurs hyperintensionally. Hence its parts ${}^{0}\!{Cot}$ and ${}^{0}{\uppi }$ also occur hyperintensionally, i.e. in displayed mode.

On the other hand, in the Composition

$$\begin{aligned} {[[{}^{0}\!{Cot}\;{}^{0}{\uppi }]} = {}^{0}{0}] \end{aligned}$$

(2)

the Composition [${}^{0}\!{Cot} \;{}^{0}{\uppi }$] occurs executed. (2) decomposes into these constituents:

• $[[{}^{0}\!{Cot} \;{}^{0}{\uppi }] = {}^{0}{0}]$

• $[{}^{0}\!{Cot}\;{}^{0}{\uppi }$]

• ${}^{0}\!{Cot}$

• ${}^{0}{\uppi }$

• ${}^{0}{0}$

• ${}^{0}{=}$

$[{}^{0}\!{Cot} \,{}^{0}\!{\uppi }$] being improper, the whole Composition (2) is improper as well: the function =, typed to take a pair of numbers to a truth-value, does not obtain the required left-hand argument to operate on.

If a construction $C$ occurs executed as a constituent of a construction $D$, then $C$ can occur in $D$ either intensionally or extensionally.²⁵ Since in (2) the Composition [${}^{0}\!{Cot}\;{}^{0}{\uppi }$] occurs executed, its part ${}^{0}\!{Cot}$ occurs executed as well, namely extensionally. The first argument of the function = is typed to be the value of the cotangent function at the argument $\uppi$. And since there is no such value, (2) comes out improper.

To adduce an example of an intensional occurrence of an executed construction, consider “The cotangent function is trigonometric”. Where $Trigonometric/(\hbox {o}({\uptau }{\uptau }))$ is the class of trigonometric functions, the sentence receives the analysis

$$\begin{aligned}{}[{}^{0}{Trigonometric}\;{}^{0}\!{Cot}] \end{aligned}$$

(3)

The construction ${}^{0}\!{Cot}$ is a constituent that occurs intensionally. The entire cotangent function, rather than any particular value, is the argument of the function Trigonometric.

A context in which constructions occur only executed, whether the context be intensional or extensional, is easy to logically operate on. For one thing, existential generalization into such contexts goes smoothly, as expected. For instance, if it is true that the cotangent is a trigonometric function then there is a trigonometric function ($f \rightarrow _{v} ({\uptau }{\uptau }))$:

$$\begin{aligned} \frac{[{{}^{0}{Trigonometric} \;{}^{0}\!{Cot}}]}{\exists f[ {{}^{0}Trigonometric\;f}]} \end{aligned}$$

If it is true that the sine of $\uppi$ equals zero then there is a function whose value at $\uppi$ is zero, and there is a number at which the value of sine equals zero:

$$\begin{aligned} \frac{[[{}^{0}{Sin}\;{}^{0}{\uppi }] = {{}^{0}{0}}]}{\exists f[[f\;{}{^{0}\!\uppi }]= {{}^{0}{0}}]} \quad \frac{[[{}^{0}{Sin}\;{}^{0}{\!\uppi }] = {{}^{0}{0}}]}{\exists x[{[{{}^{0}{Sin}\;x} ] ={}^{0}{0}}]} \end{aligned}$$

To revisit an empirical example from Sect. 3.4, from the premise that the temperature in Barcelona is rising we can deduce that there is an intension $m$ (in casu a magnitude of type $\uptau _{{\uptau }{\upomega }})$ such that $m$ is rising. But we cannot deduce that there is a particular value that is rising, for the construction of the magnitude occurs intensionally. Let the type assignments be as follows: $Rising/(\hbox {o}\uptau _{{\uptau }{\upomega }})_{{\uptau }{\upomega }}$: a property of a magnitude; $Temperature\_in/({\uptau }{\upiota })_{{\uptau }{\upomega }}; Barcelona/{\upiota }; {\lambda } w {\lambda } t\;[{}^{0} Temperature\_in_{wt}\;{}^{0}Barcelona] \rightarrow \uptau _{{\uptau }{\upomega }}$: magnitude; $m \rightarrow _{v} \uptau _{{\uptau }{\upomega }}$. Then we have the valid argument

$$\begin{aligned} \frac{{\lambda }w{\lambda }t\;[\,{}^{0}Rising_{wt}\,{\lambda }w{\lambda }t\;[ {\,{}^{0}Temperature\_in_{wt} \,{}^{0}Barcelona} ]]}{\lambda w{\lambda }t\;\exists m[ {\,{}^{0}Rising_{wt}\,m} ]} \end{aligned}$$

while this argument is invalid:

$$\begin{aligned} \frac{{\begin{array}{l} {\lambda }w{\lambda }t\;[{}^{0}Rising_{wt}\,{\lambda }w{\lambda }t\;[{{}^{0}Temperature\_in_{wt} \,{}^{0}Barcelona} ]] \\ {\lambda }w{\lambda }t\;[{}^{0}{=}\,{\lambda }w{\lambda }t\;[{{}^{0}Temperature\_in_{wt} \,{}^{0}Barcelona} ]_{wt} \,{}^{0}\hbox {90}] \\ \end{array}}}{{\lambda }w{\lambda }t\;[{{}^{0}Rising_{wt} \,{}^{0}90}]} \end{aligned}$$

In the first premise the Closure ${\lambda }w{\lambda }t\;[{}^{0} Temperature\_in_{wt} \,{}^{0}Barcelona]$ occurs intensionally while in the second, extensionally. Hence only an equivalent construction of the same function can be substituted for this Closure; a merely $v$-congruent construction will not suffice.

4.3 Substitution method

Applying logical operations to hyperintensional contexts is far from being an open-and-shut matter. The technical complications we are confronted with are rooted in displayed constructions. For instance, a variable occurring in a hyperintensional context is displayed, i.e. Trivialization-bound, which means being bound in a manner that overrides $\lambda$-binding. In particular, since a displayed construction cannot at the same time be executed, valuation does not play any role in such a context. Yet an argument of the form

$$\begin{aligned} \frac{a\;\hbox {calculates the cotangent of}\;\uppi }{a\;\hbox {calculates the cotangent of something}} \end{aligned}$$

is obviously valid. But careless existential generalization into a hyperintensional context similar to generalization into an intensional or extensional context is not valid:

$$\begin{aligned} \frac{{\lambda } w{\lambda }t\;[{{}^{0}{Calculate}_{wt}\;a\;{}^{0}} [{}^{0}\!{Cot}\;{}^{0}{\uppi }]]}{{\lambda }w{\lambda }t\;[{}^{0}\exists {\lambda }x\;[{{}^{0}{Calculate}_{wt}\;a\;{}^{0}}[{}^{0}\!{Cot}\;x]]]} \end{aligned}$$

The reason is this. The Trivialization ${}^{0}[{}^{0}\!{Cot}\;x$] constructs the Composition [${}^{0}\!{Cot}\,x$] independently of any valuation $v$. Thus from the fact that at $\langle w, t\rangle$ it is true that $a$ calculates [${}^{0}\!{Cot}\;{}^{0}{\uppi }$], we can not validly infer that $a$ calculates [${}^{0}\!{Cot}\;x$], because $a$ calculates the cotangent of $\uppi$ rather than of $x$. Put differently, the class of numbers constructed by ${\lambda }x [{}^{0}{Calculate}_{wt}\;a\;{}^{0}[{}^{0}\!{Cot}\;x]]$ will be non-empty, according as $a$ calculates [${}^{0}\!{Cot}\;x$] and regardless of $a$’s calculating [${}^{0}\!{Cot}\;{}^{0}\!{\uppi }$]. The problem just described of ${\lambda }x$ being unable to catch the occurrence of $x$ inside the Trivialized construction is TIL’s way of phrasing the standard objection to quantifying-in. Yet in TIL we have a way out (or perhaps rather, a way in). In order to validly infer the conclusion, we need to pre-process the Composition [${}^{0}\!{Cot}\;x$] and substitute the Trivialization of $\uppi$ for $x$. Only then can the conclusion be inferred. To this end we deploy the polymorphic functions $Sub^{n}/({*}_{n}{*}_{n}{*}_{n}{*}_{n})$ and $Tr^{\upalpha }/({*}_{n}\upalpha )$ that operate on constructions in the manner stipulated by the following dual definition.

Definition 5

$(Sub^{n},Tr^{\upalpha })$ Let $C_{1},C_{2},C_{3}/{*}_{n+1} \rightarrow {*}_{n}\, v$-construct constructions $D_{1}$, $D_{2}$, $D_{3}$, respectively. Then the Composition [${}^{0}\!{Sub}^{n}\;C_{1} C_{2} C_{3}]\;v$-constructs the construction $D$ that results from $D_{3}$ by collisionless substitution of $D_{1}$ for all occurrences of $D_{2}$ in $D_{3}$. The function $Tr^{{\upalpha }}/({*}_{n}{\upalpha })$ returns as its value the Trivialization of its $\upalpha$-argument. $\square$

Example 4

Let variable $y \rightarrow _{v}\uptau$. Then [${}^{0}{Tr}^{\uptau }\,y]\;v(\uppi /y)$-constructs ${}^{0}{\uppi }$. The Composition [${}^{0}\!{Sub}^{1}\; [{}^{0}Tr^{\uptau }\,y]\;{}^{0}{x} \;{}^{0}[{}^{0}\!{Cot}\;x]]\;v(\uppi /y)$-constructs the Composition [${}^{0}\!{Cot}\;{}^{0}{\uppi }$].

Remark 3

Note that there is a substantial difference between the construction Trivialization and the function $Tr^{{\upalpha }}$. Whereas ${}^{0}{y}$ constructs just the variable $y$ regardless of valuation, $y$ being ${}^{0}$-bound in ${}^{0}{y}$, $[{}^{0}{Tr}^{\uptau }\,y]\;v$-constructs the Trivialization of the object $v$-constructed by $y$. Hence $y$ occurs free in [${}^{0}Tr^{\uptau }\,y$].

Below we will omit the superscripts $n$ and $\upalpha$ and write simply ‘Sub’ and ‘Tr’ whenever no confusion can arise.

It should be clear now how to validly derive that $a$ calculates the cotangent of something if $a$ calculates the cotangent of $\uppi$. The valid argument, in full TIL notation, is this:

$$\begin{aligned} \frac{{\lambda }w{\lambda }t\,[{{}^{0}{Calculate}_{wt}\;a\;{}^{0}} [{}^{0}\!{Cot}\;{}^{0}{\uppi }]]}{{\lambda }w{\lambda }t\,[{}^{0}\exists {\lambda }y\;[{{}^{0}{Calculate}_{wt}\;a}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;y}]\;{}^{0}{x}\;{}^{0}[{{}^{0}\!{Cot}\;x}]]]]} \end{aligned}$$

Proof

Let $Empty/(\hbox {o}{\uptau })$ be an empty set of real numbers. Then for any world-time pair $\langle w, t\rangle$ the following steps are truth-preserving:

$$\begin{aligned} \begin{array}{l@{\quad }l@{\quad }l} (1)&{}{[{}^{0}{Calculate}_{wt}\;a\;{}^{0}[{}^{0}{Cot}\;{}^{0}{\uppi }]]}&{}{\varnothing } \\ (2)&{}[{}^{0}\!{=}{}_{v(\pi /y)}\;[{}^{0}{Sub}\;[{}^{0}{Tr}\;y[\;{}^{0}{x}\;{}^{0}[{}^{0}{Cot}\;x]]\,{}^{0}[{}^{0}{Cot}\;{}^{0}{\uppi }]]&{}1,\;\hbox {Definition 5} \\ (3)&{}{[{{}^{0}{Calculate}_{wt}\;a}\;[{}^{0}{Sub}\; [{{}^{0}{Tr}\;y}]\;{}^{0}{x}\;{}^{0}[{{}^{0}{Cot}\;x}]]}&{}1,2,\;\hbox {Leibniz} \\ (4)&{}[{\lambda }y\;[{{}^{0}{Calculate}_{wt}\;a}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;y}]\;{}^{0}{x}\;{}^{0}[{}^{0}{Cot}\;x]]]\;{}^{0}{\uppi }]&{} \hbox {3}, {\lambda }\hbox {-abstraction} \\ (5)&{}{\lnot }[{}^{0}{Empty}\;{\lambda }y\;[{{}^{0}{Calculate}_{wt}\;a}\; [{}^{0}{Sub}\;[{{}^{0}{Tr}\;y}]\;{}^{0}{x}\;{}^{0}[{}^{0}{Cot}\;{x}]]]]&{}\hbox {4,\;Definition}\;2\;(\hbox {iii}) \\ (6)&{}{[{}^{0}\exists {\lambda }y\,[{{}^{0}{Calculate}_{wt}\;a}\;[{}^{0}{Sub}\;[ {{}^{0}{Tr}\;y}]\;{}^{0}{x}\;{}^{0}[{{}^{0}{Cot}\;x} ]]]]}&{} 5,\;\hbox {EG} \\ \end{array} \end{aligned}$$

      

4.4 Hyperintensional individuation in terms of procedural isomorphism

Another issue we need to deal with is this. We must specify the rules for valid substitution, because our logic is an extensional logic of hyperintensions where the extensional rules of existential generalization and Leibniz’s substitution of identicals are valid in all contexts, whether extensional, intensional or hyperintensional. Again, in an extensional or intensional context there is no problem. We can substitute equivalent constructions according to these rules of substitution:²⁶

Rules of substitution into extensional and intensional contexts Let $C$, $D$ be constructions that $v$-construct the same object for a given valuation $v$. Then $C, D$ are v-congruent and can be validly substituted in extensional contexts. Let $C, D$ be constructions that $v$-construct the same object for every valuation $v$. Then $C,D$ are logically equivalent and can be validly substituted in intensional contexts.

Logically equivalent constructions are $v$-congruent, while the converse obviously does not hold. Yet the substitution of merely logically equivalent hyperintensions is not valid in hyperintensional contexts, as already (Carnap (1947), §§13ff) in effect pointed out. From the linguistic point of view, in a hyperintensional context only synonymous expressions can be substituted. The reason, phrased in TIL terminology, is that the very meaning is displayed. Our thesis is that synonymous expressions have structurally isomorphic meanings.²⁷ And since meaning is a procedure, we need to define the relation of procedural isomorphism between constructions, constructions being a bit too fine-grained from the procedural point of view. The main issue is this. Constructions that differ at most by using different $\lambda$-bound variables of the same type differ so slightly that we wish to say that such constructions are one and the same procedure. For instance, the Closures $\lambda x\; [{}^{0}{+}\;x\;{}^{0}{1}], {\lambda }y\;[{}^{0}{+}\;y \;{}^{0}{1}], {\lambda }z\;[{}^{0}{+}\;z\;{}^{0}{1}$], and so on, are by Definition 2 different constructions of the successor function. Yet from the procedural point of view they are isomorphic. They consist of the same steps:

• take the function plus

• take any number that is the value of $x$ (or $y$, or $z$, or ...)

• take the number 1

• apply the function plus to the chosen number $x$ (or $y$, or $z$, or ...) and 1

• abstract over the chosen number $x$ (or $y$, or $z$, or ...)

Thus if $a$ calculates [${\lambda }x\;[{}^{0}{+}\;x\;{}^{0}{1}]\;{}^{0}{5}$] and $b$ calculates [${\lambda }y\;[{}^{0}{+}\;y\;{}^{0}{1}]\;{}^{0}{5}$], we would like to infer that $a$ and $b$ are related to one and the same procedure, although two different constructions figure as complements. In both cases $a$ and $b$ are calculating the successor of 5. But mathematical language introduces a distinction that is absent from natural language. Thus we want something like the following sort of argument to come out valid:

$$\begin{aligned} \frac{{\begin{array}{l} a\;\hbox {calculates}\;[{\lambda } x\;[{{}^{0}{+}\;x\;{}^{0}{1}}]\;{}^{0}{5}] \\ b\;\hbox {calculates}\;[{\lambda }y\;[{{}^{0}{+}\;y\;{}^{0}{1}}]\;{}^{0}{5}] \\ \end{array}}}{\hbox {There is a procedure}\; c\;\hbox {such that}\; a\; \hbox {and}\; b\; \hbox {calculate}\; c} \end{aligned}$$

The conclusion must actually be stated more precisely, because when quantifying over procedures we are quantifying over constructions:

$$\begin{aligned} \frac{{\begin{array}{l} a\;\hbox {calculates}\;[{\lambda }x\;[{{}^{0}{+}\;x\;{}^{0}{1}}]\;{}^{0} {5}] \\ b\;\hbox {calculates}\;[{\lambda }y\;[{{}^{0}{+}\;y\;{}^{0}{1}}]\;{}^{0}{5}] \\ \end{array}}}{ \begin{array}{l} \hbox {There are constructions}\;c, c^{{\prime }}\; \hbox {such that}\; a\; \hbox {calculates}\\ c\; \hbox {and}\; b\; \hbox {calculates}\; c',\; \hbox {and}\; c,\; c'\;\hbox {are procedurally isomorphic} \end{array}} \end{aligned}$$

The notion of procedural isomorphism is a nod to Carnap’s intensional isomorphism and Church’s synonymous isomorphism. Any two terms or expressions whose respective meanings are procedurally isomorphic are deemed semantically indistinguishable, hence synonymous. Thus procedurally isomorphic constructions can be mutually substituted in any context, including hyperintensional ones. Nothing in this particular paper hinges critically on this or that particular calibration of procedural isomorphism. But it is critical to have available to us such an exact calibration. Without it our definition of hyperintensional context would lack one of its cornerstones, namely an exact criterion of valid substitution inside such contexts. Without it, we would fall short of providing a full theory of the sort of context we are explaining how to quantify into.

Church proposed several alternatives in order to specify a criterion of synonymy. The weakest, or most permissive, one is Alternative (A2), which is logical equivalence. (A1) includes $\upalpha$- and $\upbeta$-conversion, while the strongest, or most restrictive, one, (A0), includes $\upalpha$-conversion and meaning postulates for atomic constants such as ‘bachelor’ and ‘fortnight’. Church’s (A0) and (A1) leave room for additional Alternatives. One such would be (A½), another (A¾). The former includes $\upalpha$- and $\upeta$-conversion while the latter adds to these two restricted $\upbeta$-conversion by name. In Duží et al. (2010) we advocate (A½) whereas in Duží and Jespersen (2012) we prefer (A¾) to soak up those differences between $\upbeta$-transformations that concern only $\lambda$-bound variables and thus (at least appear to) lack natural-language counterparts. The restricted version of equivalent $\upbeta$-reduction by name consists in substituting free variables for $\lambda$-bound variables of the same type. For instance, the Composition [${\lambda }x\;[{}^{0}\!{+}x\;{}^{0}{1}]\,y$] can be simplified to the Composition [${}^{0}\!{+}\;y\;{}^{0}\!{1}$]. Thus this transformation is just a manipulation with $\lambda$-bound variables that has much in common with $\upeta$- and less with $\upbeta$-reduction. The latter is the operation of applying a function $f$ to its argument $a$ in order to obtain the value of $f$at $a$ (leaving it open whether a value emerges). No such features can be found in restricted $\upbeta$-reduction. It is just a formal simplification of the original construction.

Recently, however, we have grown discontent both with (A½) and (A¾). Hence we wish to suggest a new definition of procedural isomorphism, (A1$^{\prime \prime }$), which is one of the novel contributions of this paper. This variant is very close to Church’s (A1). (A1$^{\prime \prime }$) includes $\upalpha$- and $\upbeta$-conversion by value. Thus we exclude $\upeta$-conversion, and introduce a new version of $\upbeta$-conversion.²⁸

There are two reasons for not including $\upeta$-conversion. The first reason is that it is actually rather peculiar to claim that two procedures are isomorphic if they do not have the same number of constituents. Yet the $\upeta$-expanded construction of the form ${\lambda }x\;[Fx$] has two more constituents than the equivalent $\upeta$-reduced construction $F$, because the former adds the steps of applying the function $v$-constructed by $F$ to the variable $x$ followed by abstraction over the values of $x$. The second and more important reason is the fact that $\upeta$-conversion does not preserve logical equivalence in a logic of partial functions such as TIL. To see this, consider the following example. Let $F\;v$-construct a function of type (($\upalpha \upbeta ){\upgamma })$ that is not defined at the argument $v$-constructed by $A\rightarrow _{v}{\upgamma }$. Then the Composition [$F\,A$] $\rightarrow _{v} ({\upalpha }{\upbeta })$ is $v$-improper. However, the $\upeta$-expanded construction ${\lambda }x\;[[F\;A]\;x] \rightarrow _{v} ({\upalpha }{\upbeta }),x \rightarrow \upbeta ,v$-constructs a degenerate function, which is a function undefined at all its arguments. To be sure, due to the $v$-improperness of [$F\;A$] the Composition [[$F\;A]\;x$] is also $v$-improper. But $\lambda$-abstraction raises the context to an intensional one, hence the Closure $\lambda x\;[[F\;A]\;x$] $v$-constructs a degenerate function, which is an object, if a bizarre one. Hence the constructions [$F\;A$] and ${\lambda }x\;[[F\;A]\;x$] are not logically equivalent.²⁹

In practice the exclusion of $\upeta$-conversion from the definition of procedural isomorphism is going to be harmless. When analyzing expressions in TIL we apply our method of literal analysis, which consists of three steps: (i) assigning types to the objects mentioned by the sub-terms of the analyzed expression $E$; (ii) combining the Trivializations of the objects mentioned by the semantically simple sub-terms of $E$ in order to obtain the construction of the object (if any) denoted by $E$; (iii) checking whether the resulting construction is type-theoretically coherent. Due to step (ii) the application of this method yields a construction (namely the meaning of $E$) that does not contain $\upeta$-expanded subconstructions. For instance, the literal analysis of “Tilman is happy” is the Closure ${\lambda }w{\lambda }t\;[{}^{0}{Happy}_{wt}\,{}^{0}{Tilman}]$ rather than ${\lambda }w{\lambda }t\;[{\lambda }w{\lambda }t\;[{\lambda }x\;[{}^{0}{Happy}_{wt}\;x]]_{wt}\,{}^{0} Tilman]$, because the literal analysis of the predicate ‘is happy’ is the Trivialization ${}^{0}{Happy}$ rather than the Closure ${\lambda }w{\lambda }t\;[{\lambda }x\;[{}^{0}{Happy}_{wt}x$]]. The types are $Happy/(\hbox {o}\upiota )_{{\uptau }{\upomega }}; Tilman/\upiota ; x \rightarrow \upiota$.

The reasons for excluding unrestricted $\upbeta$-conversion are these. Though it is the fundamental computational rule of the $\lambda$-calculi, it is underspecified by this rule: [${\lambda }x\; C(x)\;A] \vdash C(A/x).$ The procedure of applying the function $v$-constructed by ${\lambda }x\;C(x)$ to the argument $v$-constructed by $A$ can be executed in two different ways: by value or by name. If by name then procedure $A$ is substituted for all the occurrences of $x$ into $C$. In this case there are two problems. First, conversion of this kind is not guaranteed to be a logically equivalent transformation as soon as partial functions are involved. This is due to the fact that $A$ occurs in the extensional context of the left-hand side construction, whereas when dragged into $C$ its occurrence may become intensional. Second, even in those cases where $\upbeta$-reduction is an equivalent transformation, it may yield loss of analytic information of which function has been applied to which argument.³⁰ The idea of conversion by value is simple. Execute the procedure $A$ first, and only if $A$ does not fail to produce an argument value on which $C$ is to operate, substitute this value for $x$. The solution preserves logical equivalence, avoids the problem of loss of analytic information, and moreover, in practice it is more efficient. The efficiency is guaranteed by the fact that procedure $A$ is executed only once, whereas if this procedure is substituted for all the occurrences of the $\lambda$-bound variable it can subsequently be executed more than once.

To elucidate the problem, imagine one has a procedure (embodied as a program) $C(x)$ with a ‘hole’ $x$ (i.e. an unsaturated procedure with a formal parameter $x$), and a subprogram $A$ that specifies the material (argument value) to be filled into the hole $x$. There are two ways of going about filling $x$:

• (1) (by name) inserting into the hole $x$ the whole subprogram $A$ and then computing $C(A/x)$

• (2) (by value) computing $A$ first in order to obtain the argument value $a$, and then inserting $a$ into the hole $x$ and computing $C(a/x)$

Case 1

In this case there may be an undesirable side effect. Imagine that the subprogram $A$ is somehow garbled and as a result the whole procedure $C$ gets garbled as well after the insertion, damage being propagated upwards. Moreover, instead of the hole $x$ one gets $A$, and $A$ may conflict with $C$. This is a case of invalid $\upbeta$-reduction that fails to preserve equivalence. Furthermore, even if $A$ does not damage $C$ when computing $C(A)$, after the execution of $C(A)$ one will have lost track of $A$. The two procedures have been merged together. Suppose one wants to compute another procedure $E(x)$ and to supply the same material for $x$. Even if the execution of $C(A)$ turns out to be successful, $A$ may have been changed by the execution. There is no guarantee that the same material will be supplied for $x$ into $E(x)$. This is a case of valid $\upbeta$-reduction preserving equivalence but yielding loss of analytic information.

Case 2

Keep $C(x), E(x)$, and $A$ separate. Procedure $A$ is evaluated only if needed, and if so, only once. Everything is as it should be: no loss of analytic information arises and equivalence is preserved.

Remark 4

In programming languages the difference between Cases 1 and 2 revolves around the programmer’s choice of evaluation strategy. Historically, call-by-value and call-by-name date back to Algol 60, a language designed in the late 1950s. The difference between call-by-name and call-by-value is often called passing by reference versus passing by value, respectively. Only purely functional languages such as Clean and Haskell use call-by-name. For instance, Java manipulates objects by reference. However, Java does not pass arguments by reference, but by value. Call-by-value is not a single evaluation strategy, but rather a cluster of evaluation strategies in which a function’s argument is evaluated before being passed to the function. In call-by-reference evaluation (also referred to as call-by name or pass-by-reference), a calling procedure receives an implicit reference to the argument sub-procedure. This typically means that the calling procedure can modify the argument sub-procedure. A call-by-reference language makes it more difficult for a programmer to track the effects of a procedure call, and may introduce subtle bugs. The notion of reduction strategy in the $\lambda$-calculi is similar to the evaluation strategy in programming languages, though slightly distinct. Our proposal amounts to a specification of an evaluation strategy by-value as adapted to TIL. Similar work has been done since the early 1970s, but merely for simple-typed or untyped $\lambda$-calculi. For instance, Plotkin (1975) proved that the two strategies are not operationally equivalent. Moreover, the call-by-name strategy cannot be used for a hyperintensional context like calculating, or in hyperintensional $\lambda$-calculi such as TIL due to operational non-equivalence. Our substitution method based around the functions Sub and Tr is similar to Chang and Felleisen (2012)’s call-by-need reduction by value. But their work is couched in an untyped $\lambda$-calculus. TIL, by contrast, is a hyperintensional, typed $\lambda$-calculus.

Our definition of $\upbeta$-equivalence is this:

Definition 6

($\upbeta$-conversion by value) Let $Y \!\rightarrow _{v}\!{\upalpha }; x_{1}, D_{1} \!\rightarrow _{v}\! \upbeta _{1}, \ldots , x_{n}, D_{n}\!\rightarrow _{v}\!\upbeta _{n}, [{\lambda }x_{1} \ldots x_{n} Y]\rightarrow _{v}({\upalpha }\upbeta _{1}\ldots \upbeta _{n})$. Then the conversion

$$\begin{aligned}{}[[{\lambda }x_{1} \ldots x_{n} Y] D_{1} \ldots D_{n}] \rightarrow _{\upbeta }{}^{2}[{}^{0}{Sub}\;[{}^{0}{Tr}\;D_{1}]\; {}^{0}{x}_{1} \ldots \;[{}^{0}{Sub}\;[{}^{0}{Tr}\;D_{n}]\;{}^{0}{x}_{n}\;{}^{0}{Y}]] \end{aligned}$$

is $\upbeta$-reduction by value. The reverse conversion is $\upbeta$-expansion by value. $\square$

Claim 1

Let $C,D$ be constructions such that $C$ is identical to $[[\lambda x_{1} \ldots x_{n}\;{Y}]\; D_{1} \ldots \;D_{n}]$ and $D$ to $^{2}[{}^{0}\!{Sub}\;[{}^{0}\!{Tr}\;D_{1}] \;{}^{0}\!{x_{1}} \ldots [{}^{0}\!{Sub}\;[{}^{0}\!{Tr}\; D_{n}]\;{}^{0}\!{x}_{n}\;{}^{0}\!{Y}]]$. Then $C,D$ are strictly equivalent in the sense that for any valuation $v$ they either $v$-construct one and the same entity or are both $v$-improper.

Proof of Claim 1

If one or more of the constructions $D_{1}, \ldots , D_{n}$ are $v$-improper then so are both $C$ and $D$, according to Definition 2, (iii) and (vi). Otherwise, let $D_{1}, \ldots ,D_{n}$ all be $v$-proper, $v$-constructing the objects $d_{1},\ldots ,d_{n}$, respectively. Then by Definition 2, (iv) the Closure [$\lambda x_{1} \ldots x_{n}Y$] $v$-constructs the following function $f$. If $Y$ is $v(d_{1}/x_{1},\ldots ,d_{n}/x_{n})$-improper, then $f$ is undefined on $\langle d_{1},\ldots ,d_{n}\rangle$ and thus $C$ is $v(d_{1}/x_{1},\ldots ,d_{n}/x_{n})$-improper according to Definition 2, (iii). Otherwise the value of $f$ on $\langle d_{1}, \ldots ,d_{n}\rangle$ is the $\upalpha$-entity $v(d_{1}/x_{1},\ldots ,d_{n}/x_{n})$-constructed by $Y$. Let the entity $v(d_{1}/x_{1},\ldots ,d_{n}/x_{n})$-constructed by $Y$ be $a$. Then by Definition 2, (iii) of Composition, the construction $C\;v$-constructs $a$. We are to show that the construction $D$ also $v$-constructs $a$. The first Execution of $D$ constructs $Y(x_{1}/{}^{0}{d}_{1}, \ldots , x_{n}/{}^{0}{d}_{n})$, i.e. the construction $Y$ where according to the definition of the functions Sub and Tr all the occurrences of the variables $x_{1}, \ldots ,x_{n}$ are replaced by ${}^{0}{d}_{1},\ldots ,{}^{0}{d}_{n}$, respectively. Since the Trivializations ${}^{0}d_{1}, \ldots , {}^{0}{d}_{n}$ construct the entities $d_{1},\ldots ,d_{n}$, respectively, the second Execution $v(d_{1}/x_{1},\ldots ,d_{n}/x_{n})$-constructs the entity $a$, or else nothing in case $Y$ is $v(d_{1}/x_{1}, \ldots ,d_{n}/x_{n})$-improper. Hence $C$ and $D$ come out strictly equivalent.

Remark 5

That constructions $C, D$ are $\upbeta$-equivalent will be denoted ‘${}^{0}{C} \approx _{\upbeta }\;{}^{0}\!{D}$’, $\approx _{\upbeta }/(\hbox {o}{*}_{n}{*}_{n})$. In order to avoid misconceptions, in what follows we will use the term ‘$\lambda$-conversion’ in the same sense as Church’s for the conversion that we also call ‘$\upbeta$-conversion by name’, which is specified by the following rule:

$$\begin{aligned} {[[{\lambda }x_{1} \ldots x_{n}\;Y] D_{1} \ldots D_{n}] \rightarrow Y(D_{1}/x_{1}, \ldots , D_{n}/x_{n})} \end{aligned}$$

where the contracted construction arises from $Y$ by collisionless substitution of $D_{1},\ldots ,D_{n}$ for $x_{1},\ldots ,x_{n}$, respectively. The term ‘$\upbeta$-conversion’ will be reserved for $\upbeta$-conversion by value.

In order to define procedural isomorphism on the set of constructions of a particular order, we still need another definition, to wit the definition of ${\alpha }$-conversion. The standard definition, which defines ${\alpha }$-equivalent constructions as those that differ at most by using different $\lambda$-bound variables, is insufficient, because the $\upbeta$-reduced constructions $C, D$ that arise from ${\alpha }$-equivalent constructions do not differ at most by using different $\lambda$-bound variables. For instance, the constructions

$$\begin{aligned}{}[{{\lambda }x\;[{{}^{0}{+}\;x\;{}^{0}{1}}]\;{}^{0}{5}]\;\hbox {and}\;[{\lambda }y\;[{{}^{0}{+}\;y\;{}^{0}{1}}]\;{}^{0}{5}} ] \end{aligned}$$

are ${\upalpha }$-equivalent according to the standard definition. Yet their respective $\upbeta$-reduced forms

$$\begin{aligned} {}^{2}[{}^{0}\!{Sub}\;[{}^{0}{Tr}\;{}^{0}\!{5}]\; {{}^{0}\!{x}\;{}^{0}}[{}^{0}\!{+}\;x\;{}^{0}\!{1}]]\;\hbox {and}\;{}^{2}[{}^{0}\!{Sub}\;[{}^{0}\!{Tr}\;{}^{0}\!{5}]\;{{}^{0}\!{y}\;{}^{0}}[{}^{0}\!{+}\;y\;{}^{0}\!{1}]] \end{aligned}$$

would not be ${\upalpha }$-equivalent. Yet they ought to be, because from the procedural point of view it is irrelevant which variables are used as formal parameters of the respective procedure. Thus we define:

Definition 7

($\upalpha$-conversion) Let $C, D$ be constructions. Then $C,D$ are ${\upalpha }$-equivalent, denoted ‘${}^{0}\!{C} \approx _{{\upalpha }}{}\;{}^{0}\!{D}$’, $\approx _{{\upalpha }}/(\hbox {o}{*}_{n}{*}_{n})$, if either $C,D$ differ at most by using different $\lambda$-bound variables, or their $\upbeta$-expanded forms differ at most by using different $\lambda$-bound variables.

Claim 2

${\upalpha }$-equivalent constructions are strictly equivalent by being either $v$-improper or $v$-constructing one and the same entity.

Proof of Claim 2.

Thanks to Claim 1 it suffices to prove that Closures of the form $[\lambda x_{1} \ldots x_{n} Y(x_{1},\ldots ,x_{n})], [\lambda y_{1} \ldots y_{n} Y(y_{1}, \ldots ,y_{n})$], where $Y(x_{1}, \ldots , x_{n})$ differs from $Y(y_{1},\ldots ,y_{n})$ only by collisionless substitution of the variables $x_{1},\ldots ,x_{n}$ for $y_{1},\ldots ,y_{n}$, respectively, $v$-construct one and the same function. But this immediately follows from Definition 2, (iv).

Definition 8

(procedural isomorphism) Let $C, D$ be constructions. Then $C, D$ are procedurally isomorphic iff either $C$ and $D$ are identical or there are constructions $C_{1},\ldots , C_{n} (n > 1$) such that ${}^{0}{C} \!=\! {}^{0}{C}_{1}, \;{}^{0}{D} \!=\! {}^{0}{C}_{n}$, and for each $C_{i}, C_{i+1} (1 \!\le \! \hbox {i} \!<\!n)$ it holds that ${}^{0}{C}_{\mathrm{i}} \approx _{{\upalpha }}\;{}^{0}{C}_{\mathrm{i + 1}}$ or ${}^{0}{C}_{\mathrm{i}} \approx _{\upbeta }{}^{0}{C}_{\mathrm{i+1}}$.

Corollary of Definition 8

Procedural isomorphism is an equivalence relation defined on a set of constructions such that procedurally isomorphic constructions are strictly equivalent in the sense that for any valuation $v$ they either $v$-construct one and the same entity or they are $v$-improper.

Proof of Corollary

Follows immediately from Claims 1 and 2.

Example 5

The above constructions

$$\begin{aligned}&{[{\lambda }x\;[{{}^{0}{+}\;{x}\;{}^{0}{1}}]\;{}^{0}{5}]},\;{}^{2}[{}^{0}\!{Sub}\;[{{}^{0}{Tr}\;{}^{0}\!{5}}]\;{}^{0}{x}\;{}^{0}[{{}^{0}\!{+}\;x\;{}^{0}\!{1}}]], \\&{[{\lambda }y\;[{{}^{0}{+}\;y\;{}^{0}{1}}]\;{}^{0}{5}]},\;{{}^{2}}[{}^{0}{Sub}\;[{{}^{0}{Tr}\;{}^{0}\!{5}}]\;{}^{0}{y}\;{}^{0}[{{}^{0}\!{+}\;y\;{}^{0}\!{1}}]] \end{aligned}$$

are all procedurally isomorphic, because the following equivalences hold:

$$\begin{aligned}&{}^{0}[{\lambda }x\;[{{}^{0}\!{+}\;x\;{}^{0}{1}}]\;{}^{0}{5}]\approx _{\upalpha }\;{}^{0}[{\lambda }y\;[{{}^{0}{+}\;y\;{}^{0}{1}}]\;{}^{0}{5}] \\&{}^{0}[{\lambda }x\;[{{}^{0}\!{+}\;x\;\,{}^{0}{1}}]\;{}^{0}{5}]\approx _\upbeta \;^{02}[{{}^{0}\!{Sub}}\;[{}^{0}{Tr}\;{}^{0}\!{5}]\;{{}^{0}\!{x}\;{}^{0}}[{}^{0}\!{+}\;x\;{}^{0}\!{1}]] \\&{}^{02}[{{}^{0}{Sub}}\;[{}^{0}{Tr}\;{}^{0}{5}]\;{{}^{0}{x}\;{}^{0}}[{}^{0}\!{+}\;x\;{}^{0}{1}]]\approx {}_{\upalpha }\;{}^{0}[{\lambda }y\;[{{}^{0}\!{+}\;y\;{}^{0}{1}}]\;{}^{0}{5}] \\&{}^{0}[{\lambda }y\;[{{}^{0}\!{+}\;y\;\,{}^{0}{1}}]\,{}^{0}{5}]\approx _{\upbeta } \;{}^{02}[{{}^{0}{Sub}}[{}^{0}{Tr}\;{}^{0}{5}]\;{{}^{0}{y}\;{}^{0}}[{}^{0}\!{+}\;y\;{}^{0}\!{1}]] \\&\,{}^{02}[{{}^{0}\!{Sub}}\;[{}^{0}{Tr}\;{}^{0}{5}]\;{{}^{0}{x}\;{}^{0}}[{}^{0}\!{+}\;x\;{}^{0}{1}]]\approx _{\upalpha } \;{}^{02}[{{}^{0}\!{Sub}}\;[{}^{0}\!{Tr}\;{}^{0}\!{5}]\;{{}^{0}{y}\;{}^{0}}[{}^{0}\!{+}\;y\;{}^{0}\!{1}]] \end{aligned}$$

This completes the exposition of the logical tools we need. We are now ready to specify the rules of existential generalization into hyperintensional contexts.

5 Rules for quantifying-in with applications

In (Duží et al. (2010), § 5.3) we specified what we called rules (7) and (8) for quantifying into hyperintensional objectual attitudes de dicto and de re. In what follows we adjust those rules, which is another novel contribution of this paper. First, rule (7) for quantifying into hyperintensional attitudes de dicto can be simplified in case we quantify over the complement of the attitude. Hence we specify here rule $(\hbox {R}_{1})$. Second, rule (7) is generalized to quantify into the attitude complement over a constituent $X$ of this complement. Since in a hyperintensional context we must fully respect the perspective of the agent to whom the attitude is ascribed, we can quantify only over the constituent construction $X$ rather than an object $v$-constructed by $X$: see rule $\hbox {R}_{2}$ below. Yet on the additional assumption that the constituent $X$ is $v$-proper we obtain a variant $\hbox {R}_{2}^{\prime }$ of the rule $\hbox {R}_{2}$ that quantifies also over the object $v$-constructed by $X$. Third, rule (7) makes it possible to quantify over constructions only. Yet we need to quantify over non-constructions as well. Thus we specify a stronger rule $\hbox {R}_{3}$ for quantifying into hyperintensional contexts that makes it possible to quantify over objects of any type. Yet as mentioned above, we must respect the attitude agent’s perspective. For this reason the rule $\hbox {R}_{3}$ is applicable only if the complement constituent $X$ is a Trivialization, because then we can use the Tr function: see rule $\hbox {R}_{3}$ below. Furthermore, we add a rule for factive attitudes: see rule $\hbox {R}_{4}$ below. Last but not least, the rules that were called (6) and (8) in (ibid.) for quantifying into hyperintensional contexts de re are not correct, because in the respective conclusions we failed to acknowledge the hyperintensional character of the attitude. Here we present two correct active and passive variants of rule $\hbox {R}_{5}$ for quantifying into hyperintensional contexts de re.

Remark 6

In Remark 2 we explained that since we work with properly partial functions, prior to applying an existential quantifier we must first prove that the argument class is non-empty. Thus in the proofs that follow below we will use variants of the following steps. Let $F \rightarrow _{v} (\hbox {o}{\upalpha }{\upbeta }); a\rightarrow _{v}{\upalpha }; b \rightarrow _{v} \upbeta$. If [$F\; a\; b]\;v$-constructs T then according to Definition 2 (iii) all the three constituents of this Composition are $v$-proper. In particular, if $B$ is a $\upbeta$-object $v$-constructed by $b$, then [$F\; a\; x$] $v(B/x)$-constructs T as well. Hence the Composition [${\lambda }x\;[F\; a\; x] \;{}^{0}B]\;v$-constructs T, which in turn means that the class of $\upbeta$-objects $v$-constructed by the Closure ${\lambda }x\;[F\; a\; x$] is non-empty, and the application of the existential quantifier yields T as well: [${}^{0}\exists ^{\upbeta }{\lambda }x\;[F\; a\; x]]$.

Let the types be $Att^*\rightarrow (\hbox {o}{\upiota }{*}_{n})_{{\uptau }{\upomega }}$: an arbitrary construction of a hyperintensional objectual attitude relation; $a \rightarrow _{v}\upiota$: a construction of an individual; $\exists ^{*}/(\hbox {o}(\hbox {o}{*}_{n})); C/{*}_{n}$: a construction of attitude complement; ${}^{0}\!{C}$, $c/{*}_{n+1} \rightarrow _{v}\;{*}_{n}$. Then the rule of quantifying over hyperintensional objectual contexts is straightforward:

$$\begin{aligned} \frac{[{{Att^{*}}_{wt}\; a \;{}^{0}C} ]}{[{}^{0}\exists ^{*}\lambda c\;[{{Att^{*}}_{wt}\;a\;c}]]} \qquad ({\hbox {R}_1}) \end{aligned}$$

Proof of R $_{1}.$ Let $Empty^{*}/(\hbox {o}{*}_{n})$ be an empty class of constructions. Then the following proof-steps are truth-preserving:

$$\begin{aligned} \begin{array}{l@{\quad }l@{\quad }l} (1)&{}[{{Att^{*}}_{wt}\; a \;{}^{0}C} ]&{}\varnothing \\ (2)&{}[{\lambda c\;[{{Att^{*}}_{wt}\; a\; c}] \;{}^{0}C} ]&{}{1},\;\lambda \hbox {-abstraction} \\ (3)&{}\lnot [{{}^{0}Empty^{*}\;\lambda c\;[{{Att^{*}}_{wt}\; a\; c}]}]&{}2,\;\hbox {Definition 2 (iii)} \\ (4)&{}[{}^{0}\exists ^{*}\lambda c\;[ {{Att^{*}}_{wt}\; a\; c}]]&{}3,\;\hbox {EG} \\ \end{array} \end{aligned}$$

The rule for quantifying into hyperintensional contexts makes use of the function Sub. Let $C(X)$ be a construction of an attitude complement with a constituent $X/{*}_{n} \rightarrow _{v}{\upalpha }; c/*_{(n+1)} \rightarrow _{v} {*}_{n}; {}^{2}\!{c}/{*}_{n+2} \rightarrow _{v}{\upalpha }; y\rightarrow _{v}{\upalpha }.$ Then:

$$\begin{aligned} \frac{[ {{Att^{*}}_{wt}\; a \;{}^{0}C({X/y})}]}{[{}^{0}\exists ^{*}\lambda c\;[ {{Att^{*}}_{wt}\; a}\; [{}^{0}{Sub}\;c\;{}^{0}{y}\;{}^{0}C (y)]]]} \qquad (\hbox {R}_2) \end{aligned}$$

Proof of R $_{2}.$ According to Definition 5 of the Sub function [${}^{0}{Sub}\;c\;{}^{0}{y}\;{}^{0}C(y)]\;v(X/c)$-constructs the construction $C(X/y)$. Let $=_{*}$/$(\hbox {o}{*}_{n}{*}_{n})$ be the identity of constructions of order $n$. Then the following proof-steps are truth-preserving:

$$\begin{aligned} \begin{array}{l@{\quad }l@{\quad }l} (1)&{}[{{Att^{*}}_{wt}\; a \;{}^{0}C (X/y)} ]&{}\varnothing \\ (2)&{}[{}^{0}\!{=}_{*}\;[{}^{0}{Sub}\;c\;{}^{0}{y} \;{}^{0}{C}(y)]\;{{}^{0}C({X/y})}]&{}1,\;\hbox {Definition 5}\\ (3)&{}[ {{Att^{*}}_{wt}\;a}\; [{}^{0}{Sub}\;c\;{}^{0}{y} \;{}^{0}{C} (y)]]&{}1, 2,\;\hbox {Leibniz} \\ (4)&{}[{\lambda }c\;[ {{Att^{*}}_{wt}\; a}\;[{}^{0}{Sub}\;c\;{}^{0}{y}\;{}^{0}{C}(y)]]\;{{}^{0}\!X}]&{} 3,\;\lambda \hbox {-abstraction} \\ (5)&{}\lnot [ {\,{}^{0}Empty^{*}\,\lambda c\;[ {{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;c\;{}^{0}{y}\;{}^{0}{C}(y)}]]]&{} 4,\;\hbox {Definition 2 (iii)} \\ (6)&{}[{}^{0}\exists ^{*}\lambda c\;[{{Att^{*}}_{wt}\;a}\; [{}^{0}{Sub}\;c\;{}^{0}{y}\;{}^{0}{C}(y)]]]&{} 5,\;\hbox {EG} \\ \end{array} \end{aligned}$$

If the constituent $X$ is v-proper, we can use a variant of the rule $\hbox {R}_{2}$ called $\hbox {R}_{2}^{\prime }$. Let the additional types be $x \rightarrow _{v}\upalpha ;\;\exists /(\hbox {o}(\hbox {o}{\upalpha }))$. Then:

$$\begin{aligned} \frac{[{{Att^{*}}_{wt}\;a\;{}^{0}\!{C} (X/y)}]}{[{}^{0}\exists ^{*}{\lambda }c\;[{[{{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;c\;{}^{0}{y}\;{}^{0}{C}(y)}]] \wedge {}^{0}\exists {\lambda }x\;[{x = {}^{2}\!{c}}]]]} \qquad ({\hbox {R}_{2}^{\prime }}) \end{aligned}$$

Proof of R $_{2}^{\prime }.$ Let $Proper/(\hbox {o}{*}_{n})$ be the class of constructions that are not $v$-improper, $=_{*}$/$(\hbox {o}{*}_{n}{*}_{n})$ the identity of constructions of order $n$, $=_{\upalpha }$/$(\hbox {o}{\upalpha }{\upalpha })$ the identity of ${\upalpha }$-objects, $Empty/(\hbox {o}{\upalpha })$ an empty class of ${\upalpha }$-objects. According to Definition 2 (i) and (vi), the Double Execution $^{2}c\,v(X/c)$-constructs what $X v$-constructs. Thus if $X$ is $v$-proper then [${}^{0}\!{=}_{{\upalpha }}\;{}^{2}{c}\;X]\;v$-constructs T. Hence the following proof-steps are truth-preserving:

$$\begin{aligned} \begin{array}{l@{\quad }l@{\quad }l} (1)&{}[ {{Att^{*}}_{wt}\; a \;{}^{0}{C}(X/y)}] &{} \varnothing \\ (2)&{}[ {{}^{0}\!{=}_{*}}\;[{}^{0}{Sub}\;c\;{}^{0}{y}\;{}^{0}{C}(y)]\; {{}^{0}{C}(X/y)}]&{} 1,\;\hbox {Defintion 5} \\ (3)&{}[{{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;c\;{}^{0}{y}\;{}^{0}{C}(y)]]&{} 1, 2,\;\hbox {Leibniz} \\ (4)&{}[{{}^{0}Proper\,{}^{0}\!X}]&{}\varnothing \\ (5)&{}[{{}^{0}\!{=}{}_{\upalpha } {}^{2}{c}\;X}]&{} 4, \hbox {Definition 2 (i), (vi)} \\ (6)&{}[{\lambda x}\; [{}^{0}\!{=}{}_{\upalpha } {}^{2}c\; x]\;X]&{} 5, \lambda \hbox {-abstraction} \\ (7)&{}[[{\lambda x} [{}^{0}\!{=}{}_{\upalpha } {}^{2}c\;x]\;X]\wedge [ {Att^{*}_{wt}\; a}\; [{}^{0}{Sub}\;c\;{}^{0}{y} \;{}^{0}{C}(y)]]]&{}\hbox { 6},\hbox { 3},\wedge \hbox {I} \\ (8)&{}\lnot [\,{}^{0}Empty^{*}\;{\lambda } c\;[\lnot [\,{}^{0}Empty\,\lambda x\;[{}^{0}\!{=}{}_{\upalpha } {}^{{2}}c\; x]]\\ &{}\quad \wedge [ {{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;c\;{}^{0}{y}\;{}^{0}{C}(y)]]]] &{} 7, \hbox {Definition 2 (iii)} \\ (9)&{}[{}^{0}{\exists }^{*}{\lambda }c\;[{}^{0}{\exists }\;{\lambda }x\;[{}^{0}\!{=}{}_{\upalpha } {}^{{2}}{c}\;x]\\ &{}\quad \wedge \; [{{Att^{*}}_{wt}\;a}\; [{}^{0}{Sub}\;c\;{}^{0}{y} \;{}^{0}{C} (y)]]]]&{} 8, \hbox {EG} \\ \end{array} \end{aligned}$$

If the constituent $X$ is the Trivialization of an ${\upalpha }$-object $b$, thus guaranteeing that the construction is proper, then we can access this hyperintensional context to quantify over this ${\upalpha }$-object. To this end we have another special rule $\hbox {R}_{3}$ that makes use of the function Tr:

$$\begin{aligned} \frac{[{{Att^{*}}_{wt}\; a \;{}^{0}{C} ({{}^{0}b/y})} ]}{[{}^{0}\exists {\lambda }x[{{Att^{*}}_{wt}\;a}\; [{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y}\;{}^{0}{C}(y)]]]} \qquad (\hbox {R}_{3}) \end{aligned}$$

Proof of R $_{3}.$ According to Definition 5 the Composition [${}^{0}{Sub}\;[{}^{0}{Tr}\;x] \;{}^{0}{y}\;{}^{0}{C(y)}] v (b/x)$-constructs the construction $C({}^{0}b/y)$ in which the occurrences of $y$ have been replaced by ${}^{0}{b}$. Thus the following proof-steps are truth-preserving:

$$\begin{aligned} \begin{array}{l@{\quad }l@{\quad }l} (1)&{}[{Att^{*}}_{wt}\;a\;{}^{0}{C}({}^{0}{b/y})]&{}\varnothing \\ (2)&{}[{}^{0}\!{=}_{*}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y}\;{}^{0}{C(y)}]\; {{}^{0}{C}({{}^{0}{b/y}})}]&{} 1,\;\hbox {Definition 5} \\ (3)&{}[{{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y}\;{}^{0}{C(y)}]]&{} 1, 2, \hbox {Leibniz} \\ (4)&{}[{\lambda }x[{{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y}\;{}^{0}{C(y)}]]\;{{}^{0}{b}}]&{} 3, {\lambda }\hbox {-abstraction} \\ (5)&{}\lnot [{{}^{0}{Empty}\;{\lambda }x[{{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y}\;{}^{0}{C(y)}} ]]]&{} 4, \hbox {Definition 2 (iii)} \\ (6)&{}[{}^{0}\exists {\lambda }x[ {{Att^{*}}_{wt}\;a}\; [{}^{0}{Sub}\;[{{}^{0}{Tr}\;x} ]\,{}^{0}y \;{}^{0}{C(y)}]]]&{} 5, \hbox {EG} \\ \end{array} \end{aligned}$$

Next we specify a rule for factive attitudes like finding or having solved. Factive attitudes are defined in terms of the notion of requisite. ³¹ A requisite is an analytically necessary relation-in-extension between two intensions such that, necessarily, any object that instantiates one intension also instantiates the other (though not necessarily the other way around). For instance, if the office of Head of State of the Vatican is a requisite of the office of Archbishop of Rome (i.e. the office of Pope) then, necessarily, whoever occupies the papal office must also occupy the requisite office.

Let $Att^{f*}/(\hbox {o}{\upiota }{*}_{n})_{{\uptau }{\upomega }}$ be a factive objectual attitude. The type of requisite relevant to factive hyperintensional attitudes is $Req/(\hbox {o}(\hbox {o}{\upiota }{\upalpha }{*}_{n})_{{\uptau }{\upomega }}\;(\hbox {o}{\upiota }{*}_{n})_{{\uptau }{\upomega }})$, which is defined as follows. Let $Ident^{{\upalpha }}/(\hbox {o}{\upiota }{\upalpha }{*}_{n})_{{\uptau }{\upomega }}$ be a relation between an individual, an ${\upalpha }$-object and a construction such that the individual succeeds in identifying the ${\upalpha }$-object as the product of this construction, $x \rightarrow _{v}{\upiota }, c \rightarrow _{v} {*}_{n},\;{}^{2}c \rightarrow _{v}{\upalpha }$, then:

$$\begin{aligned}{}[{}^{0}Req \;{}^{0}Ident^{{\upalpha }}\;{Att}^{{f}^{*}}] = {\forall }w {\forall }t\quad {\forall }\;x\,c\, [[Att^{f^{*}}_{wt}\,x\,c] \supset [{}^{0} Ident^{{\upalpha }}_{wt}\,x\;{}^{2}\!{c}\;c]] \end{aligned}$$

$Ident^{{\upalpha }}$ is a requisite of $Att^{f^{*}}$ iff, necessarily for all individuals $x$ and all constructions $c$, it holds that if $x$ has an attitude $Att^{f^{*}}$ to $c$ then $x$ has identified the ${\upalpha }$-product $^{2}c$ of construction $c$.

Hence we define factive hyperintensional attitudes as those for which the above requisite relation holds.

The rule $\hbox {R}_{4}$ for factive objectual attitudes is this:

$$\begin{aligned} \frac{[{Att^{f^{*}}_{wt}\; a \;{}^{0}{C}}]}{[{}^{0}\exists {\lambda } x\,[[{x = C}] \wedge [{{}^{0}Ident_{wt}\; a\; x \;{}^{0}{C}}]]]} \qquad ({\hbox {R}_{4}}) \end{aligned}$$

Additional type $C/{*}_{n} \rightarrow _{v}{\upalpha }$.

Proof of R $_{4}$

$$\begin{aligned} \begin{array}{l@{\quad }l@{\quad }l} (1)&{}[Att^{f^{*}}_{wt}\;a \;{}^{0}{C} ]&{}\varnothing \\ (2)&{}[ {}^{0}Req\;{}^{0}{Ident}^{{\upalpha }} Att^{f^{*}} ]&{}\hbox {Definition of factivity} \\ (3)&{}{\forall }w{\forall }t{\forall }x\,c[[ {Att^{f^{*}}_{wt} x c} ]\supset [{}^{0}Ident^{{\upalpha }}_{wt}\; x\;^{2}{c}\; c]]&{} 2, \hbox {Definition of}\;Req. \\ (4)&{}[[Att^{f^{*}}_{wt}\;a\;{}^{0}\!{C} ]\supset [\,{}^{0}Ident^{{\upalpha }}_{wt}\; a\;{}^{20}\!{C} \;{}^{0}\!{C}]]&{} 3, {\forall }\hbox {E},\;a/x, \;{}^{0}{C/c} \\ (5)&{}[{}^{0}Ident^{{\upalpha }}_{wt}\; a\;{}^{20}\!{C} \;{}^{0}{C}]&{} 1, 4, \hbox {MPP} \\ (6)&{}[\,{}^{0}Ident^{{\upalpha }}_{wt}\; a\; C \;{}^{0}{C}]&{} 5, \hbox {Definition 2, (vi):}\;{}^{20}\!{C} = C \\ (7)&{}[ {\,{}^{0}Proper \,{}^{0}C} ]&{} 6, \hbox {Definition\;2,\;(iii)} \\ (8)&{}[ {{}^{0}\!{=}{}_{\upalpha }\; x\;C}]&{} 7, \hbox {Definition}\; 2 \\ (9)&{}[\,{}^{0}Ident^{{\upalpha }}_{wt}\; a\; x \;{}^{0}{C}]&{} 6, 8, \hbox {Leibniz} \\ (10)&{}[[ {\,{}^{0}\!{=}{}_{\upalpha }\; x C} ]\wedge [{}^{0}Ident^{{\upalpha }}_{wt}\; a\; x \;{}^{0}{C}]]&{} 8, 9, \wedge \hbox {I} \\ (11)&{}\lnot [{}^{0}Empty\;{\lambda }x[[ {x =C} ]\wedge [{}^{0}Ident^{{\upalpha }}_{wt}\; a\; x \;{}^{0}{C}]]]&{} 10, {\lambda }\hbox {-abstraction} \\ (12)&{}[{}^{0}{\exists }{\lambda }x[[{{}^{0}\!{=}{}_{\upalpha }\; x\; C}]\wedge [{}^{0}Ident^{{\upalpha }}_{wt}\; a\; x \;{}^{0}{C}]]]&{} 11, \hbox {EG} \\ \end{array} \end{aligned}$$

The steps (6)–(8) above call for elucidation. In the Composition [${}^{0}Ident^{{\upalpha }}_{wt}\; a\; C \;{}^{0}{C}]$ the construction $C$ occurs both displayed and executed. The first occurrence of $C$ is executed while the second is displayed. Hence the first occurrence of $C$ is a constituent of [${}^{0}{Ident}^{{\upalpha }}_{wt}\;a\; C \;{}^{0}{C}]$. Since this Composition $v$-constructs T, according to Definition 2, (iii) this constituent must be proper. Thus we have step (7): [${}^{0}{Proper}\;{}^{0}{C}]$. And since $C$ is $v$-proper, it $v$-constructs an ${\upalpha }$-object, which in turn justifies step (8): ${[{}^{0}\!{=}_{{\upalpha }}\;x\;C].}$

$(\hbox {R}_{1})$–$(\hbox {R}_{4})$ are rules for quantifying into hyperintensional attitudes de dicto. Next we define a pair of rules for quantifying into hyperintensional contexts de re, both in a passive and an active variant:

$$\begin{aligned} \frac{[{Att^{*}_{wt}\;a}\; [{}^{0}{Sub}\;[{{}^{0}\!{Tr}\;X}]\;{}^{0}{y} \,{}^{0}{C(y)}]]}{[{}^{0}{\exists }{\lambda }x\;[{Att^{*}_{wt}\;a}\, [{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y} \,{}^{0}C(y)]]]} \qquad ({\hbox {R}_{5}\;act}) \end{aligned}$$

$$\begin{aligned} \frac{[{\lambda }x\;[{Att^{*}_{wt}\;a}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y}\;{}^{0}{C(y)}]\;X]]}{[{}^{0}{\exists }{\lambda }x\;[{Att^{*}_{wt}\;a}\; [{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y}\;{}^{0}{C(y)}]]]} \qquad ({\hbox {R}_{5}\;pas}) \end{aligned}$$

Types: $X/{*}_{n} \rightarrow {\upalpha }; x, y/{*}_{n}\rightarrow _{v}{\upalpha }; \exists /(\hbox {o}(\hbox {o}{\upalpha }));y$ free in $C(y)/{*}_{n}.$

Proof of R $_{5}$ act

$$\begin{aligned} \begin{array}{l@{\quad }l@{\quad }l} (1)&{}[ {{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;X}]\;{}^{0}{y}\;{}^{0}\hbox {C}(y)]]&{}\varnothing \\ (2)&{}[ {\lambda x[ {{Att^{*}}_{wt}\;a}\; [{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y} \;{}^{0}{C} (y)}]]\;X]&{} 1, {\lambda }\hbox {-abstraction} \\ (3)&{}\lnot [{}^{0}{Empty}\;{\lambda }x\;[{{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y}\;{}^{0}{C}\left( y\right) ]]]&{} 2, \hbox {Definition 2 (iii)} \\ (4)&{}[{}^{0}{\exists }{\lambda }x[{{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y} \;{}^{0}{C}\left( y\right) ]]]&{} 3, \hbox {EG} \\ \end{array} \end{aligned}$$

Proof of R $_{5}$ pas. Since $X$ occurs extensionally in the assumption, the proof is trivial:

$$\begin{aligned} \begin{array}{l@{\quad }l@{\quad }l} (1)&{}[\lambda x[{{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y} \;{}^{0}{C}\left( y\right) ]\;X]]&{}\varnothing \\ (2)&{}\lnot [{}^{0}{Empty}\;{\lambda }x[{{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;[ {{}^{0}{Tr}\;x}]\;{}^{0}{y}\;{}^{0}{C}\left( y\right) ]]]&{} 2, \hbox {Definition 2 (iii)} \\ (3)&{}[{}^{0}{\exists }{\lambda }x\;[{{Att^{*}}_{wt}\;a}\;[{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y}\;{}^{0}{C}\left( y\right) ]]]&{} 3, \hbox {EG} \\ \end{array} \end{aligned}$$

In (Duží et al. (2010), § 5.3) we specified what we called rules (2) and (4) for quantifying into intensional contexts, which are contexts of empirical attitudes $Att/(\hbox {o}\upiota {\upalpha }_{{\uptau }{\upomega }})_{{\uptau }{\upomega }}$ to intensions. In such cases the premise of the active variant has the form $[Att_{wt}\; a\;{}^{2}[{}^{0}{Sub}\;[{}^{0}{Tr}\;X]\;{}^{0} {y}\;{}^{0}{C(y)}]]$. The result of the substitution must itself be executed in order to obtain an intension, which explains the use of Double Execution. In the case of attitudes to hyperintensions, the result of the substitution is directly the construction to which $a$ is related. For this reason the Compositions $[{}^{0}{Sub}\;[{}^{0}{Tr}\;X] \;{}^{0}{y} \;{}^{0}{C(y)}]$ and [${}^{0}{Sub}\;[{}^{0}{Tr}\;x] \;{}^{0}{y}\;{}^{0}{C(y)}$] require only one execution.

5.1 Mathematical objectual attitudes: applications

As explained above, mathematical attitudes are invariably hyperintensional. For instance, if Tilman is seeking the last decimal of $\uppi$, then he is seeking something. Yet he is not seeking one particular number, because there is no such number that would be the last decimal of $\uppi$. And if per impossible there were such a number Tilman would still be related to a construction typed to construct such a number rather than the number itself, because otherwise there would be no process of seeking the last decimal of $\uppi$. Tilman would be confronted with the product (a particular number) straightaway; the seeker would ipso facto be a finder, because there would be a relation (-in-intension) between Tilman and a number.

Thus we have this valid argument:

$$\begin{aligned} \frac{\hbox {Tilman is seeking the last decimal of}\;\uppi }{\hbox {Tilman is seeking something}} \end{aligned}$$

where something is restricted type-theoretically, so that the conclusion states that Tilman is seeking something of one particular type.

In this case we apply $(\hbox {R}_{1})$:

$$\begin{aligned} \frac{{\lambda }w{\lambda }t\;[{{}^{0}{Seek}^{*}_{wt}\;{}^{0}{Tilman}\;{}^{0}}[{}^{0}{Last\_Dec}\;{}^{0}{\uppi }]]_{}}{{\lambda }w{\lambda }t\;[{}^{0}{\exists }^{*}{\lambda }c\;[{{}^{0}{{Seek}^{*}}_{\!\!wt}\;{}^{0}{Tilman}\;c}]]^{}} \qquad (\hbox {R}_1) \end{aligned}$$

Types: ${Seek}^{*}/(\hbox {o}\upiota {*}_{n})_{{\uptau }{\upomega }}$; ${Tilman}/{\upiota }; Last\_Dec/(v{\uptau })$: the function that associates a number with its last decimal digit; $\uppi /\uptau$; $c/{*}_{2} \rightarrow _{v}{*}_{1}$.

Another inference based on $(\hbox {R}_{1})$ is this:

$$\begin{aligned} \frac{\hbox {Tilman is proving Fermat's Last Theorem}_{}}{\hbox {There is a numerical construction}\; c\; \hbox {such that Tilman is proving}\;c^{}} \end{aligned}$$

Let FLT be specified as follows:³²

$$\begin{aligned} {\forall }x\; y\; z\; n[[{n >{}^{0}{2}}]\supset \lnot [{x^{n}+y^{n} = z^{n}}]] \end{aligned}$$

Then our argument obtains this analysis:

Types: $Prove/(\hbox {o}{\upiota }{*_{n}})_{{\uptau }{\upomega }}$; the other types are obvious.

Yet another example:³³

$$\begin{aligned} \frac{\hbox {Tilman is solving the equation} \left( {x{}^{{2}}+x-2} \right) =0}{\hbox {There is something Tilman is solving}} \end{aligned}$$

Here is an application of $(\hbox {R}_{2})$:

$$\begin{aligned} \frac{\hbox {Tilman computes the value of}\; sin(x)/cos(x)\;\hbox {at}\;{\uppi }}{\hbox {There is a construction such that Tilman computes its Composition with}\;{\uppi }} \end{aligned}$$

Types: $c/{*}_{2} \rightarrow _{v}\!{*}_{1}; g/{*}_{1} \rightarrow _{v} ({\uptau }{\uptau }); {\lambda }\,x\;[{}^{0}{:}\; [{}^{0}{Sin}\,x]\; [{}^{0}{Cos}\,x]]/{*}_{1} \rightarrow _{v}(\uptau \uptau )$; the other types are obvious.

Since a Closure is not $v$-improper for any valuation $v$, we can apply $(\hbox {R}_{2}^{'}$):

$$\begin{aligned}&\frac{\hbox {Tilman computes the value of}\;sin(x)/cos(x) \hbox { at}\; \uppi _{}}{\hbox {There is a construction of a function such that Tilman computes its value at } \uppi ^{}} \\&\frac{{\lambda }w{\lambda }t\;[{}^{0}{Compute}_{wt}\;{}^{0}{Tilman}\;{}^{0}[{{\lambda }x\;[{}^{0}{:}\;[{}^{0}{Sin}\;x][{}^{0}{Cos}\;x}]]\;{}^{0}{\uppi }]]_{}}{{\lambda }w{\lambda }t\;[{}^{0}{\exists }^{*}{\lambda }c\;[{}^{0}{\exists }\lambda f[{f={}^{{2}}c} ]\wedge [{}^{0}{Compute}_{wt}\;{}^{0}{Tilman}\;[{}^{0}{Sub}\,c\;{}^{0}{g}\;{}^{0}[g\;{}^{0}{\uppi }]]]]]^{}} \quad \qquad (\hbox {R}_{2}') \end{aligned}$$

Additional types: $^{2}c,g \rightarrow _{v} (\uptau \uptau )$.

From the premise in the first example above we can also derive that there is a number such that Tilman is seeking its last decimal. Thus we have another valid argument:

$$\begin{aligned} \frac{\hbox { Tilman is seeking the last decimal of} \uppi }{\hbox {There is a number such that Tilman is seeking its last decimal}} \end{aligned}$$

This inference requires $(\hbox {R}_{3})$:

$$\begin{aligned} \frac{{\lambda }w{\lambda }t\;[{{}^{0}{Seek}^{*}_{wt}\;{}^{0}{Tilman}\;{}^{0}}[{}^{0}{Last\_Dec}\;{}^{0}{\uppi }]]_{}}{{\lambda }w{\lambda }t\;[{}^{0}{\exists } {\lambda }x\;[{{}^{0}{Seek}^{*}_{wt}\;{}^{0}{Tilman}}\; [{}^{0}{Sub}\;[{{}^{0}{Tr}\;x}]\;{}^{0}{y}\;{}^{0}[{{}^{0}{Last\_Dec}\;y}]]]]^{}}\qquad \left( {\hbox {R}_{3}}\right) \end{aligned}$$

Types: $x, y/{*}_{1} \rightarrow _{v} \uptau ; {\exists }/(\hbox {o}(\hbox {o}\uptau ))$.

If Tilman is seeking the millionth digit of the decimal expansion of $\uppi$, he may succeed in his effort and identify that number. Thus we have another argument that illustrates the application of (R$_{4}$):

$$\begin{aligned}&\frac{\hbox {Tilman finds the millionth digit of the decimal expansion of} \, {\uppi }}{{\begin{array}{l} \hbox {There is a number such that Tilman identifies it} \\ \hbox {as the millionth digit of the decimal expansion of} \, {\uppi } \\ \end{array}}} \end{aligned}$$

$$\begin{aligned}&\frac{{\lambda }w{\lambda }t\;[{}^{0}{Find}_{wt}\;{}^{0}{Tilman}\;{}^{0}[{}^{0}{Mill\_Dec}\;{}^{0}{\uppi } ]]_{}}{{\lambda }w{\lambda }t\;[{}^{0}{\exists }{\lambda }x[[x =\;[{}^{0}{Mill\_Dec}\;{}^{0}{\uppi }]] \, \wedge {[} {}\,{}^{0}{Ident}_{wt}\;{}^{0}{Tilman}\; x\;{}^{0}[{}^{0}{Mill\_Dec} \, {}^{0}{\uppi }]]]] ^{}}\,\,\,\quad (\hbox {R}_{4}) \end{aligned}$$

Types: $Find/(\hbox {o}{\upiota }{*}_{n})_{{\uptau }{\upomega }}$; $v$: the type of naturals; ${Mill\_Dec}/(\nu \uptau )$: the function that associates a real number with its millionth decimal digit; $Ident/(\hbox {o}{\upiota }{{\nu }{*}}_{n})_{{\uptau }{\upomega }}$.

Suppose that Tilman is solving the equation $(x^{2}+x - 2) = 0$ and that his effort meets with success, in that he finds the solution he was seeking. We can apply rule $\hbox {R}_{1}$:

$$\begin{aligned} \frac{\hbox {Tilman has solved the equation}\;(x^{2} + x - 2) = 0}{\hbox {There is something that Tilman has solved}} \end{aligned}$$

The argument is no doubt valid. Yet in this case we would like to derive more. To this end we apply $(\hbox {R}_{4})$. If Tilman has solved the equation $x^{2}+x - 2 = 0$ then there is an ($\hbox {o}\uptau )$-object (in this case the set {1, $-2$}) satisfying the equation, and Tilman has identified this set as the product of the construction [${\lambda }x\;[x^{2}+x - 2] = 0]$. Thus we have:

$$\begin{aligned} \frac{{\lambda }w{\lambda }t\;[{{}^{0}{Solved}_{wt} \;{}^{0}{Tilman}\;{}^{0}} [{\lambda }x\;[x^{2}+x-2 ] = 0]]_{}}{ {\lambda }w{\lambda }t\;[{}^{0}{\exists }{\lambda }s\,[[{s\!=\!}\;[\lambda x[ {x{}^{{2}}\!+\!x\!-\!\hbox { 2}} ] \!=\! 0]]\,\!\wedge \!{[} {{}^{0}{Ident}_{wt}\;{}^{0}{Tilman}\;s\;{}^{0}} [\lambda x[ {x{}^{{2}}+x-\hbox { 2}} ] = 0]]]] ^{}} \end{aligned}$$

Additional types: variable $s \rightarrow _{v} (\hbox {o}{\uptau }), Ident/(\hbox {o}\upiota (\hbox {o}\uptau ){{*}_{n}})_{\uptau \upomega }$

In (Duží et al. (2010), Chap. 2) we defined the distinction between attitudes de dicto and de re for attitudes to empirical notions. In mathematics a de re attitude is characterized by an extensional occurrence of a constituent that $v$-constructs the value of the denoted function. This value is then anaphorically referred to in the attitude complement. Here is an example:

$$\begin{aligned} \frac{\hbox {The last decimal of}\;{\uppi }\;\hbox {is being calculated by Tilman}}{\hbox {There is a number such that Tilman calculates}\, { it}\, \hbox {as the last decimal of}\;{\uppi }} \end{aligned}$$

The argument is valid, though drastically unsound: the premise presupposes the existence of the last decimal of $\uppi$. And if per impossibile a number $n$ were the last decimal of $\uppi$ then Tilman would be obtaining $n$ as a result of his calculation of the last decimal of $\uppi$. Hence, existential generalization simply serves to make explicit an implicit ontological presupposition incurred in the premise. In this case it is the presupposed existence of the value of the function denoted by ‘the last decimal of’ at the argument $\uppi$.

If we analyzed the premise similarly as above, that is, in terms of the Closure

$$\begin{aligned} {\lambda }w{\lambda }t\;[{{}^{0}{Calculate}_{wt}\;{}^{0}{Tilman}\;{}^{0}} [{}^{0}{Last\_Dec}\;{}^{0}\!{\uppi }]] \end{aligned}$$

the existence of a last decimal of $\uppi$ would neither be presupposed, nor would it follow. The Composition $[{}^{0}\!{Last\_Dec}\,{}^{0}\!{\uppi }]$ occurs hyperintensionally here, but in the de re case it must occur extensionally. In order for [$\,{}^{0}\!{Last\_Dec} \,{}^{0}\!{\uppi }]$ to be a constituent occurring extensionally, we must again deploy the functions Sub and Tr:

$$\begin{aligned} {\lambda }w{\lambda }t\;[{}^{0}Calculate{_{{}{wt}}} \,{}^{0}\!{Tilman}\,[{}^{0}\!{Sub}\,[{}^{0}Tr\,[{}^{0}\!{Last\_Dec}\,{}^{0}\!{\uppi }]]\,{}^{0}\!{y}\,{}^{0} [[{}^{0}\!{Last\_Dec}\,{}^{0}\!{\uppi }]=y]]] \end{aligned}$$

Now we can apply $(\hbox {R}_{5})$-act in order to obtain the conclusion:

$$\begin{aligned} \frac{{\lambda }w{\lambda }t\;[{{}^{0}\!{Calculate}_{wt} \,{}^{0}\!{Tilman}}\,[{}^{0}\!{Sub}\,[{}^{0}\!{Tr}\,[{}^{0}\!{Last\_Dec}\,{}^{0}\!{\uppi }]]\, {{}^{0}\!{y}\,{}^{0}}[[{}^{0}\!{Last\_Dec}\,{}^{0}\!{\uppi }] = y ]]]}{{\lambda }w{\lambda }t\;[{}^{0}\exists {\lambda }x\,[{}^{0}\!{Calculate}_{wt} \,{}^{0}\!{Tilman}\,[{}^{0}\!{Sub}\,[{}^{0}\!{Tr}\;x]\,{}^{0}\!{y}\,{}^{0}[[{}^{0}\!{Last\_Dec}\,{}^{0}\!{\uppi }] = y]]]]} \end{aligned}$$

5.2 Empirical objectual attitudes: an application

In (Duží et al. (2010), § 5.2, § 5.3) much attention was devoted to objectual attitudes whose complement is an intension like seeking or finding the site of Troy. Hence we analyzed these attitudes as relations-in-intension sharing the polymorphous type $(\hbox {o}\upiota {\upalpha }_{{\uptau }{\upomega }})_{{\uptau }{\upomega }}$. We suggested that the default interpretation of objectual attitudes is as intensional attitudes, because these attitudes concern an empirical object where it is irrelevant how the intension is presented to, or conceptualized by, the ascribee.

This may often be true, but there are also cases where the mode of presentation of the intension does matter. This is so with regard to, e.g., Tilman seeking an abominable snowman without him seeking a yeti. In this case an intensional analysis will yield a contradiction, because Tilman would be related, and at the same time not related, to one and the same property by the seeking relation. Thus a truthful report of such a situation needs to be hyperintensional. A hyperintensional analysis avails itself of two different hyperintensions presenting the same property. When construed hyperintensionally, Tilman’s search is only ostensibly inconsistent.

To get the example of Tilman seeking an abominable snowman and not seeking a yeti off the ground, we are stipulating that ‘is a yeti’ and ‘is an abominable snowman’ are a pair not of synonymous but merely equivalent predicates. Their respective meanings are co-intensional, but not procedurally isomorphic (co-hyperintensional). The rationale for this stipulation is that the latter predicate has a molecular structure thanks to the application of the property modifier denoted by ‘abominable’ to the property denoted by ‘snowman’, whereas the former predicate is atomic.³⁴ One could object that it seems reasonable to assume that there is a meaning postulate in place to the effect that ‘is a yeti’ is shorthand for, or a notational variant of, ‘is an abominable snowman’, the same way ‘lasts a fortnight’ is arguably short for ‘lasts two weeks’. What speaks against this assumption, at least through the lens of TIL, is that the Trivialization $\,{}^{0}Yeti$ and the Composition $[\,{}^{0}Abominable \,{}^{0}Snowman]$ are not procedurally isomorphic, but only equivalent constructions. Furthermore, from a formal point of view at least, it is questionable what semantic and inferential gain may be accrued from introducing a redundant predicate like ‘is a yeti’, on its construal as a mere notational variant of ‘is an abominable snowman’.³⁵

What we have on our hands is an empirical hyperintensional attitude, and we can apply $(\hbox {R}_{1})$:

$$\begin{aligned} \frac{\hbox {Tilman is seeking an abominable snowman and not seeking a yeti}}{\hbox {There is something Tilman is seeking and something} \left( {\hbox {else}} \right) \hbox { he is not seeking}}\\ \end{aligned}$$

$$\begin{aligned} \frac{{\lambda }w{\lambda }t\;[[{}^{0}\!{{Seek}^{*}_{wt}}\;{}^{0}{Tilman}\,{}^{0}[{}^{0}\!{Abominable}\;{}^{0}\!{Snowman}]] \wedge \lnot [{}^{0}{Seek}^{*}_{wt}\;{}^{0}{Tilman}\,{}^{00}\!{Yeti}]]}{{\lambda }w{\lambda }t\;[{}^{0}\exists ^{*}{\lambda } c\;{}^{0}{\exists }^{*}{\lambda }\,d\;[[{{}^{0}{Seek}^{*}_{wt}\;{}^{0}\!{Tilman}\;c}] \wedge \lnot [{}^{0}{Seek}^{*}_{wt}\;{}^{0}{Tilman}\;d]]]} \end{aligned}$$

Types: $Yeti,\;Snowman/(\hbox {o}{\upiota })_{\uptau {\upomega }}; {Abominable}/((\hbox {o}{\upiota })_{\uptau {\upomega }}(\hbox {o}{\upiota })_{\uptau {\upomega }})$: a property modifier; $[{}^{0}\!{Abominable}\;{}^{0}\!{Snowman}] \rightarrow (\hbox {o}{\upiota })_{\uptau {\upomega }}; c, d/{*}_{2} \rightarrow {*}_{1};\;{}^{2}\!{c},{}^{2}\!{d} \rightarrow _{v} (\hbox {o}{\upiota })_{{\uptau }{\upomega }}$.

In this case by applying $(\hbox {R}_{2}')$ we can derive a further conclusion:

$$\begin{aligned} \frac{ {\begin{array}{l} \hbox { Tilman is seeking an abominable snowman and not seeking a yeti}\\ \end{array}}}{\begin{array}{c} \hbox {There is a property such that Tilman is seeking an instance of it via a construction}\;c \\ \hbox {and not seeking an instance of it via another construction}\;d \end{array}} \end{aligned}$$

$$\begin{aligned} \frac{\begin{array}{l} {\lambda }w{\lambda }t\;[{[{{}^{0}{Seek}^{*}_{wt}\;{}^{0}{Tilman}\;{}^{0}}[{}^{0}{Abominable}\;{}^{0}\!{Snowman}}]]\wedge \lnot [{{}^{0}{Seek}^{*}_{wt}\;{}^{0}{Tilman}^{\,00}{Yeti}} ]] \\ \end{array}^{}}{{}^{}\begin{array}{l} {\lambda }w{\lambda }t\;[{}^{0}{\exists }^{*}{\lambda }c\;{}^{0}{\exists }^{*}{\lambda }d\;{}^{0}{\exists }{\lambda }p\;[[{p = {}^{{2}}c} ]\wedge [{p ={}^{{2}}d}]\,\wedge {[}{{}^{0}\!{Seek}^{*}_{wt}\;{}^{0}{Tilman}\;c}]\wedge \lnot [{{}^{0}\!{Seek}^{*}_{wt}\;{}^{0}\!{Tilman}\;d} ]]] \\ \end{array}} \end{aligned}$$

Note that the premise demands the double Trivialization ${}^{00}\!{Yeti}$, because Tilman seeks what $^{00}\!{Yeti}$ constructs, namely ${}^{0}\!{Yeti}$.

Moreover, by applying $\hbox {R}_{3}$ we can derive that Tilman is seeking something abominable (where $p, q \rightarrow (\hbox {o}{\upiota })_{{\uptau }{\upomega }})$:

$$\begin{aligned} \frac{{\lambda }w{\lambda }t\;[{[{{}^{0}\!{Seek}^{*}_{wt}\; {}^{0}{Tilman}\;{}^{0}} [{}^{0}\!{Abominable}\;{}^{0}{Snowman}}]]\wedge \lnot [{{}^{0}\!{Seek}^{*}_{wt}\;{}^{0}\!{Tilman}\;{}^{00}\!{Yeti}}]]}{{\lambda }w{\lambda }t\;[{}^{0}{\exists }{\lambda }p\;[{{}^{0}{Seek}^{*}_{wt} \,{}^{0}{Tilman}}\;[{}^{0}\!{Sub}\;[{{}^{0}{Tr}\;p}]\;{}^{0}{q}\;{}^{0}[{{}^{0}\!{Abominable}\;q}]]]]} \end{aligned}$$

6 Conclusion

We demonstrated above how to validly quantify into various sorts of hyperintensional contexts involving objectual (i.e. non-propositional) attitude complements. This cluster of logical results was obtained in virtue of an extensional logic of hyperintensions, namely Transparent Intensional Logic, which comes with a context-invariant, top-down semantic theory that yields universal transparency to the exclusion of opaque contexts. An extensional logic of hyperintensions is permissive or inclusive in the sense of validating all the rules of extensional logic, including substitution of identicals and existential generalization, also in hyperintensional contexts, but must at the same time be restrictive or exclusive with regard to what counts as admissible operands.

The novelties of the paper are the following. The paper offers a formally worked-out, philosophically motivated criterion of hyperintensional individuation, which is defined in terms of a slightly more carefully stated version of ${\upalpha }$-conversion and $\upbeta$-conversion by value, which amounts to a modification of Church’s Alternative (A1). Moreover, we presented a detailed study of the attitude of calculating. We propounded updated rules for quantifying into hyperintensional contexts de dicto, which are an adjustment and generalization of the rules presented in Duží et al. (2010). We presented an analysis of ostensibly logically impossible empirical attitudes, which require at least two different hyperintensional presentations of one and the same empirical property. Finally, we put forward rules for quantifying into hyperintensional attitudes de re, which correct the rules presented in (Duží et al. (2010), § 5.3).

We have proved two major things. First, it is always valid to quantify into hyperintensional attitude contexts and over hyperintensional entities. Second, factive attitudes (e.g. finding an abominable snowman or having solved an equation) validate, furthermore, quantifying over the (intensional or extensional) entities presented by the respective constituent of the attitude complement, and so do non-factive attitudes provided the respective constituent of the attitude complement presents the sort of object that is to be quantified over.