Forcing as a computational process

[Philip Thrift]

https://arxiv.org/abs/2007.00418

[Submitted on 1 Jul 2020]

Forcing as a computational process

Joel David Hamkins, Russell Miller, Kameryn J. Williams

We investigate how set-theoretic forcing can be seen as a computational process on the models of set theory. Given an oracle for information about a model of set theory ⟨M,∈M⟩, we explain senses in which one may compute M-generic filters G⊆ℙ∈M and the corresponding forcing extensions M[G]. Specifically, from the atomic diagram one may compute G, from the Δ0-diagram one may compute M[G] and its Δ0-diagram, and from the elementary diagram one may compute the elementary diagram of M[G]. We also examine the information necessary to make the process functorial, and conclude that in the general case, no such computational process will be functorial. For any such process, it will always be possible to have different isomorphic presentations of a model of set theory M that lead to different non-isomorphic forcing extensions M[G]. Indeed, there is no Borel function providing generic filters that is functorial in this sense.

@philipthrift

[Lawrence Crowell]

Forcing is a bizarre idea, where one introduces some new category or objects that extends a model. In some ways we do this with the extension of mathematics from the reals to complex numbers. The forcing of one system into another has some connections to the Jordan-Banach algebra as well. The replacement of a Poisson bracket structure {X, Y} → i/ħ[X, Y], is given by the replacement of generators that are Jordan with product rule A∘B = ½(AB + BA) to a Lie algebraic ad_A(B) = [A, B] product. For a general quantum system with a Lindblad type equation 

Idρ/dt = [H, ρ] + ½([Aρ, A^†] + [A, ρA^†]),

such that the Hamiltonian is an element of the Lie group L, usually as a weight, and the operators A and A^† are operators so that AρA^†,  AA^†ρ, and ρAA^† are operations on the density matrix that are Jordan. Depending upon how one looks at this we can think of the quantum mechanical theory on Fubini-Study metric on ℂP^n, say a metric based action or Lagrangian ℒ = g_{ab}y^ay^b to ℒ = g_{ab}y^ay^b + U(x_1, x_2, … ) with a general Euler-Lagrange equation

F_i = ∂/∂x_i(∂ℒ/∂y_a)y^a - ∂ℒ/∂x_i.

This is component version in Finsler geometry of a differential 1-form ω = πdq – dη. It should be apparent this is similar to the first law of thermodynamics. This is a “practical lesson” in what is meant by forcing. The imaginary valued system is extended to components that are further multiplied by i = √(-1). This is a sort of Wick rotation version of the forcing from reals to complex numbers.

The Jordan-Banach algebra though is just a start. We have the skew symmetry that corresponds to the conjugate on I = √(-1). This Lie algebraic system is in contrast to the Jordan product and algebra. We also have in physics fundamental properties due to bosonic and fermionic statistics.  In supersymmetry there are the Grassmann numbers that enter in to intertwine between these. Further, on a 2-dimensional space the interchange of two bosons or fermions is ambiguous. This is because a clockwise and counterclockwise rotational exchange are topologically distinct. In 3 dimensions of space the paths can be exchanged, but no in two. This means a sign change is possible in either boson or fermion cases. The stretched horizon of a black hole is a 2-dimensional surface and an anionic system for quantum fields. I think this is a foundation for how there are these dichotomies in physics, such as quantum mechanics and macroscopic physics and different statistics.  Instead of physics being founded on very large algebraic systems I think that Wigner had something right with the idea of small groups. The big symmetry systems come about from symmetry breaking or the removal of a degeneracy.

The fibration and Noether’s theorem in differential forms is λ = p_idq_i – Hdt, where the 1-form has a horizonal p_idq_i and vertical Hdt  principal bundles. This is a Finsler geometric way of seeing Lagrangian dynamics. The differential dλ = dp_i∧dq_i – dH∧dt, vanishes on the contact manifold. In a strict Finsler context the horizontal and vertical bundles are annulled separately. The q_i is the generator of p_i and dp_i = 0 means momentum is invariant under translation and similarly energy is conserved under time translations. If there is a Lagrange multiplier that connects the vertical and horizontal parts of the bundle then we have 

dp_i∧dq_i – dH∧dt = (dp_i/dt)dt∧dq_i – (∂H/dq_i)dq_i∧dt = [(dp_i/dt) + (∂H/dq_i)]dq_i∧dt 

which gives us the dynamical equation (dp_i/dt) = -∂H/dq_i. 

Hamkins et al paper is dense in set theoretic constructions. These things I have some introductory acquaintance with. I am also more interested in the practical transduction of such ideas. I will try to see what I can gather from this paper. Forcing does have some algorithmic connection and the above connects 1/kT ↔ it/ħ with macroscopic system with a temperature, or gravity in the case of spacetime physics, to time in the case of quantum mechanics.

LC

[Philip Thrift]

Whether forcing does anything for physics, I don't know, but ultimately it could be in future proof assistants (like Lean, Coq, etc.) and programming languages as a continuation of

• monadic programming
  • Every function can be computable!
  • A Haskell monad for infinite search in finite time
  • Computing in Cantor’s Paradise

 https://codicalist.wordpress.com/2020/05/23/dialectical-programming/

@philipthrift

[Lawrence Crowell]

It does not need that sort of intense structuring. The extension of real to complex numbers is a case of forcing of real numbers into pairs that obey multiplication rules for complex numbers. The extension with the identification 1/kT ↔ it/ħ is the basis for quantum criticality and the foundation of phase transitions. In this sense the quantum and classical domains of physics are different phases of matter and energy. 

LC

[Philip Thrift]

An alternative to (set theoretic)

https://arxiv.org/abs/2007.00418

Forcing as a computational process

is (type theoretic)

http://guilhem.jaber.fr/ComputationalInterpretationForcingTypeTheory.pdf
A Computational Interpretation of Forcing in Type Theory

[Philip Thrift]

On forcing and quantum gravity:

https://arxiv.org/search/quant-ph?searchtype=author&query=Kr%C3%B3l%2C+J

@philipthrift

[Philip Thrift]

> On forcing and quantum gravity:
> https://arxiv.org/search/quant-ph?searchtype=author&query=Kr%C3%B3l%2C+J

Also:

https://arxiv.org/abs/1602.02667

@philipthrift

[Lawrence Crowell]

I am familiar with Asselmeyer and Krol.

LC

[Bruno Marchal]

On 3 Jul 2020, at 14:30, Lawrence Crowell <goldenfield...@gmail.com> wrote:

It does not need that sort of intense structuring. The extension of real to complex numbers is a case of forcing of real numbers into pairs that obey multiplication rules for complex numbers.

That is not forcing in the theoretical meaning of the papers referred to by P. Thrift.

Forcing is an advanced technic in the study of the models of set theory, and it requires much more work in mathematical logic and set theory than what I use in my contribution. To be sure, Forcing is used in other model theory, including the models of Arithmetic. (See the book by Boolos and Jeffrey, or the new editions with Burgess on this).

In this case of forcing viewed as computation, it concerns a non standard notion of computations, and it might be of some use in the phenomenology of matter, as most technic in model theory does.

Technically, forcing can be seen as an exercise in modal logic. For those remembering Kripke semantics, the resemblance is striking, but it took some time before this has been made explicit, like Smullyan and Fitting did in their book on (Von Neuman Bernays Gödel) set theory. They found a logic of type S4 (like the first person mechanist phenomenology which isolate S4Grz1), and amazingly, where obliged to consider a quantization ([]<>p)  in their modal translation, but this might be only a coincidence. 

Bruno

--
You received this message because you are subscribed to the Google Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/49bc5442-f75f-4e69-9fea-d9fc8aa420f3o%40googlegroups.com.

