It is the aim of INDICES to document recent explorations in the various fields of philosophical logic and formal linguistics and their applications in other disciplines. The main emphasis of this series is on self-contained monographs covering particular areas of recent research and surveys of methods, problems, and results in all fields of inquiry where recourse to logical analysis and logical methods has been fruitful. INDICES will contain monographs dealing with the central areas of philosophical logic (extensional and intensional systems, (...) indexical logics, non-classical logics, philosophy of logic, etc.) as well as studies in which these systems are applied to specific issues in philosophy, in the formal semantics of natural languages, the foundations of linguistic theory, in computational linguistics, and in theoretical computer science. Constructive type theory was first presented in 1970, by the Swedish logician Per Martin-Lof. It has become one of the main approaches used in the foundations of mathematics and computer science. But it has remained relatively unknown among linguists and philosophers, although it provides a considerable extension of the concepts and techniques of logic. The book first gives an introduction to type theory from the point of view of linguistics and the philosophy of language. Type theory is then applied in the areas of quantification, anaphora, temporal reference, and the structure of text and discourse. By virtue of the type-theoretical concepts of proof object and context, various phenomena of dependence and progression in language can be discussed in precise terms, and several well-known problems can be solved. A categorial grammar is presented togenerate formally a fragment of English, together with an example of a computer implementation. (shrink)

Without violating the spirit of Game-Theoretical semantics, its results can be re-worked in Martin-Löf''s Constructive Type Theory by interpreting games as types of Myself''s winning strategies. The philosophical ideas behind Game-Theoretical Semantics in fact highly recommend restricting strategies to effective ones, which is the only controversial step in our interpretation. What is gained, then, is a direct connection between linguistic semantics and computer programming.

We propose a shift in perspective from the view of natural languages as formal languages to natural languages as a collection of resources for constructing local languages for use in particular situations. This is suggested by our experience constructing natural language grammars for particular applications using the Grammatical Framework. It points to a research programme investigating how such resources play a role in linguistic innovation by agents constructing situation-specific local languages and how they can be made dynamic, modified by the (...) linguistic agent’s exposure to innovative linguistic data. (shrink)

The paper takes a look at the history of the idea of universal grammar and compares it with multilingual grammars, as formalized in the Grammatical Framework, GF. The constructivist idea of formalizing math- ematics piece by piece, in a weak logical framework, rather than trying to reduce everything to one single strong theory, is the model that guides the development of grammars in GF.

The paper takes a look at the history of the idea of universal grammar and compares it with multilingual grammars, as formalized in the Grammatical Framework, GF. The constructivist idea of formalizing math­ematics piece by piece, in a weak logical framework, rather than trying to reduce everything to one single strong theory, is the model that guides the development of grammars in GF.

Structural proof theory is a branch of logic that studies the general structure and properties of logical and mathematical proofs. This book is both a concise introduction to the central results and methods of structural proof theory, and a work of research that will be of interest to specialists. The book is designed to be used by students of philosophy, mathematics and computer science. The book contains a wealth of results on proof-theoretical systems, including extensions of such systems from logic (...) to mathematics, and on the connection between the two main forms of structural proof theory - natural deduction and sequent calculus. The authors emphasize the computational content of logical results. A special feature of the volume is a computerized system for developing proofs interactively, downloadable from the web and regularly updated. (shrink)

In this paper, we shall present a generalization of phrase structure grammar, in which all functional categories have type restrictions, that is, their argument types are specific domains. In ordinary phrase structure grammar, there is just one universal domain of individuals. The grammar does not make a distinction between verbs and adjectives in terms of domains of applicability. Consequently, it fails to distinguish between sentences like every line intersects every line, which is well typed, and every line intersects every point, (...) which is ill typed.Our generalization relates to ordinary phrase structure grammar in the same way as the higherlevel constructive type theory of Martin-Löf relates to the simple type theory of Church . Simple type theory has been used in linguistics and related with phrase structure grammar, especially in the tradition based on the work of Montague .Our definition of the grammar will be more formal than Montague's in the sense that we shall use a formal metalanguage, that of constructive type theory, for defining both the object language and its interpretation. The grammar, both syntax and semantics, is thus readily implementable in the type-theoretical proof system ALF . Inside type theory, a distinction can be made between the object language and the model, in other words, between syntactic and semantic types. It will turn out that the object language cannot be defined independently of the model, as in ordinary Tarski semantics. This is a direct consequence of introducing the typing restrictions.The grammar presented here can be seen as a formal linguistic elaboration of the work presented in Ranta 1991 and 1994. The organization of generative grammar as categorial grammar followed by sugaring should now look more familiar to the linguist, as the grammatical formalism on which sugaring operates is no longer full type theory but a set of phrase structure trees. (shrink)

