Bishop's Constructive Analysis

Bishop_Constructive_Analysis.txt

Text used in this video:

https://youtu.be/wuhbxJahVRE

# Overview of the book
210 pages, 6 chapters

# 1. Formal system
Bishop style:
* No fully formal set theory and
  - N and it's elements are a primitive set
    * Often starts with 1
  - As well as pairing (a, b) of two elements, but that's probably not a big deal
    * In turn, A×B exists
  - all sets have to come with an equality relation =
    * union and intersection must thus be assured to be compatible with that equality every time
* Dependent choice is adopted, at least on R (relations on A×A can be turned to functions)
  - However, LEM, LPO, MP is watched out for.

# Inequality
* It's often worked with positive apartness relations ≠
  - such as, on the reals, x ≠ y := |x-y| > 0
  - This is stronger than the logical ¬(x=y)

# 2. Reals (p. 25)
* Elements of R is are subsets of QxQ such that
  - ∀(l,u). l <= u                                (elements of x are intervals)
  - ∀(l,u), (l2,u2). ∃q∈Q. q ∈ [l, u] ∩ [l2, u2]  (all intervals intersect)
  - ∀d ∈ Q^+. ∃(l,u), u-l < d                     (arbitrary small rational element
                                                 sizes are realized)
  - Equality = ... all their intervals have a rational number in common
  - Unequality ≠ ... there's respective intervals which are disjoint

## Early propositions (pp. 28 - 29)
  * ∀x,y ∈ R. ¬(x >= y) → (y > x)             implies Marvok's principle
  * ∀x ∈ R. (x >= 0) → ((x > 0) ∨ (x = 0))    implies LPO
  * ∀x ∈ R. (x => 0) ∨ (x <= 0)               implies LLPO

# 3. Lambda technique

# 4. Finite dimensional Hilbert space

# 5. Linearity and Convexity

# 6. Operators and Locatedness

# References
- https://en.wikipedia.org/wiki/Constructive_analysis
- https://en.wikipedia.org/wiki/Axiom_of_dependent_choice

- https://www.amazon.com/Techniques-Constructive-Analysis-Universitext-Douglas/dp/038733646X
- https://www.dsbridges.com/my-mathematics2.html
- https://www.amazon.com/Apartness-Uniformity-Constructive-Applications-Computability/dp/3642224148

- http://www.math.lmu.de/~petrakis/FMV.pdf
- https://ncatlab.org/nlab/show/Bishop%27s+constructive+mathematics