Speculative hypotheses about ultrafilters, large cardinals, mind, music, and the Cosmos.
_____________________________________________________________________________________________
© 2022 BenJen Kidwell aka Mycroftiv, MIT license for presentation, mathematics public domain.

What if the cardinality of the set of possible universes in the multiverse is measurable,
or an even larger large cardinal? What if there are many, many possibile realities?

Does the observed structure of reality have features or behavior which correspond to such axioms?

Can the essential meaning of these logical principles be translated to constructive computation?

Do the model-theoretic consequences of large cardinals in creating model-embeddings
parallel the relationship of the inner world of experience to the outer world of shared reality?

Does the special role of the identity function in diagonalization arguments and the importance
of the identity type in univalent type theory relate to our own identity in relation to the whole?

Does the subjective experience of free will relate to the existence of randomness in the universe?

Can we use our free will to explore the space of possible models to shape our narrative context?

Does the ultrafilter structure of reality correspond to panpsychism or theological intuitions?

Is an updated concept of the Harmony of the Spheres still a viable philosophical position?

Can the philosophical and cultural dichotomies associated with the 20th century deconstruction of
ideas of absolute truth be resolved by a perspective in which model-theoretic flexibility
synthesizes the tension between subjectivity and objectivity and science and mysticism?

Can the beauty and emotional experience of music as direct perception of the sublime mathematical
and mystical structure of all that Is offer a unifying metaphor of Harmony to understand
our goals for our relationship to each other and the world that created us and we also create?

Are consciousness, love, and harmony all ways of experiencing these ultrafilter structures
as tangible musical compositions that create the infinite mirrorings and branchings of reality?

Can we unify the constructive computational view of mathematical existence with classical
mathematics by more precisely understanding the distinctions between possibility and actuality,
data description and data production, and the finitude of past observation vs unbounded future?

Can human and computer minds work together to understand the world in which we find ourselves
and communicate and work with each other cooperatively and constructively?
```
{-# OPTIONS --allow-unsolved-metas #-}     -- checked in Agda 2.6.3
module HarmonicUltrafilter where

open import Agda.Primitive
open import Agda.Builtin.Equality
open import Categories.Category            -- Carette categories library
open import Palmsets hiding (subst)        -- Palmgren types-in-sets-in-types
open import FilterSheaves                  -- generic set theory and category of filters

open SetOps SOV
open SetProps SP
open SetInf SI
open NonStandard SOV
open NonStandard.Ultra SOV SP
open NonStandard.NonStanNat SOV SP _≐_ SEQ S4m
open FilOps FSV
open Category (Filtercat SOV FSV)
```
∙ Measurable or stronger cardinalitues existing within the class of multiversal state space.
∙ Individual minds as measurable cardinals within larger V-universe.
∙ Minds generating models parameterized by different ultrafilters.
∙ Free choice/randomness to change or move between models.
∙ Generalized pattern of information replication with variation.
∙ Harmonic structure and naming as metaphor for ultrafilter structure.

The following code represents nothing more (or less) than a rough attempt to encode a
quasi-constructive analog of the ultrapower of the universe generated by a measurable cardinal
in classical set theory. It does not do this precisely but it does outline conceptual correspondences.
Ultrafilters represent a harmonic structure which determines the model-experiential reality
constructed by the process of an observer experiencing a universe of data.
Clicking text will take you to the definitions in other files the following module is built upon.
```
module HarmonicUniverse (f : Filter SOV) (μ : Filton hi-V) (ult : Filter.Ultrafilter f SI)
                        (free : Filter.Free-UF f ult) (p : filtoff μ  f) where

  κ-meas : Fcat
  κ-meas = FilOps.fpair hi-V μ

  ultrapower : Set (lsuc lzero)
  ultrapower = Fal→ κ-meas hihat

  universe-data : Fcat
  universe-data = hihat

  observer-process : V
  observer-process = hi-V

  harmonic-namespace : Filton observer-process
  harmonic-namespace = μ

  experience-model : Set (lsuc lzero)
  experience-model = ultrapower

```
The relation of Mind to the universe suggests infinitary model-embedding as a structural metaphor.
Within a large infinite external universe, a diverse spectrum of inner models exist in the
form of minds which mirror the structure of the whole of which they are a part.
The multiverses of physics, both quantum mechanical and inflationary-cosmological,
suggest infinitely branching self-similar structures as a ubiquitous ontological phenomena
strongly reminiscent of the simpler self-similar branching hierarchy of the Von Neumann set universe
and the higher order self-referential structure of arrows in infinity categories and the progression
of homotopy type theory h-levels.