This paper shows how a dialogue system for information-seekingdialogues can be implemented in a type-theory-based syntax editor,originally developed for editing mathematical proofs.The implementation gives a simple logical metatheory tosuch dialogue systems and also suggests new functions forthem, e.g., a local undo operation. The method developed provides alogically based declarative way of implementing simple dialoguesystems that is easy to port to new domains.

The aim of this study is to look at the the syntactic calculus of Bar-Hillel and Lambek, including semantic interpretation, from the point of view of constructive type theory. The syntactic calculus is given a formalization that makes it possible to implement it in a type-theoretical proof editor. Such an implementation combines formal syntax and formal semantics, and makes the type-theoretical tools of automatic and interactive reasoning available in grammar.In the formalization, the use of the dependent types of constructive type (...) theory is essential. Dependent types are already needed in the semantics of ordinary Lambek calculus. But they also suggest some natural extensions of the calculus, which are applied to the treatment of morphosyntactic dependencies and to an analysis of selectional restrictions. Finally, directed dependent function types are introduced, corresponding to the types of constructive type theory. (shrink)

Portable Grammar Format (PGF) is a core language for type-theoretical grammars. It is the target language to which grammars written in the high-level formalism Grammatical Framework (GF) are compiled. Low-level and simple, PGF is easy to reason about, so that its language-theoretic properties can be established. It is also easy to write interpreters that perform parsing and generation with PGF grammars, and compilers converting PGF to other formats. This paper gives a concise description of PGF, covering syntax, semantics, and parser (...) generation. It also discusses the technique of embedded grammars, where language processing tasks defined by PGF grammars are integrated in larger systems. (shrink)

En skumrand (poem) av A. Larsen.--Platons øyeblikks-filosofi eller Dialogen Parmenides' 3. hypotese, av E.A. Wyller.--Gresk og israelittisk historiesyn, av T. Boman.--Lukrets, dikter og filosof, av E. Skard.--Amor og Psyche, elskoven og sjelen, av H.P. L'Orange.--Augustins liv og lære, av P. Dietrichson.--Thomas Aquinas' syn på naturvitenskapene, av D. Føllesdal.--Mester Eckehart, av A. Brynildsen.--Renessanse-humanistene og "humanitas," av P. Svendsen.--Striden mellom de gamle og de nye, av A. Aarnes.--Harmonitanken i Schillers filosofiske avhandlinger, av O. Koppang.--Grunntrekk i Wilhelm von Humboldts sprogfilosofi, av I. Dal.--Noen (...) bemerkninger til Dostojevskijs Storinkvisitoren, av E. Krag.--Speculum og analogi i Peer Gynt, av B. Blekastad.--Om pakt-begrepet i "Kristin Lavrandsdatter," av D. Haakonsen.--Subjektivitet og sanning, av H. Skjervheim.--Refleksjoner om helhetssyn, sannhet og kunnskap, av A. Næss.--I tid og rum (poem) av A. Øverland. (shrink)

Name der Zeitschrift: Semiotica Jahrgang: 2015 Heft: 207 Seiten: 127-137.

The early Pleistocene hunt scene was instant: when an antelope jerked in the water edge, the first “drivers” of the hunt were already in motion; the moment of outburst after a long ambush lasted less than second. The sudden hunt movements were typical of every prey-abundant landscape since even earlier geological periods. The analysis of Laetoli footprints made by our evolutionary ancestors more than three millions years ago indicates that in a randomly chosen moment, the landscape was full of animals (...) of different species. The language used in the attack moment has to be agitative, only vowels in clausure between two consonants. During the process of further development, those consonants became more and more similar to delimitators, the borders where intrasemiotic realities translate extrasemiotic environment. Speech is an old Paleolithic tool for directing hunters to the useful positions. It was rather an instrument of a leader than grooming “clicks” of kin’s females. (shrink)

Name der Zeitschrift: Semiotica Jahrgang: 2017 Heft: 215 Seiten: 269-280.

This practical and essential text, co-authored by an engineer and an ethicist, covers ethical dilemmas that any engineer might encounter on the job, emphasizing the responsibility of a practicing engineer to act in an ethical manner. To illustrate the complexities involved, the authors present characters who encounter situations that test the engineering code of ethics. The dialogue between the characters highlights different perspectives of each dilemma. As they proceed through the book, students see how the code of ethics can help (...) in decision making, as well as the implications of various decisions. The philosophical theory that supports the ethical situations encountered is presented as boxed material following each section. Important Notice: Media content referenced within the product description or the product text may not be available in the ebook version. (shrink)

The complexity of chromium chemistry makes it an ideal example of how the Principle of Expediency, first articulated by sanitary pioneer Earle Phelps, can be used in a standard setting. Expediency, defined by Phelps as “the attempt to reduce the numerical measure of probable harm, or the logical measure of existing hazard, to the lowest level that is practicable and feasible within the limitations of financial resources and engineering skill”, can take on negative connotations unless subject to ethical guidance. In (...) this paper we argue that without ethical principles as a rubric for negotiating environmental regulations, communities run the risk of slipping from the Principle of Expediency as defined by Phelps to the alternative usage of expediency meaning that which does not reflect ethical consideration or concern beyond self-serving interest. Three ethical ideals—justice, mercy and humility—are suggested as values to be considered while resolving regulatory issues related to environmental protection. The Principle of Expediency serves as a working principle, but not as a rigid algorithm, for setting regulatory limits for environmental concentrations of waste products like chromium. (shrink)

The theoretical debate on the nature of narrative has been mainly concerned with literary narratives, whereas forms of non-literary and especially pictorial narrativity have been somewhat neglected. In this paper, however, I shall discuss narrativity specifically with regard to pictorial objects in order to clarify how pictorial storytelling may be based on the activation of mentally stored action and scene schemas. Approaches from cognitive psychology, such as the work of Schank, Roger C. & Robert P. Abelson. 1977. Scripts, plans, goals (...) and understanding. Hillsdale, NJ: Lawrence Erlbaum; Mandler, Jean Matter. 1984. Stories, scripts, and scenes: Aspects of schema theory. London/hillsdale, NJ: Lawrence Erlbaum; Schank, Roger C. 1995. Tell me a story: Narrative and intelligence. Evanston, IL: Northwestern University Press, suggest that cognition crucially depends on the storage and retrieval of action scripts or schemata, that is, narrative structures, which may occur at various levels of abstraction. These schemas incorporate generalized knowledge about event sequences, such as the order in which specific events will take place; causal, enabling, or conventionalized relations between these events, and what kind of events occur in certain action sequences. There also are scene schemas that are characterized by spatial rather than temporal relations. Further kinds of schemas seem also to play a decisive role. Drawing upon considerations from schema and script theory, I will focus on some concrete examples of pictorial narration, more specifically depictions of the Annunciation of the Virgin Mary, where narrative schema structures become involved and, indeed, the comprehensibility of the pictures as such presuppose mental script representations. (shrink)

