Clerbout Nicolas - Linking game-theoretical approaches with constructive type theory : dialogical strategies, CTT demonstrations and the axiom of choice

Linking game-theoretical approaches with constructive type theory : dialogical strategies, CTT demonstrations and the axiom of choice — read online for free the complete book (whole text) full work

Below is the text of the book, divided by pages. System saving the place of the last page read, allows you to conveniently read the book "Linking game-theoretical approaches with constructive type theory : dialogical strategies, CTT demonstrations and the axiom of choice" online for free, without having to search again every time where you left off. Put a bookmark, and you can go to the page where you finished reading at any time.

Light

Font size:

↓

↑

Georgia Tahoma Arial Verdana

Reset

Interval:

↓

↑

Bookmark:

Make

1234567...57

The Author(s) 2015

Nicolas Clerbout and Shahid Rahman Linking Game-Theoretical Approaches with Constructive Type Theory SpringerBriefs in Philosophy 10.1007/978-3-319-19063-1_1

1. Brief Reminder of Constructive Type Theory

Nicolas Clerbout 1

(1)

Instituto de Filosofa; CDHACS, Universidad de Valparaso, Valparaso, Chile

(2)

UMR-CNRS 8163: STL, University of Lille III, Villeneuve dAscq, France

Nicolas Clerbout (Corresponding author)

Email:

Shahid Rahman

Email:

Within Per Martin-Lfs Constructive Type Theory (CTT for short) the logical constants are interpreted through the Curry-Howard correspondence between propositions and sets. A proposition is interpreted as a set whose elements represent the proofs of the proposition. It is also possible to view a set as a problem description in a way similar to Kolmogorovs explanation of the intuitionistic propositional calculus. In particular, a set can be seen as a specification of a programming problem: the elements of the set are then the programs that satisfy the specification (Martin-Lf We will start by a quick overview of the principles of the CTT approach. We will then recall the rules of intuitionistic predicate logic in CTT.

1.1 Fundamentals of the CTT Approach

The general philosophical idea is linked to what has been called the full interpreted, p. 2), to avoid keeping content and form apart. Instead we will at the same time display certain forms of judgement and inference that are used in mathematical proofs and explain them semantically. Thus, we make explicit what is usually implicitly taken for granted. The explicitation task involves bringing into the object language level features that determine meaning and that are usually formulated at the metalevel.

According to the CTT view, premisses and conclusion of a logical inference are not propositions but judgements.

A rule of inference is justified by explaining the conclusion on the assumption that the premisses are known. Hence, before a rule of inference can be justified, it must be explained what it is that we must know in order to have the right to make a judgement of any one of the various forms that the premisses and conclusion can have (Martin-Lf , p. 2).

Two further basic tenets of CTT are the following:

No entity without type

No type without identity

Accordingly, we can take the assertion that an individual is an element of the set A as the assertion that that individual instantiates or exemplifies type A . But what is a type, and how do we differentiate between its examples and those objects that are not of a given type? Or, more fundamentally, what must we know in order to have the right to judge something as a type?

In CTT, a set is defined by specifying its canonical elements , the elements that directly exemplify the type, and its non-canonical ones, the elements that can be shown, using some prescribed method of transformation, that they are equal (in the type) to a canonical one. Moreover, it is required that the equality between objects of a type be an equivalence relation. This is what the second tenet is about: the introduction of an equivalence relation in a set (an object of the type set ).

When we have a type we know, from the semantic explanation of what it means to be a type, what the conditions are for being an object of that type. So if A is a type and we have an object b that satisfies the corresponding conditions, then b is an object of type A , which we formally write b : A . Accordingly,

Set itself does not instantiate the type set , since we do not have a general method for generating all possible ways of building a set. However, given the type set we can build the objects that instantiate it by the means described above. Certain propositional functions can be defined on such a set(-object) once it has been generated. Moreover, the type set is one of an infinite number of types: there are other types, such as the type prop .

Hypotheticals :

The judgements we have introduced so far do not depend on any assumptions. They are categorical judgements. The CTT language has also hypothetical judgements of the form

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 b is an element of the set B , under the assumption that x is an element of A :

The explicit introduction of hypotheticals comes with the explicit introduction of appropriate substitution rules. Indeed in the example above, if a : A , then the substitution in b of x by a yields an element of B ; and if , then the substitutions in b of x by a and by c are equal elements in B :

As pointed out by Granstrm (, p. 112), the form of judgement or can be generalized in three directions:

(1)

Any number of hypotheses 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 the variable introduced.

Such a list of hypotheses will be called a context. Thus we might need the forms of judgement

In general, a hypothetical judgement has the form

where we already know that is a type, is a type in the context , ..., and is a type in the context

Next page

1234567...57

Light

Font size:

↓

↑

Georgia Tahoma Arial Verdana

Reset

Interval:

↓

↑

Bookmark:

Make

Similar books «Linking game-theoretical approaches with constructive type theory : dialogical strategies, CTT demonstrations and the axiom of choice»

Look at similar books to Linking game-theoretical approaches with constructive type theory : dialogical strategies, CTT demonstrations and the axiom of choice. We have selected literature similar in name and meaning in the hope of providing readers with more options to find new, interesting, not yet read works.

Donald N. Levine

Dialogical Social Theory

Prajit K. Dutta

Strategies and Games, second edition: Theory and Practice

Jeffrey Carpenter

Game Theory and Behavior

Thompson

The Domestication of Critical Theory

Coddington Alan

Theories of the Bargaining Process

Rudolf Taschner

Game Changers: Stories of the Revolutionary Minds behind Game Theory

Raymond M. Smullyan

A Beginner’s Further Guide to Mathematical Logic

Elias

The Fragment: Towards a History and Poetics of a Performative Genre

Daniel W. Cunningham

Set Theory: A First Course

Hubert J.M. Hermans

The Dialogical Self in Psychotherapy: An Introduction

Gaisi Takeuti

Proof Theory

Jörgen W. Weibull

Evolutionary game theory

Discussion, reviews of the book Linking game-theoretical approaches with constructive type theory : dialogical strategies, CTT demonstrations and the axiom of choice and just readers' own opinions. Leave your comments, write what you think about the work, its meaning or the main characters. Specify what exactly you liked and what you didn't like, and why you think so.