Negation in the Logic of First Degree Entailment and Tonk

Abstract

The dialogical framework is an approach to meaning that provides an alternative to both the model-theoretical and the proof-theoretical semantics. The dialogical approach to logic is not a logic but a semantic rule-based framework where different logics could be developed, combined or compared. But are there any constraints? Can we introduce rules ad libitum to define whatever logical constant? In the present paper I will explore the first conceptual moves towards the notion of Dialogical Harmony. In order to highlight these specific features of the dialogical approach to meaning I will discuss the dialogical analysis of tonk, some tonk-like operators and the negation of the logic of first-degree entailment.

Appendices

Appendix 12.1 Note on Symmetric and Asymmetric Versions of the E-Rule

In the standard literature on dialogues, there is an asymmetric version of the intuitionistic rule, called E-rule since Felscher [4]. It’s formulation is the following:

• O may react only upon the immediately preceding move of P.

This produces an asymmetry: P can challenge whatever formula but O can not.

In fact these devices yield intuitionistic logic if we add that only the most recent challenge (that has not been yet responded) can be defended.

In general to introduce the E-rule could be seen as jeopardizing the (for the dialogical approach crucial distinction) between the play and the strategic level. The rule has mainly a strategic motivation. According to my view the idea of ranks deployed in the text is more adequate. Indeed, the choice of the appropriate rank number to obtain validity is part of the strategic level. In fact if the ranks have been set such that Opponent has rank 1 and the Proponent rank two and the intuitionistic structural rule is in force, then the Proponent has a winning strategy for a propositional formula iff this formula it is valid in intuitionistic propositional logic. Now, to say that the Proponent has rank 2 is and Opponent rank 1 is very close to say that the Opponent can only react upon the immediately preceding.

According to this idea Rahman [20] proposed the following analysis of the role of the E-Rule in intuitionistic logic:

• (1) The asymmetric E-Rule is based on strategic considerations, namely, the different roles in a strategy of the P- and the O-utterances.

• (2) The symmetric E-Rule is based on meaning considerations, namely the specific local and global meaning of the conditional (and the negation as a special case), that allows locally to switch the roles of challenger and defender and might trigger globally defence delays.

• (3) The asymmetric E-Rule yields a system of strategies that corresponds to Gentzen’s Calculus of 1935, the symmetric E-rule is closer to Beth tableaux. Indeed, the tableaux corresponding to Gentzen [6] do not allow two formulae to occur at the right side (do not allow that two P-formulae occur at the same time in the same branch). Beth tableaux are more permissive.

• (4) The asymmetric E-Rule allows straightforward proofs of some meta-mathematical properties of intuitionistic logic such as the interpolation theorem and the disjunctive property. For the latter see the following point.

• (5) In Rahman’s PHD it is shown how to prove the disjunctive property of intuitionistic logic with the asymmetric E-Rule. In his paper Why Dialogical Logic? [31] Rückert presents the argument with some detail. The point is that if we consider the distinction between the play and the strategic level then the proof of the disjunctive property can be carried out in the same way with symmetric or asymmetric rules (see Appendix 12.2). A more detailed presentation of the arguments involved have been published before by Rahman and Rückert in [24].

Appendix 12.2 The Disjunctive Property and the Symmetric Rule for Intuitionistic Logic

The presentation of the proof given below stems essentially from Rückert [31]. The point was raised in Rahman [20] and discussed at length in Rahman and Rückert [24]. Similar has been pointed out by Rahman [20] in relation to the existential property of intuitionistic logic—the argument works analogously.

The disjunctive property of intuitionistic logic says that $\upalpha\,\vee\,\upbeta$ is valid iff α is valid or β is valid:

$$\models \upalpha \vee \upbeta \models \upalpha \ \mathrm{or} \ \models \upbeta$$

• The proof from the right to the left is unproblematic. If P has a formal winning strategy for α or for β, it is evident that he has a winning strategy for $\upalpha \vee \upbeta$:

P starts the dialogue by stating the thesis $\upalpha \vee \upbeta$, and O attacks it with “?”. In order to win P then just has to choose the disjunct he has a winning strategy for. If he has a winning strategy for α (or β) he has to choose α (or β respectively) to answer O’s attack.

