On Hypothetical Judgements and Leibniz’s Notion of Conditional Right

Rahman, Shahid

doi:10.1007/978-3-319-16021-4_7

Shahid Rahman⁵

Part of the book series: Logic, Argumentation & Reasoning ((LARI,volume 7))

1896 Accesses
6 Citations

Abstract

Sébastien Magnier provides a remarkable analysis of the notion of conditional right with the help of public announcement logic that he generalizes for the logical study of legal norms. Magnier’s main idea, motivated by the earlier exhaustive textual and systematic work of Matthias Armgardt and the subsequent studies carried out by Alexandre Thiercelin, involves Leibniz’s notion of certification, which plays a central role in the famous De conditionibus. Magnier proposes to render the notion of certification of A as there is public evidence for A. More generally, the meanings of “conditional right” and “conditional legal norm” are established by means of identifying a specific kind of dialogical interaction during a legal trial constituted by games of giving and asking for reasons. This yields a theory of meaning rooted in the practice itself of legal debates.

The main aim of this paper is to study the notion of conditional right by means of constructive type theory (CTT) which provides the means to develop a system of contentual inferences rather than of syntactic derivations. Moreover, in line with Armgardt, I will first study the general notion of dependence as triggered by hypotheticals and then the logical structure of dependence specific to conditional right. I will develop this idea in a dialogical framework where the distinction between play-object and strategy-object leads to the further distinction between two basic kinds of pieces of evidence and where meanings is constituted by the interaction of obligations and entitlements.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Chapter: USD 29.95; Price excludes VAT (USA)

eBook: USD 39.99; Price excludes VAT (USA)

Hardcover Book: USD 54.99; Price excludes VAT (USA)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

1.
In the present paper the term is used in the sense of Leibniz rather than in the sense in which it is generally understood in legal contexts nowadays.
2.
The work of Matthias Armgardt prompted and influenced a host of new research on the bearing of Leibniz’s approach to current studies in legal rationality.
3.
In fact, Thiercelin’s research was prompted by the work of Armgardt.
4.
In fact, Magnier [1, pp. 151–157; 261–292] rejects other forms of implication interpretations too, including strict implication or connexive implication.
5.
This was suggested by Göran Sundholm in a personal email.
6.
The biconditional reading relates to the link between the condition and the conditioned. Leibniz calls this feature of the conditional right convertibility. It is not clear if, in Leibniz’s view, the biconditional reading only applies to conditional right.
7.
This seems to be rooted in actual legal practice: If the condition A is not satisfied, the benefactor is not entitled to B. The actuality of this feature of the Leibnizian approach to the notion of conditional right has been defended by modern-day scholars of Law theory such as Koch / Rüßmann [10, p. 47] and more thoroughly by Armgardt [2–4].
8.
Pol Boucher [11] provides a thorough discussion on the Roman sources of Leibniz’ own developments.
9.
See Vargas [13] for a thorough discussion on Leibniz’ view on the links between moral conditionals and hypotheticals of geometry and causal necessity.
10.
Cfr. Leibniz [8, VI, I, p. 375]. For a discussion on this issue see Thiercelin [7, p. 207].
11.
For a further discussion on the criticism of the biconditional rendering of the suspensive modality, see Magnier [1, pp. 155–156].
12.
Rahman and Rückert [16, 17] and Rahman and Redmond [18, pp. 20–57] provided a dialogical semantics for it based on the idea that this conditional is a particular kind of strict implication (defined in S4) where the head is satisfiable and the negation of the tail is also satisfiable. See also Pizzi and Williamson [19], Priest [20], and Wansing [21, 22].
13.
Note that, according to Rahman and Rückert´s semantics, although $ A\Rightarrow A $ is connexively valid, the implication $ \left(A\Rightarrow A\right)\Rightarrow \left(A\Rightarrow A\right) $ is not. For further non-classical features of their semantics (see [17, pp. 106–108; 120–121]).
14.
[φ]ψ is true at the evaluation world s iff φ is true at s implies that ψ is true at the reduced model $ \mathbf{M}\Big|\varphi $ – where the reduced model $ \mathbf{M}\Big|\varphi $ is the result of removing from M all the worlds where φ is false: $ \mathbf{M},s\mathrm{l}=\left[\varphi \right]\psi $ iff $ \mathbf{M},s\mathrm{l}=\varphi $ implies $ \mathbf{M}\Big|\varphi, s\mathrm{l}=\psi $ .
15.
In fact, this epistemic requirement for the fulfilment of the condition was already pointed out by _Thiercelin [6, p. 141]_. However, it was not incorporated in the logical analysis of the conditional before Magnier’s work_.
16.
The case of cancellation corresponds to that of PAL: since false announcements cannot be made, i.e. the system aborts. The first case, where a false announcement forces us back to the initial models, corresponds to the Total Public Announcement Logic (TPAL) of Steiner and Studer [23], where false announcements do not change the initial model at all. Indeed, if it is taken that it has been announced that A is true, then if we come to know that that A was not true after all, the original PAL process stops there since the model shrinks and there is no way of going back. However, one can imagine a system, such as TPAL, that allows us, once we come to know that A is not true, to go back to the model before it shrinks, since the grounds adduced for reducing it in the first place are no longer available. This might also relate to Armgardt’s recent work [24] on the defeasibility of the grounds adduced for the establishment of a fact (in our case the defeasibility of the grounds adduced for the fulfilment of condition).
17.
Recall that the falsity of the condition is different to producing a false announcement.
18.
For a thorough discussion on the criticism to the model-theoretical approach to meaning see Sundholm [25–29].
19.
See Appendix A.1.
20.
In Sect. 7.3, we will distinguish between play-objects and strategy-objects. While the latter correspond to proof-objects, pieces of evidence or evidence might be either play- or strategy-objects.
21.
This analysis was suggested by Göran Sundholm in a personal email.
22.
Recall that a judgement or assertion expresses that a proposition is true. The assertion A is true introduces an epistemic feature: it is known that A is the case. Furthermore, judgements can also involve sets: 1 is an element of the set of Natural numbers (in the CTT-notation: 1 : N).
23.
Cf. Granström [9, pp. 110–112]. In fact, chapter V of [9] contains a thorough discussion of the issue.
24.
Armgardt [2, p. 256] explores different kinds of interdependences between conditions discussed by Leibniz [8, A VI I, pp. 387–388], including temporally ordered conjunctions and subsidiary ones such as If it is known that the condition A cannot be fulfiled then the condition B should be fulfiled. Armgardt [1] makes ample use here, and in other parts of his book, of temporal indexes.
25.
This transition is known in CTT as definitional extension of hypotheses or contexts. For the formal details, see the presentation in Appendix AI.2.
26.
For the sake of clarity of exposition, I do not quantify over the function-dependent objects b(x). However, a full development of the definitions of statutory and conditional right should quantify universally over them.
27.
For the formation rules for functions, see Appendix A.1.
28.
For further details on the formation rules involved, see Appendix A.1.
29.
In fact, as pointed out by Armgardt in a personal email, we need the following parameters: Who grants What, Whom, When, and based on Which legal norm. I did not add all of the parameters to avoid a heavy notation. Let me mention that in the CTT-frame the introduction of temporal indexes in the object language is pretty straight-forward – see Ranta [31, pp. 101–124].
30.
See Appendix AII.4
31.
The formation play will not be developed here (see Appendix A.II).
32.
Repetition ranks establish how many times a player can defend or challenge the same move (see Appendix A.II). The notion of rank plays an important role in modelling the closing of trials – see 7.3.3 below.
33.
Cf. Ranta [31, p. 21], Nordström, Petersson and Smith [39, chapter 3.3], Primiero [34, p. 47–55] and Granström [9, p. 77–102].
34.
Ranta [31, p. 146] points out that in a series of lectures Per Martin-Löf showed how the growth of knowledge in experiments can be understood in this way: an unknown quantity is assigned a value, which may depend on other unknown quantities.
35.
For a more thorough presentation, see [41, 42].
36.
The main original papers are collected in [43]. For an historical overview see Lorenz [44]. For a presentation about the initial role of the framework as a foundation for intuitionistic logic, see Felscher [45]. Other papers have been collected more recently in Lorenz [46–48]. A detailed account of recent developments since Rahman [49], can be found in Rahman and Keiff [50], Keiff [51] and Rahman [52]. For the underlying metalogic see Clerbout [53, 54]. For textbook presentations: Kamlah and Lorenzen [55, 56], Lorenzen and Schwemmer [57], Redmond and Fontaine [58] and Rückert [40]. For the key role of dialogic in regaining the link between dialectics and logic, see Rahman and Keiff [59]. Keiff [60–62] and Rahman [63] study Modal Dialogical Logic. Fiutek et al. [64] study the dialogical approach to belief revision. Clerbout, Gorisse and Rahman [66] studied Jain Logic in the dialogical framework. Popek [67] develops a dialogical reconstruction of medieval obligationes. Rahman and Tulenheimo [68] study the links between GTS and Dialogical Logic. For other books see Redmond [69] – on fiction and dialogic – Fontaine [70] – on intentionality, fiction and dialogues – and Magnier [1] – on dynamic epistemic logic (van Ditmarsch et al. [71]) and legal reasoning in a dialogical framework.
37.
That player can be called Player 1, Myself or Proponent.
38.
Such a move could be written as ? _F∨1 : formation-request.
39.
It is an application of the original rule from CTT given in Ranta [31, p. 30].
40.
The example comes from Ranta [31, p. 31].
41.
This can be done because O has chosen 2 for her repetition rank.
42.
More precisely, conjunction and existential quantifier are two particular cases of the Σ operator (disjoint union of sets), whereas material implication and universal quantifier are two particular cases of the Π operator (indexed product on sets). See for example Ranta [31, chapter 2].
43.
Still, if we are playing with classical structural rules, there is a slight difference between material implication and universal quantification which we take from Ranta [31, Table 2.3], namely that in the second case p₂ always depends on p₁.
44.
As pointed out in Martin-Löf [38], subset separation is another case of the Σ operator. See in particular p. 53:
“Let A be a set and B(x) a proposition for x ε A. We want to define the set of all a ε A such that B(a) holds (which is usually written {x ε A : B(x)}). To have an element a ε A such that B(a) holds means to have an element a ε A together with a proof of B(a), namely an element b ε B(a). So the elements of the set of all elements of A satisfying B(x) are pairs (a; b) with b ε B(a), i.e. elements of (Σx ε A)B(x). Then the Σ-rules play the role of the comprehension axiom (or the separation principle in ZF).”
45.
The procedure is inspired by the presentation of strategic games in Rahman and Keiff [50], Sect. 2.4].
46.
As should be obvious form the context, '^∩ ' is a concatenation operator.

