Proof interpretations with truth | Zendy

Gaspar Jaime | Zendy; Oliva Paulo | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Premium

Proof interpretations with truth

Author(s) -

Gaspar Jaime,

Oliva Paulo

Publication year - 2010

Publication title -

mathematical logic quarterly

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.473

H-Index - 28

eISSN - 1521-3870

pISSN - 0942-5616

DOI - 10.1002/malq.200910112

Subject(s) - realizability , interpretation (philosophy) , truth function , bounded function , mathematics , truth value , relation (database) , intuitionistic logic , linear logic , discrete mathematics , computer science , algorithm , propositional calculus , data mining , programming language , mathematical analysis

This article systematically investigates so‐called “truth variants” of several functional interpretations. We start by showing a close relation between two variants of modified realizability, namely modified realizability with truth and q‐modified realizability. Both variants are shown tobe derived from a single “functional interpretation with truth” of intuitionistic linear logic. This analysis suggests that several functional interpretations have truth and q‐variants. These variants, however, require a more involved modification than the ones previously considered. Following this lead we present truth and q‐variants of the Diller‐Nahm interpretation, the bounded modified realizability and the bounded functional interpretation (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)

This content is not available in your region!

Continue researching here.

Having issues? You can contact us here

Accelerating Research