EM + Ext− + ACint is equivalent to ACext

Mathematical Logic Quarterly 50 (3):236-240 (2004)
  Copy   BIBTEX

Abstract

It is well known that the extensional axiom of choice implies the law of excluded middle . We here prove that the converse holds as well if we have the intensional axiom of choice ACint, which is provable in Martin-Löf's type theory, and a weak extensionality principle , which is provable in Martin-Löf's extensional type theory. In particular, EM is equivalent to ACext in extensional type theory

Categories

Keywords

Reprint years

DOI

10.1002/malq.200410100

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 105,626

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

The axiom of choice and the law of excluded middle in weak set theories.John L. Bell - 2008 - Mathematical Logic Quarterly 54 (2):194-201.
The rigid relation principle, a new weak choice principle.Joel David Hamkins & Justin Palumbo - 2012 - Mathematical Logic Quarterly 58 (6):394-398.
La consideración de Hintikka del axioma de elección y del desafío constructivista.Radmila Jovanović - 2013 - Revista de Humanidades de Valparaíso 2:135-150.
M l.John L. Bell - unknown
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
Finite type structures within combinatory algebras.Inge Bethke - 1991 - Annals of Pure and Applied Logic 55 (2):101-123.
Consistency of the intensional level of the Minimalist Foundation with Church’s thesis and axiom of choice.Hajime Ishihara, Maria Emilia Maietti, Samuele Maschio & Thomas Streicher - 2018 - Archive for Mathematical Logic 57 (7-8):873-888.
A Remark on Ascending Chain Conditions, the Countable Axiom of Choice and the Principle of Dependent Choices.Karl-Heinz Diener - 1994 - Mathematical Logic Quarterly 40 (3):415-421.
Extensionality Versus Constructivity.Silvio Valentini - 2002 - Mathematical Logic Quarterly 48 (2):179-187.
Sequential topological conditions in ℝ in the absence of the axiom of choice.Gonçalo Gutierres - 2003 - Mathematical Logic Quarterly 49 (3):293-298.

Analytics

Added to PP
2013-12-01

Downloads
59 (#397,578)

6 months
9 (#446,155)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

A minimalist two-level foundation for constructive mathematics.Maria Emilia Maietti - 2009 - Annals of Pure and Applied Logic 160 (3):319-354.
2006 Annual Meeting of the Association for Symbolic Logic.Matthew Valeriote - 2007 - Bulletin of Symbolic Logic 13 (1):120-145.

Add more citations

References found in this work

Choice Implies Excluded Middle.N. Goodman & J. Myhill - 1978 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 24 (25-30):461-461.
Choice Implies Excluded Middle.N. Goodman & J. Myhill - 1978 - Mathematical Logic Quarterly 24 (25‐30):461-461.

Add more references