References

S. Magnier, Approche dialogique de la dynamique épistémique et de la condition juridique (College Publications, London, 2013)
Google Scholar
M. Armgardt, Das rechtlogische System der “Doctrina Conditionum” von Gottfried Wilhelm Leibniz. Computer im Recht, vol. 12 (Elvert-Verlag, Marburg, 2001)
Google Scholar
M. Armgardt, Zur Bedingungsdogmatik im klassischen römischen Recht und zu ihren Grundlagen in der stoischen Logik. Tijdschrift voor Rechtsgeschiedenis 76, 219–235 (2008)
Article Google Scholar
M. Armgardt, Zur Rückwirkung der Bedingung im klassischen römischen Recht und zum stoischen Determinismus. Tijdschrift voor Rechtsgeschiedenis 76, 341–349 (2010)
Article Google Scholar
A. Thiercelin, On two argumentative uses of the notion of uncertainty in Law in Leibniz’s juridical dissertations about conditions, in [15, pp. 251–266]
Google Scholar
A. Thiercelin, La Theorie Juridique Leibnizienne des Conditions. Ce que la logique fait au droit (ce que le droit fait à la logique). Ph.D.-Universite-Charles de Gaulle, Lille, 2009
Google Scholar
A. Thiercelin, Epistemic and practical aspects of conditionals in Leibniz’s legal theory of conditions, in Approaches to Legal Rationality, ed. by D. Gabbay, P. Canivez, S. Rahman, A. Thiercelin (LEUS-Springer, Dordrecht, 2010), pp. 203–216
Chapter Google Scholar
W.G. Leibniz, Sämtliche Schriften und Briefe. Edited by the Deutsche Akademie der Wissenschaften zu Berlin. Darmstadt, 1923 sqq., Leipzig, 1938 sqq., Berlin, 1950 sqq. Cited by Series (Reihe) and Volume (Band)
Google Scholar
J. Granström, Treatise on Intuitionistic Type Theory (Springer, Dordrecht, 2011)
Book Google Scholar
H.-J. Koch, H. Rüßmann, Juristische Begründungslehre (Beck, München, 1982)
Google Scholar
P. Boucher, Leibniz: What Kind of Legal Rationalism? in [15, pp. 231–49]
Google Scholar
H. Schepers, Leibniz’ Disputationen De Conditionibus: Ansätze zu einer juristischen Aussagenlogik. Studia Leibniziana, Supplementa 15, 1–17 (1975)
Google Scholar
E. Vargas, Contingent Propositions and Leibniz’s Analysis of Juridical Dispositions, in[15, pp. 266–278]
Google Scholar
M. Dascal, Leibniz’s Two-pronged Dialectics, in [15, pp. 37–72]
Google Scholar
M. Dascal (ed.), Leibniz: What Kind of Rationalist? (LEUS-Springer, Dordrecht, 2008)
Google Scholar
S. Rahman, H. Rückert, New perspectives in dialogical logic. Synthese 1/2, 127 (2001)
Google Scholar
S. Rahman, H. Rückert, Dialogical connexive logic, in [16, pp. 105–139]
Google Scholar
S. Rahman, J. Redmond, Hugh MacColl et la Naissance du Pluralisme Logique (College Publications, London, 2008)
Google Scholar
C. Pizzi, T. Williamson, Strong Boethius’ Thesis and Consequential Implication. J. Philos. Logic 26, 569–588 (1997)
Article Google Scholar
G. Priest, Negation as cancellation and connexive logic. Topoi 18, 141–148 (1999)
Article Google Scholar
H. Wansing, Connexive modal logic, in Advances in Modal Logic, vol. 5, ed. by R. Schmidt et al. (King’s College Publications, London, 2005), pp. 367–383
Google Scholar
H. Wansing. Connexive Logic, in The Stanford Encyclopedia of Philosophy (Spring 2014 Edition), ed. by Edward N. Zalta, http://plato.stanford.edu/archives/spr2014/entries/logic-connexive/
D. Steiner, Th. Studer, Total public announcements. Typoscript (2007)
Google Scholar
M. Armgardt, Salvius Iulianus als Meister der stoischen Logik –zur Deutung von Iulian D. 34,5,13(14), 2–3, in Liber amicorum Chris-toph Krampe zum 70. Geburtstag, ed. by M. Armgardt, F. Klinck, I. Reichard, pp. 29–36. Freiburger Rechtsgeschichtliche Abhandlungen Bd. 68 (Berlin, 2013)
Google Scholar
G. Sundholm, Constructions, proofs and the meaning of the logical constants. J. Philos. Logic 12(2), 151–172 (1983)
Article Google Scholar
G. Sundholm, Proof-theory and meaning, in Handbook of Philosophical Logic, ed. by D. Gabbay, F. Guenthner, vol. 3 (Reidel, Dordrecht, 1986), pp. 471–506
Chapter Google Scholar
G. Sundholm, A plea for logical atavism, in The Logica Yearbook 2000, ed. by O. Majer (Filosofia, Prague, 2001), pp. 151–162
Google Scholar
G. Sundholm, A century of judgment and inference: 1837–1936, in The Development of Modern Logic, ed. by L. Haaparanta (Oxford University Press, Oxford, 2009), pp. 263–317
Chapter Google Scholar
G. Sundholm, Containment and variation; two strands in the development of analyticity from Aristotle to Martin-Löf, in Judgement and the Epistemic Foundation of Logic, ed. by M. van der Schaar (Springer, Dordrecht, 2013), pp. 23–35
Chapter Google Scholar
J. Hintikka, Knowledge and Belief: An Introduction to the Logic of the Two Notions (Cornell University Press, Cornell, 1962)
Google Scholar
A. Ranta, Type-theoretical grammar (Clarendon Press, Clarendon, 1994)
Google Scholar
M. Armgardt, Presumptions and Conjectures in the Legal Theory of Leibniz. In this volume
Google Scholar
D.M. Gabbay, J. Woods, Relevance in the law, in Approaches to Legal Rationality, ed. by D. Gabbay, P. Canivez, S. Rahman, A. Thiercelin (Springer, Dordrecht, 2012), pp. 239–264
Google Scholar
G. Primiero, Information and Knowledge. A Constructive Type-Theoretical Approach (Springer, Dordrecht, 2008)
Google Scholar
G. Primiero, Type-theoretical dynamics, in The Realism-Antirealism Debate in the Age of Alternative Logics, ed. by Rahman et al, (Springer, Dordrecht, 2012), pp. 191–212
Google Scholar
J. Woods, Paradox and Paraconsistency. Conflict Resolution in the Abstract Sciences (Cambridge University Press, Cambridge, 2003)
Google Scholar
D.M. Gabbay, J. Woods, Logic and the law. Crossing the lines of discipline, in Approaches to Legal Rationality, ed. by D. Gabbay, P. Canivez, S. Rahman, A. Thiercelin (Springer, Dordrecht, 2012), pp. 165–202
Google Scholar
P. Martin-Löf, Intuitionistic Type Theory – Notes by Giovanni Sambin of a Series of Lectures Given in Padua, June 1980 (Bibliopolis, Naples, 1984)
Google Scholar
B. Nordström, K. Petersson, J.M. Smith, Programming in Martin-Löf’s Type Theory – An Introduction (Oxford University Press, Oxford, 1990)
Google Scholar
H. Rückert, Dialogues as a dynamic framework for logic (College Publications, London, 2011)
Google Scholar
N. Clerbout, S. Rahman, Linking Game-Theoretical Approaches with Constructive Type Theory: From Dialogical Strategies to CTT-Demonstrations (Springer, Dordrecht, 2015, in print)
Google Scholar
S. Rahman, N. Clerbout, L. Keiff, The constructive type theory and the dialogical turn: a new start for the Erlanger Konstruktivismus, in Dialogische Logik, ed. by J. Mittelstrass, (Mentis, Münster, 2015), pp. 127–184
Google Scholar
P. Lorenzen, K. Lorenz, Dialogische Logik (Wissenschaftliche Buchgesellschaft, Darmstadt, 1978)
Google Scholar
K. Lorenz, Basic objectives of dialogue logic in historical perspective, in [16: 255–263]
Google Scholar
W. Felscher, Dialogues as a foundation for intuitionistic logic, in Handbook of Philosophical Logic, ed. by D. Gabbay, F. Guenthner, vol. 3 (Kluwer, Dordrecht, 1985), pp. 341–372
Google Scholar
K. Lorenz, Dialogischer Konstruktivismus (De Gruyter, Berlin/New York, 2008)
Book Google Scholar
K. Lorenz, Philosophische Variationen: Gesammelte Aufsatze Unter Einschluss Gemeinsam Mit Jurgen Mittelstrass Geschriebener Arbeiten Zu Platon Und Leibniz (De Gruyter, Berlin/New York, 2010)
Google Scholar
K. Lorenz, Logic, Language and Method – On Polarities in Human Experience (De Gruyter, Berlin/New York, 2010)
Google Scholar
S. Rahman, Über Dialogue, Protologische Kategorien und andere Seltenheiten (P. Lang, Frankfurt/Paris/New York, 1993)
Google Scholar
S. Rahman, L. Keiff, On how to be a dialogician, in Logic, Thought and Action, ed. by D. Vanderveken (Kluwer, Dordrecht, 2005), pp. 359–408
Chapter Google Scholar
L. Keiff, Dialogical Logic, in The Stanford Encyclopedia of Philosophy (Summer 2011 Edition), ed. by Edward N. Zalta. http://plato.stanford.edu/archives/sum2011/entries/logic-dialogical/
S. Rahman, Negation in the logic of first degree entailment and tonk: a dialogical study, in The Realism-Antirealism Debate in the Age of Alternative Logics, ed. by Rahman et al. (Springer, Dordrecht, 2012), pp. 213–250
Google Scholar
N. Clerbout, Etude sur quelques sémantiques dialogiques. Concepts fondamentaux et éléments de metathéorie (College Publications, London, 2014)
Google Scholar
N. Clerbout, First-order dialogical games and tableaux. J. Philos. Log. doi: 10.1007/s10992-013-9289-z. Online first publication
W. Kamlah, P. Lorenzen, Logische Propädeutik, 2nd edn. (Metzler, Stuttgart/Weimar, 1972)
Google Scholar
W. Kamlah, P. Lorenzen, Logical Propaedeutic. English translation of [55] by H. Robinson, University Press of America, Lanham, 1984
Google Scholar
P. Lorenzen, O. Schwemmer, Konstruktive Logik Ethik und Wissenschaftstheorie, 2nd edn. (Bibliographisches Institut, Mannheim, 1975)
Google Scholar
J. Redmond, M. Fontaine, How to play dialogues. an introduction to dialogical logic (College Publications, London, 2011)
Google Scholar
S. Rahman, L. Keiff, La Dialectique entre logique et rhétorique. Revue de Métaphysique et de Morale 66/2, 149–178 (2010)
Google Scholar
L. Keiff, Heuristique formelle et logiques modales non normales. Philosophia Scientiae 8/2, 39–57 (2004)
Article Google Scholar
L. Keiff, Introduction à la dialogique modale et hybride. Philosophia Scientiae 8/2, 89–102 (2004)
Article Google Scholar
L. Keiff, Le Pluralisme Dialogique. Approches dynamiques de l’argumentation formelle. Ph.D. thesis, Université de Lille, Lille, 2007
Google Scholar
S. Rahman, A non normal logic for a wonderful world and more, in The Age of Alternative Logics, 2nd edn, ed. by van Benthem et al. (Kluwer-Springer, Dordrecht, Second edition, 2009), pp. 311–344
Google Scholar
V. Fiutek, H. Rückert, S. Rahman, A dialogical semantics for Bonanno’s system of belief revision, in Constructions, ed. by P. Bour et al. (College Publications, London, 2010), pp. 315–334
Google Scholar
A. Ranta, Propositions as games as types. Synthese 76, 377–395 (1988)
Article Google Scholar
N. Clerbout, M.-H. Gorisse, S. Rahman, Context-sensitivity in Jain Philosophy. A dialogical study of Siddharsigani’s commentary on the handbook of logic. J. Philos. Log. 40/5, 633–662 (2011)
Google Scholar
A. Popek, Logical dialogues from Middle Ages, in Logic of Knowledge. Theory and Applications, ed. by Barés et al. , (College Publications, London, 2011), pp. 223–244
Google Scholar
S. Rahman, T. Tulenheimo, From games to dialogues and back: towards a general frame for validity, in Games: Unifying Logic, Language and Philosophy, ed. by O. Majer et al. , (Springer, Dordrecht, 2009), pp. 153–208
Google Scholar
J. Redmond, Logique dynamique de la fiction, Pour une approche dialogique (College Publications, London, 2010)
Google Scholar
M. Fontaine, Argumentation et engagement ontologique de l’acte intentionnel. Pour une réflexion critique sur l’identité dans les logiques intentionnelles explicites (College Publications, London, 2013)
Google Scholar
H. van Ditmarsch, D. van der Hoek, B. Kooi, Dynamic-Epistemic Logic (Springer, Berlin, 2007)
Book Google Scholar
J. Hintikka, Logic, Language-Games and Information: Kantian Themes in the Philosophy of Logic (Clarendon, Oxford, 1973)
Google Scholar
S. Rahman, N. Clerbout, L. Keiff, On dialogues and natural deduction, in Acts of Knowledge – History, Philosophy, Logic, ed. by S. Rahman, G. Primiero (College Publications, London, 2009), pp. 301–336
Google Scholar

