Weak Negation in Inquisitive Semantics

Abstract

This paper introduces and explores a conservative extension of inquisitive logic. In particular, weak negation is added to the standard propositional language of inquisitive semantics, and it is shown that, although we lose some general semantic properties of the original framework, such an enrichment enables us to model some previously inexpressible speech acts such as weak denial and ‘might’-assertions. As a result, a new modal logic emerges. For this logic, a Fitch-style system of natural deduction is formulated. The main result of this paper is a theorem establishing the completeness of the system with respect to inquisitive semantics with weak negation. At the conclusion of the paper, the possibility of extending the framework to the level of first order logic is briefly discussed.

1 Introduction

Inquisitive semantics is a recently developed theoretical framework which is based on the idea that the meaning expressed by a sentence is constituted not only of the informative content of the sentence but also of its inquisitive content which corresponds to the issue it raises. The main motive for this conceptual shift is an attempt to reflect the interactive use of language in exchanging information. The new notion of meaning directly captures the nature of information exchange as a cooperative process of raising and resolving issues. For a detailed exposition of the framework and a thorough explanation of its motivation, see e.g., Groenendijk and Roelofsen (2009) and Ciardelli et al. (2012, (2013).

The informative content $info (A)$ of a given sentence $A$ can be represented as a set of possible worlds and the sentence provides the information that the actual world is located somewhere in the set. The inquisitive content $inq (A)$ can be understood as a request to locate the actual world more precisely. So, the issue $inq (A)$ can be modeled as a set of those nonempty subsets of $info (A)$ that contain enough information to settle the request.

According to $A$ any world of $info (A)$ might be the actual world, so the request to locate the actual world more precisely in $info (A)$ should not a priori exclude any world of $info (A)$. As a consequence, it has to hold that $info (A)=\bigcup inq (A)$, which means that $info (A)$ can always be retrieved from $inq (A)$ and the proposition expressed by $A$ can be identified simply with $inq (A)$.

This explains why propositions in inquisitive semantics are not modeled in the standard way as sets of possible worlds but rather as sets of sets of possible worlds. Moreover, in the standard version of inquisitive semantics, a set of sets of possible worlds that represents a proposition is supposed to be downward closed. The reason is that if a subset $S$ of $info (A)$ locates the actual world with sufficient precision, then the same also holds for every subset of $S$ (see e.g., Ciardelli et al. 2013, section 3).

However, this paper is based on the observation that there are sentences for which this general picture is not appropriate. Utterances of these sentences amount to conversational moves that are about the discourse context (or some relevant information state) rather than about the localization of the actual world. Typical examples here would be ‘might’-sentences or some sentences expressing denial of conditionals. These sentences express propositions that cannot be represented by downward closed sets of sets of possible worlds.

We can express such sentences if we add weak negation to the basic language of inquisitive semantics. The main task of this paper is to explore the impact of such enrichment. It turns out that it leads to an interesting modal logic (where modal operators are not primitive symbols but are defined in terms of other symbols). According to my knowledge, this modal logic has not yet appeared in the literature but has some common features with the modal logics studied in Punčochář (2012). The main goal of this paper is to provide a syntactic characterization of this logic.

The content of this paper is structured as follows: The formal framework of inquisitive semantics will be introduced in the next section. In Sect. 3, weak negation will be added to the language and the motivation for such extension of the language and its impact will be discussed. A system of natural deduction for the resulting semantics will be formulated in Sect. 4. Section 5 contains the completeness proof. At the conclusion of the paper, we briefly discuss the possibility of extending the framework to the level of first order logic.

2 Inquisitive Semantics

In this section, we will introduce the formal semantics of inquisitive logic which will be used throughout the paper. Formal features of inquisitive semantics were studied, e.g., in Ciardelli (2009), Ciardelli and Roelofsen (2011) and Roelofsen (2013). Groenendijk and Roelofsen (2009) and Ciardelli (2009) are important early sources of the current semantic system.

Let $At$ be a set of atomic formulas. By a valuation of atoms from $At$ we will mean a function from $At$ to the set of truth values $\left\{ T, F\right\}$. Valuations will represent possible worlds.

An information state (or just state) is a nonempty set of possible worlds.¹ Sets of possible worlds can represent information states of the participants as well as the common ground or context of the conversation. This goes back to Robert Stalnaker:

A context should be represented by a body of information that is presumed to be available to the participants in the speech situation. A context set is defined as the set of possible situations that are compatible with this information—with what the participants in the conversation take to be the common shared background. (Stalnaker 1999, p. 6)

Let $L$ be the propositional language containing the atomic formulas from $At$, the constant $\bot \notin At$ (representing absurdity) and the formulas built out of atomic formulas using the connectives $\wedge , \vee$ and $\rightarrow$. The formal semantics is based on the relation of support between states and formulas of the language $L$. The relation is determined by the following conditions. Let $s$ be an arbitrary state, $p$ an atomic formula and $\varphi , \psi$ arbitrary formulas:

• $s \nvDash \bot$,

• $s \vDash p$ iff for all $v \in s, v(p)=T$,

• $s \vDash \varphi \wedge \psi$ iff $s \vDash \varphi$ and $s \vDash \psi$,

• $s \vDash \varphi \vee \psi$ iff $s \vDash \varphi$ or $s \vDash \psi$,

• $s \vDash \varphi \rightarrow \psi$ iff for any nonempty $t \subseteq s$, if $t \vDash \varphi$ then $t \vDash \psi$.

$s \vDash \varphi$ is read as follows: ‘The formula $\varphi$ is supported by the state $s$’ or simply ‘$s$ supports $\varphi$’.

In inquisitive semantics, negation ($\lnot$) is introduced as a symbol defined in the intuitionistic way:

• $\lnot \varphi =_{Df} \varphi \rightarrow \bot$

The consequence relation is defined in the obvious way: $\varDelta \vDash \varphi$ iff $s \vDash \varphi$ for every state $s$ supporting everything from $\varDelta$.

In this section, we will mention three important features of this semantics for $L$: classical behavior of singletons, persistence, and disjunction property. First, classical truth at single worlds can be viewed as the relation of support restricted to singleton states.

Proposition 1

$\varphi$ is classically true at $v$ iff $\varphi$ is supported by $\left\{ v \right\}$.²

Proof

Straightforward induction on the complexity of the formula.

Second, support is persistent with respect to substates (i.e. nonempty subsets of a given state).

Proposition 2

If a formula is supported by a state, it is supported by all substates of the state.

Proof

Induction on the complexity of the formula.

Proposition 2 is also a consequence of the fact that inquisitive semantics can be regarded as Kripke semantics for intuitionistic logic restricted to a special class of models. In particular, the models are of the structure: $\left\langle \wp (s)-\{ \emptyset \}, \supseteq , V \right\rangle$, where $s$ is a nonempty set of classical valuations, $\wp (s)$ is the powerset of $s$, $\supseteq$ is the superset relation, and $t \in V(p)$ iff $t$ is a nonempty subset of $s$ such that for all $v \in t,\,v(p)=T$. For a detailed discussion of the relation of inquisitive logic to intuitionistic logic and its extensions, see Ciardelli (2009).

Third, inquisitive logic has the disjunction property.

Proposition 3

If $\vDash \varphi \vee \psi$, then $\vDash \varphi$ or $\vDash \psi$.

Proof

Suppose that neither $\varphi$ nor $\psi$ is supported by all states. Then there is a state $s_{1}$ which does not support $\varphi$ and there is a state $s_{2}$ which does not support $\psi$. It follows from Proposition 2 that $s_{1} \cup s_{2}$ does not support $\varphi \vee \psi$.

3 Weak Negation

Inquisitive semantics has the ambition to model adequately many phenomena from natural language: It provides an enriched notion of sentential meaning that besides the informative content of a sentence captures also its inquisitive content. This leads to an analysis of linguistic discourse that is aimed at exchanging information. The new notion of meaning reflects the nature of information exchange as a cooperative process of raising and resolving issues. This perspective allows for a uniform semantic representation of a wide range of declarative and interrogative sentence types (see e.g., Ciardelli et al. 2013, section 5).

Let us mention one unintuitive feature of the semantics which concerns negated conditionals. The formula $\lnot (p \rightarrow q)$ entails both the antecedent $p$ and the negation of the consequent $\lnot q$. This can hardly be advocated and it would be difficult to find any evidence that this is in accordance with natural language.³ What do we do when we deny an indicative conditional? There is arguably more than one sense in which a conditional can be denied. Most significantly, an utterance of the form it is not the case that if A then B could amount to any of the following:

• (a) If A then not B.

• (b) If A then possibly not B.

• (c) Possibly A and not B.

The option (a) is preferred by many authors. For example, the equivalence between not if A then B and if A then not B holds in such frameworks as Stalnaker’s possible world semantics (see Stalnaker 1968), probabilistic semantics (see e.g., Adams 1975; Edgington 1995), connexive logics (see Wansing 2014), and Cantwell’s three valued logic introduced in Cantwell (2008). This equivalence was also integrated in the logic proposed in Punčochář (2014).

Some empirical evidence for the option (b) was found in Egré and Politzer (2013). This way of denying conditionals is also a part of D. Lewis’ well-known theory of centered spheres (see Lewis 1973), which, however, is formulated for subjunctive and not indicative conditionals.

Even though options (a) and (b) are both reasonable, in this paper we will concentrate on option (c), which is in accordance with the standard theories of strict conditionals originated in Lewis and Langford (1932). So we will assume that very often (but, admittedly, not always) a denial of a conditional corresponds to the claim that it might be the case that the antecedent is true and the consequent false. For example, the denial of the sentence.

• If the husband was the murderer, the motive for the murder was jealousy.

could be based on the opinion that it might be the case that the husband was the murderer and the motive for the murder was not jealousy but money. Paul Grice put it in this way ⁴:

Sometimes a denial of a conditional has the effect of a refusal to assert the conditional in question, characteristically because the denier does not think that there are adequate non-truth-functional grounds for such an assertion$\ldots$ For example, to say ‘It is not the case that if X is given penicillin, he will get better’ might be a way of suggesting that the drug might have no effect on X at all. (Grice 1991, p. 81)

It is not possible to express explicitly this kind of denial in the basic language of inquisitive semantics. To be able to do this, we need a negation which is weaker than $\lnot$. The main task of this paper is to explore the impact of adding such a negation to the language $L$.

Let us introduce the language $L^{\mathord {\sim }}$, which is the language $L$ enriched with the unary operator $\sim$ standing for the weak negation. The semantic condition for $\sim$ is very simple:

• $s \vDash \mathord {\sim }\varphi$ iff $s \nvDash \varphi$.⁵

However, this extension of the language $L$ has some serious consequences. Although Proposition 1 (classical behavior of singletons) is true even if formulated for the language $L^{\mathord {\sim }}$, Propositions 2 (persistence) and 3 (disjunction property) cease to be true. For example, the formula $\mathord {\sim }p$ is not persistent, and it holds that $\vDash p \vee \mathord {\sim }p$ but neither $\vDash p$ nor $\vDash \mathord {\sim }p$. From the fact that $\mathord {\sim }p$ is not persistent it follows that it is equivalent with no formula from the language $L$. As a consequence, $L^{\mathord {\sim }}$ has greater expressive power than $L$.

It is important for what follows that the negation $\lnot$ is still present in $L^{\mathord {\sim }}$ as a defined symbol meaning the implication of contradiction. As the name of the new symbol suggests, $\sim$ is weaker than $\lnot$. It holds that $\lnot \varphi \vDash \mathord {\sim }\varphi$ but $\mathord {\sim }\varphi \nvDash \lnot \varphi$. The former is a consequence of the fact that there is no state which would support both $\varphi$ and $\lnot \varphi$. So if a given state supports $\lnot \varphi$, it does not support $\varphi$, which means that it supports $\mathord {\sim }\varphi$. To see that $\mathord {\sim }\varphi \nvDash \lnot \varphi$, we can take, for example, an atomic formula $p$ as $\varphi$ and consider a state containing both a world at which $p$ is true and a world at which $p$ is false. Such a state supports $\mathord {\sim }p$ but not $\lnot p$.

The presence of weak negation allows for the introduction of two kinds of necessity and their duals in the following way:

$$\begin{aligned} \begin{array}{cc} \square \varphi =_{Df} \lnot \lnot \varphi , &{} \quad \lozenge \varphi =_{Df} \mathord {\sim }\square \mathord {\sim }\varphi .\\ \blacksquare \varphi =_{Df} \lnot \mathord {\sim }\varphi , &{} \quad \blacklozenge \varphi =_{Df} \mathord {\sim }\blacksquare \mathord {\sim }\varphi .\\ \end{array} \end{aligned}$$

In the rest of this section, we will explore the character of these modal operators. Let us introduce the metasymbol $\equiv$, which will stand for logical equivalence: $\varphi \equiv \psi$ means that $\varphi \vDash \psi$ and $\psi \vDash \varphi$. The following proposition is an immediate consequence of the previous definitions and expresses the relationship between the two kinds of operators.

Proposition 4

Let $\varphi$ be any formula from $L^{\mathord {\sim }}$. Then

• (i) $\square \varphi \equiv \blacksquare \blacklozenge \varphi$,

• (ii) $\lozenge \varphi \equiv \blacklozenge \blacksquare \varphi$.

Proof

• (i) $\square \varphi = \lnot \lnot \varphi \equiv \lnot \mathord {\sim }\mathord {\sim }\lnot \mathord {\sim }\mathord {\sim }\varphi = \blacksquare \blacklozenge \varphi$.

• (ii) $\lozenge \varphi = \mathord {\sim }\lnot \lnot \mathord {\sim }\varphi \equiv \mathord {\sim }\lnot \mathord {\sim }\mathord {\sim }\lnot \mathord {\sim }\varphi = \blacklozenge \blacksquare \varphi$.

The semantics of the modal operators is clarified by the following proposition, which can be easily established. It shows that the operators behave in a natural way:

Proposition 5

For any formula $\varphi$ from $L^{\mathord {\sim }}$:

• (i) $\square \varphi$ is supported by $s$ iff $\varphi$ is (classically) true at every world of $s$.

• (ii) $\blacksquare \varphi$ is supported by $s$ iff $\varphi$ is supported by every substate of $s$.

• (iii) $\lozenge \varphi$ is supported by $s$ iff $\varphi$ is (classically) true at some world of $s$.

• (iv) $\blacklozenge \varphi$ is supported by $s$ iff $\varphi$ is supported by some substate of $s$.

Proof

For an illustration, we will prove the claim (i). Assume that $s$ supports $\square \varphi$, i.e. $(\varphi \rightarrow \bot ) \rightarrow \bot$. Let $v$ be an arbitrary world of $s$. For the contradiction suppose that $\{ v \}$ does not support $\varphi$. Then $\{ v \} \vDash \varphi \rightarrow \bot$ and, as a consequence, $\{ v \} \vDash \bot$, which is in contradiction with the first semantic condition. So $\varphi$ is supported by $\{ v \}$, which entails that $\varphi$ is classically true at $v$.

Suppose that $\varphi$ is classically true at every world of $s$. We want to prove that $s \vDash (\varphi \rightarrow \bot ) \rightarrow \bot$. For the contradiction, suppose that there is a substate $t$ which supports $\varphi \rightarrow \bot$. Then, for any $v \in t$, $\{v \} \vDash \bot$, which is in contradiction with the first semantic condition.

Notice that it follows from Proposition 5 (i) that in the scope of $\square$ everything behaves classically in the following sense: It holds that $\vDash \square \varphi$ iff $\varphi$ is a classical tautology, it holds that $\square \varphi \vDash \square \psi$ iff $\psi$ follows from $\varphi$ in classical logic, and, consequently, it holds that $\square \varphi \equiv \square \psi$ iff $\varphi$ and $\psi$ are logically equivalent according to classical logic. The same holds for the operator $\lozenge$, as follows from Proposition 5 (iii).

Instead of weak negation, the operator $\blacklozenge$ might be chosen as a primitive symbol. Consider the language $L^{\blacklozenge }$, which is the language $L$ enriched with the operator $\blacklozenge$, and accept the claim (iv) of Proposition 5 as the definitory semantic condition for $\blacklozenge$. Then the languages $L^{\mathord {\sim }}$ and $L^{\blacklozenge }$ have the same expressive power in the following sense: (a) For any formula $\varphi$ from $L^{\blacklozenge }$ there is a formula $\psi$ from $L^{\mathord {\sim }}$ such that $\varphi \equiv \psi$, and (b) for any formula $\varphi$ from $L^{\mathord {\sim }}$ there is a formula $\psi$ from $L^{\blacklozenge }$ such that $\varphi \equiv \psi$. Everything that can be expressed in the first language can also be expressed in the second language and vice versa.

Since $\blacklozenge$ is definable in terms of the negations $\sim$ and $\lnot$, the claim (a) is evident. To show that the claim (b) is also true, we will introduce two translations $^{+}$ and $^{-}$ that will assign to every formula from $L^{\mathord {\sim }}$ a formula from $L^{\blacklozenge }$. These functions are defined recursively. If $\varphi$ is an atomic formula or the constant $\bot$, then $\varphi ^{+}=\varphi$ and $\varphi ^{-}= \blacklozenge \lnot \varphi$. For complex formulas we define:

$$\begin{aligned} \begin{array}{ll} \left( \mathord {\sim }\varphi \right) ^{+}=\varphi ^{-} &{}\quad \left( \mathord {\sim }\varphi \right) ^{-}=\varphi ^{+}\\ \left( \varphi \wedge \psi \right) ^{+}=\varphi ^{+}\wedge \psi ^{+} &{}\quad \left( \varphi \wedge \psi \right) ^{-}=\varphi ^{-}\vee \psi ^{-}\\ \left( \varphi \vee \psi \right) ^{+}=\varphi ^{+} \vee \psi ^{+} &{}\quad \left( \varphi \vee \psi \right) ^{-}=\varphi ^{-} \wedge \psi ^{-}\\ \left( \varphi \rightarrow \psi \right) ^{+}=\varphi ^{+} \rightarrow \psi ^{+} &{}\quad \left( \varphi \rightarrow \psi \right) ^{-}=\blacklozenge \left( \varphi ^{+}\wedge \psi ^{-}\right) \\ \end{array} \end{aligned}$$

The following proposition shows that the expressive power of $L^{\mathord {\sim }}$ is not greater than that of $L^{\blacklozenge }$.

Proposition 6

For any formula $\varphi$ from $L^{\mathord {\sim }}$:

• (i) $\varphi \equiv \varphi ^{+}$,

• (ii) $\mathord {\sim }\varphi \equiv \varphi ^{-}$.

Proof

Induction on the complexity of $\varphi$. For an illustration, we will give the proof for the atomic case. The positive part is evident. As regards the negative part, we have to show that $\mathord {\sim }p \equiv \blacklozenge \lnot p$. It holds that $s$ supports $\mathord {\sim }p$ iff $s$ does not support $p$ iff $p$ is false at a possible world from $s$ iff $\lnot p$ is supported by a substate of $s$ iff $\blacklozenge \lnot p$ is supported by $s$.

In the rest of this paper, $L^{\mathord {\sim }}$ will be considered as the basic language and the modal operators as symbols defined in this language.

It can be observed that in many cases the two kinds of modal operators behave equivalently. To describe this fact more precisely, let us introduce the following notation: Let $\left\| \varphi \right\|$ denote the proposition expressed by $\varphi$, i.e. the set of states which support $\varphi$. Then the following proposition easily follows from Proposition 5.

Proposition 7

Let $\varphi$ be any formula from $L^{\mathord {\sim }}$.

• (i) If $\left\| \varphi \right\|$ is downward closed, then $\lozenge \varphi \equiv \blacklozenge \varphi$.

• (ii) If $\left\| \varphi \right\|$ is closed under arbitrary unions, then $\square \varphi \equiv \blacksquare \varphi$.⁶

Proof

• (i) In general, it holds that $\lozenge \varphi \vDash \blacklozenge \varphi$. Suppose that $\left\| \varphi \right\|$ is downward closed and $s$ is a state that supports $\blacklozenge \varphi$. Then there is a state $t \subseteq s$ such that $t$ supports $\varphi$. Since $\left\| \varphi \right\|$ is downward closed, we can take any $v \in t$ and it holds that $\{v\}$ supports $\varphi$ and thus $\varphi$ is classically true at $v$. As a result, $s$ supports $\lozenge \varphi$.

• (ii) In general, it holds that $\blacksquare \varphi \vDash \square \varphi$. Suppose that $\left\| \varphi \right\|$ is closed under arbitrary unions and $s$ is a state that supports $\square \varphi$. Then, for all $v \in s$, $\{v\}$ supports $\varphi$. Since $\left\| \varphi \right\|$ is closed under arbitrary unions, for any state $t \subseteq s$, $t$ supports $\varphi$. As a result, $s$ supports $\blacksquare \varphi$.

It was stated in Proposition 2 that every $\left\{ \sim \right\}$-free formula expresses a downward closed proposition, so, as a result of Proposition 7, $\lozenge \varphi \equiv \blacklozenge \varphi$ for any such formula $\varphi$. Moreover, it can be verified by induction that any $\left\{ \sim , \vee \right\}$-free formula $\varphi$ expresses a proposition which is closed under arbitrary unions, and that entails $\square \varphi \equiv \blacksquare \varphi$.

(i) and (iii) of Proposition 5 might suggest that $\square$ and $\lozenge$ are $S5$-like modal operators. However, that would be a misunderstanding. The difference can be illustrated with the following remark: In $S5$ it holds that $\square \lozenge \varphi \equiv \lozenge \varphi$. This is not the case in our semantics where it holds that $\square \lozenge \varphi \equiv \square \varphi$ (because in the scope of $\square$ everything behaves classically).

In the presence of $\square$, the operator $\rightarrow$ could remind strict implication. For any $\left\{ \sim , \vee \right\}$-free formulas $\varphi , \psi$, we have the standard relationships: (1) $\varphi \rightarrow \psi \equiv \square (\varphi \supset \psi )$ where ‘$\supset$’ is the material implication defined as $\varphi \supset \psi =_{Df} \mathord {\sim }(\varphi \wedge \mathord {\sim }\psi )$, and, as a consequence, (2) $\mathord {\sim }(\varphi \rightarrow \psi ) \equiv \lozenge (\varphi \wedge \mathord {\sim }\psi )$ (as was required when we discussed the problem of denying conditional sentences). However, inquisitive implication differs from standard strict implications significantly. An untypical feature of the implication is expressed by the following equivalence, which holds for all $\varphi$ and $\psi$ from $L^{\mathord {\sim }}$:

• $\square (\varphi \rightarrow \psi ) \equiv \square \varphi \rightarrow \square \psi$.

Notice that unlike the other modal operators, the operator $\square$ is clearly expressible in the original framework of inquisitive semantics (i.e. in the language $L$). In fact, it is used very often by inquisitive semanticists and plays an important role in the theory. It is called the declarative operator and is usually denoted by the exclamation mark ‘!’ (see e.g., Ciardelli et al. 2012, p. 18).

We will define one more disjunction-like connective, $\oplus$, which will turn out to be very useful for our purposes. $\oplus$ is a flexible arity operator and by assertion of a sentence of the form $\varphi _{1} \oplus \cdots \oplus \varphi _{n}$ it is roughly said that every disjunct is true in at least one possible world and, at the same time, in every possible world at least one disjunct is true. So all the disjuncts are open possibilities which together cover the whole state. $\oplus$ is defined as follows:

• $\varphi _{1} \oplus \cdots \oplus \varphi _{n} =_{Df} \square (\varphi _{1} \vee \cdots \vee \varphi _{n}) \wedge (\lozenge \varphi _{1} \wedge \cdots \wedge \lozenge \varphi _{n})$.

The dual of $\oplus$ is $\otimes$ defined as

• $\varphi _{1} \otimes \cdots \otimes \varphi _{n} =_{Df} \lozenge (\varphi _{1} \wedge \cdots \wedge \varphi _{n}) \vee (\square \varphi _{1} \vee \cdots \vee \square \varphi _{n})$.

The following proposition describes some interactions between the introduced operators.

Proposition 8

Let $\varphi _{1}, \ldots , \varphi _{n}$ be some arbitrary formulas from $L^{\mathord {\sim }}$. Then

• (i) $\lozenge \varphi _{1} \wedge \cdots \wedge \lozenge \varphi _{n} \equiv \blacklozenge (\varphi _{1} \oplus \cdots \oplus \varphi _{n})$,

• (ii) $\square \varphi _{1} \wedge \cdots \wedge \square \varphi _{n} \equiv \blacksquare (\varphi _{1} \oplus \cdots \oplus \varphi _{n})$,

• (iii) $\lozenge \varphi _{1} \vee \cdots \vee \lozenge \varphi _{n} \equiv \blacklozenge (\varphi _{1} \otimes \cdots \otimes \varphi _{n})$,

• (iv) $\square \varphi _{1} \vee \cdots \vee \square \varphi _{n} \equiv \blacksquare (\varphi _{1} \otimes \cdots \otimes \varphi _{n})$.

Proof

We will prove only the first claim, which will play an important role in the rest of this paper. First, suppose that a state $s$ supports $\lozenge \varphi _{1} \wedge \cdots \wedge \lozenge \varphi _{n}$. Then, according to Proposition 5 (iii), there are possible worlds $v_{1}, \ldots , v_{n} \in s$ such that for all $i$ ($1\le i \le n$) $\varphi _{i}$ is (classically) true at $v_{i}$. Then, $\varphi _{1} \oplus \cdots \oplus \varphi _{n}$ is supported by $\left\{ v_{1},\ldots , v_{n} \right\}$. It follows from Proposition 5 (iv) that $s$ supports $\blacklozenge (\varphi _{1} \oplus \cdots \oplus \varphi _{n})$.

Suppose that a state $s$ supports the formula $\blacklozenge (\varphi _{1} \oplus \cdots \oplus \varphi _{n})$. Then, there is a substate $t$ (of $s$) that supports $\varphi _{1} \oplus \cdots \oplus \varphi _{n}$. Therefore, $t$ supports also $\lozenge \varphi _{1} \wedge \cdots \wedge \lozenge \varphi _{n}$. As a consequence, $s$ supports $\lozenge \varphi _{1} \wedge \cdots \wedge \lozenge \varphi _{n}$ as well.

A connective that corresponds to our $\oplus$ plays an important role in the field of coalgebraic logic, where it is called a ‘nabla operator’ (see e.g., Bílková et al. 2008). This operator was also used for example in Aloni (2007) to capture the modal force of imperatives. It is suitable for modeling such phenomena as free choice effects with disjunction under deontic modals and similar effects with epistemic modalities. The following two examples, which illustrate these phenomena, are borrowed from (Zimmermann 2000):

• (A) Mr. X may take a bus or a taxi. It follows that Mr. X may take a bus and also that he may take a taxi.

• (B) Mr. X might be in Victoria or in Brixton. It follows that Mr. X might be in Victoria and also that he might be in Brixton.

Notice that the interaction of ‘or’ with the modalities in (A) and (B) is in accordance with how $\oplus$ interacts with $\blacklozenge$ in our semantics. It follows from Propositions 7 (i) and 8 (i) that for any $\left\{ \sim \right\}$-free formulas $\varphi$ and $\psi$,

• $\blacklozenge (\varphi \oplus \psi ) \equiv \blacklozenge \varphi \wedge \blacklozenge \psi$.

This also corresponds very well with the analysis of modal/or interaction in Simons (2005) where the concept of supercover is used. A set $X$ is a supercover of a set $Y$ iff every member of $X$ contains some member of $Y$ and every member of $Y$ belongs to some member of $X$. In Simons (2005) the following truth condition is proposed for sentences of the form May[A or B]:

• May[A or B] is true iff $\{\left| \text {A}\right| , \left| \text {B}\right| \}$ is a supercover of some subset of the set of all accessible worlds (where $\left| \text {A}\right|$ denotes the set of A-worlds, i.e. worlds where A is true, and similarly with $\left| \text {B}\right|$).

The correspondence with our approach is obvious. Let $\left| \varphi \right|$ denote the set of possible worlds at which $\varphi$ is classically true. Then it holds that

• $s \vDash \varphi _{1} \oplus \cdots \oplus \varphi _{n}$ iff $\{\left| \varphi _{1}\right| , \ldots , \left| \varphi _{n}\right| \}$ is a supercover of $s$.

As a consequence,

• $s \vDash \blacklozenge (\varphi \oplus \psi )$ iff $\{\left| \varphi \right| , \left| \psi \right| \}$ is a supercover of some subset of $s$.

The main difference between this condition and that of Simons (2005) is that the semantics we are working with is not based on truth conditions but on the relation of support. A serious objection to the formalization of ‘or’ with the operator $\oplus$ is that the operator integrates into semantics some essentially pragmatic features of disjunction. In particular, it can be argued that if a speaker utters a disjunctive sentence A or B, it is not a part of what is said that A and B are possible (even though this is usually pragmatically implied). The reason is that A or B does not seem to be incompatible with not-A even though there is a sense in which maybe A is incompatible with not-A.

Whether or not the disjunctive interpretation of $\oplus$ is acceptable, this connective is important for our purposes since, with its help, we will be able in the following section to construct a relatively elegant system of natural deduction which is complete with respect to inquisitive semantics with weak negation.

In Sect. 5, the operator $\oplus$ will enable us to describe completely states by formulas: We will see that if we restrict ourself to a finite set of atomic formulas $At$, then for every state $s$ (whose valuations are functions from $At$ to the set of truth values), there is a formula $\varPhi _{s}$ which is supported by the state $s$ but not by any other state. This fact has one important consequence. As was already mentioned in the introduction, in the original inquisitive semantics propositions are modeled as nonempty downward closed sets of states. Since persistence does not hold generally in our extension of the system, we have to admit propositions that are not downward closed. The natural question arises whether there remains a weaker restrictive property. The possibility to describe any state leads to a negative answer. Each set of states represents a proposition and if the set of atoms is finite, every proposition can be expressed by a formula. If $\{s_{1}, \ldots , s_{n}\}$ is a proposition, then it is expressed by the formula $\varPhi _{s_{1}} \vee \cdots \vee \varPhi _{s_{n}}$.

Let us briefly discuss in this connection another important issue. In inquisitive semantics there is a very specific idea about how a proposition $P$ expressed by a sentence $A$ is connected to the effects of uttering $A$. The proposition $P$ is viewed as a set of states (i.e. a set of sets of possible worlds). The utterance of $A$ provides the information that the actual world is located somewhere in the union of $P$ and by this it excludes from the common ground all those possible worlds which are not contained in the union. Besides that, if the proposition is inquisitive,⁷ a request is expressed in the utterance to locate the actual world more precisely by establishing a state that supports $A$. As we already mentioned in the introduction, a consequence of this interpretation is that propositions should be closed under substates.

This general idea cannot be applied when weak negation is added to the framework because this operator generates non-persistent propositions. Standard inquisitive semantics works with the Stalnaker’s view that an essential feature of learning new information is that it results in elimination of some possibilities. It seems that this view does not have a general validity because sentences informing us about the existence of some possibilities (typically ‘might’-sentences) do not have this eliminative effect. An analogous complication is faced for example in section 4 of Groenendijk et al. (1996) where the authors wrote:

In many cases, a sentence of the form might-$\phi$ will have the effect that one becomes aware of the possibility of $\phi$. The present framework is one in which ...growth of information about the world is explicated in terms of elimination of possibilities. Becoming aware of a possibility can not be accounted for in a natural fashion in such an eliminative approach ...⁸

[E]pistemic modal statements such as might-$\phi$ are not primarily meant as providing information about the world as such; they rather provide information about the information of the speaker. If a speaker utters might-$\phi$ the hearer may infer, on the assumption that the speaker’s utterance is correct, that his information is consistent with $\phi$.

It is evident that we need an account that is not world-eliminative to understand the effect of uttering a sentence that expresses a non-persistent proposition. Admittedly, this difficult issue is not satisfactorily settled in the present paper and has to be further pursued in future research.

4 System of Natural Deduction

The main task of this paper is to find a deductive apparatus that is appropriate for inquisitive semantics enriched with weak negation. In this section an adequate Fitch-style system of natural deduction will be introduced.

It is clear from the semantics of weak negation that this connective could also be called classical negation. The problem of integrating classical negation into the framework of inquisitive semantics is in some respects similar to the task of combining intuitionistic and classical connectives. The reason is that inquisitive semantics is intimately connected with Kripke semantics for intuitionistic logic as was mentioned in Sect. 2.

A framework which integrated intuitionistic and classical first-order logic in one system was introduced in Lucio (2000). The author constructed for this purpose a structured sequent calculus which differs significantly in its nature from the deductive apparatus which will be introduced in this section. On the level of propositional logic, intuitionistic and classical connectives were also, for example, combined in Humberstone (1979) and Fariñas and Herzig (1996). These papers are closer to our approach. In both cases, the authors constructed a formal system in which some rules or axioms had to be restricted to a syntactically defined class of formulas that had the property of being persistent in the corresponding semantics. Even though the calculi from Humberstone (1979) and Fariñas and Herzig (1996) differ in many respects from our natural deduction system, this is an important common feature: Some class of persistent formulas is defined, and these formulas function in a specific way in the formal system. In our case, these formulas will be called safe and will play a special role in conditional proofs.

Notice that we need a system in which conditional proof is not a generally valid rule of inference. For instance, $\lozenge \lnot p, p \vDash \bot$ but $\lozenge \lnot p \nvDash p \rightarrow \bot$, i.e. $\lozenge \lnot p \nvDash \lnot p$. That corresponds very well with natural language. For example, there is a clear sense in which the set of the following two sentences

• The husband might not be the murderer.

  The husband is the murderer.

is not consistent. If someone asserted the conjunction of these two sentences, she would obviously contradict herself. However, from the claim that the husband might not be the murderer it does not follow that the husband is not the murderer.

Nevertheless, a restricted version of conditional proof is sound and will be included in the system of natural deduction as a basic rule. For this reason, we will use two kinds of brackets (square brackets and round brackets) to express provability under hypotheses.

By square brackets we indicate that in a subordinate proof all formulas from its outer proof can be used. For example, by ‘$[\mathord {\sim }\varphi : \bot ]/\varphi$’ we mean the standard rule of indirect proof: $\varphi$ can be proved by a derivation of a contradiction from the hypothetical assumption $\mathord {\sim }\varphi$. In the scope of the hypothetical assumption, everything can be used that was available before the assumption was made.⁹

When we use the round brackets, this possibility is restricted. Round brackets indicate that in a subproof we can use only so called safe formulas occurring in its outer proof. The set of safe formulas is defined as the set containing (1) all formulas of the language $L$ and (2) all formulas from $L^{\mathord {\sim }}$ that are of the form $\varphi \rightarrow \psi$. Notice that all safe formulas are persistent with respect to substates.

This restriction is applied only to conditional proof and the restricted version of this rule is denoted as ‘$(\varphi :\psi )/\varphi \rightarrow \psi$’. In a sequent calculus, this rule would correspond to the rule

• $\underline{\varDelta ^{s} \cup \{\varphi \} \Rightarrow \psi }$

• $\varDelta \Rightarrow \varphi \rightarrow \psi$

where $\varDelta ^{s}$ is the set of safe formulas from $\varDelta$. The restriction could be illustrated also in the following way. Suppose that there is a derivation of the following shape:

Suppose that $\chi$ is not safe. Then such a derivation is in accordance with the rule $(\varphi :\psi )/\varphi \rightarrow \psi$ only if the occurrence of $\chi$ in step 3 is not used in the derivation of $\psi$ form $\varphi$ in steps 6–8.

The impact of the restriction will be illustrated on a concrete example below after the formulation of the system.

The system of natural deduction consists of two groups of rules. The first group of rules is a standard system for classical propositional logic where, however, the conditional proof is restricted as described above:

$$\begin{aligned} \begin{array}{llll} (\wedge I) &{} \quad \varphi ,\psi /\varphi \wedge \psi &{} (\wedge E) &{} \quad \mathrm{(i)} \varphi \wedge \psi / \varphi , \mathrm{(ii)} \varphi \wedge \psi / \psi \\ (\vee I) &{} \quad \mathrm{(i)} \varphi / \varphi \vee \psi , \mathrm{(ii)} \psi / \varphi \vee \psi &{} (\vee E) &{} \quad \varphi \vee \psi , [\varphi :\chi ], [\psi :\chi ] / \chi \\ (\rightarrow I)^{*} &{} \quad (\varphi :\psi )/\varphi \rightarrow \psi &{} (\rightarrow E) &{} \quad \varphi , \varphi \rightarrow \psi / \psi \\ (\bot I) &{} \quad \varphi , \mathord {\sim }\varphi / \bot &{} ( IP ) &{} \quad [\mathord {\sim }\varphi : \bot ]/\varphi \end{array} \end{aligned}$$

We also assume the rule of repetition as a part of the system: A formula which occurs earlier in a proof can be repeated at any later stage, provided its earlier occurrence did not depend on any hypothetical assumption which is not being made at the later place.

The restriction applied to the conditional proof is partly balanced by four rules from the second group which concern the defined symbols. The first rule (R1) is restricted to atomic formulas:

$$\begin{aligned} \begin{array}{ll} (\hbox {R}1) &{}\quad \square p / p \\ (\hbox {R}2) &{}\quad / \square (\varphi \vee \lnot \varphi ), \\ (\hbox {R}3) &{}\quad \square \varphi \wedge \square \psi / \square (\varphi \wedge \psi )\\ (\hbox {R}4) &{}\quad \lozenge \varphi _{1} \wedge \cdots \wedge \lozenge \varphi _{n}/\blacklozenge (\varphi _{1} \oplus \cdots \oplus \varphi _{n}). \end{array} \end{aligned}$$

$\varphi _{1}, \ldots , \varphi _{n} \vdash \psi$ will stand for the claim that in the system, there is a proof of the formula $\psi$ from the set of premises (formulas) $\varphi _{1}, \ldots , \varphi _{n}$.

Since we have the strong version of indirect proof $( IP )$, the weak version denoted as $[\varphi : \bot ]/ \mathord {\sim }\varphi$ is a derivable rule as the following derivation shows. It is an important application of the fact that double negation $\mathord {\sim }\mathord {\sim }$ can be always eliminated.

¹⁰ We will denote the rule $[\varphi : \bot ]/ \mathord {\sim }\varphi$ as (WIP). Whenever the rule (WIP) will be used in the following text, we will know that its occurrence could be eliminated by replacing the derivation of $\bot$ from the assumption $\varphi$ with the above more complex derivation.

Now we will provide the promised example illustrating the effect of the restriction of conditional proof. The following derivation is an unsuccessful attempt to derive $p$ from $\mathord {\sim }(p \rightarrow q)$:

The problem is in step 7. We cannot use the rule $(\rightarrow I)^{*}$ since the formula $\mathord {\sim } p$, which was used in step 5, is not safe.

The natural deduction system will be used heavily in “Appendices 1 and 2” which can serve also as an illustration of how the whole system works.

5 Completeness Proof

In this section, it will be proved that the system of natural deduction introduced in the previous section is sound and complete with respect to inquisitive semantics with weak negation.

First, we will discuss the soundness of the rules. As regards the first group, the rules that do not use hypothetical assumptions [i.e. $(\wedge I),\,(\wedge E),\,(\vee I),\,(\rightarrow E)$, and $(\bot I)$] are unproblematic. They all are support preserving. As regards the rules $( IP ),\,(\vee E)$, and $(\rightarrow I)^{*}$, it should be stressed that the two kinds of brackets represent two kinds of hypothetical assumptions which differ from the semantic point of view. Suppose that a state $s$ is given. Informally speaking, by making the hypothetical assumption in the conditional proof we are moving from $s$ to an arbitrary substate. Using indirect proof and proof by cases, we do not change the given state. We are just exploring what would be the case if the assumption was supported by $s$. Now the difference will be explained more precisely.

Consider the rule $( IP )$. Let $s$ be an arbitrary state which supports some set of formulas $\varDelta$. We would like to show that the state $s$ also supports the formula $\psi$. We could do that indirectly by assuming that $s$ does not support $\psi$ and showing that this leads to a contradiction. If the contradiction is derivable with the help of sound rules from the set $\varDelta \cup \{\mathord {\sim }\psi \}$, then $s$ has to support $\psi$. For this reason, the rule $( IP )$ is sound.

As regards the rule $(\vee E)$, let $s$ be an arbitrary state which supports some set of formulas $\varDelta \cup \{\varphi \vee \psi \}$. If a formula $\chi$ is derivable (with the help of sound rules) from $\varDelta \cup \{\varphi \}$ as well as from $\varDelta \cup \{\psi \}$, then $\chi$ has to be supported by $s$ since $s$ supports everything from $\varDelta \cup \{\varphi \}$ or everything from $\varDelta \cup \{\psi \}$. Hence the rule $(\vee E)$ is sound.

Consider the rule $(\rightarrow I)^{*}$. Suppose that a state $s$ supporting some set of formulas $\varDelta$ is given and we would like to show that $s$ also supports the formula $\varphi \rightarrow \psi$. We could do this by taking an arbitrary substate $t$ and showing that if $t$ supports $\varphi$, then it supports $\psi$. In general, the state $t$ does not support all formulas supported by $s$. However, $t$ supports all such formulas that are persistent with respect to substates. In particular, $t$ supports all safe formulas supported by $s$. As a result, if we can derive $\psi$ from $\varphi$ together with some safe formulas from $\varDelta$ (using only sound rules), then $s$ has to support $\varphi \rightarrow \psi$. This is soundness of $(\rightarrow I)^{*}$.

As regards the rules from the second group, the soundness of (R1)–(R3) follows directly from Proposition 5 (i) and of (R4) from 8 (i).

Lemma 1

Let $\varphi , \psi$ be any formulas and $p$ any atomic formula. Then

• (i) If $\varphi \vdash \lnot p$ then $\lozenge \varphi \vdash \mathord {\sim }p$,

• (ii) $\mathord {\sim }\blacklozenge \varphi \vdash \lnot \lozenge \varphi$,

• (iii) $\square \varphi \vdash \lozenge \varphi$,

• (iv) $\vdash \lozenge \varphi \vee \lnot \lozenge \varphi$,

• (v) $\lozenge (\varphi \vee \psi ) \vdash \lozenge \varphi \vee \lozenge \psi$,

• (vi) $\square (\varphi \vee \psi ), \lnot \lozenge \psi \vdash \square \varphi$,

• (vii) $\varphi _{1} \oplus \cdots \oplus \varphi _{n}, \varphi _{1} \rightarrow p, \ldots , \varphi _{n} \rightarrow p \vdash p$.

Proof

See “Appendix 1”.

We say that $\psi _{1}\wedge \cdots \wedge \psi _{n}$ is a variation of $\varphi _{1}, \ldots , \varphi _{n}$ if for every $i$ ($1\le i \le n$), $\psi _{i}$ is either $\varphi _{i}$ or $\lnot \varphi _{i}$. We define the formula $\varGamma (\varphi _{1},\ldots , \varphi _{n})$ as the disjunction of all variations of the formulas $\varphi _{1}, \ldots , \varphi _{n}$.¹¹ For example,

• $\varGamma (p,q)=(p \wedge q) \vee (p \wedge \lnot q) \vee (\lnot p \wedge q) \vee (\lnot p \wedge \lnot q)$.

Lemma 2

Let $\varphi _{1}, \ldots , \varphi _{n}$ be arbitrary formulas. Then

• (i) $\vdash \square \varGamma (\varphi _{1}, \ldots , \varphi _{n})$,

• (ii) $\vdash \varGamma (\lozenge \varphi _{1}, \ldots , \lozenge \varphi _{n})$,

Proof

• (i) Due to the rules (R2) and $(\wedge I)$, $\square (\varphi _{1} \vee \lnot \varphi _{1}) \wedge \cdots \wedge \square (\varphi _{n} \vee \lnot \varphi _{n})$ is provable. Using the rule (R3) we get $\square ((\varphi _{1} \vee \lnot \varphi _{1}) \wedge \cdots \wedge (\varphi _{n} \vee \lnot \varphi _{n}))$ which is provably equivalent with $\square \varGamma (\varphi _{1}, \ldots , \varphi _{n})$ since distributive laws are derivable in the system.

• (ii) Due to Lemma 1 (iv), the formula $(\lozenge \varphi _{1} \vee \lnot \lozenge \varphi _{1}) \wedge \cdots \wedge (\lozenge \varphi _{n} \vee \lnot \lozenge \varphi _{n})$ is provable. Using this fact and distributive laws we can prove $\varGamma (\lozenge \varphi _{1}, \ldots , \lozenge \varphi _{n})$.

Let $At$ be a finite set of atoms. Variations of these atoms are called (world) descriptions, and they correspond to valuations of atoms from $At$. If we work only with formulas which contain no other atoms than those from $At$, we can suppose that states contain also only such restricted valuations. Such restricted states will be called states on $At$. Let $s$ be a state on $At$ which consists of valuations $v_{1}, \ldots , v_{n}$. Let $\sigma _{1}, \ldots , \sigma _{n}$ be the corresponding descriptions. Then, we define the formula $\varPhi _{s}$ as $\sigma _{1} \oplus \cdots \oplus \sigma _{n}$. This formula is a syntactic correlate of the state $s$.

$s$ can be syntactically represented also as follows:

• $\varPsi _{s}= \lozenge \sigma _{1} \wedge \cdots \wedge \lozenge \sigma _{n} \wedge \lnot \lozenge \sigma _{n+1} \wedge \cdots \wedge \lnot \lozenge \sigma _{n+m}$,

where $\sigma _{n+1}, \ldots , \sigma _{n+m}$ are all the remaining descriptions relative to $At$. $\varPsi _{\bot }$ will denote the formula $\lnot \lozenge \sigma _{1} \wedge \cdots \wedge \lnot \lozenge \sigma _{n+m}$.

These notions will be illustrated with the set $At=\left\{ p,q\right\}$ and state $s=\left\{ v_{1}, v_{2}\right\}$, where $v_{1}(p)=T,\,v_{1}(q)=F$, $v_{2}(p)=F$ and $v_{2}(q)=F$. Then

• $\sigma _{1}= p \wedge \lnot q$, $\sigma _{2}= \lnot p \wedge \lnot q$, $\sigma _{3}=p \wedge q$, $\sigma _{4}= \lnot p \wedge q$,

• $\varPhi _{s}= \sigma _{1} \oplus \sigma _{2}=\lozenge \sigma _{1} \wedge \lozenge \sigma _{2} \wedge \square (\sigma _{1} \vee \sigma _{2})$,

• $\varPsi _{s}= \lozenge \sigma _{1} \wedge \lozenge \sigma _{2} \wedge \lnot \lozenge \sigma _{3} \wedge \lnot \lozenge \sigma _{4}$,

• $\varPsi _{\bot }= \lnot \lozenge \sigma _{1} \wedge \lnot \lozenge \sigma _{2} \wedge \lnot \lozenge \sigma _{3} \wedge \lnot \lozenge \sigma _{4}$.

In the following text, $\varphi \dashv \vdash \psi$ means that $\varphi \vdash \psi$ and $\psi \vdash \varphi$.

Lemma 3

Let $s$ be a state based on a finite set of atoms. Then

• (i) $\vdash \mathord {\sim } \varPsi _{\bot }$,

• (ii) $\varPhi _{s} \dashv \vdash \varPsi _{s}$.

Proof

• (i) Let $\sigma _{1}, \ldots , \sigma _{r}$ be all the descriptions relative to a set of atoms $\left\{ p_{1},\ldots ,p_{k} \right\}$. Due to Lemma 2 (i) we have $\vdash \square \varGamma (p_{1},\ldots ,p_{k})$. Applying Lemma 1 (iii) we obtain $\vdash \lozenge \varGamma (p_{1},\ldots ,p_{k})$ which means that the formula $\lozenge (\sigma _{1} \vee \cdots \vee \sigma _{r})$ is provable. It follows from Lemma 1 (v) that $\lozenge \sigma _{1} \vee \cdots \vee \lozenge \sigma _{r}$ is provable as well. As a consequence, $\vdash \mathord {\sim } \varPsi _{\bot }$.

• (ii) Suppose a set of atoms $\left\{ p_{1},\ldots ,p_{k} \right\}$ is fixed. Relative to this set, let $\sigma _{1}, \ldots ,$ $\sigma _{n}, \sigma _{n+1}, \ldots \sigma _{n+m}$ be all the descriptions such that $\sigma _{1}, \ldots , \sigma _{n}$ correspond to the possible worlds of a given state $s$. To show that $\varPhi _{s} \dashv \vdash \varPsi _{s}$ we have to prove that

  • $\square (\sigma _{1} \vee \cdots \vee \sigma _{n}) \dashv \vdash \lnot \lozenge \sigma _{n+1} \wedge \cdots \wedge \lnot \lozenge \sigma _{n+m}$.

First, we prove that for all $i$ ($1 \le i \le m$), $\square (\sigma _{1} \vee \cdots \vee \sigma _{n}) \vdash \lnot \lozenge \sigma _{n+i}$:

Second, according to Lemma 2 (i) we have $\vdash \square \varGamma (p_{1},\ldots , p_{k})$, i.e. $\vdash \square (\sigma _{1} \vee \cdots \vee \sigma _{n} \vee \sigma _{n+1} \vee \cdots \vee \sigma _{n+m})$. Then, we can $m$-times apply Lemma 1 (vi), and infer $\square (\sigma _{1} \vee \cdots \vee \sigma _{n})$ from $\lnot \lozenge \sigma _{n+1} \wedge \cdots \wedge \lnot \lozenge \sigma _{n+m}$.

We say that a set $\varDelta$ of formulas is consistent iff $\varDelta \nvdash \bot$.

Lemma 4

Let $\varDelta$ be a set of formulas which contains only atoms from a finite set $At$. If $\varDelta$ is consistent, then there is a state $s$ such that $\varDelta \cup \left\{ \varPhi _{s}\right\}$ is consistent.

Proof

Let $\varDelta$ be a set of formulas which contains only atoms from a finite set $At$. Suppose that $\sigma _{1},\ldots , \sigma _{m}$ is the set of all descriptions and $s_{1},\ldots ,s_{n}$ are all the states (relative to $At$). Due to Lemma 2 (ii) we have $\vdash \varGamma (\lozenge \sigma _{1}, \ldots , \lozenge \sigma _{m})$. It means that $\varPsi _{s_{1}} \vee \cdots \vee \varPsi _{s_{n}} \vee \varPsi _{\bot }$ is provable. Using Lemma 3 (i), we obtain $\vdash \varPsi _{s_{1}} \vee \cdots \vee \varPsi _{s_{n}}$. Then, using Lemma 3 (ii), it follows that $\vdash \varPhi _{s_{1}} \vee \cdots \vee \varPhi _{s_{n}}$. This means that if all $\varDelta \cup \left\{ \varPhi _{s_{i}}\right\}$ were inconsistent, then $\varDelta$ would be inconsistent as well. Since $\varDelta$ is consistent, there is a state $s$ such that $\varDelta \cup \left\{ \varPhi _{s}\right\}$ is consistent.

Lemma 5

Let $s$ be a state on a finite set of atoms $At$. Then, for every formula $\varphi$ based on $At$, either $\varPhi _{s} \vdash \varphi$ or $\varPhi _{s} \vdash \mathord {\sim }\varphi$.

Proof

We will proceed by induction on the complexity of $\varphi$. Suppose that $\varPhi _{s}=\sigma _{1} \oplus \cdots \oplus \sigma _{n}$. For the induction basis, consider an arbitrary atom $p \in At$. We will distinguish two cases:

First, suppose that for all $i$ ($1\le i\le n$), $p$ occurs in $\sigma _{i}$ in the positive form (i.e. without the negation $\lnot$). Then for all such $i$, $\vdash \sigma _{i} \rightarrow p$ and it follows from Lemma 1 (vii) that $\varPhi _{s} \vdash p$.

Second, suppose that for some $i$ ($1\le i\le n$), $p$ occurs in $\sigma _{i}$ in the negative form (i.e. with the negation $\lnot$). Then $\sigma _{i} \vdash \lnot p$ and according to Lemma 1 (i) $\lozenge \sigma _{i} \vdash \mathord {\sim }p$. As a consequence $\varPhi _{s} \vdash \mathord {\sim }p$.

The induction hypothesis says that our claim holds for every state $s$ (on $At$) for some arbitrary formulas $\varphi$ and $\psi$. We have to prove that then the claim holds also for $\mathord {\sim }\varphi , \varphi \wedge \psi , \varphi \vee \psi$, and $\varphi \rightarrow \psi$. The cases of negation, conjunction and disjunction are straightforward. We will concentrate on the most complicated case of implication.

Assume that $\varPsi _{s}=\lozenge \sigma _{1} \wedge \cdots \wedge \lozenge \sigma _{n} \wedge \lnot \lozenge \sigma _{n+1} \wedge \cdots \wedge \lnot \lozenge \sigma _{n+m}$. Let us start with the positive case. Suppose that there is no substate $t$ of the state $s$, such that $\varPhi _{t} \vdash \varphi$ and $\varPhi _{t} \vdash \mathord {\sim }\psi$. Let $t$ be an arbitrary substate of $s$. Then $\varPsi _{t}$ can be obtained from $\varPsi _{s}$ by substituting a variation of the formulas $\lozenge \sigma _{1}, \ldots , \lozenge \sigma _{n}$ for the initial segment $\lozenge \sigma _{1} \wedge \cdots \wedge \lozenge \sigma _{n}$. The only exception is the use of the variation $\chi _{0}=\lnot \lozenge \sigma _{1} \wedge \cdots \wedge \lnot \lozenge \sigma _{n}$. In that case, the result of the substitution is not a formula representing a substate but $\varPsi _{\bot }$. Let $\chi _{1}, \ldots , \chi _{k}$ be all the remaining variations and $s_{1},\ldots , s_{k}$ the corresponding substates of $s$. So, for every $i$ ($1 \le i \le k$), $\chi _{i}\wedge \lnot \lozenge \sigma _{n+1} \wedge \cdots \wedge \lnot \lozenge \sigma _{n+m}=\varPsi _{S_{i}}$.

Since $\varPhi _{s_{i}} \dashv \vdash \varPsi _{s_{i}}$ [according to Lemma 3 (ii)], our induction hypothesis leads to the statement that there are only three possible cases:

• (a) $\varPsi _{s_{i}} \vdash \varphi$ and $\varPsi _{s_{i}} \vdash \psi$.

• (b) $\varPsi _{s_{i}} \vdash \mathord {\sim }\varphi$ and $\varPsi _{s_{i}} \vdash \psi$.

• (c) $\varPsi _{s_{i}} \vdash \mathord {\sim }\varphi$ and $\varPsi _{s_{i}} \vdash \mathord {\sim }\psi$.

It follows in each of these cases that $\varPsi _{s_{i}}, \varphi \vdash \psi$. So, the following derivation can be constructed.

It remains to consider the negative case for implication. Assume that there is a substate $t$ of the state $s$ such that $\varPhi _{t} \vdash \varphi$ and $\varPhi _{t} \vdash \mathord {\sim }\psi$. The following derivation proves what we need.

Now we are prepared to formulate and prove the main result of this paper which holds for any formulas $\varphi _{1}, \ldots , \varphi _{n}, \psi$ from the language $L^{\sim }$.

Theorem 1

$\varphi _{1}, \ldots , \varphi _{n} \vdash \psi$ iff $\varphi _{1}, \ldots , \varphi _{n} \vDash \psi$.

Proof

The implication from left to right requires the verification of soundness of all rules. That was discussed at the beginning of this section. We will prove the implication from right to left. Suppose that $\varphi _{1}, \ldots , \varphi _{n} \nvdash \psi$. Then $\{\varphi _{1}, \ldots , \varphi _{n}, \mathord {\sim }\psi \}$ is consistent. From Lemma 4 it follows that there is a state $s$ such that $\{\varphi _{1}, \ldots , \varphi _{n}, \mathord {\sim }\psi , \varPhi _{s} \}$ is consistent. As a consequence of Lemma 5, every formula from $\{\varphi _{1}, \ldots , \varphi _{n}, \mathord {\sim }\psi \}$ is provable from $\varPhi _{s}$. Since it holds that $s \vDash \varPhi _{s}$, every formula from $\{\varphi _{1}, \ldots , \varphi _{n} \}$ is supported by $s$ but $\psi$ is not supported by $s$. Therefore $\varphi _{1}, \ldots , \varphi _{n} \nvDash \psi$.

It is a trivial semantic observation that for any $\varphi _{1}, \ldots , \varphi _{n}, \psi$ from the language $L$ it holds that $\psi$ follows from $\varphi _{1}, \ldots , \varphi _{n}$ in the original inquisitive semantics iff $\psi$ follows from $\varphi _{1}, \ldots , \varphi _{n}$ in inquisitive semantics with weak negation. In this sense, it can be said that inquisitive logic with weak negation is a conservative extension of standard inquisitive logic.

Inquisitive logic was axiomatized by a Hilbert-style axiomatic system in Ciardelli (2009) and Ciardelli and Roelofsen (2009, (2011). The system is formulated for the language $L$ and consists of modus ponens, axioms of intuitionistic logic, Kreisel–Putnam schema (KP) and double negation law restricted to atomic formulas (DN). Thus the system enriches intuitionistic logic by the following two schemata where $\varphi , \psi , \chi$ range over the formulas from $L$ and $p$ over atomic formulas¹²:

• (KP) $(\lnot \varphi \rightarrow (\psi \vee \chi )) \rightarrow ((\lnot \varphi \rightarrow \psi ) \vee (\lnot \varphi \rightarrow \chi ))$,

• (DN) $\lnot \lnot p \rightarrow p$.

Let $\vdash _{InqL}$ denote the derivability relation of this system. The system is sound and complete with respect to inquisitive semantics. Using this fact, the following proposition is a consequence of Theorem 1 and the above semantic observation. It holds for any $\varphi _{1}, \ldots , \varphi _{n}, \psi$ from the language $L$.

Proposition 9

$\varphi _{1}, \ldots , \varphi _{n} \vdash _{InqL} \psi$ iff $\varphi _{1}, \ldots , \varphi _{n} \vdash \psi$.

In this sense the derivability relation of our natural deduction system is conservative with respect to the derivability relation $\vdash _{InqL}$. However, the relation between the two calculi is not straightforward. (DN) corresponds to the rule (R1), but to show that (KP) is derivable in our system is not an easy task. In “Appendix 2”, we will provide a proof of this fact which is independent of any semantic considerations. This proof can serve also as an example of a non-trivial use of the rule (R4).

6 Conclusion

To conclude, let us summarize the main points of this article. We added weak negation to the basic language of inquisitive semantics and showed that such extension of the language has some serious consequences. Even though we lose some important general features of the original framework (most importantly persistence with respect to substates), we are able to model new linguistic phenomena (weak denial, modal assertions) in a natural way. As a result, we obtained a nonstandard modal logic where the modalities are defined in terms of other symbols. The main result of this paper was a syntactic characterization of this logic.

The plan for future work is to explore the first-order extension of the framework. The semantics presented in this paper can be extended to the level of first order logic in a very straightforward way.¹³ States can be modeled as pairs $\left\langle U, W \right\rangle$, where $U$ is a nonempty set of objects (the universe of discourse) and $W$ is a nonempty set of possible worlds understood as structures of first order predicate logic whose domain is $U$. A state $t=\left\langle U', W' \right\rangle$ is a substate of a state $s=\left\langle U, W \right\rangle$ iff $U'=U$ and $W' \subseteq W$. The relation of support $\vDash _{e}$ (relative to an evaluation of variables $e$) between states and formulas of first-order predicate logic can be introduced in the following way¹⁴:

• $s \nvDash _{e} \bot$,

• $s \vDash _{e} P(t_{1}, \ldots , t_{n})$ iff for all $v \in s$, $\left\langle ve(t_{1}),\ldots , ve(t_{n}) \right\rangle \in v(P)$,

• $s \vDash _{e} \mathord {\sim }\varphi$ iff $s \nvDash _{e} \varphi$,

• $s \vDash _{e} \varphi \vee \psi$ iff $s \vDash _{e} \varphi$ or $s \vDash _{e} \psi$,

• $s \vDash _{e} \varphi \wedge \psi$ iff $s \vDash _{e} \varphi$ and $s \vDash _{e} \psi$,

• $s \vDash _{e} \varphi \rightarrow \psi$ iff for any substate $t$ of $s$, if $t \vDash _{e} \varphi$ then $t \Vdash _{e} \psi$,

• $s \vDash _{e} \forall x \varphi$ iff for all $a \in U$, $s \vDash _{e_{x:a}} \varphi$,

• $s \vDash _{e} \exists x \varphi$ iff for some $a \in U$, $s \vDash _{e_{x:a}} \varphi$.

In this semantics, a quantifier version of the operator $\oplus$ might play an important role. Let us define this quantifier and its dual in the following way¹⁵:

• $\nabla x \varphi =_{Df} \forall x \lozenge \varphi \wedge \square \exists x \varphi$,

• $\Delta x \varphi =_{Df} \exists x \square \varphi \vee \lozenge \forall x \varphi$.

For these quantifiers, equivalences analogous to those expressed in proposition 8, seem to be crucial:

• $\forall x \lozenge \varphi \equiv \blacklozenge \nabla x \varphi$,

• $\forall x \square \varphi \equiv \blacksquare \nabla x \varphi$,

• $\exists x \lozenge \varphi \equiv \blacklozenge \Delta x \varphi$,

• $\exists x \square \varphi \equiv \blacksquare \Delta x \varphi$.

So far no calculus proposed for standard first-order inquisitive semantics has been proved to be complete. It can be therefore expected that also the task to find a syntactic characterization of its extension with weak negation is difficult.

Appendices

Appendix 1

We will prove all the statements of Lemma 1. (i) If $\varphi \vdash \lnot p$ then $\lozenge \varphi \vdash \mathord {\sim }p$.¹⁶

(ii) $\mathord {\sim }\blacklozenge \varphi \vdash \lnot \lozenge \varphi$.

(iii) $\square \varphi \vdash \lozenge \varphi$.

(iv) $\vdash \lozenge \varphi \vee \lnot \lozenge \varphi$.

(v) $\lozenge (\varphi \vee \psi ) \vdash \lozenge \varphi \vee \lozenge \psi$.

(vi) $\square (\varphi \vee \psi ), \lnot \lozenge \psi \vdash \square \varphi$.

(vii) $\varphi _{1} \oplus \cdots \oplus \varphi _{n}, \varphi _{1} \rightarrow p, \ldots , \varphi _{n} \rightarrow p \vdash p$. Notice that here is the only place in the completeness proof where the rule (R1) is used.

Appendix 2

We will provide a proof that Kreisel–Putnam schema (KP) restricted to the language $L$ is derivable in our system. This result can be easily obtained by semantic considerations using Theorem 1. Here, we will give a purely syntactic proof of this fact.

In the following text, $\varphi , \psi , \chi$ (possibly indexed) will range over all formulas from $L$ and $\alpha , \beta , \gamma$ (possibly indexed) only over disjunction-free formulas from $L$.

Lemma 6

For any $\alpha , \varphi _{1},\ldots ,\varphi _{n}, \varphi , \psi$:

• (i) $\square \alpha \vdash \alpha$,

• (ii) $\square \lnot \varphi \vdash \lnot \varphi$,

• (iii) $\mathord {\sim }(\varphi _{1} \vee \cdots \vee \varphi _{i} \vee \cdots \vee \varphi _{n}) \vdash \mathord {\sim }\varphi _{i}$,

• (iv) $\mathord {\sim }(\lnot \varphi \rightarrow \alpha ) \vdash \lozenge (\lnot \varphi \wedge \lnot \alpha )$,

• (v) $\varphi , \lozenge \lnot \varphi \vdash \bot$,

• (vi) $\square (\varphi \wedge \psi ) \vdash \square \varphi$,

• (vii) $\lozenge (\varphi \wedge \psi ) \vdash \lozenge \varphi$,

• (viii) if $\varphi \vdash \psi$ then $\blacklozenge \varphi \vdash \blacklozenge \psi$.

Proof

(i) Induction on the complexity of $\alpha$. For atomic formulas, the claim holds due to the rule (R1). For $\bot$ there is the following derivation:

Suppose that the claim holds for some $\beta$ and $\gamma$. We will prove that then it holds also for $\beta \wedge \gamma$ and $\beta \rightarrow \gamma$.

(ii) The following derivation can be constructed:

(iii) The following derivation can be constructed:

(iv) The following derivation can be constructed:

(v) The following derivation can be constructed:

(vi) The following derivation can be constructed:

(vii) The following derivation can be constructed:

(viii) Suppose that $\varphi \vdash \psi$.

The following lemma shows that a restricted version of (KP) schema is derivable in the natural deduction system. Let us remind that $\alpha _{1},\ldots ,\alpha _{n}$ range over disjunction-free formulas from $L$.

Lemma 7

$\vdash (\lnot \varphi \rightarrow (\alpha _{1} \vee \cdots \vee \alpha _{n})) \rightarrow ((\lnot \varphi \rightarrow \alpha _{1}) \vee \cdots \vee (\lnot \varphi \rightarrow \alpha _{n}))$.

Proof

The following derivation can be constructed:

The following lemma shows that every formula from $L$ is provably equivalent with some disjunction of disjunction-free formulas from $L$. An analogous result (concerning, however, different calculi) was exploited also in Punčochář (2009, (2012, (2014).

Lemma 8

For any $\varphi$ there are some $\alpha _{1}, \ldots , \alpha _{n}$ such that $\varphi \dashv$ $\vdash \alpha _{1} \vee \cdots \vee \alpha _{n}$.

Proof

This can be proved by induction on the complexity of the formula $\varphi$. We will show only the inductive step for implication which is most difficult and in which Lemma 7 is used. Suppose that

• (a) $\psi \dashv$ $\vdash \beta _{1} \vee \cdots \vee \beta _{k}$ ($k \ge 1$),

• (b) $\chi \dashv$ $\vdash \gamma _{1} \vee \cdots \vee \gamma _{l}$ ($l \ge 1$).

Then the following formulas are provably equivalent:

• 1. $\psi \rightarrow \chi$,

• 2. $(\beta _{1} \vee \cdots \vee \beta _{k}) \rightarrow (\gamma _{1} \vee \cdots \vee \gamma _{l})$,

• 3. $\bigwedge ^{k}_{i=1}(\beta _{i} \rightarrow (\gamma _{1} \vee \cdots \vee \gamma _{l}))$,

• 4. $\bigwedge ^{k}_{i=1}(\lnot \lnot \beta _{i} \rightarrow (\gamma _{1} \vee \cdots \vee \gamma _{l}))$,

• 5. $\bigwedge ^{k}_{i=1}((\lnot \lnot \beta _{i} \rightarrow \gamma _{1}) \vee \cdots \vee (\lnot \lnot \beta _{i} \rightarrow \gamma _{l}))$,

• 6. $\bigvee ^{l}_{i_{1}=1} \ldots \bigvee ^{l}_{i_{k}=1}((\lnot \lnot \beta _{1} \rightarrow \gamma _{i_{1}}) \wedge \ldots \wedge (\lnot \lnot \beta _{k} \rightarrow \gamma _{i_{k}}))$.

The equivalence of 1. and 2. follows from the induction hypotheses (a) and (b). 3. can be easily derived from 2. with the help of the rules $(\wedge I)$, $(\vee I)$, $(\rightarrow$ $E)$, and $(\rightarrow$ $I)^{*}$. 2. can be derived from 3. using the rules $(\wedge E)$, $(\vee E)$, $(\rightarrow$ $E)$, and $(\rightarrow$ $I)^{*}$. The equivalence between 3. and 4. is a consequence of Lemma 6 (i). The derivation of 5. from 4. is an application of Lemma 7 and in the derivation from 5. to 4. it suffices to use the rules $(\vee E)$, $(\vee I)$, $(\rightarrow$ $E)$, and $(\rightarrow$ $I)^{*}$. The equivalence of 5. and 6. can be established with the help of the derivable distributive laws.

Theorem 2 is a consequence of Lemmas 7 and 8. Let us stress once again that in this theorem $\varphi ,\,\psi$ and $\chi$ range over formulas from $L$.

Theorem 2

$\vdash (\lnot \varphi \rightarrow (\psi \vee \chi )) \rightarrow ((\lnot \varphi \rightarrow \psi ) \vee (\lnot \varphi \rightarrow \chi ))$.