ترغب بنشر مسار تعليمي؟ اضغط هنا

Dialectica Logical Principles

145   0   0.0 ( 0 )
 نشر من قبل Matteo Spadetto
 تاريخ النشر 2021
  مجال البحث
والبحث باللغة English




اسأل ChatGPT حول البحث

Godels Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in conjunction with the double negation interpretation to obtain the consistency of Peano arithmetic. In recent years, proof theoretic transformations (so-called proof interpretations) that are based on Godels Dialectica interpretation have been used systematically to extract new content from proofs and so the interpretation has found relevant applications in several areas of mathematics and computer science. Following our previous work on Godel fibrations, we present a (hyper)doctrine characterisation of the Dialectica which corresponds exactly to the logical description of the interpretation. To show that we derive in the category theory the soundness of the interpretation of the implication connective, as expounded on by Spector and Troelstra. This requires extra logical principles, going beyond intuitionistic logic, Markovs Principle (MP) and the Independence of Premise (IP) principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight (internal language) correspondence between the logical system and the categorical framework. This tight correspondence should come handy not only when discussing the applications of the Dialectica already known, like its use to extract computational content from (some) classical theorems (proof mining), its use to help to model specific abstract machines, etc. but also to help devise new applications.



قيم البحث

اقرأ أيضاً

The categorical modeling of Petri nets has received much attention recently. The Dialectica construction has also had its fair share of attention. We revisit the use of the Dialectica construction as a categorical model for Petri nets generalizing th e original application to suggest that Petri nets with different kinds of transitions can be modeled in the same categorical framework. Transitions representing truth-values, probabilities, rates or multiplicities, evaluated in different algebraic structures called lineales are useful and are modeled here in the same category. We investigate (categorical instances of) this generalized model and its connections to more recent models of categorical nets.
134 - Michael Shulman 2018
Cheng, Gurski, and Riehl constructed a cyclic double multicategory of multivariable adjunctions. We show that the same information is carried by a double polycategory, in which opposite categories are polycategorical duals. Moreover, this double poly category is a full substructure of a double Chu construction, whose objects are a sort of polarized category, and which is a natural home for 2-categorical dualities. We obtain the double Chu construction using a general Chu-Dialectica construction on polycategories, which includes both the Chu construction and the categorical Dialectica construction of de Paiva. The Chu and Dialectica constructions each impose additional hypotheses making the resulting polycategory representable (hence *-autonomous), but for different reasons; this leads to their apparent differences.
We survey several problems related to logical aspects of quantum structures. In particular, we consider problems related to completions, decidability and axiomatizability, and embedding problems. The historical development is described, as well as recent progress and some suggested paths forward.
We show that the classifying topos for the theory of fields does not satisfy De Morgans law, and we identify its largest dense De Morgan subtopos as the classifying topos for the theory of fields of nonzero characteristic which are algebraic over their prime fields.
The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. We study this and related principles in an intuitionistic setting. Am ong other things, we show that Bourbaki-Witt fails exactly when the trichotomous ordinals form a set, but does not imply that fixed points can always be found by transfinite iteration. Meanwhile, on the side of models, we see that the principle fails in realisability toposes, and does not hold in the free topos, but does hold in all cocomplete toposes.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا