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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,069

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

EM + Ext_ + AC~i~n~t is equivalent to AC~e~x~t.Jesper Carlström - 2004 - Mathematical Logic Quarterly 50 (3):236.
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.
Hintikka’s Take on the Axiom of Choice and the Constructivist Challenge.Radmila Jovanović - 2013 - Revista de Humanidades de Valparaíso 2:135-150.
M l.John L. Bell - unknown
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.
Cut-Elimination for Simple Type Theory with an Axiom of Choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
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.

Analytics

Added to PP
2013-12-01

Downloads
33 (#500,331)

6 months
4 (#862,832)

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

Add more references