L. Notons-ici-que, P. ??-est-une-instruction-qui-engage, and E. A3, dans notre exemple la structure du jeu l'engage à défendre la proposition existentielle (?y : D)A(y) associée à cette instruction. 1. an elementary posit by P preceded by a O-posit of ?, 2. an elementary posit by P (different to the preceeding case) 3. a P-move " sic(n) " for some move numbered n 4. a P-equality that results from applying the Socratic Rule But all this is guaranteed by steps

O. L^, A [!, 10] 11, 10] 13. O ! c 2.2 : C [!
URL : https://hal.archives-ouvertes.fr/hal-00143882

P. L^, A [!, 17] 18. P ! R^(d 1 ): B [!, 17] 18

P. Aczel, The Type Theoretic Interpretation of Constructive Set Theory, Logic Colloquium 77, pp.55-66, 1978.
DOI : 10.1016/S0049-237X(08)71989-X

J. Almog, The What and the How, The Journal of Philosophy, vol.88, issue.5, pp.225-244, 1991.
DOI : 10.2307/2026927

J. L. Austin, Other Minds " . The Aristotelian Society Supplementary Volume, pp.148-187, 1946.

. Barnes, The Complete Works of Aristotle. The Revised Oxford Translation, Princeton NJ, 1984.

M. Beirlaen and M. Fontaine, Inconsistency-Adaptive Dialogical Logic". Logica Universalis. Online first, DOI 10 The Axiom of Choice, 2009.
DOI : 10.1007/s11787-016-0139-y

E. Bishop, Foundations of constructive mathematics, 1967.

R. Brandom, Making it Explicit, 1994.

R. Brandom, Articulating Reasons, 2000.

W. Breckenridge and O. Magidor, Arbitrary reference, Philosophical Studies, vol.57, issue.3, pp.377-400, 2012.
DOI : 10.1007/s11098-010-9676-z

P. Cardascia, Dialogique des matrices, Revista de Humanidades de Valparaíso, 2016.
DOI : 10.22370/rhv/20156/36

R. Carnap, Logische Syntax der Sprache, 1934.
DOI : 10.1007/978-3-662-25376-2

A. Church, The Calculi of Lambda Conversion, 1941.

N. Clerbout, First-Order Dialogical Games and Tableaux, Journal of Philosophical Logic, vol.127, issue.4, pp.785-801, 2014.
DOI : 10.1007/s10992-013-9289-z

N. Clerbout, Etude sur quelques semantiques dialogiques: Concepts fondamentaux et éléments de metathéorie, 2014.

N. Clerbout, Finiteness of Plays and the Dialogical Problem of Decidability, IfCoLog Journal of Logics and their Applications, vol.1, issue.1, pp.115-130, 2014.

N. Clerbout, M. H. Gorisse, and S. Rahman, Context-Sensitivity in Jain Philosophy: A Dialogical Study of Siddhar???iga???i???s Commentary on the Handbook of Logic, Journal of Philosophical Logic, vol.40, issue.5, pp.633-662, 2011.
DOI : 10.1007/s10992-010-9164-0

N. Clerbout and S. Rahman, Linking Game-Theoretical Approaches with Constructive Type Theory: Dialogical Strategies as CTT-Demonstrations, 2015.
DOI : 10.1007/978-3-319-19063-1

J. Corcoran, Aristotle???s Natural Deduction System, Synthese Historical Library, vol.9, pp.85-131, 1974.
DOI : 10.1007/978-94-010-2130-2_6

M. Crubellier, The Programme of Aristotelian Analytics, Dialogues, Logics and Other Strange Things. Essays in honour of Shahid Rahman, pp.103-129, 2008.

M. Crubellier, Aristote, Premiers Analytiques ; traduction, introduction et commentaire, 2014.

B. and H. Curry, Outlines of a Formalist Philosophy of Mathematics, 1952.

A. B. Dango, Des dialogues aux tableaux dans le contexte de révision des croyances : De l'oralité à l'écriture, C. Bowao et S. Rahman (éd.) Entre l'orature et l'écriture : Relations croisées, pp.175-192, 2014.

A. B. Dango, Interaction et révision de croyances, Revista de Humanidades de Valparaíso, pp.75-98, 2015.
DOI : 10.22370/rhv/20155/30

A. B. Dango, Approche dialogique de la révision des croyances dans le contexte de la théorie constructive des types, 2016.

R. Diaconescu, Axiom of choice and complementation, Proc. Amer, pp.176-178, 1975.
DOI : 10.1090/S0002-9939-1975-0373893-X

J. Diller and A. Troelstra, Realizability and intuitionistic logic, Synthese, vol.39, issue.2, pp.253-282, 1984.
DOI : 10.1007/BF00485463

M. Dummett, Frege. Philosophy of Language, 1973.

C. Dutilh-novaes and . Dialectica, A Dialogical, Multi-Agent Account of the Normativity of Logic, Dialectica, vol.50, issue.3, pp.587-609, 2015.
DOI : 10.1111/1746-8361.12118

K. Ebbinghaus, Ein formales Modell der Syllogistik des Aristoteles, 1964.

W. Felscher, Dialogues as a foundation for intuitionistic logic, Handbook of Philosophical Logic, pp.341-372, 1985.
DOI : 10.1007/978-94-009-5203-4_5

M. Fontaine, Argumentation et engagement ontologique. Être, c'est être choisi, 2013.
URL : https://hal.archives-ouvertes.fr/tel-01137248

A. Fraenkel, Y. Bar-hillel, and A. Levy, Foundations of Set Theory, 1973.

G. Frege, Über Sinn und Bedeutung". Zeitschrift für Philosophie und philosophische Kritik, Frege, pp.25-50, 1892.

G. Frege, Grundgesetze der Arithmetik I, 1893.

R. Garner, On the strength of dependent products in the type theory of Martin-L??f, Annals of Pure and Applied Logic, vol.160, issue.1, pp.1-12, 2009.
DOI : 10.1016/j.apal.2008.12.003

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1933.
DOI : 10.1007/BF01201353

G. Gentzen, The Collected Papers of Gehard Gentzen, 1969.

N. D. Goodman and J. Myhill, Choice Implies Excluded Middle, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, p.461, 1978.
DOI : 10.1002/malq.19780242514

J. Granström, Treatise on Intuitionistic Type Theory, 2011.
DOI : 10.1007/978-94-007-1736-7

B. Hale and C. Wright, To Bury Caesar .??.??., The Reason's Proper Study, pp.335-396, 2001.
DOI : 10.1093/0198236395.003.0015

G. W. Hegel, Wissenschaft der Logik, 1999.

G. W. Hegel, The Science of Logic, 2010.

J. Hintikka, Logic, Language-Games and Information: Kantian Themes in the Philosophy of Logic, 1973.

J. Hintikka, Game-theoretical semantics: insights and prospects., Notre Dame Journal of Formal Logic, vol.23, issue.2, pp.219-249, 1983.
DOI : 10.1305/ndjfl/1093883627
URL : http://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093883627

J. Hintikka, The Principles of Mathematics Revisited, 1996.
DOI : 10.1017/CBO9780511624919

J. Hintikka, Lingua Universalis vs. Calculus Ratiocinator: An Ultimate Presupposition of Twentieth-Century Philosophy, 1996.
DOI : 10.1007/978-94-015-8601-6

J. Hintikka, Intuitionistic Logic as Epistemic Logic, Synthese, vol.127, issue.1/2, pp.7-19, 2001.
DOI : 10.1023/A:1010357829038

M. Hofmann, Extensional Concepts in Intensional Type Theory, 1995.
DOI : 10.1007/978-1-4471-0963-1

M. Hofmann and T. Streicher, The groupoid interpretation of type theory, Twenty-five Years of Constructive Type Theory, pp.83-111, 1998.

W. A. Howard, The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980.

V. Ilievski, Language and Knowledge in Plato's Cratylus and beyond it, Journal of Philosophical Inquiry, vol.2, issue.35, p.925, 2013.

R. Jovanovic, Hintikkas Take on the Axiom of Choice and the Constructivist Challenge, Revista de Humanidades de Valparaiso, pp.135-152, 2013.

R. Jovanovic, Hintikkas Take on Realism and the Constructivist Challenge, 2015.

L. Keiff, Le Pluralisme Dialogique: Approches dynamiques de largumentation formelle, 2007.

L. Keiff, Dialogical Logic, The Stanford Encyclopedia of Philosophy, 2009.

A. Klev, Categories and Logical Syntax, 2014.

E. C. Krabbe and E. C. , Studies in Dialogical Logic, 1982.

E. C. Krabbe, Formal systems of dialogue rules, Synthese, pp.295-328, 1985.
DOI : 10.1007/BF00485598

E. C. Krabbe, Dialogue logic, Handbook of the History of Logic, pp.665-704, 2006.
DOI : 10.1016/S1874-5857(06)80035-X

K. Lorenz, Elemente der Sprachkritik.Eine Alternative zum Dogmatismus und Skeptizismus in der Analytischen Philosophie, 1970.

K. Lorenz, Basic objectives of dialogue logic in historical perspective, pp.255-263, 2001.

K. Lorenz, Logic, Language and Method: On Polarities in Human Experience, 2010.
DOI : 10.1515/9783110216790

K. Lorenz, Philosophische Variationen: Gesammelte Aufstze unter Einschluss gemeinsam mit J¨urgen Mittelstraß geschriebener Arbeiten zu Platon und Leibniz, 2010.
DOI : 10.1515/9783110218800

K. Lorenz, J. Mittelstrass, and J. , RECONSIDERED, Mind, vol.LXXVI, issue.301, pp.301-302, 1967.
DOI : 10.1093/mind/LXXVI.301.1

P. Lorenzen, Einfürung in die operative Logik und Mathematik, 1955.
DOI : 10.1007/978-3-642-86518-3

P. Lorenzen, Normative Logic and Ethics, 1969.

P. Lorenzen and O. Schwemmer, Konstruktive Logik, Ethik und Wissenschaftstheorie, Mannheim: Bibliographisches Institut, 1975.
DOI : 10.1007/978-3-322-96251-5_1

P. Lorenzen and K. Lorenz, Dialogische Logik, 1978.

J. V. Luce, Plato On Truth And Falsity In Names, The Classical Quarterly, vol.19, issue.02, pp.222-232, 1969.
DOI : 10.1017/S0009838800024630

J. Lukasiewicz, Aristotle's Syllogistic from the Standpoint of Modern Formal Logic, 1957.

S. Magnier, Approche dialogique de la dynamique épistémique et de la condition juridique, 2013.

M. Marion, Hintikka on Wittgenstein: From language games to game semantics, Acta Philosophica Fennica, vol.78, pp.223-242, 2006.

M. Marion, Why Play Logical Games?, Games: Unifying Logic, Language and Philosophy, pp.3-26, 2009.
DOI : 10.1007/978-1-4020-9374-6_1

M. Marion, Between saying and doing: From Lorenzen to Brandom and Back, 2010.

M. Marion and H. Rückert, Aristotle on Universal Quantification: A Study from the Point of View of Game Semantics, History and Philosophy of Logic, vol.21, issue.4, pp.201-229, 2015.
DOI : 10.1017/CBO9780511518508

P. Martin-löf, Hauptsatz for the intuitionistic theory of iterated inductive def-initions, Proceedings of the Second Scandinavian Logic Symposium, pp.179-216, 1971.

P. Martin-löf, About Models for Intuitionistic Type Theories and the Notion of Definitional Equality, Proceedings of the Third Scandinavian Logic Symposium, pp.81-109, 1975.
DOI : 10.1016/S0049-237X(08)70727-4

P. Martin-löf, An Intuitionistic Theory of Types: Predicative Part, Logic Colloquium '73. Amterdam: North-Holland, pp.73-118, 1975.
DOI : 10.1016/S0049-237X(08)71945-1

P. Martin-löf, Constructive Mathematics and Computer Programming, Logic, Methodology and Philosophy of Science VI, pp.153-175, 1979.
DOI : 10.1016/S0049-237X(09)70189-2

P. Martin-löf, Intuitionistic Type Theory. Notes by Giovanni Sambin of a series of lectures given in Padua, 1980.

P. Martin-löf, Substitution calculus". Lecture notes. Avail-able at http://archivepml .github.io/martin-lof/pdfs/ Substitution-calculus-1992, 1992.

P. Martin-löf, On the meanings of the logical constants and the justifications of the logical laws, Nordic Journal of Philosophical Logic, vol.1, pp.11-60, 1996.

P. Martin-löf, 100 years of Zermelo's axiom of choice: what was the problem with it?". The Computer Journal, pp.345-350, 2006.

P. Martin-löf, When did 'judgement' come to be a term of logic?". Lecture held at Ecole Normale Supérieure on 14, 2011.

P. Martin-löf, Truth of empirical propositions". Lecture held at the University of Leiden, Transcription by Amsten Klev, 2014.

P. Martin-löf, Is logic part of normative ethics?". Lecture held at the research unity Sciences, normes, décision (FRE 3593, 2015.

B. Nordström, K. Petersson, and J. M. Smith, Programming in Martin-Löf's Type Theory: An Introduction, 1990.

B. Nordström, K. Petersson, and J. M. Smith, Martin-Löf's type theory Logic and Algebraic Methods, Handbook of Logic in Computer Science, pp.1-37, 2000.

G. Nzokou, Logique de l'argumentation dans les traditions orales africaines, 2013.

T. Piecha, Formal Dialogue Semantics for Definitional Reasoning and Implications as Rules, 2012.

T. Piecha and P. Schroeder-heister, Implications as Rules in Dialogical Semantics The Logica Yearbook, pp.211-225, 2011.

A. Popek, Logical dialogues from Middle Ages, 2012.

. Salguero, Logic of Knowledge, Theory and Applications, pp.223-244

D. Prawitz, Natural Deduction, 1965.

G. Primiero, Information and Knowledge, 2008.
DOI : 10.1007/978-1-4020-6170-7

W. V. Quine, Ontological Relativity and Other Essays, 1969.

S. Rahman, Über Dialogue, Protologische Kategorien und andere Seltenheiten, 1993.

S. Rahman and N. Clerbout, Constructive Type Theory and the Dialogical Approach to Meaning, Baltic International Yearbook of Cognition, Logic and Communication, vol.8, issue.1, 2013.
DOI : 10.4148/1944-3676.1077
URL : https://hal.archives-ouvertes.fr/halshs-01225723

S. Rahman and N. Clerbout, Constructive Type Theory and the Dialogical Turn ? A new Approach to Erlangen Constructivism, Dialogische Logik, pp.91-148, 2015.

S. Rahman, N. Clerbout, and L. Keiff, On dialogues and natural deduction, 2009.
URL : https://hal.archives-ouvertes.fr/halshs-00713187

. Rahman, Acts of Knowledge: History, Philosophy and Logic: Essays Dedicated to Göran Sundholm, pp.301-336

S. Rahman, N. Clerbout, and R. Jovanovic, The Dialogical Take on Martin-Löf's Proof of the Axiom of Choice, South American Journal of Logic, vol.1, issue.1, pp.179-208, 2015.

S. Rahman, N. Clerbout, and Z. M. Conaughey, On play objects in dialogical games. Towards a Dialogical approach to Constructive Type Theory, Modestly radical or radically modes . Festschrift for Jean-Paul van Bendegem, pp.127-154, 2014.

S. Rahman and /. J. Granström, IBN S??N?????S APPROACH TO EQUALITY AND UNITY, Arabic Sciences and Philosophy, vol.24, issue.02, pp.297-307, 2014.
DOI : 10.2307/2219014
URL : https://halshs.archives-ouvertes.fr/halshs-01216178/document

S. Rahman, Z. Conaughey, and M. Crubellier, A Dialogical Framework for Aristotle's Syllogism, 2015.

S. Rahman and L. Keiff, On How to Be a Dialogician, Logic, Thought, and Action, pp.359-408, 2005.
DOI : 10.1007/1-4020-3167-X_17
URL : https://hal.archives-ouvertes.fr/halshs-00195931

S. Rahman and L. Keiff, La Dialectique entre logique et rhetorique, pp.149-178, 2010.
URL : https://hal.archives-ouvertes.fr/halshs-01216206

S. Rahman and J. Redmond, A Dialogical Frame for Fictions as Hypothetical Objects, Filosofia Unisinos, vol.16, issue.1, pp.2-21, 2015.
URL : https://hal.archives-ouvertes.fr/halshs-01216227

S. Rahman and J. Redmond, Armonía DialógicaTeoría Constructiva de Tipos y Reglas para Jugadores Anónimos " (Dialogical Harmony: Tonk, Constructive Type Theory and Rules for Anonymous Players"), Theoria. S. Rahman/J. Redmond. (ISI), vol.31, issue.1, pp.27-53, 2016.

S. Rahman and T. Tulenheimo, From Games to Dialogues and Back, Games: Unifying Logic, Language and Philosophy, pp.153-208, 2009.
DOI : 10.1007/978-1-4020-9374-6_8
URL : https://hal.archives-ouvertes.fr/halshs-00713228

A. Ranta, Propositions as games as types, Synthese, vol.42, issue.3, pp.377-395, 1988.
DOI : 10.1007/BF00869607

A. Ranta, Type-Theoretical Grammar, 1994.

R. Recorde, The Whetstone of Witte, 1577.

J. Redmond, Logique dynamique de la fiction: Pour une approche dialogique, 2010.

J. Redmond and M. Fontaine, How to Play Dialogues: An Introduction to Dialogical Logic, 2011.

J. Redmond and S. Rahman, Armon??a Dial??gica: tonk, Teor??a Constructiva de Tipos y Reglas para Jugadores An??nimos, THEORIA. An International Journal for Theory, History and Foundations of Science, vol.31, issue.1, pp.31-58, 2016.
DOI : 10.1387/theoria.13949

H. Rückert, Dialogues as a Dynamic Framework for Logic, 2011.

H. Rückert, The conception of validity in dialogical logic, Talk at the workshop Proofs and Dialogues, 2011.

P. Schroeder-heister, A natural extension of natural deduction, The Journal of Symbolic Logic, vol.36, issue.04, pp.1284-1300, 1984.
DOI : 10.1007/978-94-009-9825-4_2

