Unpublished, Draft, To Appear
@UnPublished
Unveröffentlicht, Entwurf


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:









Author, Editor

Author(s):

Rizkallah, Christine

dblp

Not MPG Author(s):

Brown, Chad E.

BibTeX citekey*:

BrownRizkallah2011

Title, Booktitle

Title*:

Glivenko and Kuroda for Simple Type Theory

Vol, No, pp., Year

Month:

December

Year:

2011

Language:

English

Pages:

14

Abstract, Links, ©

Note:

Submitted

LaTeX Abstract:

Glivenko’s theorem states that an arbitrary proposi- tional formula is classically provable if and only if its double nega- tion is intuitionistically provable. The result does not extend to full first-order predicate logic, but does extend to first-order pred- icate logic without the universal quantifier. A recent paper by Zdanowski shows that Glivenko’s theorem also holds for second- order propositional logic without the universal quantifier. We prove that Glivenko’s theorem extends to some versions of simple type theory without the universal quantifier. Moreover we prove that Kuroda’s negative translation, which is known to embed clas- sical first-order logic into intuitionistic first-order logic, extends to the same versions of simple type theory. We also prove that the Glivenko property fails for simple type theory once a weak form of functional extensionality is included.

Categories / Keywords:

Glivenko Kuroda Higher-order Logic classical intuitionistic intensional extensional

HyperLinks / References / URLs:

http://www.mpi-inf.mpg.de/~crizkall/Publications/BrownRizkallah2011.pdf

Personal Comments:


File Upload:




Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Algorithms and Complexity Group

Audience:

experts only

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort

BibTeX Entry:
@UNPUBLISHED{BrownRizkallah2011,
AUTHOR = {Rizkallah, Christine},
TITLE = {Glivenko and Kuroda for Simple Type Theory},
YEAR = {2011},
PAGES = {14},
MONTH = {December},
NOTE = {Submitted},
}


Entry last modified by Christine Rizkallah, 02/09/2012
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Christine Rizkallah
Created
02/09/2012 03:26:35 PM
Revision
0.



Editor
Christine Rizkallah



Edit Date
02/09/2012 03:26:35 PM



Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
BrownRizkallah2011.pdf