[Bruno Marchal]

> On 4 Jul 2020, at 09:52, Philip Thrift <cloud...@gmail.com> wrote:
>
>
>
>
> On forcing and quantum gravity:
>
> https://arxiv.org/search/quant-ph?searchtype=author&query=Kr%C3%B3l%2C+J

I will take a closer look (in summer when I got more time). This looks more interesting … for physics, and perhaps Mechanism.

It might provides helpful tool to get the QM GR from the universal machine introspection, some day. People needs to first get well familiarised with the (mechanist) mind-body problem before (to be sure).

Bruno



>
>
> @philipthrift

>
> --
> You received this message because you are subscribed to the Google Groups "Everything List" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/ffe844fa-a026-4b50-ae09-d6bb8b1deeeao%40googlegroups.com.

[Philip Thrift]

On Saturday, July 4, 2020 at 5:39:49 AM UTC-5 Bruno Marchal wrote:

> On 4 Jul 2020, at 09:52, Philip Thrift <cloud...@gmail.com> wrote:
>
>
>
>
> On forcing and quantum gravity:
>
> https://arxiv.org/search/quant-ph?searchtype=author&query=Kr%C3%B3l%2C+J

I will take a closer look (in summer when I got more time). This looks more interesting … for physics, and perhaps Mechanism.

It might provides helpful tool to get the QM GR from the universal machine introspection, some day. People needs to first get well familiarised with the (mechanist) mind-body problem before (to be sure).

Bruno

Simple, right? :)

Add forcing 

     Forcing as a computational process

     https://arxiv.org/abs/2007.00418

to a proof assistant for QM

   Physics and proof assistants 

   http://hvg.ece.concordia.ca/events/formal-physics.htm

   https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4066961/

    Categorical quantum mechanics

    https://www.cs.ox.ac.uk/teaching/courses/2019-2020/cqm/

    w/ https://ncatlab.org/nlab/show/homotopy.io [proof assistant]

to get gravity

   https://arxiv.org/abs/quant-ph/0303089

   https://arxiv.org/abs/1602.02667

@philipthrift

 

[Lawrence Crowell]

On Saturday, July 4, 2020 at 5:31:24 AM UTC-5, Bruno Marchal wrote:

On 3 Jul 2020, at 14:30, Lawrence Crowell <goldenfield...@gmail.com> wrote:

It does not need that sort of intense structuring. The extension of real to complex numbers is a case of forcing of real numbers into pairs that obey multiplication rules for complex numbers.

That is not forcing in the theoretical meaning of the papers referred to by P. Thrift.

It is and is not. Agreed forcing is a dense set theoretic technique on how to extend a model into some other model. I think it was Hamkins who wrote on how forcing was really not that mysterious and used the example of extending integers into rationals, those into reals and those into ,,, . Set theory without some connection to actual mathematics is about as useless as tits on a boar hog. 

LC

 

To unsubscribe from this group and stop receiving emails from it, send an email to everyth...@googlegroups.com.

[Philip Thrift]

On Thursday, July 2, 2020 at 6:48:08 AM UTC-5 Philip Thrift wrote:

https://arxiv.org/abs/2007.00418

[Submitted on 1 Jul 2020]

Forcing as a computational process

Something in a real language (Lean 3):

A formalization of forcing and the unprovability of the continuum hypothesis [in Lean]

https://arxiv.org/abs/1904.10570

authors: 

   https://jesse-michael-han.github.io/

   http://florisvandoorn.com/

https://github.com/jesse-michael-han/flypitch

https://flypitch.github.io/

The Flypitch project aimed to produce a formal proof of the independence of the continuum hypothesis.

We have completed our original objective. We are now refining our library and exploring other formalization projects related to forcing and mathematical logic.

Our formalization uses Lean, an open source theorem prover and programming language primarily developed by Leonardo de Moura at Microsoft Research.

@philipthrift 