Within cognitive science, narratives are regarded as crucial and fundamental cognitive instruments or tools. As Roger Schank suggests, the identity of (sub-)cultures is to a considerable extent based upon the sharing of narrative structures (Schank. 1995.Tell me a story: Narrative and intelligence. Evanston, IL: Northwestern University Press.). According to Schank, culturally shared stories, as do many other stories, occur frequently in highly abbreviated form, as “skeleton stories” or “gists.” Collective identities are conveyed in and between cultures not only through verbal (...) discourse, but also by pictorial means. Many pictures and visual artworks have indeed been produced in order to establish and to consolidate a home-culture and to demarcate it from conceived extra-cultural counterparts.Some of my previous work on these lines has been concerned with demarcation efforts in visual media of “Jews” as extra-cultural, since the Middle Ages onwards, in the Third Reich’s iconography, as well as in modern, radicalized forms of anti-Semitic picturing in Arab media (Ranta. 2016. The (pictorial) construction of collective identities in the Third Reich.Language and Semiotic Studies2(3). 107–124, Ranta. 2017. Master narratives and the (pictorial) construction of otherness: Anti-semitic images in the Third Reich and beyond.Contemporary Aesthetics15.https://contempaesthetics.org/newvolume/pages/article.php?articleID=765(accessed 17 November 2019.). In building upon and extending this work, I shall focus in the current paper upon attempts of creating cultural and political cohesion by means of pictorial propaganda in post-war China from the early 1950’s onwards, as promoted by the Chinese Communist Party (CCP) under the leadership by Mao Zedong. Some concrete pictorial examples indicating these attempts will be discussed from a narratological and cultural semiotic perspective. (shrink)

Engineering is 'the people-serving profession'. The work of engineers involves interaction with clients, other engineers, and the public at large. More than any other profession, their work also directly involves and affects the environment. This book makes the case that engineers have special professional obligations to protect and enhance the environment, and the authors - one, an engineer and the other, a philosopher - seek to provide an ethical basis for these obligations. In exploring these ethical issues, the authors aim (...) to show that engineers make a difference. The text opens with a series of case studies in which engineers face complex and challenging decisions about the environment. Succeeding chapters examine different ideas about environmental ethics for engineers, including professional codes and both modern and historical discussions of environmental responsibility. The book concludes with a collection of readings that complement the text. Students, as well as practising engineers, will find much of interest in this well-argued and thought-provoking book. (shrink)

The eight pieces constituting this Meeting Report are summaries of presentations made during a panel session at the 2011 Association for Practical and Professional Ethics (APPE) annual meeting held between March 3rd and 6th in Cincinnati. Lisa Newton organized the session and served as chair. The panel of eight consisted both of pioneers in the field and more recent arrivals. It covered a range of topics from how the field has developed to where it should be going, from identification of (...) issues needing further study to problems of training the next generation of engineers and engineering-ethics scholars. (shrink)

So why be a good engineer? There are basically three reasons: 1) possible detection and the harm that dishonorable acts might cause, 2) a common responsibility to the professional engineering community, and 3) a negative impact on one’s own integrity when one behaves badly. But what if, in the face of these arguments, one is still not convinced? I must admit that there appears to be no knock-down ethical argument available to change the mind of a person set on behaving (...) badly. There remains the option to act in whatever way one may wish. Engineers must realize however that bad manners and/or immorality and/or illegality, even if undetected, will most likely result in harm to themselves and thus rational behavior should result in honorable conduct of professional duties. While the Viking society of northern Europe was in many ways cruel and crude, they had a very simple code of honor. Their goal was to live life so that when they died, others would say He was a good man . The definition of what they meant by a good man might be quite different by contemporary standards but the principle is important. If engineers conduct their professional lives so as to uphold the exemplary values of engineering, the greatest professional honor would be to be remembered as a good engineer. (shrink)

Engineers and scientists, whose professional responsibilities often influence the natural environment, have sought to develop an environmental ethic that will be in tune with their attitudes toward the non-human environment, and that will assist them in decision making regarding questions of environmental quality. In this paper the classical traditions in normative ethics are explored in an attempt to formulate such an environmental ethic. I conclude, however, that because the discipline of ethics is directed at person-person interactions, ethics as a scholarly (...) discipline does not help us understand how we ought to treat non-human nature. We therefore cannot look to ethics as a source for understanding our attitudes and for providing guidance to our actions with regard to the environment. To do so is to ask too much of ethics. If we are to find an acceptable environmental morality, it must come from a new paradigm. One approach might be to understand our attitudes on the basis of spirituality, modeled after animistic religions. (shrink)

Engineers and scientists, whose professional responsibilities often influence the natural environment, have sought to develop an environmental ethic that will be in tune with their attitudes toward the non-human environment, and that will assist them in decision making regarding questions of environmental quality. In this paper the classical traditions in normative ethics are explored in an attempt to formulate such an environmental ethic. I conclude, however, that because the discipline of ethics is directed at person-person interactions, ethics as a scholarly (...) discipline does not help us understand how we ought to treat non-human nature. We therefore cannot look to ethics as a source for understanding our attitudes and for providing guidance to our actions with regard to the environment. To do so is to ask too much of ethics.If we are to find an acceptable environmental morality, it must come from a new paradigm. One approach might be to understand our attitudes on the basis of spirituality, modeled after animistic religions. (shrink)