Download references

Acknowledgments

Many thanks to Matthias Armgardt, Nicolas Clerbout, Johan Granström and Göran Sundholm, who were closely involved with the writing of the present text from its conception down to the nitty-gritty details of the last stages. The inputs of Granström and Clerbout reflect the results of ongoing joint papers, and those of Sundholm and Armgardt further research collaborations. Moreover, without the inputs on CTT by Granström and Sundholm, and the ones on the theory and history of Law by Armgardt, the paper would not have been possible. In fact, the paper is the first result of 1 year of research in the framework of the Franco-German ANR-DFG project, JURILOG (ANR11 FRAL 003 01), between the Universities of Konstanz (Chair of Civil Law and History of Law, Prof. Dr. Matthias Armgardt) and Lille (Chair of Logic and Epistemology, Prof. Dr. Shahid Rahman), supported by the Maison Européenne des Sciences de l’ Homme et de la Société - USR 3185. I would also like to thank the following permanent members of JURILOG for fruitful discussions and remarks: Giuliano Bacigalupo (Konstanz), P. Canivez (Lille3), Sandrine Chassagnard-Pinet (Lille2), Karl-Heinz Hülser (Konstanz), Bettine Jankowski (Konstanz), Sébastien Magnier (Lille3), Juliette Sénéchal (Lille2) and Juliele Sievers (Lille3). The paper is also linked with my research within the “Argumentation, Decision, Action” (ADA) research program supported by USR 3185 mentioned above and the “Langage, Argumentation et Cognition dans les Traditions Orales” (LACTO) networks.