[Bruno Marchal]

On 4 Jul 2020, at 19:25, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Saturday, July 4, 2020 at 5:31:24 AM UTC-5, Bruno Marchal wrote:

On 3 Jul 2020, at 14:30, Lawrence Crowell <goldenfield...@gmail.com> wrote:

It does not need that sort of intense structuring. The extension of real to complex numbers is a case of forcing of real numbers into pairs that obey multiplication rules for complex numbers.

That is not forcing in the theoretical meaning of the papers referred to by P. Thrift.

It is and is not. Agreed forcing is a dense set theoretic technique on how to extend a model into some other model. I think it was Hamkins who wrote on how forcing was really not that mysterious and used the example of extending integers into rationals, those into reals and those into ,,, . Set theory without some connection to actual mathematics is about as useless as tits on a boar hog. 

I agree with you. I have made my master thesis on some extension of the forcing technic extending it to classes. 

Philosophically set theory is also a bit problematical, even if only because there are different conception of sets, from rather different theories, like Quine’s NF (well studied in my country), or by the infinitely many boolean and non boolean toposes.

Yet, we all use some set theory when doing mathematics, and the axiom of infinity is priceless, even in engineering.

With mechanism, the platonic realism, that is the belief in (A v ~A) is used only on a potential infinite, and concerning ways finite entities. Now, like mechanism entails a form of physical realism, it entails a sort of set-theorical realism too, which is hard to determine. The physical and the set theoretical being mainly phenomenological.

Forcing is not mysterious. It is really modal logic in disguise, but then it is also used in a context where something is not obvious at all, which is the notion of model of ZF. 

This is an extraordinary complicated object, which cannot be build for any “usual mathematics”, and which leads to even more extraordinary objects when we begun to study the large and the large large cardinals. It is a sort of vertical theology. The attempt to give a description of the “universe” (the collection of all sets).

I am teaching set theory this year, but I am still not sure I can progress enough to teach the technic of forcing. To show the independence of the axiom of infinity, and of the axiom of foundations, although much simpler, is not that simple for the student, and the difficulties are in the notion of model, especially of ultra-strong theories like ZF.

There is an extraordinary unexpected connection between the theory of braids and the theory of large large cardinal. A quite intriguing algebra is lurking there (the self-distributive algebra). Their main law is self-distributive, meaning that for all x, y z we have 

x(yz) = (xy)(xz). 

A result in the theory of braids (the existence of some order) has been found and proved by using the large large cardinal, by Laver,  but then an elementary proof has been found (by Dehornoy). 

Yet some result about the finite table of Laver remains proved only by using those extremely large cardinal. 

Braids are important in topological quantum computation, so set theory might have important applications, we never know… 

Of course, like with all powerful tool in math, you can also make a lot of abstract nonsense, or other advanced Sunday Philosophy!

Bruno

To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/57d45029-8821-4883-931c-42e161b959b2o%40googlegroups.com.

[Lawrence Crowell]

On Monday, July 6, 2020 at 9:29:31 AM UTC-5, Bruno Marchal wrote:

On 4 Jul 2020, at 19:25, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Saturday, July 4, 2020 at 5:31:24 AM UTC-5, Bruno Marchal wrote:

On 3 Jul 2020, at 14:30, Lawrence Crowell <goldenfield...@gmail.com> wrote:

It does not need that sort of intense structuring. The extension of real to complex numbers is a case of forcing of real numbers into pairs that obey multiplication rules for complex numbers.

That is not forcing in the theoretical meaning of the papers referred to by P. Thrift.

It is and is not. Agreed forcing is a dense set theoretic technique on how to extend a model into some other model. I think it was Hamkins who wrote on how forcing was really not that mysterious and used the example of extending integers into rationals, those into reals and those into ,,, . Set theory without some connection to actual mathematics is about as useless as tits on a boar hog. 