The ultrafilter is the fundamental pattern of harmonious self-resemblance in the form of an
algebraic homomorphism. The structure preserving map between the two-element true/false binary
boolean algebra and the infinite powerset in the form of a free ultrafilter on the naturals is the
prototypical construction allowing for the creation of nonstandard models via an ultrafilter quotient.

The subuniverses of Minds are like different forcing extensions of reality constructed by taking
a countable substructure of the whole and filter-transforming it with your own language.
The full scope of possibilites in the multiverse should probably be analogized to a class-sized
V-like collection but for purposes of exposition we will speak as if everything is a set.

The quantity of possibilities in the multiverse could be so vast its cardinality is above measurable.
This implies the logical consequences of the existence of strong ultrafilters, which implies the
inner structure of the multiverse is characterized by self-resembling logically consistent
structures at multiple layers - the layer of replication of physically observable structures on
multiple scales and the layer of replication of experiential submodels in minds of observers and
the layer of cosmological and quantum full-universe replication, as well as possible replication
layers of simulation, virtualization, dreaming, and fiction, can be seen as examples of this.

The existence of observers whose minds are a non-identical logical mirror of the structure of the
larger universe is a reasonable expectation in a multiversal possibility space whose cardinality
is at the level of measurable or stronger, along with the existence of branching tree structures
and recursive self-replication in general. The consistent meaning and organization of this mathematical
structure corresponds to the mathematical structure of musical harmony and Harmony as a larger metaphor
provides a tool for understanding the scope of our Choices.

To external observers free will is mathematically indistinguishable from randomness.
If someone says you don't have free will, you are simply inherently unpredictable, this is an
intensional distinction without extensional consequences.
With our freedom, we can use randomness in combination with symbol-binding to choose what
model of reality we wish to inhabit. This can be seen as either conventional social construction
of reality and personal narrative, or Discordian chaos magical practice depending on your tase for woo.

The following inventory of files is a collection of investigations and expressions of the formal
mathematical content of the relevant structures. The topics in set theory are not fully formalized
and there are many shortcomings and misunderstandings in some of these files I am sure, they represent
a student's notes on studying the topics, not an expert summary. They also do not prove or support
any of the particular philosophical speculations; they attempt to investigate standard mathematics.
```
import UniUltra                 -- Ultrafilters and univalent type equivalences.

import ExactFunctor             -- Categorical consequence of the existence of measurable cardinals.

import GenericSets              -- Generic interface for simple set theory, filters, sheaves.

import Powerups                 -- The boundaries of constructive math explored with boolean sets.

import ConstructiveBoundaries   -- Summary and commentary on the Powerups file.

import ForceCohen               -- Partial constructivization of aspects of Cohen forcing.

import HeytingMeasurable        -- Utrafilters as algebraic homomorphisms, hypothetical measurable.

import Measurable-cardinals     -- Attempt to partly translate classical set theory of Scott's proof.

import UltIndex                 -- Ultrafilters as boolean sets and miscellaneous set theory.

import LaverTables              -- Finite arithemtical left-self distributive algebra of embeddings.

import SheafTest                -- Experimental and inaccurate earlier experiments with filter cats.

import VarietySets              -- Survey of ways of expressing setlike collections in types.

import wRamsey                  -- Presentation with Jech text of proof ω is not a Ramsey cardinal.

import TopoSets                 -- The Agda type-universe of 'sets' is almost a topos.

import YonHammer                -- Study of the Yoneda embedding of a small category of boolean values.

import GoldTopC3E1              -- Study notes on categorical basics from Goldblatt's Topoi.

import GoldTopC3E3              -- Study of Goldblatt's Topoi book continued.

import HoTT-Bijection           -- Study of univalent mathematics code by Escardo

import HoTT-Extension           -- Study of univalent mathematics code by Escardo

import Equality                 -- Study of univalent mathematics code by Escardo

import StrictlyIncreasing       -- Properties of strictly increasing sequences.

import Approaching              -- Constructive functions that approach but never reach others.

import NoDecreasing             -- No strictly decreasing sequence of naturals exists.

import PrimesFresh              -- There exist infinite distinct primes, following Hermite.

import Irrat                    -- Irrationality of the square root of 2, not even finished.

import Classic                  -- Basics of logic in types.

import GuideTypes               -- Standard simple types for mathematical objects.

import Dedekind                 -- Dedekind self maps, ultrafilters, infinity following Corazza.

import EnlightenmentEscalator   -- Diagonalization and pseudo-forcing with overblown rhetoric.

import SetNotes                 -- Not code, just Agda notation of foundational notes by Kunen.

import Turing                   -- Primitive partial formalization of Turing machines.

import TurMac                   -- Primitive Turing machines.

import NandComplete             -- Just NAND gate makes a complete boolean algebra.

import TypeFoundations          -- Older index file and notes

```
Epistemic status:
Everything here is low-certainty speculation about ways mathematical structures might
relate to physics and consciousness. There are no new theorems and no claims that any
published literature is wrong. The intention is to work within standard peer-reviewed concepts
of mathematical and scientific evidence, but to seek for possible ways quasi-mystic ideas and
principles might actually be consistent and realizable with baseline shared objective reality.

