ファイル置き場 Sendai Logic Homepage 101112sanders

(1)

Sam Sanders

Mathematical Institute, Tohoku University

Sendai, Logical Seminar, Friday Nov. 12, 2010

(2)

Constructive Mathematics

. . . isErret Bishop-style mathematics, in this talk.

(3)

Constructive Mathematics

We introduce Constructive Mathematics and discuss its connections to Nonstandard Analysis.

(4)

Constructive Mathematics

We introduce Constructive Mathematics and discuss its connections to Nonstandard Analysis.

(Conference Reuniting the antipodes + Several papers)

(5)

The prehistory: Intuitionistic Mathematics

L.E.J. Brouwer founded intuitionism, a vagueanti-platonist philosophy of Mathematics.

(6)

The prehistory: Intuitionistic Mathematics

1 An object only exists after it is constructed.

(7)

The prehistory: Intuitionistic Mathematics

2 Brouwer rejects the principle of excluded middle.

(8)

The prehistory: Intuitionistic Mathematics

3 Actual infinity does not exist, potential infinity does.

(9)

The prehistory: Intuitionistic Mathematics

3 Actual infinity does not exist, potential infinity does.

4 No ‘sterile’ formalism: only intuitions of the creative subject.

(10)

Arend Heyting formalized Intuitionism into Intuitionistic Logic (IL).

(11)

1 _∧,_∀ have the usual meaning.

(12)

2 _(∃x)A(x)means a witness x0 s.t.A(x0) can be computed.

(13)

3 _{A proof of} _{A ∨ B} consists of a proof ofA or a proof ofB.

(14)

4 _¬A means a proof ofAimplies a contradiction/is impossible.

(15)

5 _{A → B} means a proof ofA can be converted to a proof ofB.

(16)

5 _{A → B} means a proof ofA can be converted to a proof ofB. (Brouwer-Heyting-Kolmogorov (BHK) intepretation)

(17)

Properties of IL