I think mathematics is best when it can be used to actually calculate things, whether that be with the physical world or in expanding areas of mathematics itself. The one thing that always caused some distaste for axiomatic set theory is that it often seems so detached and remote from anything else. 

LC

 

To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/57d45029-8821-4883-931c-42e161b959b2o%40googlegroups.com.

[Philip Thrift]

On Tuesday, July 7, 2020 at 9:10:28 AM UTC-5 Lawrence Crowell wrote:

I think mathematics is best when it can be used to actually calculate things, whether that be with the physical world or in expanding areas of mathematics itself. The one thing that always caused some distaste for axiomatic set theory is that it often seems so detached and remote from anything else. 

LC

Set theory (mathematics) does seem pretty irrelevant for (computational) physics today.

But forcing might be the way it could be:

Scientific proof-oriented programming (S-pop)

https://codicalist.wordpress.com/2020/07/06/scientific-proof-oriented-programming-s-pop/

@philipthrift

[Bruno Marchal]

On 7 Jul 2020, at 16:10, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Monday, July 6, 2020 at 9:29:31 AM UTC-5, Bruno Marchal wrote:

On 4 Jul 2020, at 19:25, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Saturday, July 4, 2020 at 5:31:24 AM UTC-5, Bruno Marchal wrote:

On 3 Jul 2020, at 14:30, Lawrence Crowell <goldenfield...@gmail.com> wrote:

It does not need that sort of intense structuring. The extension of real to complex numbers is a case of forcing of real numbers into pairs that obey multiplication rules for complex numbers.

That is not forcing in the theoretical meaning of the papers referred to by P. Thrift.

It is and is not. Agreed forcing is a dense set theoretic technique on how to extend a model into some other model. I think it was Hamkins who wrote on how forcing was really not that mysterious and used the example of extending integers into rationals, those into reals and those into ,,, . Set theory without some connection to actual mathematics is about as useless as tits on a boar hog. 

I think mathematics is best when it can be used to actually calculate things, whether that be with the physical world or in expanding areas of mathematics itself. The one thing that always caused some distaste for axiomatic set theory is that it often seems so detached and remote from anything else. 

Set theory is useful to make clear the semantic of simpler system. Cantor was trying to make sense of the differential equation of heat propagation.

But, unlike arithmetic, there is no real consensus of what a set should be, and there are different theories, like ZF and NF.

Intuitionist set theory can have application in numerical analysis, constructive computer science, etc.

Then, there is that extraordinary use of the most abstract (and theological) part of set theory (the Large large cardinal) which have been used to discover and proof the existence of some interesting order structure on the (infinite) braids, …

We never know. We cannot predict if some mathematics will or will not been applied. Hardy apologised for doing useless mathematics (number theory) which today is used each time we pay something on the net…

Bruno

To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/151a74ed-1cf8-4af5-9412-8b6ed6f68db3o%40googlegroups.com.

[Bruno Marchal]

On 8 Jul 2020, at 13:57, Philip Thrift <cloud...@gmail.com> wrote:

On Tuesday, July 7, 2020 at 9:10:28 AM UTC-5 Lawrence Crowell wrote:

I think mathematics is best when it can be used to actually calculate things, whether that be with the physical world or in expanding areas of mathematics itself. The one thing that always caused some distaste for axiomatic set theory is that it often seems so detached and remote from anything else. 

LC

Set theory (mathematics) does seem pretty irrelevant for (computational) physics today.

But forcing might be the way it could be:

But the links you gave us are not quite convincing for this, as it use the non standard models (which I take as a defect of first order logic) to develop a non standard notion of computation. It will be useful if Mechanism is wrong, but until there are some evidence for this, it looks a bit like advanced Sunday philosophy …. (Grin).

Scientific proof-oriented programming (S-pop)

https://codicalist.wordpress.com/2020/07/06/scientific-proof-oriented-programming-s-pop/

