The ghosts of departed quantities as the soul of
computation
Sam Sanders1
Tokyo, Feb. 22, 2012
1This research is generously supported by the John Templeton Foundation.
The nature of algorithm
The nature of algorithm
Algorithm≈finite procedure ≈explicit computation.
The nature of algorithm
Algorithm≈finite procedure ≈explicit computation.
The technical definition: Definition (Algorithm)
The nature of algorithm
Algorithm≈finite procedure ≈explicit computation.
The technical definition: Definition (Algorithm)
We’ll know it when we see it. . .
The nature of algorithm
Algorithm≈finite procedure ≈explicit computation.
The technical definition: Definition (Algorithm)
We’ll know it when we see it. . .
In this talk, we (partially) formalize the notion of algorithm using Nonstandard Analysis.
The nature of algorithm
Algorithm≈finite procedure ≈explicit computation.
The technical definition: Definition (Algorithm)
We’ll know it when we see it. . .
In this talk, we (partially) formalize the notion of algorithm using Nonstandard Analysis.
We consider the philosophical implications for physics, mathematics and computer science.
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’.
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thenaturalnumbers
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thenaturalnumbers
new numbers, not in N
z }| {
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thenaturalnumbers
new numbers, not in N
z }| {
ω
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thenaturalnumbers
new numbers, not in N
z }| {
ω ω− 1
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thenaturalnumbers
new numbers, not in N
z }| {
ω ω− 1 2ω
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thenaturalnumbers
new numbers, not in N
z }| {
ω ω− 1 2ω
⌈√ω⌉
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thenaturalnumbers
ω ω− 1 2ω
⌈√ω⌉
| {z }
Ω, theinfinitenumbers
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thefinitenumbers
ω ω− 1 2ω
⌈√ω⌉
| {z }
Ω, theinfinitenumbers
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thefinitenumbers
ω ω− 1 2ω
⌈√ω⌉
| {z }
Ω, theinfinitenumbers
∗N,thehypernaturalnumbers
z }| {
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thefinitenumbers
ω ω− 1 2ω
⌈√ω⌉
| {z }
Ω, theinfinitenumbers
∗N,thehypernaturalnumbers
z }| {
N= finite (or standard) numbers
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thefinitenumbers
ω ω− 1 2ω
⌈√ω⌉
| {z }
Ω, theinfinitenumbers
∗N,thehypernaturalnumbers
z }| {
N= finite (or standard) numbers
∗N\ N = Ω = infinite (or nonstandard) numbers
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis
Nonstandard Analysis (NSA) formalizes ‘calculus with infinitesimals’. For this talk, we only need∗N.
0 1 2 3 . . . ✲
| {z }
N,thefinitenumbers
ω ω− 1 2ω
⌈√ω⌉
| {z }
Ω, theinfinitenumbers
∗N,thehypernaturalnumbers
z }| {
N= finite (or standard) numbers
∗N\ N = Ω = infinite (or nonstandard) numbers Universal Transfer: (∀n ∈ N)ϕ(n) → (∀n ∈∗N)ϕ(n).
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis: the fourth way
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis: the fourth way
Ω-invariance≈algorithm≈finite procedure≈explicit computation.
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis: the fourth way
Ω-invariance≈algorithm≈finite procedure≈explicit computation.
Definition (Ω-invariance) A set A⊂ N isΩ-invariant
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis: the fourth way
Ω-invariance≈algorithm≈finite procedure≈explicit computation.
Definition (Ω-invariance)
A set A⊂ N isΩ-invariant if there is aquantifier-free formula ψ such thatfor all ω∈ Ω,
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis: the fourth way
Ω-invariance≈algorithm≈finite procedure≈explicit computation.
Definition (Ω-invariance)
A set A⊂ N isΩ-invariant if there is aquantifier-free formula ψ such thatfor all ω∈ Ω,
A={k ∈ N : ψ(k,ω)}.
Introduction NSA and Constructive Analysis Philosophical implications
Nonstandard Analysis: the fourth way
Ω-invariance≈algorithm≈finite procedure≈explicit computation.
Definition (Ω-invariance)
A set A⊂ N isΩ-invariant if there is aquantifier-free formula ψ such thatfor all ω∈ Ω,
A={k ∈ N : ψ(k,ω)}.
Note that A depends onω∈ Ω, but not on thechoiceofω∈ Ω.
Introduction NSA and Constructive Analysis Philosophical implications
Two theorems
Theorem (Finiteness)
For everyΩ-invariant A⊂ N and k ∈ N, there is M ∈ N, such that
Introduction NSA and Constructive Analysis Philosophical implications
Two theorems
Theorem (Finiteness)
For everyΩ-invariant A⊂ N and k ∈ N, there is M ∈ N, such that k ∈ A ⇐⇒ ψ(k,ω)⇐⇒ ψ(k,M).
Introduction NSA and Constructive Analysis Philosophical implications
Two theorems
Theorem (Finiteness)
For everyΩ-invariant A⊂ N and k ∈ N, there is M ∈ N, such that k ∈ A ⇐⇒ ψ(k,ω)⇐⇒ ψ(k,M).
Thus, to verify whetherk ∈ A, we only need to performfinitely many operations (i.e. determine ifψ(k, M)).
Introduction NSA and Constructive Analysis Philosophical implications
Two theorems
Theorem (Finiteness)
For everyΩ-invariant A⊂ N and k ∈ N, there is M ∈ N, such that k ∈ A ⇐⇒ ψ(k,ω)⇐⇒ ψ(k,M).
Thus, to verify whetherk ∈ A, we only need to performfinitely many operations (i.e. determine ifψ(k, M)).
Theorem (Finiteness II) Every∆01-set isΩ-invariant.
Introduction NSA and Constructive Analysis Philosophical implications
Two theorems
Theorem (Finiteness)
For everyΩ-invariant A⊂ N and k ∈ N, there is M ∈ N, such that k ∈ A ⇐⇒ ψ(k,ω)⇐⇒ ψ(k,M).
Thus, to verify whetherk ∈ A, we only need to performfinitely many operations (i.e. determine ifψ(k, M)).
Theorem (Finiteness II) Every∆01-set isΩ-invariant.
EveryTuring Machine is anΩ-invariant procedure!
Introduction NSA and Constructive Analysis Philosophical implications
Two theorems
Theorem (Finiteness)
For everyΩ-invariant A⊂ N and k ∈ N, there is M ∈ N, such that k ∈ A ⇐⇒ ψ(k,ω)⇐⇒ ψ(k,M).
Thus, to verify whetherk ∈ A, we only need to performfinitely many operations (i.e. determine ifψ(k, M)).
Theorem (Finiteness II) Every∆01-set isΩ-invariant.
EveryTuring Machine is anΩ-invariant procedure! (Given the right axiom system; and probably vice versa).
Introduction NSA and Constructive Analysis Philosophical implications
Two theorems
Theorem (Finiteness)
For everyΩ-invariant A⊂ N and k ∈ N, there is M ∈ N, such that k ∈ A ⇐⇒ ψ(k,ω)⇐⇒ ψ(k,M).
Thus, to verify whetherk ∈ A, we only need to performfinitely many operations (i.e. determine ifψ(k, M)).
Theorem (Finiteness II) Every∆01-set isΩ-invariant.
EveryTuring Machine is anΩ-invariant procedure! (Given the right axiom system; and probably vice versa). How well does Ω-invariance capture ‘algorithm’ ?
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL)
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL)
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B”
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0)
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
(∀n ∈ N)C (n) ⇛ (∀m ∈ N)D(m) is
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
(∀n ∈ N)C (n) ⇛ (∀m ∈ N)D(m) is
(∀n ∈∗N)C (n)→(∀m ∈∗N)D(m)
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
(∃n ∈∗N)E (n) ⇛ (∃m ∈∗N)F (m) is
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
(∃n ∈∗N)E (n) ⇛ (∃m ∈∗N)F (m) is
(∃n ≤ω)E (n)→(∃m ≤ω)F (m)
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
¬A: A→ (0 = 1)
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
¬A: A→ (0 = 1) ∼A: A ⇛ (0 = 1)
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
¬A: A→ (0 = 1) ∼A: A ⇛ (0 = 1)
∼[(∀n ∈ N)A(n)]
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
¬A: A→ (0 = 1) ∼A: A ⇛ (0 = 1)
∼[(∀n ∈ N)A(n)] ≡ (∃n ∈∗N)¬A(n) WEAKERthan (∃n ∈ N)¬A(n).
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
¬A: A→ (0 = 1) ∼A: A ⇛ (0 = 1)
∼[(∀n ∈ N)A(n)] ≡ (∃n ∈∗N)¬A(n) WEAKERthan (∃n ∈ N)¬A(n).
¬[(∀n ∈ N)A(n)] isWEAKER
than (∃n ∈ N)¬A(n).
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
¬A: A→ (0 = 1) ∼A: A ⇛ (0 = 1)
WHY is this a good/faithful/reasonable/. . . translation?
Introduction NSA and Constructive Analysis Philosophical implications
Lost in translation
BISH (based on IL) NSA (based on CL) Central:algorithmandfinite procedure
A∨ B: analgodecides if A or if B is true
Central:Ω-invariant procedure A V B: “an Ω-inv.proc.decides if A or if B” (∃x)A(x): analgocomputes x0
such that A(x0)
(∃x)A(x): anΩ-inv. proc.computes x0
such that A(x0) A→ B: analgoconverts a proof of A
to a proof of B A ⇛ B: “anΩ-inv. procconverts a proof of A to a proof of B”
¬A: A→ (0 = 1) ∼A: A ⇛ (0 = 1)
WHY is this a good/faithful/reasonable/. . . translation? BECAUSEthenon-algorithmic/non-constructive principles behave the same!
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
non-Ω-invariant
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
non-Ω-invariant LPO: For P ∈ Σ1, P V∼P
l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
non-Ω-invariant LPO: For P ∈ Σ1, P V∼P
l
LPR:(∀x ∈ R)(x > 0 V ∼(x < 0)) l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
non-Ω-invariant LPO: For P ∈ Σ1, P V∼P
l
LPR:(∀x ∈ R)(x > 0 V ∼(x < 0)) l
MCT: monotone convergence thm l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
non-Ω-invariant LPO: For P ∈ Σ1, P V∼P
l
LPR:(∀x ∈ R)(x > 0 V ∼(x < 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
non-Ω-invariant LPO: For P ∈ Σ1, P V∼P
l
LPR:(∀x ∈ R)(x > 0 V ∼(x < 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm (limit computed by algo)
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
non-Ω-invariant LPO: For P ∈ Σ1, P V∼P
l
LPR:(∀x ∈ R)(x > 0 V ∼(x < 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
(limit computed by algo) (limit computed by Ω-inv. proc.)
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
non-Ω-invariant LPO: For P ∈ Σ1, P V∼P
l
LPR:(∀x ∈ R)(x > 0 V ∼(x < 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
(limit computed by algo) (limit computed by Ω-inv. proc.)
(point in intersection computed by algo)
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
non-Ω-invariant LPO: For P ∈ Σ1, P V∼P
l
LPR:(∀x ∈ R)(x > 0 V ∼(x < 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
(limit computed by algo) (limit computed by Ω-inv. proc.)
(point in intersection computed by algo)
(point in intersection computed by Ω-inv. proc.)
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LPO: For P ∈ Σ1, P∨ ¬P l
LPR:(∀x ∈ R)(x > 0 ∨ ¬(x > 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
non-Ω-invariant LPO: For P ∈ Σ1, P V∼P
l
LPR:(∀x ∈ R)(x > 0 V ∼(x < 0)) l
MCT: monotone convergence thm l
CIT: Cantor intersection thm
(limit computed by algo) (limit computed by Ω-inv. proc.)
l
Universal Transfer
(∀n ∈ N)ϕ(n) → (∀n ∈∗N)ϕ(n)
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 → x = 0 ∨ y = 0) l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 → x = 0 ∨ y = 0) l
IVT: Intermediate value theorem
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 → x = 0 ∨ y = 0) l
IVT: Intermediate value theorem
non-Ω-invariant
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 → x = 0 ∨ y = 0) l
IVT: Intermediate value theorem
non-Ω-invariant LLPO
For P, Q∈ Σ1,∼(P ∧ Q) ⇛ ∼P V ∼Q l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 → x = 0 ∨ y = 0) l
IVT: Intermediate value theorem
non-Ω-invariant LLPO
For P, Q∈ Σ1,∼(P ∧ Q) ⇛ ∼P V ∼Q l
LLPR:(∀x ∈ R)(x ≥ 0 V x ≤ 0) l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 → x = 0 ∨ y = 0) l
IVT: Intermediate value theorem
non-Ω-invariant LLPO
For P, Q∈ Σ1,∼(P ∧ Q) ⇛ ∼P V ∼Q l
LLPR:(∀x ∈ R)(x ≥ 0 V x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 ⇛ x = 0 V y = 0) l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 → x = 0 ∨ y = 0) l
IVT: Intermediate value theorem
non-Ω-invariant LLPO
For P, Q∈ Σ1,∼(P ∧ Q) ⇛ ∼P V ∼Q l
LLPR:(∀x ∈ R)(x ≥ 0 V x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 ⇛ x = 0 V y = 0) l
IVT: Intermediate value theorem
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 → x = 0 ∨ y = 0) l
IVT: Intermediate value theorem
non-Ω-invariant LLPO
For P, Q∈ Σ1,∼(P ∧ Q) ⇛ ∼P V ∼Q l
LLPR:(∀x ∈ R)(x ≥ 0 V x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 ⇛ x = 0 V y = 0) l
IVT: Intermediate value theorem (int. value computed by algo)
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 → x = 0 ∨ y = 0) l
IVT: Intermediate value theorem
non-Ω-invariant LLPO
For P, Q∈ Σ1,∼(P ∧ Q) ⇛ ∼P V ∼Q l
LLPR:(∀x ∈ R)(x ≥ 0 V x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 ⇛ x = 0 V y = 0) l
IVT: Intermediate value theorem (int. value computed by algo) (int. value computed by Ω-inv. proc.)
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 → x = 0 ∨ y = 0) l
IVT: Intermediate value theorem
non-Ω-invariant LLPO
For P, Q∈ Σ1,∼(P ∧ Q) ⇛ ∼P V ∼Q l
LLPR:(∀x ∈ R)(x ≥ 0 V x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 ⇛ x = 0 V y = 0) l
IVT: Intermediate value theorem (int. value computed by algo) (int. value computed by Ω-inv. proc.) Axioms of R:¬(x > 0 ∧ x < 0)
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics II
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
LLPO
For P, Q∈ Σ1,¬(P ∧ Q) → ¬P ∨ ¬Q l
LLPR:(∀x ∈ R)(x ≥ 0 ∨ x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 → x = 0 ∨ y = 0) l
IVT: Intermediate value theorem
non-Ω-invariant LLPO
For P, Q∈ Σ1,∼(P ∧ Q) ⇛ ∼P V ∼Q l
LLPR:(∀x ∈ R)(x ≥ 0 V x ≤ 0) l
NIL
(∀x, y ∈ R)(xy = 0 ⇛ x = 0 V y = 0) l
IVT: Intermediate value theorem (int. value computed by algo) (int. value computed by Ω-inv. proc.) Axioms of R:¬(x > 0 ∧ x < 0) Axioms of R:∼(x > 0 ∧ x < 0)
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
MP: For P ∈ Σ1,¬¬P → P l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
MP: For P ∈ Σ1,¬¬P → P l
MPR:(∀x ∈ R)(¬¬(x > 0) → x > 0) l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
MP: For P ∈ Σ1,¬¬P → P l
MPR:(∀x ∈ R)(¬¬(x > 0) → x > 0) l
EXT: the extensionality theorem
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
MP: For P ∈ Σ1,¬¬P → P l
MPR:(∀x ∈ R)(¬¬(x > 0) → x > 0) l
EXT: the extensionality theorem
non-Ω-invariant
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
MP: For P ∈ Σ1,¬¬P → P l
MPR:(∀x ∈ R)(¬¬(x > 0) → x > 0) l
EXT: the extensionality theorem
non-Ω-invariant MP: For P ∈ Σ1,∼∼P ⇛ P
l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
MP: For P ∈ Σ1,¬¬P → P l
MPR:(∀x ∈ R)(¬¬(x > 0) → x > 0) l
EXT: the extensionality theorem
non-Ω-invariant MP: For P ∈ Σ1,∼∼P ⇛ P
l
MPR:(∀x ∈ R)(∼∼(x > 0) ⇛ x > 0) l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
MP: For P ∈ Σ1,¬¬P → P l
MPR:(∀x ∈ R)(¬¬(x > 0) → x > 0) l
EXT: the extensionality theorem
non-Ω-invariant MP: For P ∈ Σ1,∼∼P ⇛ P
l
MPR:(∀x ∈ R)(∼∼(x > 0) ⇛ x > 0) l
EXT: the extensionality theorem
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
MP: For P ∈ Σ1,¬¬P → P l
MPR:(∀x ∈ R)(¬¬(x > 0) → x > 0) l
EXT: the extensionality theorem
non-Ω-invariant MP: For P ∈ Σ1,∼∼P ⇛ P
l
MPR:(∀x ∈ R)(∼∼(x > 0) ⇛ x > 0) l
EXT: the extensionality theorem WLPO: For P ∈ Σ1,¬¬P ∨ ¬P
l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
MP: For P ∈ Σ1,¬¬P → P l
MPR:(∀x ∈ R)(¬¬(x > 0) → x > 0) l
EXT: the extensionality theorem
non-Ω-invariant MP: For P ∈ Σ1,∼∼P ⇛ P
l
MPR:(∀x ∈ R)(∼∼(x > 0) ⇛ x > 0) l
EXT: the extensionality theorem WLPO: For P ∈ Σ1,¬¬P ∨ ¬P
l
WLPR:(∀x ∈ R)¬¬(x > 0) ∨ ¬(x > 0) l
Introduction NSA and Constructive Analysis Philosophical implications
Constructive Reverse Mathematics III
BISH (based on IL) NSA (based on CL) non-constructive/non-algorithmic
MP: For P ∈ Σ1,¬¬P → P l
MPR:(∀x ∈ R)(¬¬(x > 0) → x > 0) l
EXT: the extensionality theorem
non-Ω-invariant MP: For P ∈ Σ1,∼∼P ⇛ P
l
MPR:(∀x ∈ R)(∼∼(x > 0) ⇛ x > 0) l
EXT: the extensionality theorem WLPO: For P ∈ Σ1,¬¬P ∨ ¬P
l
WLPR:(∀x ∈ R)¬¬(x > 0) ∨ ¬(x > 0) l
DISC:
A discontinuous 2N→ N-function exists.
