Abstract
In this chapter, I first consider mode standard constructive semantic approaches to the formal propositional logics for proofs and refutations. Whilst these illuminate aspects of the structure of interactive logic, they also highlight the shortcomings of standard semantics, even in dualised form. Nonetheless, the way in which these structures “objectify” propositions is useful for considering propositions as stable objects subsequent to their construction in interaction. These ideas are made more precise through the notion of bisimulation equivalence, and closure under bisimulation. To finish, I provide a number of examples, using these to highlight a slightly more liberal conception of the coherence of interactions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
To be brief, I leave details aside, and assume some familiarity with constructive type theory. For a simple introduction, see (e.g. [1]). Even in the absence of familiarity, the discussion should be fairly self-evident.
- 2.
- 3.
The use of the term “computing” is not accidental. Types are foundational in many areas of programming, particularly functional approaches to programming, so types are often understood to specify a task carried out by a program, and as such, a proof is also identifiable with the running of such a programme (at least in some cases).
- 4.
See [6] for details of this system in natural deduction form.
- 5.
The following is folklore, but further details can be found in [8, p. 50ff].
- 6.
What follows is well-known, for details see [9].
- 7.
Though sometimes it is called a Brouwerian algebra, for example, [10].
- 8.
This follows an informal proof given in correspondence by Peter Johnstone available at: http://permalink.gmane.org/gmane.science.mathematics.categories/7045, and [15] provides a formal proof with discussion.
- 9.
- 10.
As is typical, we may slightly abuse notation and say that a subobject may be a member of \(\Omega \), since this makes little difference in practice (in the context of propositional logic), though to be more precise we should say that the equivalence class for a subobject is a member of \(\Omega \).
- 11.
This follows the account given in [16].
- 12.
This follows the account given in [16].
- 13.
- 14.
The point is arguable. For example, [19] discusses the suggestion in [17] that, in fact, this is not a problematic deficiency since mathematics depends less on an object-language implication operator, than it does a deducibility relation, which can be constructed in terms of the ordering on the complement classifier. I will not take a stance on this here, since the current construction does not require such an operator.
- 15.
Thanks to Dave Ripley for pushing me on this issue.
- 16.
For example, [19] points out that in effect, SET, therefore always has both classifiers.
- 17.
As such, the key distinction between the approach suggested here, and the construction in [7, 17, 19] is that, in the latter, a paraconsistent topos is understood as a complete mathematical universe, which is, at the least, capable of expressing a “full” propositional logic. Here, we take an ordinary topos and a paraconsistent topos to express two “halves” of a logic, with the former dealing proof-objects, and the latter, refutation-objects. This allows us to deal with complications that can they can not, such as the fact that a paraconsistent topos (and logic in general) is incapable of expressing a detachable conditional operator for proofs.
- 18.
Of course, on the interactive approach, we do have such an account, and without requiring any external approach to justification, since justification is achieved through the testing relationship.
- 19.
Proofs and further discussion may be found in detail in [20], and are also given by Todd Trimble here: https://ncatlab.org/nlab/show/Heyting+algebra#ToBooleanAlgebras.
- 20.
- 21.
Note that, whilst we are calling these dialogue topoi, there is no real relationship between them in terms of the structure of interaction, proofs (refutations) carried out within them are much more like concurrent processes.
- 22.
We should say something here about the syntax of the Boolean topos \(T_B\), which we are loosely specifying in the following as simply \(S, S^d\). This looseness is harmless since it is possible to define all of the syntax of both within a topos whose internal language is Boolean, and this follows from the collapse result in the previous section. For example, \(\lnot _I\) is definable by means of \(\rightarrow \) and 0 as usual, and \(\lnot _C\) by \(\leftarrow \) and 1, as they were for \(L_I\) and \(L_C\), respectively. The difference here is that they collapse into each other by the fact that \(\lnot _I \lnot _C = id\) in \(T_B\). As such, and due to the (non-formal) interpretation of conclusive proofs and refutations, it is safe to replace \(\lnot _I\) and \(\lnot _C\) in \(T_B\) by the single external negation \(\sim \) defined above.
- 23.
This latter point is important, since, for example, it allows that \(\alpha ^+ \#^{c}_{2} \beta ^+\) and \(\alpha ^- \#^{s}_{2} \beta ^-\) are coherent, whilst the move in \(A^+\) requires support from both \(\alpha ^+\) and \(\beta ^+\), and the move in \(A^-\) requires support from \(\alpha ^-\) or \(\beta ^-\).
- 24.
Further discussion of these, apparently contradictory “foundations” of local truth and falsity can be found in the following chapter. This testing relationship is heavily inspired by the constructions of geometry of interaction discussed in the previous chapter. As I say there, the details, and aims, substantially differ.
- 25.
Though, note that the reducibility condition allows some maneuverability over the course of an interaction.
- 26.
It should be noted that we are using bisimulation in a manner that is quite different to its use in other mathematical structures, including in the context of logical games, where they are taken to represent relationships between bisimilar strategies. Further discussion of the latter may be found in [24].
- 27.
See the example in the following section.
- 28.
I keep to the standard use of \(\sim \) to identify bisimilarity, since, whilst used briefly above and in the following chapter to indicate an external negation, I trust that the context of the formalism makes clear the usage of the symbol.
- 29.
- 30.
Interestingly, determining when a relationship between the two processes is not a bisimilarity requires us to look for transitions that do not match-up “from the inside”, by enumerating all actions and looking to see if there are any non-bisimilar actions.
- 31.
We let the superscript \(\Rightarrow ^{at_\alpha ^{+/-}}\) indicate a move with reasons in support of an atomic formula. Of course, this may be further broken down by testing reasons for it, but in many cases this may not be required.
- 32.
Note that, whilst stages \(s_3\) and \(s_4\) are not pair-wise coherent, they do conform to the definition of coherence by means of the “transformable in a single move” clause.
References
Erik Palmgren. Constructive logic and type theory, 2014.
Per Martin-Löf. On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic, 1(1):11–60, 1996.
W. A. Howard. The formulæ-as-types notion of construction. In Philippe De Groote, editor, The Curry-Howard Isomorphism. Academia, 1995.
Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical structures in computer science, 11(04):511–540, 2001.
A. N Kolmogorov. Zur deutung der intuitionistischen logik. Mathematische Zeitschrift, 35:58–65, (English translation in Mancosu 1998, pp. 328–334) 1932.
Luca Tranchini. Natural deduction for dual-intuitionistic logic. Studia Logica, 100(3):631–648, 2012.
Luis Estrada-González. From (paraconsistent) topos logic to universal (topos) logic. In Buchsbaum Arthur (Eds.) Koslow, Arnold, editor, The Road to Universal Logic, chapter 12. Birkhäuser Basel, 2015.
Saunders Mac Lane and Ieke Moerdijk. Sheaves in geometry and logic. Springer Science & Business Media, 1992.
A. S. Troelstra. Constructivism in Mathematics: An Introduction. Sole Distributors for the U.S.A. And Canada, Elsevier Science Pub. Co., 1988.
Nicholas Goodman. The logic of contradictions. Zeitschrift fur Mathematische Logic und Grundlagen der Arithmetik, 27:119–126, 1981.
Robert Goldblatt. Topoi: the categorial analysis of logic. Elsevier, 2014.
Andreas B. M. Brunner and Walter A. Carnielli. Anti-intuitionism and paraconsistency. In URL = http://www.cle.unicamp.br/e-prints/vol3,n1,2003.html, 2003.
James Trafford. Co-constructive logic for proofs and refutations. Studia Humana, 3(4):22–40, 2015.
Cecylia Rauszer. Applications of Kripke models to Heyting-Brouwer logic. Studia Logica, 36(1-2):61–71, 1977.
Tristan Crolard. Subtractive logic. Theoretical computer science, 254(1):151–185, 2001.
S. Awodey. Structure in mathematics and logic: A categorical perspective. Philosophia Mathematica, 4(3):209–237, 1996.
Chris Mortensen. Inconsistent mathematics, volume 312. Springer, 1995.
John L Bell. From absolute to local mathematics. Synthese, 69(3):409–426, 1986.
Luis Estrada-González. Complement-topoi and dual intuitionistic logic. Australasian Journal of Logic, 9:26–44, 2010.
Saunders MacLane and Ieke Moerdijk. Sheaves in geometry and logic: A first introduction to topos theory. Springer Science & Business Media, 2012.
Jean-Pierre Marquis and Gonzalo Reyes. The history of categorical logic: 1963–1977. In Dov Gabbay, Akihiro Kanamori, and John Woods, editors, Handbook of the history of logic. Elsevier, 2011.
Johan Van Benthem. Program constructions that are safe for bisimulation. Studia logica, 60(2):311–330, 1998.
Johan Van Benthem. Extensive games as process models. Journal of Logic, Language and Information, 11(3):289–313, 2002.
Johan Van Benthem. Logical dynamics of information and interaction. Cambridge University Press, 2011.
Johan Van Benthem and Jan Bergstra. Logic of transition systems. Journal of Logic, Language and Information, 3(4):247–283, 1994.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Trafford, J. (2017). Structuring Interactions. In: Meaning in Dialogue. Studies in Applied Philosophy, Epistemology and Rational Ethics, vol 33. Springer, Cham. https://doi.org/10.1007/978-3-319-47205-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-47205-8_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47204-1
Online ISBN: 978-3-319-47205-8
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)