• On the level of plays the notion of meaning underlying intuitionistic logic is captured by the socalled intuitionistic structural rule that we called above the asymmetric E-Rule:

In any move, each player may attack a (complex) formula asserted by his partner

or he may defend himself against the last attack that has not yet been answered.

• The crucial point of this rule with regard to the present argumentation is that P is not allowed to defend himself against an attack of O he has already answered, unless O renews his attack.

In our example this means that P is not allowed to defend himself again with β (or α) against the attack “?” on $\upalpha \vee \upbeta$ if he has already defended himself with α (or β respectively).

Now we go to the level of strategies and recall the definition of validity in the dialogical approach: A formula is valid iff P has a formal winning strategy for it.

Thus, from the left to the right the meta-theorem of the disjunctive property says, that if P has a winning strategy for $\upalpha \vee \upbeta$ he also has a winning strategy for at least one of the two disjuncts. And to have a winning strategy means for P that he is able to win the dialogue no matter how O plays.

If we look at the beginning of a dialogue with the thesis $\upalpha \vee \upbeta$, it is clear that the first move of O has to be the attack “?” and that P has to reply α (or β) in the second move. Now, the dialogue continues with an argumentation about α (or β respectively) alone, if O does not renew his attack on $\upalpha \vee \upbeta$. Consequently, if P has a winning strategy for $\upalpha \vee \upbeta$, he must also have a winning strategy for at least one of the two disjuncts alone (independently of the hope that O might renew his challenge).

Quod erat demonstrandum.

Appendix 12.3 Examples

In the following examples, the outer columns indicate the numerical label of the move, the inner columns state the number of a move targeted by an attack. Expressions are not listed following the order of the moves, but writing the defence on the same line as the corresponding attack, thus showing when a round is closed. Recall, from the particle rules, that the sign “—” signalises that there is no defence against the attack on a negation.

For the sake of a simpler notation we will not record in the dialogue the rank choices but assume the uniform rank O: n=1 P: m=2:

Example 1:

Classical and intuitionistic rules

In the following dialogue played with classical structural rules P’ move 4 answers O’s challenge in move 1, since P, according to the classical rule, is allowed to defend (once more) himself from the challenge in move 1. P states his defence in move 4 though, actually O did not repeat his challenge—we signalise this fact by inscribing the not repeated challenge between square brackets.

In the dialogue displayed below about the same thesis as before, O wins according to the intuitionistic structural rules because, after the challenger’s last attack in move 3, the intuitionist structural rule forbids P to defend himself (once more) from the challenge in move 1.

Example 2:

FDE^L-rules

Ex. 3:

FDE^L-rules

Ex. 4:

FDE^L-rules

Appendix 12.4 Soundness and Completeness of Hintikka-Trees* for Enquiry Games in Relation to M. Dunn’s Relational Semantics for FDE

The following proofs are standard and there is no claim of originality here beside the remark that Hintikka trees* describe FDE. In fact the proofs are a variation of Dunn’s prove [3] in relation to Jeffrey’s coupled trees.²⁹

12.4.1 Soundness

The main job is done by the following definition 1 the rest is mechanical

Definition 1 (DS1):

Let us consider a set S of signed formulae such as T $\upalpha \wedge \upbeta$, $_{i.n}\textbf{F} \upalpha \vee \upbeta$, occurring in a branch b. We say that S is faithful in the relational model M defined by means of the relation R described before if there is a mapping f such that:

• (a) If Tα is in S, then the mapping yields αR1 in M

• (b) If Fα is in S, then the mapping is such that it is not the case that αR1 is in M (that is, α might be related either to 0 or to neither but not with 1)

  • We say that a branch of a tree is faithful if the set of signed formulae on it is faithful in some model.

  • We say that a tree is faithful if some branch of it is faithful

Soundness Lemma 1 (SL1):

A closed tree is not faithful.

Proof:

• Suppose that we have a tree closed and faithful.

• Since it is faithful, some branch of it is. Let S be the set of formulae on that branch and let it be faithful in the model M by means of the mapping f.

