Type-Theoretical Approaches to Problems and Solutions

k 2015

Type-Theoretical Approaches to Problems and Solutions

PEZLAR, Ivo

Basic information

Original name

Type-Theoretical Approaches to Problems and Solutions

Authors

PEZLAR, Ivo (203 Czech Republic, guarantor, belonging to the institution)

Edition

15th Congress of Logic, Methodology and Philosophy of Science, 3.-8. August, 2015, Helsinki, 2015

Other information

Language

English

Type of outcome

Prezentace na konferencích

Field of Study

60300 6.3 Philosophy, Ethics and Religion

Country of publisher

Finland

Confidentiality degree

není předmětem státního či obchodního tajemství

References:

URL

RIV identification code

RIV/00216224:14210/15:00083750

Organization unit

Faculty of Arts

Keywords in English

constructive type theory; transparent intensional logic; logic of problems

Abstract

V originále

We examine two possible approaches to the formal treatment of the notion of problem in the type-theoretical paradigm. More specifically, we will explore an approach put forward by Martin-Löf's Constructive Type Theory (abbr. CTT, based on BHK interpretation of intuitionistic logic and Curry-Howard-de Bruijn correspondence), which can be seen as a direct continuation of Kolmogorov's original calculus of problems, and an approach put forward by Materna utilizing Tichý's Transparent Intensional Logic (abbr. TIL, based on partial lambda calculus and ramified classical type theory), which can be viewed as a realist attempt of interpreting Kolmogorov's logic of problems. Thus both of these theories can be seen as building upon Kolmogorov's first key insight that (constructive) logic is better understood as dealing with problems rather than with propositions. We conclude that neither of these theories can be considered at their current state as providing satisfactory account of the notion of problem. CTT due to its insufficient treatment of empirical problems (specifically, it is unclear how to apply the concepts of canonical and non-canonical proofs in the realm of empirical discourse). TIL due to its incomplete analysis of non-empirical problems (specifically, its inability to track, and thus distinguish different logical proofs). We propose our own approach called Transparent Intensional Logic of Problems (abbr. TILP, an extension based on modified TIL emulating some of the properties of CTT) that tries to combine strengths of both approaches without retaining any of their weak points. Further, TILP can be seen as building upon Kolmogorov's second (and often neglected) key insight that (constructive) logic is best understood as dealing with both problems and propositions, but without conflating them together.

Links

MUNI/A/1153/2014, interní kód MU

Name: Soudobé problémy a minulé podoby filozofické diskuse

Investor: Masaryk University, Category A

Citovat

PEZLAR, Ivo. Type-Theoretical Approaches to Problems and Solutions. In 15th Congress of Logic, Methodology and Philosophy of Science, 3.-8. August, 2015, Helsinki. 2015.

@proceedings{1310387,
   author = {Pezlar, Ivo},
   booktitle = {15th Congress of Logic, Methodology and Philosophy of Science, 3.-8. August, 2015, Helsinki},
   keywords = {constructive type theory; transparent intensional logic; logic of problems},
   language = {eng},
   title = {Type-Theoretical Approaches to Problems and Solutions},
   url = {http://clmps.helsinki.fi/},
   year = {2015}
}

TY  - CONF
ID  - 1310387
AU  - Pezlar, Ivo
PY  - 2015
TI  - Type-Theoretical Approaches to Problems and Solutions
KW  - constructive type theory
KW  - transparent intensional logic
KW  - logic of problems
UR  - http://clmps.helsinki.fi/
N2  - We examine two possible approaches to the formal treatment of the notion of problem in the type-theoretical paradigm. More specifically, we will explore an approach put forward by Martin-Löf's Constructive Type Theory (abbr. CTT, based on BHK interpretation of intuitionistic logic and Curry-Howard-de Bruijn correspondence), which can be seen as a direct continuation of Kolmogorov's original calculus of problems, and an approach put forward by Materna utilizing Tichý's Transparent Intensional Logic (abbr. TIL, based on partial lambda calculus and ramified classical type theory), which can be viewed as a realist attempt of interpreting Kolmogorov's logic of problems. Thus both of these theories can be seen as building upon Kolmogorov's first key insight that (constructive) logic is better understood as dealing with problems rather than with propositions. We conclude that neither of these theories can be considered at their current state as providing satisfactory account of the notion of problem. CTT due to its insufficient treatment of empirical problems (specifically, it is unclear how to apply the concepts of canonical and non-canonical proofs in the realm of empirical discourse). TIL due to its incomplete analysis of non-empirical problems (specifically, its inability to track, and thus distinguish different logical proofs). We propose our own approach called Transparent Intensional Logic of Problems (abbr. TILP, an extension based on modified TIL emulating some of the properties of CTT) that tries to combine strengths of both approaches without retaining any of their weak points. Further, TILP can be seen as building upon Kolmogorov's second (and often neglected) key insight that (constructive) logic is best understood as dealing with both problems and propositions, but without conflating them together.
ER  -

PEZLAR, Ivo. Type-Theoretical Approaches to Problems and Solutions. In \textit{15th Congress of Logic, Methodology and Philosophy of Science, 3.-8. August, 2015, Helsinki}. 2015.

Detailed Information on Publication Record