Don’t hesitate to sum up your point. Forcing is just a powerful technic to build weird model of set theory. Forcing is a particular S4-like modal logic.  The relation between Smullyan-Fitting “quantisation in S4” and the material mode of the self-referential machine is a bit an open problem for me. I might say more on this in some future.

Bruno

@philipthrift

--
You received this message because you are subscribed to the Google Groups "Everything List" group.

To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/47655ad1-c084-4693-afa0-f5011340a1can%40googlegroups.com.

[Philip Thrift]

On Friday, July 10, 2020 at 7:28:13 AM UTC-5 Bruno Marchal wrote:

On 8 Jul 2020, at 13:57, Philip Thrift <cloud...@gmail.com> wrote:

Scientific proof-oriented programming (S-pop)

https://codicalist.wordpress.com/2020/07/06/scientific-proof-oriented-programming-s-pop/

Don’t hesitate to sum up your point. Forcing is just a powerful technic to build weird model of set theory. Forcing is a particular S4-like modal logic.  The relation between Smullyan-Fitting “quantisation in S4” and the material mode of the self-referential machine is a bit an open problem for me. I might say more on this in some future.

Bruno

As outlined there: Repurpose a proof-oriented programming system (Coq, Lean, Agda) with forcing, e.g. 

        forcing in Lean: https://github.com/jesse-michael-han/flypitch

to do physics, e.g.

      categorical quantum mechanics - https://www.cs.ox.ac.uk/teaching/courses/2019-2020/cqm/

and implement 

      set-theoretical forcing in quantum mechanics - https://arxiv.org/abs/quant-ph/0303089

@philipthrift 

[Lawrence Crowell]

On Friday, July 10, 2020 at 7:21:29 AM UTC-5, Bruno Marchal wrote:

On 7 Jul 2020, at 16:10, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Monday, July 6, 2020 at 9:29:31 AM UTC-5, Bruno Marchal wrote:

On 4 Jul 2020, at 19:25, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Saturday, July 4, 2020 at 5:31:24 AM UTC-5, Bruno Marchal wrote:

On 3 Jul 2020, at 14:30, Lawrence Crowell <goldenfield...@gmail.com> wrote:

It does not need that sort of intense structuring. The extension of real to complex numbers is a case of forcing of real numbers into pairs that obey multiplication rules for complex numbers.

That is not forcing in the theoretical meaning of the papers referred to by P. Thrift.

It is and is not. Agreed forcing is a dense set theoretic technique on how to extend a model into some other model. I think it was Hamkins who wrote on how forcing was really not that mysterious and used the example of extending integers into rationals, those into reals and those into ,,, . Set theory without some connection to actual mathematics is about as useless as tits on a boar hog. 

I think mathematics is best when it can be used to actually calculate things, whether that be with the physical world or in expanding areas of mathematics itself. The one thing that always caused some distaste for axiomatic set theory is that it often seems so detached and remote from anything else. 

Set theory is useful to make clear the semantic of simpler system. Cantor was trying to make sense of the differential equation of heat propagation.

But, unlike arithmetic, there is no real consensus of what a set should be, and there are different theories, like ZF and NF.

Intuitionist set theory can have application in numerical analysis, constructive computer science, etc.

Then, there is that extraordinary use of the most abstract (and theological) part of set theory (the Large large cardinal) which have been used to discover and proof the existence of some interesting order structure on the (infinite) braids, …

We never know. We cannot predict if some mathematics will or will not been applied. Hardy apologised for doing useless mathematics (number theory) which today is used each time we pay something on the net…

Bruno

That is a part of my understanding. We have ZF set theory, with and without the axiom of choice, and then there are other very different set theories, such as Polish set theory. Then there is the HoTT homotopy type theory. It seems the goal of set theory to reduce all of mathematics to some completely fundamental objects, whether sets or types etc, that we have a plethora of these systems and a host of complexity.

LC

 

To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/151a74ed-1cf8-4af5-9412-8b6ed6f68db3o%40googlegroups.com.