P. Schroeder-heister, Lorenzen's operative justification of intuitionisitic logic, One Hundred Years of Intuitionism Basel: Birkhäuser, pp.214-240, 1907.

R. Smith, What is Aristotelian Ecthesis?, History and Philosophy of Logic, vol.23, issue.2, pp.113-127, 1982.
DOI : 10.1080/01445348208837035

G. Sundholm, Implicit epistemic aspects of constructive logic, Journal of Logic, Language and Information, vol.6, issue.2, pp.191-212, 1997.
DOI : 10.1023/A:1008266418092

G. Sundholm, Inference versus Consequence The Logica Yearbook, Filosofia, pp.26-36, 1997.

G. Sundholm, A Plea for Logical Atavism The Logica Yearbook, Filosofia, pp.151-162, 2000.

B. G. Sundholm, Semantic Values for Natural Deduction Derivations, Synthese, pp.623-638, 2006.
DOI : 10.1007/s11229-004-6298-z

B. G. Sundholm, A century of judgement and inference, 1837-1936: Some strands in the development of logic The Development of Modern Logic, pp.263-317, 2009.

G. Sundholm, Inference versus consequence" revisited: inference, conditional, implication " Synthese, pp.943-956, 2012.
DOI : 10.1007/s11229-011-9901-0
URL : http://dx.doi.org/10.1007/s11229-011-9901-0