(#1) IL rejects the principle of excluded middle (PEM):

(18)

Properties of IL

A ∨ ¬Ameans ‘We have a proof of A or a proof of ¬A’. (Omniscience)

(19)

Properties of IL

A ∨ ¬Ameans ‘We have a proof of A or a proof of ¬A’. (Omniscience) (#2) IL rejects the double negation elimination (DNE):

(20)

Properties of IL

¬¬A → Ameans ‘If it is impossible that a proof of A is impossible, then we have a proof of A’.

(21)

Properties of IL

(#3) No proofs by contradiction in IL: only direct constructions.

(22)

Properties of IL

(#3) No proofs by contradiction in IL: only direct constructions. (#4) Results in IL are not ‘safer’ than classical logic (CL):

(23)

Properties of IL

(#3) No proofs by contradiction in IL: only direct constructions. (#4) Results in IL are not ‘safer’ than classical logic (CL):

If CL ⊢ [0 = 1], then IL ⊢ [0 = 1].

(24)

Strange consequences

Mathematics based on IL can be strange:

(25)

Strange consequences

(#1) IL rejectsAC: some vector spaces do not have a basis.

(26)

Strange consequences

(#1) IL rejectsAC: some vector spaces do not have a basis. Solution: talk only about vector spaces with a (constructive) basis.

(27)

Strange consequences

(#1) IL rejectsAC: some vector spaces do not have a basis. Solution: talk only about vector spaces with a (constructive) basis. (#2)CZFproves ‘Each total function from R to R is continuous’.

(28)

Strange consequences

(#1) IL rejectsAC: some vector spaces do not have a basis. Solution: talk only about vector spaces with a (constructive) basis. (#2)CZFproves ‘Each total function from R to R is continuous’. CZF and ZF prove the samearithmetical theorems

(29)

Strange consequences

(#3) The following principle, calledLPO, is rejected: For any real number x, we havex > 0 ∨ ¬(x > 0). Similarly, IVT is rejected.

(30)

Strange consequences

(#3) The following principle, calledLPO, is rejected: For any real number x, we havex > 0 ∨ ¬(x > 0). Similarly, IVT is rejected.

(#4) The following is provable in CZF:

It is false that a real number is either rational or irrational.

(31)

Erret Bishop’s Constructive Mathematics

The aim: to give numerical meaning to as much as possible of classical mathematics.

(32)

Erret Bishop’s Constructive Mathematics

Three central principles:

(33)

Erret Bishop’s Constructive Mathematics

1 Every concept is affirmative/positive. (Use of IL)

(34)

Erret Bishop’s Constructive Mathematics

2 Only use relevant definitions. (Uniform cont. and diff.)

(35)

Erret Bishop’s Constructive Mathematics

3 Avoid pseudogeneralities. (Spaces are separable to avoid AC)

(36)

Erret Bishop’s Constructive Mathematics

3 Avoid pseudogeneralities. (Spaces are separable to avoid AC) Hence, Bishop’s constructive mathematics (or BISH) is similar to RCA0.

(37)

Mathematics in BISH: some examples

(38)

Mathematics in BISH: some examples

Bishop: Every theorem of classical mathematics presents a challenge: find aconstructive version with a constructive proof.

(39)

Mathematics in BISH: some examples

Bishop: Every theorem of classical mathematics presents a challenge: find aconstructive version with a constructive proof. Thisconstructive versioncan be obtained by strengthening the conditionsor weakening the conclusionof the theorem.

(40)

Mathematics in BISH: some examples

Peano’s theorem for y^′ = f (x, y ) is equivalent to WKL within RCA₀. Hence, too strong for BISH.

(41)

Mathematics in BISH: some examples

Peano’s theorem for y^′ = f (x, y ) is equivalent to WKL within RCA₀. Hence, too strong for BISH.

ImposingLipschitz conditions on f (x, y ) results in Picard’s theorem, which is provable in BISH.

(42)

Mathematics in BISH: some examples

(43)

Mathematics in BISH: some examples

The Supremum Principle implies PEM:

A set S ⊂ R that is bounded above hasa least upper bound.

(44)

Mathematics in BISH: some examples

A set S ⊂ R that is bounded above hasa least upper bound. The weaker constructive version is:

A set S ⊂ R that is bounded above satisfies, for all α, β ∈ R, either β is an upper bound for S or there is s ∈ S such that s > α.

(45)

Mathematics in BISH: some examples

A set S ⊂ R that is bounded above hasa least upper bound. The weaker constructive version is:

A set S ⊂ R that is bounded above satisfies, for all α, β ∈ R, either β is an upper bound for S or there is s ∈ S such that s > α. For IVT, we also need to weaken the conclusion.

(46)

Mathematics in BISH: IVT

Definition

A real number x is a Cauchy sequence (x_n) with modulus h(k) s.t. (∀k)(∀n, m ≥ h(k))(|x_n− x_m| < ¹_k).

(47)

Mathematics in BISH: IVT

Definition

Theorem

A real number x = (x_n) satisfies x > 0 iff (∃N)(∀n)(x_n> _N¹).

(48)

Mathematics in BISH: IVT

Definition

Theorem

A real number x = (x_n) satisfies x > 0 iff (∃N)(∀n)(x_n> _N¹). We havex = y iff (∀k)(∃N)(∀n ≥ N)(|x_n− y_n| < ¹_k).

(49)

Mathematics in BISH: IVT

Definition

Theorem

A real number x = (x_n) satisfies x > 0 iff (∃N)(∀n)(x_n> _N¹). We havex = y iff (∀k)(∃N)(∀n ≥ N)(|x_n− y_n| < ¹_k).

Note that theN can be computed by an algorithm/witnessing function/modulus.

(50)

Mathematics in BISH: IVT

Let GC (n) be ‘Goldbach’s conjecture holds for the number 2n + 4’.

(51)

Mathematics in BISH: IVT

Let GC (n) be ‘Goldbach’s conjecture holds for the number 2n + 4’. Define

a_n:=

(−2⁻ⁿ if ¬GC (n)

2⁻ⁿ if GC (n) ^{and a :=}

+∞

X

n=1

a_i.

(52)

Mathematics in BISH: IVT

a_n:=

(−2⁻ⁿ if ¬GC (n)

+∞

X

n=1

a_i.

ThenGoldbach’s conjecture holds iffa = 1.

(53)

Mathematics in BISH: IVT

a_n:=

(−2⁻ⁿ if ¬GC (n)

+∞

X

n=1

a_i.

Define f (x) as the piecewise linear function such that f (0) = −1, f (1) = 1 and f (¹₃) = f (²₃) = a.

(54)

Mathematics in BISH: IVT

a_n:=

(−2⁻ⁿ if ¬GC (n)

+∞

X

n=1

a_i.

Define f (x) as the piecewise linear function such that f (0) = −1, f (1) = 1 and f (¹₃) = f (²₃) = a.

ThenGoldbach’s Conjecture holds ifff (1/6) = 0.

(55)

Mathematics in BISH: IVT

Assume IVT is provable in BISH.

(56)

Mathematics in BISH: IVT

Assume IVT is provable in BISH. Theorem (IVT)

If f : [0, 1] → [0, 1] is (uniformly ) continuous and f (0) < 0 and f (1) > 0, then (∃x0∈ [0, 1])[f (x0) = 0].

(57)

Mathematics in BISH: IVT

As we cancompute x₀ in BISH,

(58)

Mathematics in BISH: IVT

As we cancompute x₀ in BISH, we now can decide whether x₀ is 1/6 or not.

(59)

Mathematics in BISH: IVT

As we cancompute x₀ in BISH, we now can decide whether x₀ is 1/6 or not. Hence, we can decideGoldbach’s conjecturein BISH, given IVT.

(60)

Mathematics in BISH: IVT

Thus, IVT cannot be provable in BISH.

(61)

Mathematics in BISH: IVT

Thus, IVT cannot be provable in BISH.

The function f is called a Brouwerian counterexample. Similar coding tricks show that LPO (x > 0 ∨ ¬(x > 0)) cannot be proved in BISH.

(62)

Constructive Reverse Mathematics

... is Reverse Mathematics in a constructive base theory C (BISH, EL0).

(63)

Constructive Reverse Mathematics

... is Reverse Mathematics in a constructive base theory C (BISH, EL0). Classical Reverse Mathematics: given a theorem of ordinary mathematics T , find a logical principle A such thatRCA0⊢ (A ↔ T ).

(64)

Constructive Reverse Mathematics

... is Reverse Mathematics in a constructive base theory C (BISH, EL0). Classical Reverse Mathematics: given a theorem of ordinary mathematics T , find a logical principle A such thatRCA0⊢ (A ↔ T ).

Constructive Reverse Mathematics(or CRM): given T , a theorem of ordinary mathematics, find A, a logical principle, andL, aninstance of PEM, such thatC ⊢ (A +L↔ T ).

(65)

Constructive Reverse Mathematics

Theorem

In BISH, LLPO (¬(x > 0) ∨ ¬(x < 0)) is equivalent to

1 _WKL

2 _IVT

3 Weierstrass Extremum theorem

4 Hahn Banach theorem

5 Rhas no nilpotent elements.

(66)

Constructive Reverse Mathematics

Theorem

1 _WKL

2 _IVT

5 Rhas no nilpotent elements. In BISH, FAN is equivalent to

1 Dini’s theorem

2 Heine’s theorem

3 Heine-Borel theorem for cozero sets.

(67)

Constructive Reverse Mathematics

Theorem

1 _WKL

2 _IVT

5 Rhas no nilpotent elements. In BISH, FAN is equivalent to

1 Dini’s theorem

2 Heine’s theorem

3 Heine-Borel theorem for cozero sets.

FAN is the Fan Theorem for detachable bars. Classically, FAN ↔ WKL.

(68)

Constructive Reverse Mathematics

Theorem

In BISH, LPO is equivalent to

1 Bolzano-Weierstrass theorem

2 montone convergence theorem

3 Cantor’s intersection theorem

(69)

Constructive Reverse Mathematics

Theorem

In BISH, most theorems classically equivalent to ACA0, are equivalent to LPO.

(70)

Constructive Reverse Mathematics

Theorem

In BISH, most theorems classically equivalent to ACA0, are equivalent to LPO.

However, BISH proves the Cauchy convergence theorem (Every Cauchy sequence converges).

(71)

Constructive Reverse Mathematics

The theory EL0, a constructive version of RCA0, is a better base theory.

(72)

Constructive Reverse Mathematics

Theorem

In EL₀, themonotone convergence theoremis equivalent to Σ₁-PEM + Π⁰₁-AC₀₀.

(73)

Constructive Reverse Mathematics

Theorem

Σ₁-PEM:excluded middle axiom

(74)

Constructive Reverse Mathematics

Theorem

Π⁰₁-AC00: function existence axiom, similar to ACA0.

(75)

Constructive Reverse Mathematics

Theorem

Π⁰₁-AC00: function existence axiom, similar to ACA0. . . . and many theorems like this.

(76)

Constructive Reverse Mathematics

Theorem

Π⁰₁-AC00: function existence axiom, similar to ACA0. . . . and many theorems like this.

(77)

Similarities

We claim there are many similarities between Nonstandard Analysis in ERNA and Constructive Mathematics in BISH.

(78)

Similarities

We claim there are many similarities between Nonstandard Analysis in ERNA and Constructive Mathematics in BISH. In particular,computability/decidabilityin BISH seems to correspond to external operationsin ERNA (operations on formulas with≈).

(79)

Similarities

We claim there are many similarities between Nonstandard Analysis in ERNA and Constructive Mathematics in BISH. In particular,computability/decidabilityin BISH seems to correspond to external operationsin ERNA (operations on formulas with≈).

Recall that ERNA is a nonstandard extension of I ∆₀+ exp.

(80)

Similarities between NSA and Constructive Mathematics

Constructive Mathematics in BISH Nonstandard Analysis in ERNA

(81)

Similarities between NSA and Constructive Mathematics

The predicates x > y , x = y , x ≫ y and x ≈ y are not decidable. Constructive Mathematics in BISH Nonstandard Analysis in ERNA

x > y and x = y x ≫ y and x ≈ y

(82)

Similarities between NSA and Constructive Mathematics

We havex = y ↔ (∀n)(|x_n− y_n| < ¹_n) andx ≈ y ↔ (∀n ∈ N)(|x − y | < ¹_n). The predicatex ≫ y is defined asx > y ∧ x 6≈ y.

Constructive Mathematics in BISH Nonstandard Analysis in ERNA x > y and x = y x ≫ y and x ≈ y

(83)

Similarities between NSA and Constructive Mathematics

In ERNA, we need f^′(x₀) ≫ 0 to ensure f (x) increases around x₀. Constructive Mathematics in BISH Nonstandard Analysis in ERNA

x > y and x = y x ≫ y and x ≈ y

(84)

Similarities between NSA and Constructive Mathematics

standard part function: st(x + ε) = x, with x standard and ε ≈ 0 Constructive Mathematics in BISH Nonstandard Analysis in ERNA

x > y and x = y x ≫ y and x ≈ y no standard part function no standard part function

(85)

Similarities between NSA and Constructive Mathematics

Constructive Mathematics in BISH Nonstandard Analysis in ERNA x > y and x = y x ≫ y and x ≈ y no standard part function no standard part function

uniform cont. and diff. uniform cont. and diff.

(86)

Similarities between NSA and Constructive Mathematics

uniform cont. and diff. uniform cont. and diff. finite set property hyperfinite set property

(87)

Similarities between NSA and Constructive Mathematics

finite set property: not every subset of a finite set is finite hyperfinite set property: not every subset of ahyperfiniteset is hyperfinite

uniform cont. and diff. uniform cont. and diff. finite set property hyperfinite set property

(88)

Similarities between NSA and Constructive Mathematics

uniform cont. and diff. uniform cont. and diff. finite set property hyperfinite set property computable witnesses computable witnesses

(89)

Similarities between NSA and Constructive Mathematics

‘(∃x)ϕ(x)’ means ‘there is an algorithm to compute x₀ s.t. ϕ(x₀)’. Constructive Mathematics in BISH Nonstandard Analysis in ERNA

x > y and x = y x ≫ y and x ≈ y no standard part function no standard part function

uniform cont. and diff. uniform cont. and diff. finite set property hyperfinite set property computable witnesses computable witnesses

(90)

Similarities between NSA and Constructive Mathematics

In Constructive RM, an important principle is Principle (Σ₁-excluded middle)

For every q.f. formula ϕ, we have (∃n)ϕ(n) ∨ (∀n)¬ϕ(n).

(91)

Similarities between NSA and Constructive Mathematics

For every q.f. formula ϕ, we have(∃n)ϕ(n)∨ (∀n)¬ϕ(n).

In constructive math.,(∃n)ϕ(n)means ‘we can compute a number n₀ s.t. ϕ(n₀)’.

(92)

Similarities between NSA and Constructive Mathematics

Principle (Π1-transfer)

For every q.f. formula ϕ, we have (∃n ∈ N)ϕ(n) ∨ (∀n ∈^∗^N)¬ϕ(n).

(93)

Similarities between NSA and Constructive Mathematics

For every q.f. formula ϕ, we have(∃n ∈ N)ϕ(n)∨ (∀n ∈^∗^N)¬ϕ(n). To find a witness for(∃n ∈ N)ϕ(n), calculate (µn ≤ ω)ϕ(n).

(94)

Similarities between NSA and Constructive Mathematics

In Constructive RM, an important principle is Principle (Σ1-excluded middle)

For every q.f. formula ϕ, we have (∃n ∈ N)ϕ(n) ∨ (∀n ∈^∗^N)¬ϕ(n). To find a witness for(∃n ∈ N)ϕ(n), calculate (µn ≤ ω)ϕ(n). Thus, Π₁-transfer is ‘hyperexcluded middle’: it excludes the possibility ‘(∀n ∈ N)¬ϕ(n) ∧ ϕ(ω)’ for some infinite ω.

(95)

Similarities between NSA and Constructive Mathematics

For every q.f. formula ϕ, we have (∃n ∈ N)ϕ(n) ∨ (∀n ∈^∗^N)¬ϕ(n). To find a witness for(∃n ∈ N)ϕ(n), calculate (µn ≤ ω)ϕ(n). Recall, Σ1-PEM makes Σ1-formulas decidable.

(96)

Similarities between NSA and Constructive Mathematics

For every q.f. formula ϕ, we have (∃n ∈ N)ϕ(n) ∨ (∀n ∈^∗^N)¬ϕ(n). To find a witness for(∃n ∈ N)ϕ(n), calculate (µn ≤ ω)ϕ(n). Recall, Σ1-PEM makes Σ1-formulas decidable. Also, Π1-TRANS makes Σ1-formulas decidable: replace(∃n ∈^∗^N)ϕ(n)with(∃n ≤ ω)ϕ(n).

(97)

Similarities between NSA and Constructive Mathematics

1 Both BISH and ERNA + Π1-TRANS prove the Cauchy Convergence Theorem, but do notprove the Monotone Convergence Theorem or Bolzano-Weierstrass.

(98)

Similarities between NSA and Constructive Mathematics

1 Both BISH and ERNA + Π1-TRANS prove the Cauchy Convergence Theorem, but do notprove the Monotone Convergence Theorem or Bolzano-Weierstrass. We need LPO (x > 0 ∨ ¬(x > 0)) and EXIT.

(99)

Similarities between NSA and Constructive Mathematics

2 Both BISH and ERNA + Π1-TRANS do not prove IVT: only a version up to arbitrary ε ∈ R⁺/infinitesimals.

(100)

Similarities between NSA and Constructive Mathematics

3 Both BISN and ERNA + Π1-TRANS do not prove the Supremum Principle: only a version up to arbitrary ε ∈ R⁺/infinitesimals.

(101)

Similarities between NSA and Constructive Mathematics

4 Both BISH and ERNA + Π1-TRANS only prove a weak version of Weierstrass’ Extremum Theorem/Taylor’s theorem/. . . .

(102)

Similarities between NSA and Constructive Mathematics

(103)

Similarities between NSA and Constructive Mathematics

5 _Σ₂-PEM corresponds to Σ2-TRANS. The latter, together with EXIT, makes standard Σ2-formulas decidable.

(104)

Real Computability?

Recall: Constructive Mathematics is all about numerical content.

(105)

Real Computability?

Recall: Constructive Mathematics is all about numerical content. Let f (x) be continuous in the sense of Bishop:

(∀k)(∀x, y ∈ [0, 1])(|x − y | < _h(k)¹ → |f (x) − f (y )| < ¹_k). (1)

(106)

Real Computability?

(∀k)(∀x, y ∈ [0, 1])(|x − y | < _h(k)¹ → |f (x) − f (y )| < ¹_k). (1) What do we see when zooming in on f (x)?

(107)

Real Computability?

According to (1), we can keep zooming on f and see a continuous line.

(108)

Real Computability?

According to (1), we can keep zooming on f and see a continuous line. In reality, amethod/machine/measurement M has aresolution R. Thus, M cannot distinguish two points x and y if |x − y | < _R¹.

(109)

Real Computability?

According to (1), we can keep zooming on f and see a continuous line. In reality, amethod/machine/measurement M has aresolution R. Thus, M cannot distinguish two points x and y if |x − y | < _R¹. If M cannot distinguish x and y , it cannot distinguish f (x) and f (y ).

(110)

Real-world Computability!

If Mcannot distinguishx and y , it cannot distinguishf (x) and f (y ).

(111)

Real-world Computability!

If Mcannot distinguishx and y , it cannot distinguishf (x) and f (y ). What about: if x and y arevery close(compared to M), then f (x) and f (y ) arevery close?

(112)

Real-world Computability!

What about: if x ≈y , then f (x)≈f (y )?

(113)

Real-world Computability!

What about: if x ≈y , then f (x)≈f (y )? This is not so crazy: recall Herbrand’s Theorem!

(114)

Real-world Computability!

BIG CONJECTURE:

NSA can provide asuperior notion of real-world computability.

(115)

Real-world Computability!

BIG CONJECTURE:

NSA can provide asuperior notion of real-world computability. ps: Yokoyama is working on a combination of Recursion Theory and NSA!

(116)

Real-world Computability!

BIG CONJECTURE:

NSA can provide asuperior notion of real-world computability. ps: Yokoyama is working on a combination of Recursion Theory and NSA!

Thanks for your attention!

Any questions?