[FRIAM] Constructive mathematics.

[Frank Wimberly]

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 <wimberly3 at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://redfish.com/pipermail/friam_redfish.com/attachments/20200731/aa8b4863/attachment.html>