: Professional engineers are bound by their code of ethics to place paramount the health, safety, and welfare of the public. If the "public" includes future people, then the engineer is also morally responsible for not destroying the supporting environment that will make future generations possible. In this essay I suggest that the present engineering codes of ethics are inadequate in addressing the problem of maintaining environmental quality. Engineers can, while staying well within the bounds of the present codes of (...) ethics, destroy or modify the environments that support the global ecosystem and in such manner kill future humans on a grand scale. The moral responsibilities of engineers must therefore include the commitment to provide a high quality and sustainable environment for future generations and this requires that the engineering codes of ethics be modified to encourage engineers to make decisions that promote environmental stability and sustainability. (shrink)

Today, monitoring of patient complaints in healthcare services is being used as a tool for quality assurance systems and in the future development of services. This nationwide register study describes the number of all complaints processed, number of complaints between different state provinces, healthcare services and healthcare professionals, and outcomes of complaints in Finland during the period 2000–2004. All complaints processed at the State Provincial Offices and the National Authority for Medicolegal Affairs were analysed by statistical methods. Complaints about mental (...) healthcare were explored in greater detail. The analysis showed that the number of patient complaints increased considerably during the study period. There were changes in the number of complaints between study years in different provinces. Out of different healthcare services, an especially marked increase was seen in private healthcare. Nearly all complaints were lodged against physicians, and over half of the complaints were made because of medical error. In mental health care, patients more often complained about unsatisfactory certificates and statements and the use of compulsory hospital care. An analysis of the outcomes revealed that in mental health care complaints more seldom led to consequences. The results need to be utilised when planning interventions for advanced supervision, prevention of adverse events and patient safety in healthcare, and especially in mental health care. From the patients’ perspective, it is important to create a culture where most problem situations are handled where the treatment was provided, thus avoiding a complex complaints process. (shrink)

Research on the predictors of outcome for early, community-based, and time-limited interventions targeted for clinical depression in adolescents is still scarce. We examined the role of demographic, psychosocial, and clinical variables as predictors of outcome in a trial conducted in Finnish school health and welfare services to identify factors associating to symptom reduction and remission after a brief depression treatment. A total of 55 12–16-year-olds with mild to moderate depression received six sessions of either interpersonal counseling for adolescents or brief (...) psychosocial support. Both interventions resulted in clinical improvement at end of treatment and 3- and 6-month follow-ups. Main outcome measures were self-rated BDI-21 and clinician-rated Adolescent Depression Rating Scale. Latent change score models were used to identify predictors of change in depressive symptom scores and clinical remission at end of treatment and 3- and 6-month follow-ups over the combined brief intervention group. Symptom improvement was predicted by younger age and having a close relationship with parents. Both symptom improvement and clinical remission were predicted by male gender, not having comorbid anxiety disorder, and not having sleep difficulties. Our results add to knowledge on factors associating with good treatment outcome after a brief community intervention for adolescent depression. Brief depression interventions may be useful and feasible especially for treatment of mild and moderate depression among younger adolescents and boys, on the other hand clinicians may need to cautiously examine sleep problems and anxiety comorbidity as markers of the need for longer treatment. (shrink)

In the article, I discuss some ideas of the type theoretical grammar of Aarne Ranta and the analysis of the problem of Quine (Ralph and Ortcutt), which Oleg Domanov implemented by means of this theory. There are more similarities than differences in TT grammar with well-known ideas, including “fine grinding” of meanings, counterparts, procedural understanding of – intensions. The main problem, which, in my opinion, exists in the TT grammar, consists in understanding how another agent’s epistemic attitudes can (...) be justified for me. Ranta proceeds from the metaphor of the agent as a calculator, which for the general case is unacceptable. I believe that the interpretation of the epistemic attitudes of another agent must be externalistic, that is, referring not to the agent’s worlds, but to his actions in the actual world: “agent X believes that A” is true when the interpreter sees the behavior of the agent in situations that the interpreter would consider adequate for himself if he believed A and would be “in place” of X. To formalize here, it would take complicated tools which are used for describing actions. I’ve come to the conclusion that an understanding of the type in TT grammar makes it intensional in some extended sense, since the working with the naming relation is already an element of a specific pragmatics. (shrink)