Author information

Authors and Affiliations

Département de philosophie, UFR Humanités, UMR 8163 Savoirs, Textes, Langage, Université de Lille 3, Villeneuve-d’Ascq, France
Shahid Rahman

Authors

Shahid Rahman
View author publications
You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Shahid Rahman .

Editor information

Editors and Affiliations

Universität Konstanz, Konstanz, Baden-Württemberg, Germany
Matthias Armgardt
UMR 8163 Savoirs, Textes, Langage, Université Lille UFR Humanités Département Philosophie, Villeneuve d'Ascq, France
Patrice Canivez
Equipe René Demogue (CRD&P, EA 4487), Université de Lille (UDSL), Lille, France
Sandrine Chassagnard-Pinet

Appendices

Appendix I: The Basic CTT-Frame for Intuitionistic Predicate Logic

1.1 AI. 1. CTT and Intuitionistic Logic

The following presentation and (brief) commentary of the rules has been extracted literally from the (more exhaustive) text of Martin-Löf [38, pp. 13–15 and 20–21] with the only minimal notational variation of using “:” instead of “є”. We present the rules for product Π (the applications of which include universal quantification and material implication), disjoint union Σ (the applications of which include existential quantification, subset separation and conjunction) and for sum (or coproduct) + (the applications of which include disjunction).