[Bruno Marchal]

Forcing is a technic to construct models. As such it is used mainly to prove that some statement are not provable in some theory. The book by Boolos and Jeffrey contains a section on the use of forcing in arithmetic, but the most famous use are in set theory. In the long run this will be used in “theology”, but it is way to soon for this.

Bruno

@philipthrift 

--
You received this message because you are subscribed to the Google Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/7bc60b1c-f4b9-4696-b7fd-1f57665de911n%40googlegroups.com.

[Bruno Marchal]

On 10 Jul 2020, at 20:57, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Friday, July 10, 2020 at 7:21:29 AM UTC-5, Bruno Marchal wrote:

On 7 Jul 2020, at 16:10, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Monday, July 6, 2020 at 9:29:31 AM UTC-5, Bruno Marchal wrote:

On 4 Jul 2020, at 19:25, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Saturday, July 4, 2020 at 5:31:24 AM UTC-5, Bruno Marchal wrote:

On 3 Jul 2020, at 14:30, Lawrence Crowell <goldenfield...@gmail.com> wrote:

It does not need that sort of intense structuring. The extension of real to complex numbers is a case of forcing of real numbers into pairs that obey multiplication rules for complex numbers.

That is not forcing in the theoretical meaning of the papers referred to by P. Thrift.

It is and is not. Agreed forcing is a dense set theoretic technique on how to extend a model into some other model. I think it was Hamkins who wrote on how forcing was really not that mysterious and used the example of extending integers into rationals, those into reals and those into ,,, . Set theory without some connection to actual mathematics is about as useless as tits on a boar hog. 

I think mathematics is best when it can be used to actually calculate things, whether that be with the physical world or in expanding areas of mathematics itself. The one thing that always caused some distaste for axiomatic set theory is that it often seems so detached and remote from anything else. 

Set theory is useful to make clear the semantic of simpler system. Cantor was trying to make sense of the differential equation of heat propagation.

But, unlike arithmetic, there is no real consensus of what a set should be, and there are different theories, like ZF and NF.

Intuitionist set theory can have application in numerical analysis, constructive computer science, etc.

Then, there is that extraordinary use of the most abstract (and theological) part of set theory (the Large large cardinal) which have been used to discover and proof the existence of some interesting order structure on the (infinite) braids, …

We never know. We cannot predict if some mathematics will or will not been applied. Hardy apologised for doing useless mathematics (number theory) which today is used each time we pay something on the net…

Bruno

That is a part of my understanding. We have ZF set theory, with and without the axiom of choice, and then there are other very different set theories, such as Polish set theory. Then there is the HoTT homotopy type theory. It seems the goal of set theory to reduce all of mathematics to some completely fundamental objects, whether sets or types etc, that we have a plethora of these systems and a host of complexity.

We know today that there are no foundational theory which could based all of mathematics, and it is important to continue the distinction between basic concepts like numbers and functions from their representations in set theory, or even in category theory. But will mechanism, we get a very simple ontology to explain the “physical experience”, without having the assume a physical reality. With or without Mechanism, the fact that universal machine exist makes it impossible to have any complete theory about reality, whatever that reality is. But that means that even just in arithmetic, we must expect an infinity of surprises in the exploration. With Mechanism, *we* are such surprises already.

Set theory should be renamed. It is really the theory of the infinite(s). It is a sort of vertical theology: how to figure out what looks like a universe of sets. It attracts the lover of vertigo … Then, like always in mathematics, unexpected application rise up, like the apparent link between braids and some *very* large cardinal (Wooden, Laver, …).

Bruno

To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/ae8e661f-50d1-48a6-aabf-f55b4e8fe6deo%40googlegroups.com.

[Lawrence Crowell]

On Monday, July 13, 2020 at 7:07:36 AM UTC-5, Bruno Marchal wrote:

On 10 Jul 2020, at 20:57, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Friday, July 10, 2020 at 7:21:29 AM UTC-5, Bruno Marchal wrote:

On 7 Jul 2020, at 16:10, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Monday, July 6, 2020 at 9:29:31 AM UTC-5, Bruno Marchal wrote:

On 4 Jul 2020, at 19:25, Lawrence Crowell <goldenfield...@gmail.com> wrote:

On Saturday, July 4, 2020 at 5:31:24 AM UTC-5, Bruno Marchal wrote:

On 3 Jul 2020, at 14:30, Lawrence Crowell <goldenfield...@gmail.com> wrote:

It does not need that sort of intense structuring. The extension of real to complex numbers is a case of forcing of real numbers into pairs that obey multiplication rules for complex numbers.

That is not forcing in the theoretical meaning of the papers referred to by P. Thrift.

It is and is not. Agreed forcing is a dense set theoretic technique on how to extend a model into some other model. I think it was Hamkins who wrote on how forcing was really not that mysterious and used the example of extending integers into rationals, those into reals and those into ,,, . Set theory without some connection to actual mathematics is about as useless as tits on a boar hog. 

I think mathematics is best when it can be used to actually calculate things, whether that be with the physical world or in expanding areas of mathematics itself. The one thing that always caused some distaste for axiomatic set theory is that it often seems so detached and remote from anything else. 

Set theory is useful to make clear the semantic of simpler system. Cantor was trying to make sense of the differential equation of heat propagation.

But, unlike arithmetic, there is no real consensus of what a set should be, and there are different theories, like ZF and NF.

Intuitionist set theory can have application in numerical analysis, constructive computer science, etc.

Then, there is that extraordinary use of the most abstract (and theological) part of set theory (the Large large cardinal) which have been used to discover and proof the existence of some interesting order structure on the (infinite) braids, …

We never know. We cannot predict if some mathematics will or will not been applied. Hardy apologised for doing useless mathematics (number theory) which today is used each time we pay something on the net…

Bruno

That is a part of my understanding. We have ZF set theory, with and without the axiom of choice, and then there are other very different set theories, such as Polish set theory. Then there is the HoTT homotopy type theory. It seems the goal of set theory to reduce all of mathematics to some completely fundamental objects, whether sets or types etc, that we have a plethora of these systems and a host of complexity.

We know today that there are no foundational theory which could based all of mathematics, and it is important to continue the distinction between basic concepts like numbers and functions from their representations in set theory, or even in category theory. But will mechanism, we get a very simple ontology to explain the “physical experience”, without having the assume a physical reality. With or without Mechanism, the fact that universal machine exist makes it impossible to have any complete theory about reality, whatever that reality is. But that means that even just in arithmetic, we must expect an infinity of surprises in the exploration. With Mechanism, *we* are such surprises already.

Set theory should be renamed. It is really the theory of the infinite(s). It is a sort of vertical theology: how to figure out what looks like a universe of sets. It attracts the lover of vertigo … Then, like always in mathematics, unexpected application rise up, like the apparent link between braids and some *very* large cardinal (Wooden, Laver, …).

Bruno

I prefer in ways category theory, for at least it is connected to topology with Grothendieck and Etale cohomology. I am not highly learned in the subject, just the basic essentials. There is also the Langlands program where all theory can be reduced to numbers. The monstrous moonshine of Borscherds is interesting, and the bosonic string obeys the automorphism on the Fischer-Greiss group. 

We may never come to any pinnacle on this. It is my suspicion the human condition can be summed up as two stone ages punctuated by a disequilibrium situation. We happen to be in that disequilibrium situation, we call it civilization and history. The first stone age was in the Pleistocene when the Earth was biologically rich and the next one is in what might be called the anthropocene where the Earth will be depleted in a post-mass extinction period. I have suspicions we are near the peak of this disequilibrium situation, and if we are to come to some sort of summation of things, or at least known be a few of us, it might have to happen pretty soon.

LC