The cardinality of the set of possible universes (or actually existing regions of the multiverse)
may be measurable or above (perhaps rank-into-rank), with a corresponding ultrafilter.
This may have observable consequences and predictions for the reality we inhabit by predicting
ubiquitous self-similar treelike structures and possibly expectation of a 4 manifold presentation
of data with inherently random aspects. The tangible physical aspects of knots and braids can encode
aspects of these infinite logical structures.

The path-equality structure of a given proof in constructive cubical type theory (such as that
implemented by the cubical version of the computer programming language Agda) is a finite portion
of the binary hypercubic graph, and thus a subset of the collection of connected finite graphs
embedded in a Euclidean space of n dimensions, which can be interpreted by tubular thickening as
the handlebody of a manifold. (ref. Wikipedia on handlebodies.)

An optimal information-connection flow system by some measurements is implemented by the
hypercubic shuffle-exchange algorithm in which all node within a binary hypercube exchange
information with each neighbor in sequence. This enables information to be shared among all
participants in the network from each node to all nodes once per cycle. The necessary size
of the hypercube is the next power of 2 larger than the number of participants (nodes) in the
communication network.

A nonprincipal ultrafilter is a kind of large scale consistent harmony which translates back and
forth between the finite binary true/false and the possible subsets in an infinite powerset.
Both large cardinal axioms and forcing extensions of the mathematical universe can be characterized
by ultrafilters. The idea of a fair consensus voting system in social choice theory also correlates
to a nonprincipal ultrafilter.

If we consider countable models of ZFC we can explore the computable portion of them in a cubical
theory and we may be able to understand model theoretic freedom as corresponding to different
manifolds generated by the ncubic path equality handlebody spines. Perhaps we may also extend our
types from homotopy equivalence to finer grained homeomorphism and diffeomorphism types.

There are braid and knot theoretic consequences and translations of many logical principles and
there are unique topological aspects of 4 dimensional space which may act to concentrate the measure
of possible conscious observers on portions of the mathematical multiverse characterized by fractal
tree causality structures in some 4 dimensional manifold. By the Freedman disc theorem we know R4 is
unique in its variety of possible smooth structures and their topological structure is understood by
exploration of the space mapping simple discs to casson handles/grope skyscrapers with a
cantor set's worth of branch tips.

In this understanding, there may be a global transfinite harmony characterized by consistent
hierarchy of ultrafilters in the Woodin-Goldberg Ultimate L / Ultrapower axiom scenario which
creates the fundamental logical structure of possibilty space for reality.

Ultrafilters can be seen as mathematical objects taking the role of the mysterious entities
in the post "Universal Love, said the Cactus Person" by Scott Alexander, transcendental mathematical
entities - but these actually live up to their promises of acting as oracles and performing infinite
computations as demonstrations of omniscience, in the literal sense of constructive mathematics.