Given a set A and a family of sets B(x) over the set A, we can form the product:

Π -formation

$$ \begin{array}{l}\kern5.04em \left(x:A\right)\kern7.56em \left(x:A\right)\\ {}A\kern0.5em set\kern3.72em B(x)\kern0.5em set\kern3em A=c\kern2.64em B(x)=D(x)\\ {}--------------\kern2.28em -----------------\\ {}\left(\varPi x:A\right)\;B(x)\; set\kern4.8em \left(\varPi x:A\right)\;B(x)=\left(\varPi x:C\right)\;D(x)\end{array} $$

Π -introduction

$$ \begin{array}{l}\kern4.08em \left(x:A\right)\kern6.6em \left(x:A\right)\\ {}\kern3.84em b(x):B(x)\kern4.56em b(x)=d(x):B(x)\\ {}------------\kern1.8em -----------------\\ {}\left(\lambda x\right)b(x):\kern0.36em \left(\varPi x:A\right)\;B(x)\kern0.72em \left(\lambda x\right)b(x)=\left(\lambda x\right)d(x):\kern0.24em \left(\varPi x:A\right)\;B(x)\end{array} $$

Note that these rules introduce canonical elements and equal canonical elements, even if b(a) is not a canonical element of B(a) for a : A. Also, we assume that the usual variable restriction is met, i.e. that x does not appear free in any assumption except (those of the form) x : A.

Π -elimination

$$ \begin{array}{l}\begin{array}{ll}c:\left(\varPi x:A\right)\;B(x)\hfill & a:A\hfill \end{array}\kern0.96em c=d:\left(\varPi x:A\right)\kern0.24em \begin{array}{ll}\;B(x)\hfill & a=b:A\hfill \end{array}\\ {}-------------\kern0.72em -----------------\\ {}Ap\left(c,a\right):B(a)\kern3.12em Ap\left(c,a\right)=Ap\kern0.5em \left(d,b\right):B(a)\end{array} $$

We have to explain the meaning of the new constant Ap (Ap for Application). Ap(c; a) is a method of obtaining a canonical element of B(a), and we now explain how to execute it. We know that c : (Πx : A)B(x), that is, that c is a method which yields a canonical element (λx) b(x) of (Πx : A)B(x) as result. Now take a : A and substitute it for x in b(x). Then b(a) : B(a). Calculating b(a), we obtain as result a canonical element of B(a), as required.

The second group of rules is about the disjoint union of a family of sets.

Σ -formation

$$ \begin{array}{l}\kern5.52em \left(x:A\right)\\ {}A\kern0.5em set\kern3.6em B(x)\kern0.5em set\\ {}----------------\\ {}\kern0.96em \left(\varSigma x:A\right)\;B(x) set\end{array} $$

Σ -introduction

$$ \begin{array}{l}\kern11.76em \left(x:A\right)\\ {}a:A\kern1.56em b:B(a)\kern2.52em A=C\kern1.56em B(x)=D(x)\\ {}------------\kern0.84em ---------------\\ {}\left(a,b\right):\kern0.24em \left(\varSigma x:A\right)B(x)\kern1.56em \left(\varSigma x:A\right)B(x)=\left(\varSigma x:C\right)D(x)\end{array} $$

In fact, any canonical element of (Σx : A)B(x) is of the form (a, b) with a : A and b : B(a) by Σ−introduction. But then we also have a : C and b : D(a) by equality of sets and substitution. Hence (a, b) : (Σx : C)D(x) by Σ-introduction. The other direction is similar.

Σ -elimination

$$ \begin{array}{l}\kern7.56em \Big(x:A,y:B(x)\\ {}c:\left(\varSigma x:A\right)B(x)\kern1.8em d\left(x,y\right):C\left(\left(x,y\right)\right)\\ {}---------------------\\ {}\kern2.28em E\left(c,\left(x,y\right)\;d\left(x,y\right)\right):C(c)\Big)\end{array} $$