PREFACEProf. Göran Sundholm of Leiden University inspired the group of Logic at Lille and Valparaíso to start a fundamental review of the dialogical conception of logic by linking it to constructive type logic. One of Sundholm's insights was that inference can be seen as involving an implicit interlocutor. This led to several investigations aimed at exploring the consequences of joining winning strategies to the proof-theoretical conception of meaning. The leading idea is, roughly, that while introduction rules lay down the conditions (...) under which a winning strategy for the Proponent may be built, the elimination rules lay down those elements of the Opponent's assertions that the Proponent has the right to use for building winning strategy. It is the pragmatic and ethical features of obligations and rights that naturally lead to the dialogical interpretation of natural deduction.During the Visiting Professorship of Prof. Sundholm at Lille in (2012) the group of Lille started delving into the ways of implementing Per Martin-Löf's Constructive Type Theory with the dialogical perspective. In particular, Aarne Ranta's (1988) paper, the first publication on the subject, was read and discussed during Sundholm’s seminar. The discussions strongly suggested that the game-theoretical conception of quantifiers as deploying interdependent moves provide a natural link between CTT and dialogical logic. This idea triggered several publications by the group of Lille in collaboration with Nicolas Clerbout and Juan Redmond at the University of Valparaíso, including the publication of the book (2015) by Clerbout / Rahman that provides a systematic development of this way of linking CTT and the dialogical conception of logic. However the Clerbout / Rahman book was written from the CTT perspective on dialogical logic, rather than the other way round. The present book should provide the perspective from the other side of the dialogue between the Dialogical Framework and Constructive Type Theory. The main idea of our present study is that Sundholm's (1997) notion of epistemic assumption is closely linked to the Copy-Cat Rule or Socratic Rule that distinguishes the dialogical framework from other game-theoretical approaches. One way to read the present book is as a further development of Sundholm’s extension of Austin's (1946, p. 171) remark on acts of assertion to inference. Indeed, Sundholm (2013, p. 17) gave the following forceful formulation: When I say therefore, I give others my authority for asserting the conclusion, given theirs for asserting the premisses.Per Martin-Löf, in recent lectures, have utilized the dialogical perspective on epistemic assumptions to get out of a certain circle that threatens the explanation of the notions of inference and demonstration. A demonstration may be explained as a chain of (immediate) inferences starting from no premisses. That an inference J1... Jn—————Jis valid means that the conclusion J can be made evident on the assumption that J1, …, Jn are known. The notion of epistemic assumption thus enters in the explanation of valid inference. We cannot, however, in this explanation understand 'known' in the sense of demonstrated, for then we are explaining the notion of inference in terms of demonstration, whereas demonstration has been explained in terms of inference. Martin-Löf suggests that we here understand 'known' in the sense of asserted, so that epistemic assumptions are judgements others have made, judgements for which others have taken the responsibility; that the inference is valid then means that, given that others have taken responsbility for the premisses, I can take responsibility for the conclusion:The circularity problem is this: if you define a demonstration to be a chain of immediate inferences, then you are defining demonstration in terms of inference. Now we are considering an immediate inference and we are trying to give a proper explanation of that; but, if that begins by saying: Assume that J1, …, Jn have been demonstrated – then you are clearly in trouble, because you are about to explain demonstration in terms of the notion of immediate inference, hence when you are giving an account of the notion of immediate inference, the notion of demonstration is not yet at your disposal. So, to say: Assume that J1, …, Jn have already been demonstrated, makes you accusable of trying to explain things in a circle. The solution to this circularity problem, it seems to me now, comes naturally out of this dialogical analysis. […]The solution is that the premisses here should not be assumed to be known in the qualified sense, that is, to be demonstrated, but we should simply assume that they have been asserted, which is to say that others have taken responsibility for them, and then the question for me is whether I can take responsibility for the conclusion. So, the assumption is merely that they have been asserted, not that they have been demonstrated. That seems to me to be the appropriate definition of epistemic assumption in Sundholm's sense. One of the main tenets of the present study is that the further move of relating the Socratic Rule rule with judgemental equality provides both a simpler and more direct way to implement the constructive type theoretical approach within the dialogical framework. Such a reconsideration of the Socratic Rule, roughly speaking, amounts to the following. 1.A move from P that brings-forward a play-object in order to defend an elementary proposition A can be challenged by O. 2.The answer to such a challenge, involves P bringing forward a definitional equality that expresses the fact that the play-object chosen by P copies the one O has chosen while positing A. For short, the equality expresses at the object-languaje level that the defence of P relies on the authority given to O to be able to produce the play-objects she brings forward. More generally, according to this view, a definitional equality established by P and brought forward while defending the proposition A, expresses the equality between a play-object (introduced by O) and the instruction for building a play-object deployed by O while affirming A. So it can be read as a computation rule that indicates how to compute O's instructions. Let us recall that from the strategic point of view, O's moves correspond to elimination rules of demonstrations. Thus, the dialogical rules that prescribe how to introduce a definitional equality – correspond – at the strategic level – to the definitional equality rules for CTT as applied to the selector-functions involved in the elimination rules. So, what we are doing here is extending the dialogical interpretation of Sundholm's epistemic assumption to the rules that set up the definitional equality of a type.The present work is structured in the following way:•In the Introduction we state the main tenets that guide our book•Chapter II contains a brief overview of Constructive Type Theory penned by Ansten Klev with exercises and their solutions. •Chapter III offers a novel presentation of the dialogical conception of logic. In fact, the first two sections of the chapter provide an overview of standard dialogical logic – including solved exercises, slightly adapted to the content of the present volume. The rest of the sections develop a new dialogical approach to Constructive Type Theory. •Chapters IV and V contain the main body of our study, namely the relation between the Socratic Rule, epistemic assumptions, and equality. The chapter provides the reader with thoroughly worked out examples with comments. •After the Final Remarks the book containsa.An appendix containing a an overview of all the rules for the new formulation of dialogical approach to constructive type theory developed in the book; b.a brief outline of Per Martin-Löf's informal presentation of the demonstration of the axiom of choice.c.two examples of a tree-shaped graph of an extensive strategy. Acknowledgments: Many thanks to Mark van Atten (Paris1), Giuliano Bacigalupo (Zürich), Charles Zacharie Bowao (Univ. Ma Ngouabi de Brazzaville, Congo), Christian Berner (Lille3), Michel Crubellier (Lille3), Pierre Cardascia (Lille3), Oumar Dia (Dakar), Marcel Nguimbi ((Univ. Marien Ngouabi de Brazzaville, Congo), Adjoua Bernadette Dango (Lille3 / Alassane Ouattara de Bouaké, Côte d'Ivoire), Steephen Rossy Eckoubili (Lille3), Johan Georg Granström (Zürich), Gerhard Heinzmann (Nancy2), Muhammad Iqbal (Lille3), Matthieu Fontaine (Lille3), Radmila Jovanovic (Belgrad), Hanna Karpenko (Lille3), Laurent Keiff (Lille3), Sébastien Magnier (Saint Dennis, Réunion), Clément Lion (Lille3), Gildas Nzokou (Libreville), Fachrur Rozie (Lille3), Helge Rückert (Mannheim), Mohammad Shafiei (Paris1), and Hassan Tahiri (Lisbon), for rich interchanges, suggestions on the main claims of the present study and proof-reading of specific sections of the text. Special thanks to Gildas Nzokou (Libreville), Steephen Rossy Eckoubili (Lille3) and Clément Lion (Lille3), with whom a Pre-Graduate Textbook in French on dialogical logic and CTT is in the process of being worked out – during the visiting-professorship in 2016 of the former. Eckoubili is the author of the sections on exercises for dialogical logic, Nzokou cared of those involving the development of CTT-demonstrations out of winning-strategies. Special thanks also to Ansten Klev (Prague) for helping with technical details and conceptual issues on CTT, particularly so as author of the chapter introducing CTT. (shrink)