G. Sundholm, Inference and Consequence in an Interpeted Language, Talk at the Workshop PROOF THEORY AND PHILOSOPHY, 2013.

G. Sundholm, Containment and Variation; Two Strands in the Development of Analyticity from Aristotle to Martin-Löf Judgement and the Epistemic Foundation of Logic, pp.23-35, 2013.

G. Sundholm, Independence Friendly Language is First Order after all, 2016.

A. Tasistro, Formulation of Martin-Löf's theory of types with explicit substi-tutions, 1993.

S. Thompson, Type Theory and Functional Programming, 1991.

J. Van-heijenoort, Logic as calculus and logic as language, Synthese, vol.17, issue.1, pp.324-330, 1967.
DOI : 10.1007/BF00485036

E. Zermelo, Beweis, da??? jede Menge wohlgeordnet werden kann, Mathematische Annalen, vol.59, issue.4, pp.514-530, 1904.
DOI : 10.1007/BF01445300

E. Zermelo, Untersuchungen ???ber die Grundlagen der Mengenlehre. I, Mathematische Annalen, vol.65, issue.2, pp.261-281, 1908.
DOI : 10.1007/BF01449999

E. Zermelo and E. , Über Grenzzahlen und Mengenbereiche, Fundamenta Mathemat-icae, vol.16, pp.29-47, 1930.