where we presuppose the premise C(z) set (z : (Sx : A)B(x)), although it is not written out explicitly. (To be precise, we should also write out the premises A set and B(x) set (x : A).) We explain the rule of Σ-elimination by showing how the new constant E operates on its arguments. So assume we know the premises. Then we execute E(c; (x; y)d(x; y)) as follows. First execute c, which yields a canonical element of the form (a, b) with a : A and b 2 B(a). Now substitute a and b for x and y, respectively, in the right premise, obtaining d(a; b) : C((a; b)). Executing d(a, b) we obtain a canonical element e of C((a; b)). We now want to show that e is also a canonical element of C(c). It is a general fact that, if a : A and a has value b, then a = b : A (note, however, that this does not mean that a = b : A is necessarily formally derivable by some particular set of formal rules). In our case, $ c=\left(a;b\right):\left(\_x:A\right)B(x) $ and hence, by substitution, $ C(c)=C\left(\left(a;b\right)\right) $. Remembering what it means for two sets to be equal, we conclude from the fact that e is a canonical element of C((a; b)) that e is also a canonical element of C(c).

We now give the rules for the sum (disjoint union or coproduct) of two sets.

+− formation

$$ \begin{array}{l}A\kern0.5em set\kern0.72em B\kern0.5em set\\ {}--------\\ {}A+B\kern0.5em set\end{array} $$

The canonical elements of A + B are formed using:

+−introduction

$$ \begin{array}{l}a:A\kern2.76em b:B\\ {}------\kern0.6em -----\\ {}i(a):A+B\kern0.72em j(b):A+B\end{array} $$

where i and j are two new primitive constants; their use is to give the information that an element of A+B comes from A or B, and which of the two is the case. It goes without saying that we also have the rules of +−introduction for equal elements:

$$ \begin{array}{l}a = c\ :\ A\kern3.6em b=d:B\\ {}----------\kern0.72em -------\\ {}i(a)=i(c):A+B\kern0.84em j(b)=j(d):A+B\end{array} $$

Since an arbitrary element c of A + B yields a canonical element of the form i(a) or j(b), knowing c : A + B means that we also can determine from which of the two sets A and B the element c comes.

+−elimination

$$ \begin{array}{l}\kern3.72em \left(x:A\right)\kern3.96em \left(y:B\right)\\ {}c:A+B\kern0.72em d(x):C\left(i(x)\right)\kern1.2em e(y):C\left(j(y)\right)\\ {}----------------------------\\ {}\kern3em D\left(c,(x)d(x),(y)e(y)\right):C(c)\end{array} $$

where the premises A set, B set and C(z) set (z : A + B) are presupposed, although not explicitly written out.

+−equality

$$ \begin{array}{l}\kern3.96em \left(x:A\right)\kern3.12em \left(y:B\right)\\ {}a:A\kern2.4em d(x):C\left(i(x)\right)\kern1.68em e(y):C\left(j(y)\right)\\ {}-----------------------------\\ {}\kern2.88em D\left(i,(a),(x)\kern0.5em d(x),(y)e(y)\right)=d(a):C\left(i(a)\right)\\ {}\kern6em \left(x:A\right)\kern1.56em \left(y:B\right)\\ {}b:B\kern2.28em d(x):C\left(i(x)\right)\kern0.96em e(y):C\left(j(y)\right)\\ {}----------------------------\\ {}\kern0.72em D\left(j,(a),(x)\kern0.5em d(x),(y)e(y)\right)=e(b):C\left(j(b)\right)\end{array} $$

1.2 AI.2. Hypotheticals

1.2.1 AI.2.a. Hypotheticals and Dependent Objects

The CTT language has also hypothetical judgements of the form

$$ B\ type\ \left(x:A\right) $$

Where A is a type which does not depend on any assumptions and B is a type when x : A (the hypothesis for B). In the case of sets we have that b is an element of the set B, under the assumption that x is an element of the A:

$$ \begin{array}{ll}b:B\left(x:A\right)\hfill & \left(\mathrm{more}\ \mathrm{precisely}:b:el(B)\ \left(x:el\ (A)\right)\right)\hfill \end{array} $$

The explicit introduction of hypotheticals carries with it the explicit introduction of appropriate substitution rules. Indeed, if in the example above, a : A, then the substitution of x by a in b yields an element of B; and if a =c : A, then the substitutions of x by a and by c in b are equal elements in B (cfr. Granström[9, pp. 111–112]):

$$ \begin{array}{l}a:A\kern1.44em b:B\left(x:A\right)\kern3.48em a=c:A\kern0.96em b:B\left(x:A\right)\\ {}------------\kern3em -------------\\ {}\kern2.28em b\left(a/x\right):B\kern4.8em b\left(a/x\right)=b\left(c/x\right):B\end{array} $$

As pointed out by Granström [9, p. 112] the form of assertion b : B (x : A) (b : el (B) (x : el (A))) can be generalized in three directions:

1.
Any number of assumptions will be allowed, not just one;
2.
The set over which a variable ranges may depend on previously introduced variables;
3.
The set B may depend on all introduced variables

Such a list of assumptions will be called a context. Thus we might need the forms of assertion

$$ \begin{array}{c}\hfill b:B\ \left(\varGamma \right)\hbox{--} \mathrm{where}\ \varGamma \kern0.5em \mathrm{is}\ \mathrm{a}\ \mathrm{context}\ \left(\mathrm{i}.\mathrm{e}.,\ \mathrm{a}\ \mathrm{list}\ \mathrm{of}\ \mathrm{a}\mathrm{ssumptions}\right)\hfill \\ {}\hfill \varGamma : context\hfill \end{array} $$

In general, a hypothetical judgment has the form

$$ {x}_1:{A}_1,{x}_2:{A}_2,\dots {x}_n:{A}_n $$

where we already know that A ₁ is a type, A ₂ is a type in the context x ₁ : A ₁ , …, and A _n is a type in the context x ₁ : A ₁ , x ₂ : A ₂ , … x _n–1 : A _n–1 :

$$ \begin{array}{l}{A}_1\kern0.5em type\kern0.5em \left[\mathrm{depending}\ \mathrm{on}\ \mathrm{no}\ \mathrm{assumption}\right]\\ {}{A}_2\kern0.5em type\kern0.5em \left({x}_1:{A}_1\right)\\ {}\dots \\ {}{A}_n\kern0.5em type\kern0.5em \left({x}_1:{A}_1,{x}_2:{A}_2,\dots {x}_{n-1}:{A}_{n-1}\right)\\ {}A\kern0.5em type\kern0.5em \left({x}_1:{A}_1,{x}_2:{A}_2,\dots {x}_n:{A}_n\right)\\ {}-------------------\\ {}x:A\kern0.5em \left({x}_1:{A}_1,{x}_2:{A}_2,\dots {x}_n:{A}_{n,}x:A\right)\end{array} $$

