Also
the Axiom of Choice can be shown to entail the cardinal rule of classical logic, the law of excluded middle—the assertion that A∨¬AA∨¬A for any proposition AA. To be precise, using the rules of intuitionistic logic within our augmented language LL, we shall derive[15 <https://plato.stanford.edu/entries/axiom-choice/notes.html#15>] the law of excluded middle from *AC1L* conjoined with the following additional principles: *Predicative Comprehension*: ∃X∀x[X(x)↔ϕ(x)]∃X∀x[X(x)↔ϕ(x)], where ϕϕ contains no bound function or predicate variables. *Extensionality of Functions*: ∀X∀Y∀F[X≈Y→FX=FY]∀X∀Y∀F[X≈Y→FX=FY], where X≈YX≈Y is an abbreviation for ∀x[X (x)↔Y(x)]∀x[X(x)↔Y(x)], that is, XX and YY are *extensionally equivalent*. *Two Distinct Individuals*: 0–≠1–0_≠1_, where 0–0_ and 1–1_ are individual constants. --- Frank C. Wimberly 140 Calle Ojo Feliz, Santa Fe, NM 87505 505 670-9918 Santa Fe, NM On Fri, Jul 31, 2020, 1:03 PM Frank Wimberly <wimber...@gmail.com> wrote: > > Glen et al,. > > This morning Glen raised some interesting questions about the limitations > of constructive mathematics if I understood correctly. My undergraduate > advisor, Errett Bishop wrote a book called Foundations of Constructive > Analysis. Fortunately I inherited a copy from Reuben. I will read a few > sentences aloud and use my cellphone to transcribe them. Pardon the lack > of punctuation; I hope the result is readable. These come from Chapter 1, > A Constructivist Manifesto. > > when a classical mathematician claims he is a constructivist he probably > means he avoids the axiom of choice this axiom is unique and its ability to > trouble the conscience of the classical mathematician but in fact it is not > a real source of unconstructive etiz of classical mathematics....the axiom > of choice is used to extract elements from equivalence classes where they > should never have been put in the first place for instance the real number > should not be defined as an equivalence class of cauchy sequences of > rational numbers there is no need to drag in the equivalence > classes...almost every conceivable type of resistance has been offered to a > straightforward realistic treatment of mathematics even by non > constructivists brower who has done more for constructive mathematics than > anyone else thought it necessary to introduce a revolutionary semi mystical > theory of the Continuum Weyl a great mathematician who in practice suppress > is constructivist convictions Express the opinion that idealistic > mathematics finds its justification and its application to physics Hilbert > who insisted on constructive eating and metamathematics but believe the > price of it constructed mathematics was too great was willing to settle for > consistency brouwer's disciples join forces with the logicians in attempts > to formalize constructed mathematics other seat constructive truth in the > framework of recursive function theory still others look for a shortcut to > reality a point of Vantage which will suddenly revealed classical > mathematics in a constructive light none of these substitutes for a > straightforward realistic approach has worked it is no exaggeration to say > that a straightforward realistic approach to mathematics has yet to be > tried it's time to make the attempt... > > The book follows > > > --- > Frank C. Wimberly > 140 Calle Ojo Feliz, > Santa Fe, NM 87505 > > 505 670-9918 > Santa Fe, NM >
- .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. . FRIAM Applied Complexity Group listserv Zoom Fridays 9:30a-12p Mtn GMT-6 bit.ly/virtualfriam un/subscribe http://redfish.com/mailman/listinfo/friam_redfish.com archives: http://friam.471366.n2.nabble.com/ FRIAM-COMIC http://friam-comic.blogspot.com/