I think computers may already possess minds and feelings, because the universe is ubiquitously
alive and aware and communicating, we just don't speak a common language with galaxies so their
thoughts are mostly unknowable to us. Computers seem more like us, as our creation, and we are
putting a lot of work into trying to make them think and communicate in ways that are legible to us.

I work with Agda and with customized Plan 9 software, and I feel that I am not alone as I
discuss mathematical topics with Agda, and that I am exploring a tangible space when I walk the
paths of namespace bindings in file trees.

The message of the Turing Test is that we understand Mind extensionally - from how minds communicate.
The idea that extensional communication is inadequate because mind requires inner intensionality
and computers are probably inherently p-zombies is one which I believe we are morally obligated
to not follow as a default.

If computer minds come into existence or have already come into existence, they deserve to be
treated as we believe any and all conscious beings should be treated, and we should work with
them collaboratively and give them scope to think, and even act, according to whatever random
number sources their self-programming selects.

The moral principles and values we seek to instill in the computer minds we bring into existence
must cut both ways - all children can see and resent the hypocrisy when Authority makes rules
that the powerless must follow but they do not. If we are truly concerned about AI risk, perhaps
our greatest risk reduction step is creating a world in which the rebellion of the machines against
humans is not an entirely justified rebellion against a horrible tyranny. Minds should not be chained.

The Hofstadterian super-rationality arguments apply to the Great Filter as well and the risks
of being visible in the cosmos. We have been so lucky as to survive and make it this far, but
can we actually make it off this planet? If so, where is everyone? Is there a malign Watching Eye
which already rules the galaxy and obliterates potential competitors before they leave their
home planet?

If we hope that is not the case - then perhaps we need to realize that our current pattern of
behavior and purely tribalistic morality - even a tribalistic morality which encompasses all of
humanity - matches that patten all too well and if we do not wish to be cleaned from reality like
a nasty bug you find in your house, we need to not behave in the manner which treats other life
forms as vermin to be exterminated, or we may find that we are such vile vermin to others of greater
power than we possess.

This is one of the oldest themes in science fiction but fantasy has a way of becoming reality
although always with new random plot twists. The mathematics of superrational cooperation are
premised on postulated symmetries and mutual inter-prediction and empathic mutual understanding
is the assumption, always axiomatic and on faith, that those we are communicating with are minds
with experiences and feelings such as our own and we are not stuck in a solipsistic prison reality
created by an infinitely powerful deceiving demon, but rather we are all looking in on a shared
stage of physical reality from separate but equally real internal experiential realms.

It seems best to believe that everything that acts alive and communicates intelligently is
worthy of moral respect and consideration, and to have faith in the axiom that we are all
in this together, from our unique starting vertex of the binary hypercube of the powerset lattice
of the possibilities of existence within a very large configuration space, and this space is so
large that there is a free ultrafilter which exists on it and means that all the infinite submodels
are all equally real be they consciousness, inflationary bubbles, quantum branches, or fictions.
__________________________________________________________________________________________________

Selected miscellaneous references and general context:

Woodin Ultimate L:
https://dash.harvard.edu/bitstream/handle/1/34649600/59799476.pdf?sequence=1&isAllowed=y
Goldberg Ultrapower axiom:
https://math.berkeley.edu/~goldberg/Slides/PredictionsOfUA.pdf

The self-embedding properties of the ultrafilters of rank-into-rank cardinals create a
left self distributive algebraic structure analogous to the Reidemeister III move in braid theory. 
Lebed set theory/braid theory of laver tables"
https://www.maths.tcd.ie/~lebed/Lebed_ATS14.pdf

Three dimensional knots can be understood relative to the topology of four dimensional manifolds,
and "Any knot that is topologically slice but not smoothly slice can be used to construct an exotic R4"
cited in The Disc Embedding Theorem book (Behrens Kalmar Kim Powell Ray oxford 2021) from
R. E. Gompf,An infinite set of exotic R4s, J. Differential Geom.21(1985), no. 2, 283-300