The rules for substitution and equality are generalized accordingly:

Hypothetical judgements introduce functions from A to B:

$$ f(x):B\left(x:A\right) $$

It can be read in several ways, for example:

f(x) : B for arbitrary x : A
f(x) : B under the hypothesis x :A
f(x) : B provided x : A
f(x) : B given x :A
f(x) : B if x : A
f(x) : B in the context x : A

It is crucial to notice that the notion of function is intentional rather than an extensional. Indeed, the meaning of an hypothetical function that introduces a function is that whatever element a is substituted for x in (f(x), an element f(a) of B results . Moreover, the equality of two functions defined by establishing that substitutions of equal elements of A result in equal elements of B as regulated by the rules of substitution given above – where b(x) is interpreted as function from A to B.^{Footnote 33}:

In addition to domains of individuals, an interpreted scientific language requires propositions. They are introduced in CTT by laying down what counts as proof of a proposition. Accordingly, a proposition is true if there is such a proof. We write

$$ A: prop $$

to formalize the judgement that A is a proposition. Propositional functions are introduced by hypothetical judgements. The hypothetical judgement required to introduce propositional functions is of the form:

$$ B(x): prop\left(x:A\right) $$

that reads, B(x) is of the type proposition, provided it is applied to elements of the (type-)set A. The rule by which we produce propositions from propositional functions is the following:

$$ \begin{array}{l}a\ :\ A\kern0.6em B(x)\ :\ prop\ \left(x:\ A\right)\\ {}--------------\\ {}\kern1.56em Ba: prop\end{array} $$

And it requires also of the formulation of an appropriate rule that defines the equivalence relation within the type prop:

$$ \begin{array}{l}a=b\ :\ A\kern0.98em B(x)\ :\ prop\ \left(x:\ A\right)\\ {}-----------------\\ {}\kern1.08em Ba=Bb: prop\end{array} $$

The notion of propositional function as hypothetical judgement allows the (intensional) introduction of subsets by separation:

$$ \begin{array}{l}A\ :\ set\kern0.84em B(x)\ :\ prop\ \left(x:\ A\right)\kern0.48em b\ :\ A\kern2.25em Bb\ true\\ {}--------------\kern1.92em ----------\\ {}\left\{x:A/B(x)\right\}: set\kern3.96em b:\left\{x:A/B(x)\right\}\end{array} $$

This explanation of subsets also justifies the following rules:

$$ \begin{array}{l}b:\left\{x:A/B(x)\right\}\kern2.04em b:\left\{x:A/B(x)\right\}\\ {}---------\kern1.8em ---------\\ {}b:A\kern5.16em Bb\kern0.5em true\end{array} $$

What is given in a context, the given contextually-dependent knowledge, is whatever can be derived from the hypotheses constituting the context. Actually, it is usually distinguished between what is actually given in the context (actual knowledge), namely the variables themselves and the judgements involving these variables and what is potentially given (potential knowledge), namely what can be derived by the rules of type theory from what is actually given. Now, actual and potential knowledge can be increased by extending a given context in ways to be described below.

1.2.2 AI.2.b. Extending Hypotheticals

Let us consider once more the hypothetical

$$ B(x): prop\left(x:A\right) $$

Then, we can produce an extension of the context by interpretation by means of definitional equalities such as a=x : A yielding

$$ B(a): prop\;\left(a=x:A\right) $$

Ranta [31, pp. 135–137] applies it to the study of a literary text where the text is seen as defining a context. That is, as a series of hypothetical judgements that can be interpreted by equating the variables with actual objects:

An interpretation of Hemingway’s short story ‘The Battler’ might start with the definition

Nick Adams = Ernest Hemingway : man

and go on assigning events from the young Hemingway’s life to the variable proofs of even propositions asserted in the story. [40, p. 136]

More generally one could extend a context by another context that interprets the variables of the original context in terms of the new ones (cfr. [31, pp. 145–147]). Extensions can in principle induce the growing of knowledge (cfr. Primiero[34, pp. 155–163]). In fact, a context can be enlarged by:

(a)
Addition of hypotheses. For instance the context

$ \varGamma =\left({x}_1:{A}_1,\dots {x}_n:{A}_n\right) $ is extended to the context

$ \varDelta =\left({x}_1:{A}_1,\dots {x}_n:{A}_n,{x}_{n+1}:{A}_{n+1}\right) $ . It is clear that everything that is given in Γ is given in the new context as well and thus in the new context we know what we knew in the original one. It may also happen that in the new context proofs are now available that were not at all available in Γ – not even potentially. In this case an increasing grow of knowledge obtains.
(b)
Addition of definitions that interpret one of its variables. This the case already mentioned at the start of the paragraph. A more general formulation is the following: the context

$ \varGamma =\left({x}_1:{A}_1,\dots {x}_n:{A}_n\right) $ is extended to the context

$ \varDelta =\left(\varGamma, {x}_k=a:{A}_k\right) $

So that in the new context every occurrence of x _k is substituted by a. The new context is obtained from Γ by removing the hypothesis x _k : A _k by a(x ₁ … x _n). Thus the new context is shorter than the original. Still, this operation furnishes not only the knowledge of the original context but the value of the one variable reduces the uncertainty within the context.^{Footnote 34}
(c)
Addition of a sequence of definitions of all variables in terms of the variables of the new context (the new context need not look the same as the original one). The context

$ \varGamma ={x}_1:{A}_1,\dots {x}_n:{A}_n\left({x}_1\dots {x}_{n-1}\right) $ is extended to the context

$ \varDelta ={y}_1:{B}_1,\dots {y}_m:{B}_m\left({y}_1\dots {y}_{m-1}\right) $ by a mapping f from Δ to Γ constituted by a sequence of functions such that

$ \begin{array}{l}{x}_1=f\left({y}_1\right)\dots \left({y}_m\right):{A}_1\left(\varDelta \right)\hfill \\ {}\dots \hfill \\ {}{x}_n=f\left({y}_1\right)\dots \left({y}_m\right):{A}_n\left(f\left({y}_1\right)\dots \left({y}_m\right)\dots {f}_{n-1}\left({y}_1\right)\dots \left({y}_m\right)\right)\ \left(\varDelta \right)\hfill \end{array} $

The third operation of extension can be seen as a generalization of the other two (if the new context results by addition of hypotheses we have the first case; if the new context results from the introduction of only one definition, then we have the second case) by translating the old context into the new. Thus, the existence of a mapping $ \mathbf{f}:\varDelta \to \varGamma $ is usually taken to be the definition of what it is for a context to be an extension of another context.

It might be even argued as Primiero [34, p. 187] does, that this extension amounts to knowledge enlargement in the sense that the new context can show some properties holding in the old context in such a way that new concepts might elucidate the older ones.

Appendix II: Dialogical Logic and Constructive Type Theory

The dialogical approach to logic is not a specific logical system but rather a rule-based semantic framework in which different logics can be developed, combined and compared.^{Footnote 35} An important point is that the rules that fix meaning are of more than one kind.^{Footnote 36} This feature of its underlying semantics quite often motivated the dialogical approach to be understood as a pragmatist semantics. More precisely, in a dialogue two parties argue about a thesis respecting certain fixed rules. The player that states the thesis is called Proponent (P), his rival, who contests the thesis is called Opponent (O). In its original form, dialogues were designed in such a way that each of the plays end after a finite number of moves with one player winning, while the other loses. Actions or moves in a dialogue are often understood as speech-acts involving declarative utterances or posits and interrogative utterances or requests. The point is that the rules of the dialogue do not operate on expressions or sentences isolated from the act of uttering them. The rules are divided into particle rules or rules for logical constants (Partikelregeln) and structural rules (Rahmenregeln). The structural rules determine the general course of a dialogue game, whereas the particle rules regulate those moves (or utterances) that are requests (to the moves of a rival) and those moves that are answers (to the requests).

Crucial for the dialogical approach are the following points (cfr. Rahman [52]):

1.
The distinction between local (rules for logical constants) and global meaning (included in the structural rules that determine how to play).
2.
The player independence of local meaning.
3.
The distinction between the play level (local winning or winning of a play) and the strategic level (existence of a winning strategy).
4.
A notion of validity that amounts to winning strategy independently of any model instead of winning strategy for every model.
5.
The distinction between non formal and formal plays – the latter notion concerns plays that are played independently of knowing the meaning of the elementary sentences involved in the main thesis.

In the framework of constructive type theory propositions are sets whose elements are called proof-objects. When such a set is not empty, it can be concluded that the proposition has a proof and that it is true. In his 1988 paper [65], Ranta proposed a way to make use of this approach in relation to game-theoretical approaches. Ranta took Hintikka’s Game Theoretical Semantics as a case study, but the point does not depend on this particular framework. Ranta’s idea was that in the context of game-based approaches, a proposition is a set of winning strategies for the player positing the proposition.^{Footnote 37} Now in game-based approaches, the notion of truth is to be found at the level of such winning strategies. This idea of Ranta’s should therefore enable us to apply safely and directly methods taken from constructive type theory to cases of game-based approaches.

But from the perspective of game theoretical approaches, reducing a game to a set of winning strategies is quite unsatisfactory, all the more when it comes to a theory of meaning. This is particularly clear in the dialogical approach in which different levels of meaning are carefully distinguished. There is thus the level of strategies which is a level of meaning analysis, but there is also a level prior to it which is usually called the level of plays. The role of the latter level for developing an analysis is, according to the dialogical approach, crucial, as pointed out by Kuno Lorenz in his 2001 paper [44]:

[…] for an entity [A] to be a proposition there must exist a dialogue game associated with this entity […] such that an individual play where A occupies the initial position […] reaches a final position with either win or loss after a finite number of moves […]

For this reason we would rather have propositions interpreted as sets of what we shall call play-objects, reading an expression

$$ p:\upvarphi $$

as “p is a play-object for φ “.

Thus, Ranta’s work on proof objects and strategies constitutes the end not the start of the dialogical project.

2.1 The Formation of Propositions

Before delving into the details about play-objects, let us first discuss the issue of the formation of expressions and in particular of propositions in the context of dialogical logic.

In standard dialogical systems, there is a presupposition that the players use well-formed formulas. One can check the well formation at will, but only with the usual meta reasoning by which one checks that the formula indeed observes the definition of wff. The first enrichment we want to make is to allow players to question the status of expressions, in particular to question the status of something as actually standing for a proposition. Thus, we start with rules giving a dialogical explanation of the formation of propositions. These are local rules added to the particle rules which give the local meaning of logical constants (see next section).

Let us make a remark before displaying the formation rules. Because the dialogical theory of meaning is based on argumentative interaction, dialogues feature expressions which are not posits of sentences. They also feature requests used for challenges, as illustrated by the formation rules below and the particle rules in the next section. Now, by the no entity without type principle, the type of these actions, which we may write “formation-request”, should be specified during a dialogue. Nevertheless we shall consider that the force symbol ? _F already makes the type explicit. Indeed a request in a dialogue should not be confused with a move by the means of which it is posited that some entity is of the type request.^{Footnote 38} Hence the way requests are written in rules and dialogues in this work (see Table 7.2).

Table 7.2 Formation rules

On Hypothetical Judgements and Leibniz’s Notion of Conditional Right

Abstract

Access this chapter

Notes

References

Acknowledgments

Author information

Authors and Affiliations

Corresponding author

Editor information

Editors and Affiliations

Appendices

Appendix I: The Basic CTT-Frame for Intuitionistic Predicate Logic

1.1 AI. 1. CTT and Intuitionistic Logic

1.2 AI.2. Hypotheticals

1.2.1 AI.2.a. Hypotheticals and Dependent Objects

1.2.2 AI.2.b. Extending Hypotheticals

Appendix II: Dialogical Logic and Constructive Type Theory

2.1 The Formation of Propositions

Posit-Substitution

Remark

Explanations

2.2 Play Objects

2.3 The Development of a Play

Important Remark

2.4 From Play-Objects to Strategies

Preliminaries

Procedure

Important Remark

2.5 Equality

2.5.1 Definitional Equality

2.5.2 The Equality-Predicate

Rights and permissions

Copyright information

About this chapter

Cite this chapter

Download citation

Share this chapter

Publish with us

Search

Navigation