Skip to main content

Axiom of Choice Math Model Stanford by John Bell


 For it amounts to nothing more than the claim that, given any collection of mutually disjoint nonempty sets, it is possible to assemble a new settransversal or choice set—containing exactly one element from each member of the given collection. Nevertheless, this seemingly innocuous principle has far-reaching mathematical consequences—many indispensable, some startling—and has come to figure prominently in discussions on the foundations of mathematics.  

The fact that the Axiom of Choice implies Excluded Middle seems at first sight to be at variance with the fact that the former is often taken as a valid principle in systems of constructive mathematics governed by intuitionistic logic, e.g. Bishop’s Constructive Analysis[16] and Martin-Löf’s Constructive Type Theory[17], in which Excluded Middle is not affirmed. In Bishop’s words, “A choice function exists in constructive mathematics because a choice is implied by the very meaning of existence.” Thus, for example, the antecedent xyϕ(x,y)∀x∃yϕ(x,y) of ACL, given a constructive construal, just means that we have a procedure which, applied to each xx, yields a yy for which ϕ(x,y)ϕ(x,y). But this is precisely what is expressed by the consequent fxϕ(x,fx)∃f∀xϕ(x,fx) of ACL.
To resolve the difficulty, we note that in deriving Excluded Middle from ACL1 essential use was made of the principles of Predicative Comprehension and Extensionality of Functions[18]. It follows that, in systems of constructive mathematics affirming AC (but not Excluded Middle) either the principle of Predicative Comprehension or the principle of Extensionality of Functions must fail. While the principle of Predicative Comprehension can be given a constructive justification, no such justification can be provided for the principle of Extensionality of Functions. Functions on predicates are given intensionally, and satisfy just the corresponding principle of Intensionality XYF[X=YFX=FY]∀X∀Y∀F[X=Y→FX=FY]. The principle of Extensionality can easily be made to fail by considering, for example, the predicates PPrational featherless biped and QQhuman being and the function KK on predicates which assigns to each predicate the number of words in its description. Then we can agree that PQP≈Q but KP=3KP=3 and KQ=2KQ=2.
In intuitionistic set theory (that is, set theory based on intuitionistic as opposed to classical logic—we shall abbreviate this as IST) and in topos theory the principles of Predicative Comprehension and Extensionality of Functions (both appropriately construed) hold and so there AC implies Excluded Middle.[19] , [20]
The derivation of Excluded Middle from AC was first given by Diaconescu (1975) in a category-theoretic setting. His proof employed essentially different ideas from the proof presented above; in particular, it makes no use of extensionality principles but instead employs the idea of the quotient of an object (or set) by an equivalence relation. It is instructive to formulate Diaconescu’s argument within IST. To do this, let us call a subset UU of a set AA detachable if there is a subset VV of AA for which UV=U∩V= and UV=AU∪V=A. Diaconescu’s argument amounts to a derivation from AC4 (see above) of the assertion that every subset of a set is detachable, from which Excluded Middle readily follows.
Intuitionistic Type Theory
First published Fri Feb 12, 2016
Intuitionistic type theory (also constructive type theory or Martin-Löf type theory) is a formal logical system and philosophical foundation for constructive mathematics. It is a full-scale system which aims to play a similar role for constructive mathematics as Zermelo-Fraenkel Set Theory does for classical mathematics. It is based on the propositions-as-types principle and clarifies the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic. It extends this interpretation to the more general setting of intuitionistic type theory and thus provides a general conception not only of what a constructive proof is, but also of what a constructive mathematical object is. The main idea is that mathematical concepts such as elements, sets and functions are explained in terms of concepts from programming such as data structures, data types and programs. This article describes the formal system of intuitionistic type theory and its semantic foundations.

Metamathematic properties of Type Normalization & Type Check.. Law of Reflexivity


Popular posts from this blog

🧿 New Form of Matter 🟠

"Measurements on a superconducting material show an abrupt transition between a normal metal and a "strange" metal. The really strange thing, however, is that this abruptness disappears when the temperature falls.

The moral of the story, says Zaanen, is that the origin of superconductivity itself is increasingly a side issue. "After thirty years, evidence is mounting that high Tc -superconductivity is pointing toward a radically New Form of Matter, which is governed by the consequences of Quantum Entanglement in the macroscopic world."

The Vision in the Mission of the San Joaquin River by CORE Talks
The diversity in access points for the San Joaquin River, in the heart of the Central Valley of California, is time sensitive to the life force and spark of the character of Fresno County and specifically, the Fresno/Clovis/Madera citizens.  

Imagine if one of the three access points could simply be put to use now, while working on the other ideas for the next 8 months?  Finding harmony in the heart of California, with the goal of healthy minds and hands will find a way to create a core talk about the necessity of creativity when it comes to economic development, creating jobs and furthering education and housing for the health and safety of our people.

In consideration, Fresno is the 5th largest city in the state, we are a fantastic and affordable city for relocation, with great schools and a wonderful travel destination point to which can enhance our economic development through this project sooner than later.  
While the law ma…