All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

Natural Deduction for Partial Type Theory with 'Evaluation Terms'

The result's identifiers

  • Result code in IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14210%2F21%3A00119213" target="_blank" >RIV/00216224:14210/21:00119213 - isvavai.cz</a>

  • Result on the web

    <a href="http://imft.ftn.uns.ac.rs/math/cms/LAP2021" target="_blank" >http://imft.ftn.uns.ac.rs/math/cms/LAP2021</a>

  • DOI - Digital Object Identifier

Alternative languages

  • Result language

    angličtina

  • Original language name

    Natural Deduction for Partial Type Theory with 'Evaluation Terms'

  • Original language description

    The talk proposes an expressive natural deduction system in sequent style ND-TT* for a higher-order partial type theory TT*. TT* treats both total and partial functions-as-graphs and also acyclic algorithmic computations, called constructions (of certain objects of TT*). The system is usable e.g. for the analysis of fine-grained hyperintensionality (see e.g. Tichy 1988) and meta-logical notions. The basic part is adjusted from Tichy's 1982 convenient natural deduction system for his partial type theory (for other approaches, see e.g. Farmer 1990, Muskens 1995, Moschovakis 2005). TT* mainly extends his system by admission of 'evaluation terms' (cf. e.g. Tichy 1988, Farmer 2016, Raclavsky 2020). Our ND-TT* provides all basic rules governing those special constructions. Finally, we sketch a Henkin-style completeness proof for ND-TT*.

  • Czech name

  • Czech description

Classification

  • Type

    O - Miscellaneous

  • CEP classification

  • OECD FORD branch

    60301 - Philosophy, History and Philosophy of science and technology

Result continuities

  • Project

    <a href="/en/project/GA19-12420S" target="_blank" >GA19-12420S: Hyperintensional Meaning, Type Theory and Logical Deduction</a><br>

  • Continuities

    P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Others

  • Publication year

    2021

  • Confidentiality

    S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů