Supplement to Dialogical Logic
Some Dialogical Systems for Non-Classical Logics
As we suggested in the introduction of the main entry, dialogical logic is best viewed as a conceptual framework in which logical systems can be studied, compared and combined. In this supplement, we wish to illustrate this point further. We cover some forms of paraconsistent and free logic, a combination of both, and then a specifically dialogical reading of connexive logic.
See the entry on Paraconsistent Logic for a general overview of the field. Paraconsistent dialogues have been introduced in Rahman & Carnielli , Rahman  and Rahman & van Bendegem .
The idea behind any paraconsistent logic is that one should distinguish between inconsistencies (classically unsatisfiable formulae), and triviality (the logical validity of an arbitrary formula). Both are connected in standard logic via the well known inference pattern Ex Contradictione Quodlibet (ECQ). A logical system is called explosive when the derivation of an inconsistency in it yields triviality. Paraconsistency in a system is usually implemented by giving semantic means to distinguish between explosive contradictions (contradictions proper) and non explosive ones (inconsistencies).
In the dialogical framework, this idea is implemented on the basis of the following observation. Assuming that argumentation takes place in a paraconsistent environment, one cannot assume in general that a negative literal (i.e. a negated atom) can be attacked by its positive counterpart (i.e. the same atom without the negation). Indeed, such an argumentation form relies on the (classical) intuition that one cannot assert in the same argument a literal in its positive and negative versions. Of course, this does not mean that there is no contradiction. The fact that a literal is a term of a contradiction depends on O's choice: by attacking a negative literal ¬α with its positive counterpart α, O implicitly concedes that (α∧¬α) is explosive.
Let us describe a dialogue system for Sette's paraconsistent logic P1. We will need a syntactic adjustment of our language. Following Gentzen, we'll read negation ¬A as A→⊥. But here, we will enrich our vocabulary with a specific absurdum for every formula. Thus an inconsistency will yield its own local absurdity, without trivializing the whole system. Let ⊥A denote the absurdity generated from a formula A. So the negation of A is written A→⊥A. Let us call this a Gentzen-style relativized negation.
A dialogical system for propositional logic (either classical or intuitionistic) with negation in the relativized Gentzen-style form can be restricted to a paraconsistent one equivalent to P1 by adding the following rule:
SR-9: Formal Use of Elementary Absurdities.
For any atomic formula α, P may use the corresponding elementary absurdity ⊥α iff O introduced it in a previous move.
See the (forthcoming) entry on Free Logic for a general overview of the field. Free dialogues have been developed in Rahman .
Free logic is the fruit of a reflection on the existential import of the quantifiers. This aspect of the theory of quantification has been notoriously rich in philosophical controversies. Following Bencivenga , we will define free logic as a “formal system of quantification theory [… ] which allows for some singular terms in some circumstances to be thought of as denoting no existing object, and in which a given set of quantifiers is thought of as having an existential import.” The dialogical approach on this stems from the following idea: in the course of an argumentation, it may be the case that an individual constant is introduced “for the sake of argument” by a player who is not prepared to assume the existential commitment that is classically attached to such a move. Typically, one may want to argue that Pegasus is a winged horse without being committed to defend the idea that there is such a thing as a winged horse. Notice that the choice of an instantiation for the interpretation of bound variables is an official move in the dialogical game, i.e. it belongs to the object language of dialogues. This feature is quite specific of dialogical logic, and provides for an immediate connection between classical and free logic : extending the formal restriction rule of classical dialogues to such moves will yield a free logic.
Definition: Constant Introduction.
An individual constant c is said to be introduced by X when X has chosen c in order to defend (resp. attack) an existential (resp. universal) quantifier, and c has never been chosen before.
SR-10: Formal Use of Constants.
Only O is allowed to introduce a constant.
The set of rules of a dialogue system for either classical or intuitionistic first-order logic, supplemented with SR-10, yields a free logic, i.e. a logic where it is not assumed that every individual constant denotes an object. This idea can be generalized in the following way: suppose one wants to distinguish an arbitrary number n of domains d1,...,dn in the ontology his logic is talking about. It is then possible to replace in the vocabulary of first-order logic the usual quantifiers with n pairs of di-quantifiers (for i=1 to n), meant to correspond to each domain of the ontology. Then one defines for any domain di that a constant has been introduced as a di-constant iff it has been chosen to attack (resp. defend) a universal (resp. existential) di-quantifier. Then of course a di-constant is assumed to denote an object from the domain di, and only such a constant can be used to attack or defend a di quantifier. This proviso is added to the definition of the particle rules for di-quantifiers. The SR-10 rule is the same, and holds for any kind of constant.
Rahman  proposes a philosophically motivated combination of intuitionistic, free and paraconsistent logic, called Frege's Nightmare. The main idea is threefold:
- when what is at stake in a dialogue is a formula where singular terms were not explicitly conceded by the opponent, there is no reason to assume that those terms refer, hence no conclusive reason either that Excluded Middle should hold for any statement regarding them (thus the logic is intuitionistic in general);
- in a formal dialogue, when a singular term has been introduced by the Opponent, this term can be assumed to refer and Excluded Middle should hold with respect to the atom where the term occurs (thus the logic is locally classical);
- singular terms introduced by the Proponent may be considered fictional. There is no overwhelming argument to the effect that fiction must behave consistently (thus Non Contradiction fails to hold in general, and the logic is paraconsistent).
See the entry on Connexive Logic for a different account of this topic. Connexive dialogues were introduced in Rahman & Rückert .
Connexive dialogues stem from the desire to investigate a strange property of Aristotelian logic. It seems that in some passages (e.g. Prior Analytics 57b3), Aristotle considers that such statements expressing propositions of the form A→¬A or ¬A→A are contradictory. Obviously, such propositions are not classical contradictions, nor can they be added to classical logic as axioms without trivializing it. The challenge is thus to find a logic which validates ¬(A→¬A) and ¬(¬A→A).
One way to understand the problem is to revise the semantics of implication, in order to eliminate the trivial cases, namely cases where the antecedent cannot be true, or the consequent cannot be false. Under this reading, a connexive claim that A→B must be understood as a triple claim: (i) A→B holds classically; (ii) A is not unsatisfiable and (iii) B is not valid. Besides the elimination of “Aristotelian” contradictions, part of the motivation of connexive logic is that classical entailment cannot discriminate between the trivially true conditionals and those which express some determinate kind of meaning connection linking the if-part to the then-part. One way to achieve this is to introduce in the object language two operators (V and F) in order to express the constraint that the antecedent of a connexive implication must be verifiable, and the consequent must be falsifiable (i.e. not valid). In dialogical terms, these concepts amount to the following:
(i) to claim that some formula is verifiable is to claim that one can conceive a situation in which the formula is true. Now recall that in a dialogue, the formal restriction SR-5 says in substance that only what is asserted by O can be assumed to be true, and therefore that O is the builder of the model. So to challenge such a claim, a player opens a subdialogue where he commits himself to defend the negation of the formula while playing under formal restriction, i.e. to defend that the formula is a contradiction.
(ii) dually, to claim that some formula is falsifiable is to claim that there is a conceivable situation where this formula is false. The challenger of such a claim is thus committed to defend that the formula is valid. Again, this amounts, for the challenger, to accepting the burden of the formal restriction in a subdialogue where he will defend the (validity of the) formula.
Let us give the particle rules for the V and F operators:
(in a subdialogue where the challenger plays under formal restriction)
(in a subdialogue where the challenger plays under formal restriction)
The particle rules for V and F operators make use of a notion of subdialogue which is akin to its modal counterpart. Hence the states of the connexive game will look like the modal ones, but supplemented with an assignment of formal restriction. Such states are tuples of the form S=〈ρ,σ,Φ,λ〉, where ρ and σ are as usual, Φ is a connexive formula, and λ is an assignment of dialogical contexts.
Let S1 = 〈ρ,σ,ρ−1(!)-VA,λ〉. S2 is accessible from S1 iff
where λA/ν denotes the result of extending λ by assigning context ν to the formula A. S2 is reached after an attack ρ−1(?)-V. ν is a dialogical context chosen by ρ−1(!), where ρ−1(?) plays under formal restriction.
Let S1 = 〈ρ,σ,ρ−1(!)-FA ,λ〉. S2 is accessible from S1 iff
S2 = 〈ρ,σ,ρ−1(!)-¬A,λA/ν〉
where λA/ν denotes the result of extending λ by assigning context ν to the formula A. S2 is reached after an attack ρ−1(?)-F. ν is a dialogical context chosen by ρ−1(!), where ρ−1(?) plays under formal restriction.
Subdialogues are labelled parts of a dialogue, determined by the player who opened them, and labelled to order them. The labelling introduces a tree-based order identical to that used in modal logic.
The connexive If-Then is denoted by ⇒ to avoid confusion. With respect to states of the game, the particle rules of ⇒ are the obvious ones: from S1 = 〈ρ,σ,ρ−1(!)-A⇒B ,λ〉, any of these three states is reachable:
S2 = 〈ρ,σ,ρ−1(!)-VA,λ〉
following an attack ?-V of ρ−1(?).
S3 = 〈ρ,σ,ρ−1(!)-FB,λ〉
following an attack ?-F of ρ−1(?).
S4 = 〈ρ',σ,ρ'-1(!)-A,λ〉
which is a standard attack against a classical conditional A→B. Notice though that the classical conditional does not belong to the syntax of connexive dialogical logic. From S4 (up to the choice of ρ−1(!)) the game may proceed according to the relevant particle rule for A, or with the usual defense of the conditional (ρ−1(!) defends B). Of course, such a reading of the connexive implication ⇒ requires the presence of V and F, but we do not allow these operators to occur freely in the formulas of the language: their role is (in this system) purely ancillary.
S5 = 〈ρ,σ,ρ−1(!)-B,λ〉.
Two structural rules need amendment:
SR-13: Connexive Formal Rule.
At the start of the dialogue for A it is P who plays under formal restriction. If X plays under formal restriction in a given section (subdialogue) he cannot use an atomic formula if Y did not utter this formula first in the same section. Dually, Y can introduce a new atomic formula in the given section any time he wants, according to the other rules. The only changes in this distribution of the formal rule are those regulated by V and F.
SR-14: Connexive Subdialogue Relations.
In a given subdialogue, X may choose as a target of his attacks any (complex) Y-formula of this section (in so far as the other rules allow it). X may also choose conditionals (Y-A⇒B) of the corresponding upper section, provided he attacks with the classical X-A. No other type of attack is allowed.
A dialogue system with the rules for propositional classical logic, where the formal rule SR-5 has been replaced by SR-13 and augmented with SR-14, will validate the desired connexive formulae such as ¬(A⇒¬A) or ¬(¬A⇒A).
It should be noted that if one requires for a (connexive) implication to hold, that its antecedent should not be contradictory and its consequent tautological, then one looses Uniform Substitution of arbitrary formulas for propositional letters.