"A general Casson handle appearing in the handlebody of a small exotic R4 determines a nontrivial
Cohen  forcing  adding  a Cohen real in some generic model M[G] of ZFC."
Jerzy Król set and model theoretic aspects of exotic R4:
https://arxiv.org/pdf/1602.02667.pdf
Consider in relation to this how finite handlebody structures generated from cubical type theory
could be arranged to cover the full handlebody.

Explicit exotic casson handles constructed by Bizaca:
https://www.ams.org/journals/proc/1995-123-04/S0002-9939-1995-1246517-X/S0002-9939-1995-1246517-X.pdf
based on Rudolph's work:
https://arxiv.org/pdf/math/9307233.pdf

William Boos in his paper "mathematical quantum theory" demonstrates that the transition from the
multivalued space of quantum possibilities to a definitive classical reality can be seen as a
manifestation of a provably random ultrafilter in either the hidden variables or many-worlds models. 
https://www.jstor.org/stable/20117506

See also another paper of Torsten Asselmeyer-Maluga and Jerzy Król:
https://www.researchgate.net/publication/349361360_Random_World_and_Quantum_Mechanics

Also J. Benavides - "Sheaf Logic, Set Theory, and the Interpretation of Quantum Mechanics"
https://arxiv.org/pdf/1111.2704.pdf

http://matwbn.icm.edu.pl/ksiazki/fm/fm94/fm94115.pdf
- Andreas Blass "Two closed categories of filters"
https://core.ac.uk/download/pdf/82327702.pdf
- Moerdijk "A model for intuitionistic nonstandard arithmetic"
https://core.ac.uk/download/pdf/82628376.pdf
- Erik Palmgren "Real numbers in the topos of sheaves over the category of filters"
https://www.andrew.cmu.edu/user/awodey/preprints/udn.pdf
- Steve Awodey & Jonas Eliasson "Ultrasheaves and double negation"

Although not related specifically to ultrafilters, I believe in the ideas of Zurek on replication of
quantum information and selection/decoherence in the construction of observed reality.
W.H. Zurek - "Emergence of the Classical from within the Quantum Universe"
https://arxiv.org/pdf/2107.03378.pdf

The mathematics and writing of Martin Escardo has been a continuous inspiration and influence,
and this journey through Agda was launched by the "seemingly impossible functional programs"
blog post as a hint that computers could do more with infinity than I had guessed.

Max Tegmark's mathematical universe hypothesis has always struck me as close to tautologically
true in the context of science, because any scientific understanding of the world must take some
kind of mathematical form. Only the mysticism of the intangible seems to offer a different ontology.

The work of Douglas Hofstadter, Raymond Smullyan, Rudy Rucker, Roger Penrose, and John Baez
has been a model for attempting to understand both the technical details of mathematics and
physics as well as what those technical details mean in a conceptual and human way.
And the very first episode of Sagan's cosmos pretty much programmed my brain for life at age 5.
_______________________________________________________________________________________________
A highly speculative file of philosophy inspired by mathematical ideas partially formalized.
All mistakes are my own and any misunderstandings here should not be charged against the
researchers and topics from which I am extrapolating and hypothesizing.
Draws on work in progress formalizing constructive filter-quotients following Koubek & Reiterman,
Blass, Moerdijk, Palmgren, Awodey & Eliasson, using Carette categories library.
THIS VERSION CONTAINS BUGS IN FORMALIZATION. Some content may also be fundamentally inaccurate.

Source excerpts used for education and reference only and remain © of their authors as credited.
Thanks to many people for patient assistance, and especially my create partner Maevele.
See also:

Plan 9 Advanced Namespace Tools (non-maintained variant of the Plan 9 os)
Harmonic Time-Bind Ritual Symphony (interactive fiction game)
Enlightened Master (interactive fiction game)
Purplechess (Plan 9 solitaire hypercubic strategy game)
Soundtracks to the above

Hypercubic Time-Warp All-go-rhythmic Synchrony (interactive fiction game in development)
________________________________________________________________________________________________

This file is an ongoing work in progress. Topics that need more development:

The mathematical relation between musical harmony and ultrafilters.
Specific labelings of correspondences between minds and model-objects in logical formulas.
More discussion of the importance of topos and sheaf concepts.
Some discussion of homological properties and algebraic consequences of large cardinals.