• Since the tree is closed then for some atomic formula α we must have Tα and Fα. But then αR1 must be in M but this is impossible since the mapping of Fα will prevent this to happen.

Soundness Lemma 2 (SL2):

If (a section of) a tree is faithful and a branch of that (section of the) tree is extended by tree-rules, the result is another faithful (section of) a tree.

(Obviously this assumes that the formula that triggers the extension is not atomic).

Proof:

Let ${\mathcal T}$ be a faithful tree and let b be the branch that is extended.

The proof requires several steps. We begin with two main steps:

• By hypothesis at least one branch is faithful, now this branch could be b or could be B*.

• (I) if the faithful branch is B* the extension of b will leave B* unchanged, thus after the particle rule has been applied to b, ${\mathcal T}$ will still be faithful (because B* is).

• (II) if the faithful branch is b and it faithful in the model M the proof is by cases.

That is, by the consideration of all the ways to extend the branch b by the application of the corresponding tree-rule to a labelled and signed formula at the end of that branch. Namely by the application of a T-signed conditional-rule and a F-signed conditional rule etc.

Let us work with $\textbf{F}(\upalpha \wedge \upbeta)$. Since the model is faithful to the branch, it is not the case that $(\upalpha \wedge \upbeta)$ R1 is in M.

Hence, either it is not the case that αR1 or it is not the case that βR1. Thus, at least one of the branches will be faithful and hence the extended tree will be faithful too.

Soundness Theorem:

If there is Hintikka-tree-proof of α, α is valid in the relational semantics for FDE.

Proof:

Assume that there is tree-proof of α, but α is not valid. We show that from this a contradiction follows.

Since there is a (Hintikka-)tree-proof of α there is a closed tree ${\mathcal T}$ that starts with Fα. Thus, the first section of ${\mathcal T}$ is ${\mathcal T}_{0}$ that consists in the thesis Fα. The following sections of ${\mathcal T}$ are constructed by extending ${\mathcal T}_{0}$.

Since α is not valid, there is some model M at which α is not true. Let assume this model and an adequate mapping such that {Fα} is faithful to M. Thus ${\mathcal T}_{0}$ is faithful, since the set of formulae on its only branch is faithful.

Since ${\mathcal T}_{0}$ is faithful by lemma SL2 so is any tree ${\mathcal T}$ we get that starts with ${\mathcal T}_{0}$ and results by extending ${\mathcal T}_{0}$.

It follows that ${\mathcal T}$ is faithful.

${\mathcal T}_{0}$ is closed by hypothesis, and this is impossible by SL1.

12.4.2 Completeness of Hintikka-Trees* for Enquiry Games in Relation to M. Dunn’s Relational Semantics for FDE Worked Out Trees

Let us say that a Hintikka-tree* (for enquiry games) has been worked out if all appropriate tree-rule applications have been made.

What we need is a systematic method for constructing a tree that ensures that if we start a tree for a given formula, we can always produce a worked out a tree. There are many options available the following, as we will discuss below. Now, systematic worked out trees do not contribute to no insight it is only a mechanical procedure:

• 1. First stage: thesis

• 2. Any other stage:

  • 2.1 pick up the leftmost open branch

  • 2.2 pick up a formula that is neither an atomic formula and do the following going from top to bottom:

    • 2.2.1 If it is a formula of the form $\textbf{F}-{\sim}\upvarphi$, simply apply the appropriate rule to it. In such a way that the resulting subformula will be added to the end of each open branch on which this negation occurs only if it does not occur there before. Similar for $\textbf{T}-{\sim}\upvarphi$,

    • 2.2.2 If the formula is a T-conjunction or a F-disjunction add both of the corresponding subformulae to the end of each open branch on which the conjunction/disjunction occurs only if it does not occur there before. Similar for a F-conditional

    • 2.2.3 If the formula is a T-conjunction or a F-disjunction split the end of each open branch on which the conjunction/disjunction occurs and add the corresponding subformulae only if it does not occur there before. Similar for a T-conditional

  (Tick any formula that has been subject of the application of a rule)

After all this has been done, do the same for the second from the left and so on.

Comments

• Notice that systematic trees avoid repetitions. In fact it is a systematic formulation of the non-repetition rule.

Definition 1:

Construction of a relational model from a branch (CD1)):

Let us consider a systematically worked out (Hintikka-)tree* with the open branch b. We show how to construct a relational model M in which b is faithful for α atomic and occurring in b.

• 1. Tα iff αR1 in M

• 2. T∼α iff αR0 in M

Completeness Lemma (CL):

• THESIS:

For each formula Φ (atomic or not) on the open branch b of a given worked out tree we can determine a relational model M in the following way:

• (a) If Tα occurs in b, then αR1 is in M

• (b) If Fα occurs in b, then it is not the case that αR1 is in M (that is, α might relate to 0 or to neither but not to 1)

• (c) If T∼α occurs in b, then αR0 is in M

• (d) If F∼α occurs in b, then it is not the case that αR0 is in M (that is, α might relate to 1 or to neither but not to 0)

Proof:

By induction on the complexity of the formula Φ.

The property at stake in our case is the one described in the thesis

BASE CASE: Assume Φ is the atomic formula α

• (1) If Tα occurs on b, by CD1 we have αR1 in M as required by (a).

• (2) If Fα occurs on b, then, since the branch is open, Tα does not occur. Hence, by CD1, it is not the case we have αR1 in M as required by (b).

• (3) If T∼α occurs in b, by CD1 we have αR0 in M as required by (c).

• (4) If F∼α occurs in b, then, since the branch is open, T∼α does not occur. Hence, by CD1, it is not the case we have ∼αR1 in M, but then, by the relational semantics for the negation it is not the case that αR0 as required by (d).

• INDUCTION CLAUSE

Assume (induction hypothesis) that we know the result for formulae simpler than Φ.

Let us start with the case Φ is $\textbf{T}(\upalpha \wedge \upbeta)$. If $\textbf{T}(\upalpha \wedge \upbeta)$occurs on b, since the tree has been worked out, the following formulae occur on b, too:

$$\begin{aligned}& \textbf{T}\upalpha \\ &\textbf{T}\upbeta\end{aligned}$$

Since, these are simpler than Φ, by induction hypothesis we will have in M that:

$$\begin{aligned}& \upalpha\textsf{R}1 \textbf{\textit{M}}. \textrm{and} \\ & \upalpha\textsf{R}1\textbf{\textit{M}}.\end{aligned}$$

Thus, as required, in M we have

$$(\upalpha \wedge \upbeta)\textsf{R}1$$

Let us take $\textbf{F}(\upalpha \wedge \upbeta)$. If $\textbf{F}(\upalpha \wedge \upbeta)$ occurs on b, since the tree has been worked out, one of the following formulae occur on b, too:

$$\textbf{F}\upalpha \textrm{or} \textbf{F}\upbeta$$

Then by induction hypothesis, we have that

• it is not the case that αR1 or it is not the case that βR1 is in M. Thus, it is not the case that $(\upalpha \wedge \upbeta)$ R1 is in M.

Negated conjunction and disjunction are proven similarly.

Suppose that T∼α occurs on b. Since we know the case of for T∼α whenα is atomic, we have that, as required, αR0 is in M. Similarly for F∼α.

Suppose that T(F)∼∼α occurs on b. Then, T(F)α occurs on b. Hence by induction hypothesis, αR1 is (is not) in M.

Completeness Theorem:

• THESIS:

• If Φ is valid in a relational semantics, then there is a proof using rules of Hintikka’s trees for Enquiry games

We prove the contrapositive:

• If there no proof in the tree-system at stake, Φ is not valid.

If we start the proof with P Φ, and work out a systematic tree, it will not close (since by assumption of the contraposition there is no proof for P Φ,).

Let us pick up the open branch b of the tree. With help of the CD1 we can create a relational for which the thesis CL holds. In particular, if P Φ’ occurs on b, then it is not the case that Φ R1 is in M. But P Φ occurs on b, since it is the signed formula at root of the tree, so it is on every branch. Thus there is a models such that Φ does not relate to 1, so it is not valid in the relations semantics for FDE.

Quod erat demonstrandum