Title of article
Light Dialectica revisited
Author/Authors
Hernest، نويسنده , , Mircea-Dan and Trifonov، نويسنده , , Trifon، نويسنده ,
Issue Information
روزنامه با شماره پیاپی سال 2010
Pages
11
From page
1379
To page
1389
Abstract
We upgrade the light Dialectica interpretation (Hernest, 2005) [6] by adding two more light universal quantifiers, which are both semi-computational and semi-uniform and complement each other. An illustrative example is presented for the new light quantifiers and a new application is given for the older uniform quantifier. The realizability of new light negative formulations for the Axiom of Choice and for the Independence of Premises is explored in the new setting.
Keywords
Computational content of proofs , Functional interpretations , Program extraction from proofs , Light Dialectica interpretation , Light/uniform quantifiers , Automated program synthesis
Journal title
Annals of Pure and Applied Logic
Serial Year
2010
Journal title
Annals of Pure and Applied Logic
Record number
1444487
Link To Document