Non-standard analysis

Stream: mathlib4

[Violeta Hernández]

I've been thinking about non-standard analysis recently. We currently have a very bare-bones theory of hyperreals at docs#Hyperreal - though note that two thirds of this file is deprecated at #33650. I'm wondering if it'd be worth expanding this out, or whether the subject is too niche to have anything beyond the most basic theorems.

[Ruben Van de Velde]

I guess we should ask @Kevin Buzzard if he encountered any nonstandard analysis in the Annals :)

[Violeta Hernández]

To be clear, I don't want to re-do the theory of calculus that Mathlib already has using hyperreals, I think that effort would be redundant and quite naive. But I would like to at least prove some basic results: hyperreals are real-closed, there is a floor/ceiling function into the hyperintegers, they are an η₁ order, that kind of stuff.

[Violeta Hernández]

I'd also like to point out that we probably don't even want the hyperreals themselves! We could very well define:

def Hyper (R : Type*) : Type* := (Filter.hyperfilter ℕ).Germ R

scoped postfix:max "*" => Hyper

And this lets us talk about hypernaturals, hyperintegers, etc. all at once. The vast majority if not all of non-standard analysis should generalize to the setting of a real-closed field.

[Kevin Buzzard]

I supervised the project which turned into the hyperreals (and I certainly didn't, and don't, have a good understanding of what we should have done, if it's not what Abhi did) but I didn't see any nonstandard analysis in the Annals. But that's not really relevant -- even though my personal view on where mathlib should be concentrating its efforts is "towards stating recent papers in the top journals" this is certainly not a view shared by all the maintainers, and indeed the maintainers are unable to come to a coherent position about what areas we'd like to see being developed because we have too many contradictory opinions on the matter :-)

[Violeta Hernández]

Well, perhaps I could rephrase my question. Is there any maintainer with the domain knowledge to review my work if I started working on this?

[Mirek Olšák]

Violeta Hernández said:

I'd also like to point out that we probably don't even want the hyperreals themselves! We could very well define:

def Hyper (R : Type*) : Type* := (Filter.hyperfilter ℕ).Germ R

scoped postfix:max "*" => Hyper

And this lets us talk about hypernaturals, hyperintegers, etc. all at once. The vast majority if not all of non-standard analysis should generalize to the setting of a real-closed field.

A student (Daniel Perout) asked me recently about non-standard analysis in Lean. So I also recommended him doing something similar:

def ultraFilter : Ultrafilter ℕ := Ultrafilter.of .atTop

/--
Converts a Type into a nonstandard Type using an ultrafilter,
for example `Ultra ℕ` are non-standard natural numbers. -/
def Ultra (α : Type) : Type := ultraFilter.Product (fun _ ↦ α)

Your proposal might be more idiomatic (and working across universes, which I prefered not to start with for pedagogical reasons).

[Mirek Olšák]

I would see as a nice test for a non-standard analysis system the proof of

• every continuous function on a closed interval has a maximum

with the reasoning:

• subsample the interval on N points where N is nonstandard natural number,
• in the nonstandard world, this set of positions is finite, so we can find the position with maximal value.
• rounding the nonstandard value to a real value gives the maximum of the real continuous function

[Mirek Olšák]

And by the way, here is a draft file of more detailed ideas of how imagined basic building blocks of the theory.
Nonstandard.lean

[Violeta Hernández]

I don't think we have the stuff for finite types or the app function, but everything else should be in there.

[Violeta Hernández]

docs#Filter.Germ has a pretty good API from what I've seen and we can largely just reuse that

[Violeta Hernández]

Mirek Olšák said:

I would see as a nice test for a non-standard analysis system the proof of

• every continuous function on a closed interval has a maximum

with the reasoning:

• subsample the interval on N points where N is nonstandard natural number,
• in the nonstandard world, this set of positions is finite, so we can find the position with maximal value.
• rounding the nonstandard value to a real value gives the maximum of the real continuous function

Does this argument really work? I'm not confident you can write down "every set of size n has a maximum element" as a first-order predicate.

[Mirek Olšák]

I would argue it works although at the same time, I didn't lay out very precisely how it is supposed to work (also depends on the exact way of building the system)

[Mirek Olšák]

If I wanted to do this in some FOL, I just start with big enough model containing all the concepts -- functions, sets, and take the ultraproduct of that.

[Mirek Olšák]

Of course "every set of size n has a maximum element" is true in ZFC for example (and some weaker systems too)

[Mirek Olšák]

In a typed system, prefer to imagine what is going on. The Ultra type of nonempty finite sets is an infinite sequence of actual finite sets (modulo ultrafilter). The maximum of this Ultra-set is just the maximum taken element-wise.

[Mirek Olšák]

By the way, I would use the nonstandard definition of "continuous": It is a standard function such that its lift returns infinitesimally close values at any two finitely large points that are infinitesimally close.

[Matt Insall]

I'm new to Lean, though I've known of its existence for a while, but I've done research in Nonstandard Analysis. I'll try to learn enough about Lean to look at what you want to do with this.

[Matt Insall]

I'd prefer that someone include the theory of superstructures and non-standard enlargements in much more general terms than just the hyperreals.

[Violeta Hernández]

I'd like to warn everyone that I know next-to-nothing about model theory. My interest in hyperreals is mostly just a by-product of my interest in the surreals, which have at least some surface-level similarities.

[Violeta Hernández]

(In other words, I'll help, but I shouldn't be at the helm of any project)

[Violeta Hernández]

Mirek Olšák said:

By the way, I would use the nonstandard definition of "continuous": It is a standard function such that its lift returns infinitesimally close values at any two finitely large points that are infinitesimally close.

Is there a topology that recovers this? Or would we need a new Hyper.Continuous definition for this?

[Mirek Olšák]

It can be proven equivalent to the classical definition.

[Violeta Hernández]

Ah, then we should probably do that, rather than reinventing the theory of topology.

[Mirek Olšák]

Matt Insall said:

I'm new to Lean

Violeta Hernández said:

I'd like to warn everyone that I know next-to-nothing about model theory.

When we are in the process of introducing ourselves :slight_smile: , I know just enough about nonstandard analysis to give a single talk about it (maybe two) -- defining hyper-reals & other hyper-objects, prove Łoś's theorem, and prove the demo theorem I outlined above.

@Matt Insall , the difficulty is that I have seen NA usually done in FOL (Łoś's theorem in particular). Although Lean has Łoś's theorem in its model theory, it seems highly unpractical to use it because we work with different types in Lean, not in some FOL model. Do you know if there is an equivalent for Łoś in dependent type systems? Could you also look at the outline I have posted above? My idea was that first of all I want to be able to

• Lift any object of type A to a hyper-object Hyper A (with the constant sequence). This could be also done with functions, so we can lift A -> B to Hyper (A -> B)
• Apply hyper-function to a hyper-object, so basically coerce Hyper (A -> B) to (Hyper A) -> (Hyper B)
• In the case of finite types, un-hyper it, so get A from Hyper A. I imagine this particularly useful for Prop.

[Matt Insall]

It's nice that you provide this, but I'm so new to using Lean that I don't know yet how to make use of the file Nonstandard.lean. I downloaded it and tried to open it using my Lean extension in VS Code, but got an error message because I don't have in the folder a file called "leantoolchain". This will take some getting accustomed to, because I'm not really very adept at programming... The mathematics is my thing...

[Matt Insall]

Well... There are caveats to this statement.

[Mirek Olšák]

Ok, maybe not important to study the file, it contains some really Lean-specific constructs. What do you think about the three basic building blocks in the post just above? Also, what are your thoughts about Łoś's theorem for a system based on type theory (most importantly, DTT doesn't distinguish much propositions and types, there is no concept of FOL formula)?

[Matt Insall]

Have you looked at Institution-Independent Model Theory? (see https://www.google.com/url?sa=t&source=web&rct=j&opi=89978449&url=https://link.springer.com/book/10.1007/978-3-031-68854-6&ved=2ahUKEwjT1vmM5sWSAxWpGlkFHfEwEEMQFnoECCYQAQ&usg=AOvVaw3lcZYAxxH8zWxuABfyb1yJ)

[Matt Insall]

Those are good starts to the ideas of NSA. To accomplish this, there are various paths in FOL, and ultrafilters provide one such path; Robinson originally used the compactness theorem, so any logic system (FOL or fragments of HOLs, etc) that satisfies a compactness theorem is likely to admit constructions like you suggest.

[Matt Insall]

In DTT (again, I'm newish to thinking about things this way), it's my understanding that the mantra "propositions as types" applies. In FOL, a proposition is a "generic" formula, in the sense that FOL formulas can be substituted for propositions in any propositional tautology and obtain an FOL universally valid formula.

[Matt Insall]

BTW, you can get a PDF of Diaconescu's book, and in there, various institutions are investigated in terms of properties like the compactness principle, Łos Theorems, etc. Maybe that can help you to see better whether a Łoš-type theorem holds in DTT.

[Violeta Hernández]

Mirek Olšák said:

Although Lean has Łoś's theorem in its model theory, it seems highly unpractical to use it because we work with different types in Lean, not in some FOL model.

What exactly is the problem? Say we want to prove every non-negative hyperreal has a square root. Then surely we can write some docs#FirstOrder.Language.Sentence in the language of ordered rings which spells this out, transfer it from ℝ into ℝ*, and then prove (likely via simp) that realizability of this sentence is equivalent to the actual proposition ∀ x ≥ 0, ∃ y, y² = x that we want?

[Violeta Hernández]

(I'm speaking from inexperience here, correct me if there's some subtlety I haven't considered)

[Matt Insall]

These are not the kinds of results that non-standard analysits are trying to prove using nonstandard analysis. A result such as "Every non-negative hyperreal has a square root" are immediate results of the transfer principle, which can be viewed as either a truth-preserving syntactic transform or as a semantic transform on the hyperreal numbers.

While the transfer principle is an important tool of nonstandard analysis, one combines it with other important principles (concurrency principles or overspill principles or saturation principles) to draw new conclusions about the original standard models (the real number system with all of the objects of interest to analysts, in the case of the hyperreal numbers).

[Mirek Olšák]

Violeta Hernández said:

(I'm speaking from inexperience here, correct me if there's some subtlety I haven't considered)

I have to confess, I have not tried to use the Model theory API myself, so I might be mistaken too. Just the need to provide a model, theory, sentence, etc. scared me. Perhaps there is a convenient API... although when I asked in person @Jonas van der Schaaf, he agreed it is not very reasonable to go through model theory.

[Matt Insall]

It's not that you are wrong; it's just that when you discuss results about real numbers holding for the hyperreals, you're only at the start of it all.

[Violeta Hernández]

This is perhaps somewhat of a pointed question, but is this really what we want to do here? For instance, the result @Mirek Olšák mentions:

every continuous function on a closed interval has a maximum

Though we certainly want to build an API that's capable of proving this via hyperreal arguments, I don't think we actually want to add such an argument to Mathlib. This theorem already exists somewhere else.

[Mirek Olšák]

I was rather thinking that we might need a dependent hyper-type (ultraproduct instead of ultra-power), so we can handle better dependent functions.

[Violeta Hernández]

docs#Filter.Product ?

[Matt Insall]

Even in FOL, thinking in terms of ultraproducts is important. The theory of enlargements of superstructures really uses that.

[Mirek Olšák]

What is that?

[Matt Insall]

With filtered products, some aspects of the transfer principle become less immediate or false because (roughly) ultraproducts preserve negations and products filtered by non-maximal filters don't quite.

[Violeta Hernández]

Mirek Olšák said:

I was rather thinking that we might need a dependent hyper-type (ultraproduct instead of ultra-power), so we can handle better dependent functions.

What sorts of things would we need dependent functions for? I was thinking that we could be able to use currying to our advantage; for instance, the statement ∀ x : ℝ, ∃ y : ℤ, y ≤ x < y + 1 could first be rewritten as a statement on ℝ × ℤ, then transferred to (ℝ × ℤ)* ≃ ℝ* × ℤ*, then uncurried as ∀ x : ℝ*, ∃ y : ℤ*, y ≤ x < y + 1.

[Matt Insall]

The notion of a superstructure is covered in the following texts:
Hurd & Loeb: An Introduction to Nonstandard Real Analysis (https://books.google.com.fj/books?id=jgH3mmbs59IC&printsec=frontcover#v=onepage&q&f=false)
Loeb and Wolff (eds): Nonstandard Analysis for the Working Mathematician (https://link.springer.com/book/10.1007/978-94-011-4168-0)

Briefly, begin with a set X_0, whose members are not sets (the elements of X_0 are called urelements), and recursively define, for each non-negative integer n,

X_{n+1}:=X_n\cup P(X_n),

where P is the power set operator.

The superstructure over X is the union of this tower of "cumulative power sets". Denote it by S(X_0). Then S(X_0) includes all of the set-theoretic entities of interest to analysts who want to study functions defined on X_0 and function spaces related to those, etc.

An enlargement of S(X_0) is given by forming an ultrapower of X_0 and the superstructure over that ultrapower and then the subsets of S(X_0) are "stratified" by a rank function in terms of where they first "appear" in the naturally occurring hierarchy determined by the cumulative power set construction. Accordingly, the enlargement, denoted S(X_0), is not exactly an ultrapower of S(X_0), but the transfer principle applies for a fragment of FOL in which only bounded (by rank, essentially) quantifiers are allowed.

[Matt Insall]

Oh, you are putting the stars on the right... That can get confusing, but ok.

[Violeta Hernández]

Matt Insall said:

Briefly, begin with a set X_0, whose members are not sets (the elements of X_0 are called urelements), and recursively define, for each non-negative integer n,

X_{n+1}:=X_n\cup P(X_n),

where P is the power set operator.

What would be the Lean analogue of this? Some sigma type Σ n, Set^[n] α?

[Violeta Hernández]

Matt Insall said:

Oh, you are putting the stars on the right... That can get confusing, but ok.

Sorry, I thought this was the standard convention. What do you suggest?

[Aaron Liu]

Violeta Hernández said:

Matt Insall said:

Briefly, begin with a set X_0, whose members are not sets (the elements of X_0 are called urelements), and recursively define, for each non-negative integer n,

X_{n+1}:=X_n\cup P(X_n),

where P is the power set operator.

What would be the Lean analogue of this? Some sigma type Σ n, Set^[n] α?

not quite, since that doesn't contain {a,{}} for a a member of the X_0

[Matt Insall]

In Hurd &Loeb's text, and in the Loeb & Wolff text, and in Robinson's work, the syntactic transform of a formula s is denoted by *s. For the corresponding semantic transform (an elementary embedding between superstructures), an object a of type S(X_0) is mapped to an object *a of type *S(X_0), and this mapping is a morphism in the category of superstructures; model theoretically, it's an embedding that preserves truth both ways -- an elementary embedding.

[Aaron Liu]

what you get are the finite rank ZFA sets with atoms from X_0

[Matt Insall]

Yup

[Violeta Hernández]

Finally an actual use for this: docs#Lists

[Aaron Liu]

doesn't contain infinite sets

[Mirek Olšák]

Violeta Hernández said:

Mirek Olšák said:

I was rather thinking that we might need a dependent hyper-type (ultraproduct instead of ultra-power), so we can handle better dependent functions.

What sorts of things would we need dependent functions for? I was thinking that we could be able to use currying to our advantage; for instance, the statement ∀ x : ℝ, ∃ y : ℤ, y ≤ x < y + 1 could first be rewritten as a statement on ℝ × ℤ, then transferred to (ℝ × ℤ)* ≃ ℝ* × ℤ*, then uncurried as ∀ x : ℝ*, ∃ y : ℤ*, y ≤ x < y + 1.

Yes, I was first thinking of (as automatically as possible) translating proofs to the hyper-world. Applying theorem to a specific instance is a dependent function application. The basics I have so far only covers applying simple functions.

But I can imagine this being extended to any dependent function. Say the function that takes a natural number n, and returns a zero matrix n × n Or we could have say nonstandard-large x of the (kind of) type Fin N for nonstandard N...

[Violeta Hernández]

Aaron Liu said:

doesn't contain infinite sets

haha nevermind then

[Violeta Hernández]

Mirek Olšák said:

Yes, I was first thinking of (as automatically as possible) translating proofs to the hyper-world. Applying theorem to a specific instance is a dependent function application. The basics I have so far only covers applying simple functions.

But I can imagine this being extended to any dependent function. Say the function that takes a natural number n, and returns a zero matrix n × n Or we could have say nonstandard-large x of the (kind of) type Fin N for nonstandard N...

It's probably too early to think of automation, when we don't even have results to automate!

[Violeta Hernández]

I'm not sure if we need a dependent function of Łos for this, though. Instead of translating a theorem ∀ n, ∀ x : Fin n, P x via Łos, you could instead just translate ∀ n, ∀ x < n, P x, and hopefully in practice this is sufficient?

[Mirek Olšák]

On the other hand, I don't see why I would want to limit myself to not using dependent types.

[Violeta Hernández]

Well, if there's some easily provable version of Łos that allows for dependent types then we should just use that, yes

[Violeta Hernández]

I was half-assuming this wasn't the case

[Mirek Olšák]

And my intention was that rather than proving Łos, I would like it to come out as a result of the type system.

[Violeta Hernández]

In what sense?

[Violeta Hernández]

I half-recall similar conversations where people discussed a hypothetical tactic to automatically prove a function computable by translating its Lean code into a proof. Given that this hasn't happened, I imagine it's generally difficult to achieve this sort of behavior.

But maybe this is unrelated to your idea.

[Violeta Hernández]

It's perhaps a good idea to get the opinon of other people working in model theory in Lean before doing any big changes to that infrastructure.

[Mirek Olšák]

Just to be clear, I don't want to change model theory in Lean. I was rather thinking of doing hyper-objects using different basics. I just thought it could be possible to avoid touching model theory's Łoś by going through the type system.

[Matt Insall]

If you only want to study analysis of the real numbers using nonstandard methods, then you take $X_0$ to be a set equipollent to the real line. If you only want to study number theory and combinatorics using nonstandard methods, take $X_0$ to be a countably infinite set. In the first case, the structure of interest may be, say, the Archimedean ordered ring consisting of the real numbers, $(R; \leq; +, \cdot; -; 0, 1)$, and the point of using superstructures for this is that this object is an element of $S(X_0)$, and the corresponding hyperreal number system, $*(R; \leq; +, \cdot; -; 0, 1)=(*R; *\leq; *+, *\cdot; *-; *0, *1)$ is an element of the enlargement, but also, if you want to study in the same context the real line as a topological space, then the set theoretic object $(R; \tau)$ is in $S(X_0)$ as well, and its nonstandard analog, the hyperreal line, $*(R; \tau)$ is in $*S(*X_0)$, and the function spaces consisting of continuous functions on the line are objects of type $S(X_0)$, and so they have analogues in $*S(*X_0)$, etc, etc, etc...

The function $\phi$ that maps an ordered ring $(F; \leq; +, \cdot; -; 0, 1)$ to its ring reduct $(F;+, \cdot; -; 0, 1)$ is a forgetful functor with domain the superstructure $S(X_0)$. It is an example of a functor that is not an element of type $S(X_0)$, because its domain is (of course) not an element of $S(X_0)$. Thus it does not strictly have a transform "$*\phi$"; However, we can create one on the enlarged superstructure $*S(*X_0)$, because the set of all $(*a,*b)$ for which $(a,b)$ is on the graph of $\phi$ is a subset of $*S(*X_0)$ that happens to be a binary relation on $*S(*X_0)$ with the function property.

The issue illustrated above is both a bug and a feature. We cannot immediately apply the transfer principle to \phi because it is not in the domain of the elementary embedding used for nonstandard methods on the universe constructed from $X_0$, but if we are careful in a manner similar to type theories, we can "fudge" it, as is done by many authors of nonstandard analysis articles.

[Violeta Hernández]

(you can use double dollar signs $$ to write down LaTeX)

[Matt Insall]

That is likely to depend upon which type system you are using. Again, I point to Diaconescu and his rather informative text on institution independent model theory.

[Matt Insall]

Thanks... When I clicked on the math symbol in the toolbar, I was confused by what I saw...

[Mirek Olšák]

Violeta Hernández said:

In what sense?

First, let's see, how a general dependent application should work. Let me denote H A : Sort u the hyper-type (ultrapower) of A : Sort u, and a dependent hyper-type dH B : Sort u for B : H (Sort u). Recall that a non-dependent function H (A → C) can be lifted to (H A) → (H C).

Now, let's say, I have A : Type, B : A → Type, and a dependent hyper-function f : H ((a : A) → B a). How does the hyper-lifting works here?

The lifted ⇑f should take a : H A, and return b : dH (⇑B a).

Now, let's consider the case of B : A → Prop being a proposition, and f being a theorem stating that B holds for every standard a : A. The same dependent function application gives us a function that takes a : H A, and returns b : dH (⇑B a).

My claim is that this is almost Łoś's Theorem, except we need to simplify the type of b : dH (⇑B a) into just b' : (⇑B a).toBase : Prop.

That looks somewhat technical but doesn't seem impossible. Since (⇑B a) : H Prop, and Prop is finite, there is an isomorphism H Prop ≅ Prop translating (⇑B a) to the appropriate B' : Prop := (⇑B a).toBase. Under such circumstances, also the dependent hyper-object is not necessary because the type is not really a hyper-object, and should be able to simplify to b' : H B'.

[Jireh Loreaux]

One thing I've been wondering about (unrelated to the discussion thus far): docs#Hyperreal uses an ultrafilter on ℕ, but what if you want a higher level of saturation?

[Mirek Olšák]

Violeta Hernández said:

docs#Filter.Product ?

I wonder if this definition is correct. If I understand correctly, whenever one of the factors is empty, the result is empty as well, even though a single item should not have an effect on the entire structure. I would expect the underlying type to be a partial function from an element of the filter to the types.

Anyway, in the dependent hyper-type I envision, we don't even have an explicit function Nat -> Type but a Hyper Type, which makes the individual type elements even more irrelevant.

[François G. Dorais]

See also https://mathoverflow.net/questions/11261/is-the-ultraproduct-concept-fundamentally-category-theoretic

[James E Hanson]

Violeta Hernández said:

The vast majority if not all of non-standard analysis should generalize to the setting of a real-closed field.

My understanding is that non-standard analysis needs more than just a real-closed field.

[James E Hanson]

Mirek Olšák said:

I wonder if this definition is correct. If I understand correctly, whenever one of the factors is empty, the result is empty as well, even though a single item should not have an effect on the entire structure. I would expect the underlying type to be a partial function from an element of the filter to the types.

You're right. The definition as written does not correctly handle empty types, although for many applications it really isn't an issue.

[Mirek Olšák]

James E Hanson said:

You're right. The definition as written does not correctly handle empty types, although for many applications it really isn't an issue.

Then the question is: should someone fix it? If so, who should fix it? Could changing the definition cause complications in the uses so far?

I can imagine that it should not make much difference in model theory which require each model to be non-empty. On the other hand, it could help in more native uses of ultraproducts, as discussed here.

[François G. Dorais]

It does make a little difference, see my answer at https://mathoverflow.net/questions/105397/there-are-two-slightly-different-notions-of-ultraproduct-why-is-one-said-to-be

[James E Hanson]

Mirek Olšák said:

I can imagine that it should not make much difference in model theory which require each model to be non-empty. On the other hand, it could help in more native uses of ultraproducts, as discussed here.

For what it's worth, not all model theorists agree about that convention.

[François G. Dorais]

I'm not sure "agree" is the right word, I believe all model theorists agree that Free Logics are a thing, but many don't use them, if only for the sake of simplicity.

[James E Hanson]

What I mean is that there are model theorists who think that allowing empty structures should be standard.

[Mirek Olšák]

If I am looking correctly into Lean's docs#FirstOrder.Language.Theory.Model, it allows empty domain.

[James E Hanson]

Yes, it's not requiring that structures be non-empty.

[Aaron Liu]

but docs#FirstOrder.Language.Theory.ModelType does bundle nonemptyness

[François G. Dorais]

If the theory T proves $\exists x(x=x)$ then it does not allow empty models.

[François G. Dorais]

So it really depends on the definition of theory used there.

[Aaron Liu]

well if the theory proves nonempty I would expect all its models to be nonempty

[Mirek Olšák]

Oh, nonemptiness is explicitly assumed in Lean's Los theorem: docs#FirstOrder.Language.Ultraproduct.sentence_realize, that's why it doesn't mind wrong ultraproduct :slight_smile:

[François G. Dorais]

In classical first-order logic with equality, $\exists x(x=x)$ is provable from the empty theory.

[Aaron Liu]

no I don't think so?

[James E Hanson]

It depends on the particular proof system you use. In most treatments though, it is provable.

[Aaron Liu]

so we have different ideas about what "classical first-order logic with equality" means

[Aaron Liu]

my version doesn't prove nonempty

[François G. Dorais]

There is only one thing called "classical first-order logic with equality". The key is that $\lnot \exists x(x = x)$ is equivalent to $\forall x(x\neq x)$ and this leads to a contradiction with the generalization rule and the reflexivity axiom. To avoid this, free logics impose restriction on generalization.

[James E Hanson]

An unrelated point: One thing to keep in mind is that there's really two applications in logic where you might want to 'take an ultrapower of the whole universe'. There's non-standard analysis, which we're already discussing, but then there's also certain things involving large cardinals.

Like, if one ever wanted to formalize the fact that the existence of a measurable cardinal is equivalent to the existence of an exact functor from Set to Set that is not naturally isomorphic to the identity, having this kind of machinery would be useful.

[Mirek Olšák]

That relates a bit to @Jireh Loreaux question. My attitude is that ideally, the ultraproduct API should be developed so that it can deal with arbitrary ultrafilters, and the non-standard analysis should be not so large layer on top of it.
There is one difference, in small ultraproducts, we only preserve finite types. For the use of large cardinals, this should be generalized based on the ultrafilter properties (as they preserve much more).

[James E Hanson]

Violeta Hernández said:

I was half-assuming this wasn't the case

There should be a version of Łoś's theorem for (classical) DTT relative to Henkin semantics, because the Henkin semantics of DTT can be encoded faithfully in a first-order theory.

[Aaron Liu]

François G. Dorais said:

There is only one thing called "classical first-order logic with equality". The key is that $\lnot \exists x(x = x)$ is equivalent to $\forall x(x\neq x)$ and this leads to a contradiction with the generalization rule and the reflexivity axiom. To avoid this, free logics impose restriction on generalization.

I think you get $\forall x, \text{False}$ but you can't conclude $\text{False}$ from this unless you can prove nonempty.

[François G. Dorais]

Aaron Liu said:

I think you get $\forall x, \text{False}$ but you can't conclude $\text{False}$ from this unless you can prove nonempty.

---

That's true in Lean, but in classical first-order logic, $\forall x, \text{False}$ implies False since $x$ does not occur free in False.

[Aaron Liu]

then whatever rule says you can do that my version doesn't have that rule

[François G. Dorais]

James E Hanson said:

Violeta Hernández said:

I was half-assuming this wasn't the case

There should be a version of Łoś's theorem for (classical) DTT relative to Henkin semantics, because the Henkin semantics of DTT can be encoded faithfully in a first-order theory.

I can't recall whether they get to Łoś's theorem but Makkai and Reyes First Order Categorical Logic work through most of the framework to get there in a context that is similar to DTT.

[François G. Dorais]

Aaron Liu said:

then whatever rule says you can do that my version doesn't have that rule

Your "version" is some kind of Free Logic then, not classical first-order logic with equality. By definition of classical first-order logic: $\exists x(x = x)$ is a tautology of classical first-order logic with equality and $\forall x \phi(x) \to \exists x \phi(x)$ is a theorem of classical first-order logic (with or without equality).

[Mirek Olšák]

I wonder if rather than discussing model-theoretic terminology & proof systems, we could agree (or not):

[Mirek Olšák]

(1) That the ultra-product definition should be changed

[Mirek Olšák]

(2) To add API to translate a Germ back to the original type in case of a finite type

[Mirek Olšák]

(3) To add another product-like API to allow T : Germ filter Type as the base type for the ultra-product

[Mirek Olšák]

(4) That we don't want Lean-level Łoś's theorem explicitly (because inducting on the size of Lean term doesn't make much sense), and rather just support well propagating dependent function applications through the ultra-products.

[François G. Dorais]

The way to unify the two ultraproduct definitions is to take a classical ultraproduct of Option A_i instead of just A_i but then you need to throw out elements that are none almost always according to the ultrafilter.

[Aaron Liu]

or you could take a colimit over functions defined on sets in the filter

[François G. Dorais]

I think you missed the word "unify".

[François G. Dorais]

The "free" ultraproduct is Equiv to the subtype of the classical ultraproduct as I explained above. The Equiv can be used to transfer theorems.

[Mirek Olšák]

Do you think it is worth it to keep the more basic definition?

[Mirek Olšák]

By the way, Lean also has Part which is very similar to Option. I am not exactly sure what is better here.

[François G. Dorais]

I don't know. But "more basic" is unclear. The reason Model Theory uses the "less basic" definition is that very early on, when he initiated what became Model Theory, Tarski showed that multiple sorts and empty domains could be faithfully interpreted in classical first-order logic (which is single-sorted and doesn't allow an empty universe). Tarski also explained that this simplifies many logical rules.

That was around 90 years ago. Does it need to be revised today? I'm not sure but I'm fine with updating archaic definitions and decisions. I personally think reconsidering established ideas and definitions should happen periodically. Tarski's realization still remains: multi-sorted, empty sorts, and even dependent types can be faithfully interpreted in first-order logic.

[Matt Insall]

The stars usually go on the left in the literature, but I saw today in the Mathlib that there the stars are on the right, like you’re doing. What is used for complex numbers, conjugation, and in complex hole spaces, the conjugate transpose? In that literature, one often sees a star on the right, so this can be confusing when working on the nonstandard complex numbers and related structures.

[Matt Insall]

Jireh Loreaux said:

One thing I've been wondering about (unrelated to the discussion thus far): docs#Hyperreal uses an ultrafilter on ℕ, but what if you want a higher level of saturation?

I’m new enough to not know how best to discuss how you’d do this in LEAN, but in practice, instead of $\mathbb N$, you use an indexing set $J$ of higher cardinality than $\aleph_0$ for this. A related notion is polysaturation, and I would hope to see in LEAN someday an implementation of that. I guess that means I hope for a type named something like “polysaturated enlargement”.

[Matt Insall]

Mirek Olšák said:

Violeta Hernández said:

docs#Filter.Product ?

I wonder if this definition is correct. If I understand correctly, whenever one of the factors is empty, the result is empty as well, even though a single item should not have an effect on the entire structure. I would expect the underlying type to be a partial function from an element of the filter to the types.

Anyway, in the dependent hyper-type I envision, we don't even have an explicit function Nat -> Type but a Hyper Type, which makes the individual type elements even more irrelevant.

Even for direct product, if any factor is empty, the product should be empty, and hence for filtered products, that would happen as well, because a filtered product in a concrete category is a quotient of a direct product. In more general categories, while I’ve not delved into the details, I expect that the same would hold.

It can help to keep in mind that many constructs like sum and product, a special case is addition of natural numbers and multiplication in natural numbers. Consequently, in the natural numbers, multiplication of cardinal numbers can be modeled in terms of direct products, so that a direct product involving a finite sequence of finite sets of certain cardinalities will have as its cardinality the product of the individual cardinalities of its factors, so if one of them is empty (and hence of zero cardinality), then the direct product has zero cardinality. This carries over to general direct products (e.g. with infinitely many factors), and then for filtered products even more-so, since surjections cannot increase cardinality, and quotients can be realized as ranges of canonical surjections.

[Mirek Olšák]

@Matt Insall I know that if you use the definition: "Build the standard product, and then factor out by an ultrafilter" (which is exactly what Lean does), then a single empty type collapses this construction. The question rather was if this is intended -- I would rather expect it is not. So I am asking if there is any need for this current definition as opposed to:

• We are building ultraproduct based on a function T : Nat -> Type
• The base type will be partial functions x : (n : Nat) -> T n such that their domain is in the filter (the current definition would use full functions).
• We take the quotient of the base type as usual

[Matt Insall]

James E Hanson said:

Violeta Hernández said:

The vast majority if not all of non-standard analysis should generalize to the setting of a real-closed field.

My understanding is that non-standard analysis needs more than just a real-closed field.

Most of nonstandard mathematics needs much more than enlargements of a real-closed field. To find out more, I’d suggest that you read the book by Loeb and Wolff, but even as early as the 1960s, Abraham Robinson was discussing the use of nonstandard analysis to study Lie groups, which aren’t fields at all.

[Matt Insall]

James E Hanson said:

Mirek Olšák said:

I wonder if this definition is correct. If I understand correctly, whenever one of the factors is empty, the result is empty as well, even though a single item should not have an effect on the entire structure. I would expect the underlying type to be a partial function from an element of the filter to the types.

You're right. The definition as written does not correctly handle empty types, although for many applications it really isn't an issue.

I’m not sure what’s wrong with the definition, probably just because I’ve not yet learnt enough of LEAN.

[Mirek Olšák]

Here is one option how we could build a better ultra-product on top of the existing one. Perhaps the proof could be improved (I feel a bit cumbersome whenever proving something with quotients...)

def Filter.Product.satisfies {α : Type*} {filter : Filter α} {β : α → Type*}
    (p : {a : α} → β a → Prop) (x : Filter.Product filter β) : Prop :=
  x.lift (fun x ↦ {a | p (x a)} ∈ filter) (by
    let setoid := filter.productSetoid β
    have one_side (x y : (a : α) → β a) (eq : x ≈ y) :
        {a | p (x a)} ∈ filter → {a | p (y a)} ∈ filter := by
      intro h
      apply filter.sets_of_superset (filter.inter_sets h eq)
      rintro elem ⟨elem_x, elem_eq⟩
      simp only [Set.mem_setOf_eq] at elem_x elem_eq ⊢
      rw [←elem_eq]
      exact elem_x
    intro x y eq
    simp only [eq_iff_iff]
    constructor
    · exact one_side x y eq
    · exact one_side y x (symm eq)
  )

def Filter.BetterProduct {α : Type*} (filter : Filter α) (β : α → Type*) :=
  {x : filter.Product (Part ∘ β) // x.satisfies Part.Dom}

[Matt Insall]

François G. Dorais said:

It does make a little difference, see my answer at https://mathoverflow.net/questions/105397/there-are-two-slightly-different-notions-of-ultraproduct-why-is-one-said-to-be

Thanks for linking that. Accordingly, I suggest that the more categorical version be adopted (Type 2 in the linked mathoverflow question).

[Matt Insall]

James E Hanson said:

What I mean is that there are model theorists who think that allowing empty structures should be standard.

I recall that when I was learning model theory I was at some point forgetting that it was assumed that empty structures weren’t allowed, and I became concerned that this meant that there were issues with universal quantification, in that an empty model of FOL would vacuously satisfy both $(\forall x)(x\neq x)$ and $(\forall x)(x=x)$, but reviewing and finding that structures are nonempty calmed me down about that. Now, the issue seems to be resurfacing…

Of course, it is possible to construct an alternative approach that allows empty structures but avoid semantic discombobulation, but I didn’t see the need to concern myself with that, since I expected that results can be “ported over” between them….

Shouldn’t a system like LEAN and its mathlib be built with flexibility in mind?

Regarding some issues raised in the mathoverflow linked by Francois, in universal algebra, algebras are presumed to be nonempty (“inhabited types”?), but I was at a universal algebra workshop attended by a number of computer scientists and category theorists who wanted to allow empty algebras; in any case, universal algebraic call a one element algebra “trivial”, as is done in group theory for singleton groups. In topology, the empty space is available, but in my experience is typically avoided more for a lack of interesting results than anything else. In continuum theory (a branch of topology), it’s typical to require all continua to be nonempty, and a continuum having only one element is called “degenerate”.

[François G. Dorais]

Matt Insall said:

Shouldn’t a system like LEAN and its mathlib be built with flexibility in mind?

Lean's logical basis is not first-order logic and it does treat the empty domain issue correctly. The issue is a technical one: do you want to formalize classical model theory à la Tarski or a more permissive model theory with multiple sorts, including empty sorts? The latter is more difficult but it is manageable. For example, I formalized basics of multi-sorted equational logic a long time ago in Lean 3 <https://github.com/fgdorais/lean-universal>. (I think I have an old attempt at a Lean 4 update for that but I lost interest so its at best very dusty by now.)

[Jireh Loreaux]

Matt Insall said:

Jireh Loreaux said:

One thing I've been wondering about (unrelated to the discussion thus far): docs#Hyperreal uses an ultrafilter on ℕ, but what if you want a higher level of saturation?

but in practice, instead of $\mathbb N$, you use an indexing set $J$ of higher cardinality than $\aleph_0$ for this.

Right, I know. This was my question. I should have asked more it directly as "why isn't the definition of hyperreal parameterized over the index set?"

[Matt Insall]

François G. Dorais said:

If the theory T proves $\exists x(x=x)$ then it does not allow empty models.

I would like to agree, IF by $(\exists x)\phi$, one means the classical semantic interpretation (e.g. Tarskian semantics).

However, here’s a conundrum I alluded to a little while ago: if empty models are allowed, then in the Tarskian inductive definition of satisfaction, any empty model satisfies both $(\forall x)(x=x)$ and $(\forall x)(x\neq x)$ vacuously, as there’s no member of the domain to falsify either one. The usual FOL axiom scheme makes $(\forall x)\phi$ and $(\forall x)(\not\phi)$ incompatible, as $\not(\forall x)\phi$ is derivable from $(\forall x)(\not\phi)$. Thus empty structures have a theory that proves every formula—from $(\forall x)(x\neq x)$ derive $\not(\forall x)(x=x)$ and from $(\forall x)(x=x)$ and $\not(\forall x)(x=x)$, derive all FOL formulas. But this means that such a theory proves also $(\exists x)(x=x)$, so that it has no empty models.

Thus I think that by allowing empty models, you implicitly don’t use classical FOL.

[Mirek Olšák]

Jireh Loreaux said:

Matt Insall said:

Jireh Loreaux said:

One thing I've been wondering about (unrelated to the discussion thus far): docs#Hyperreal uses an ultrafilter on ℕ, but what if you want a higher level of saturation?

but in practice, instead of $\mathbb N$, you use an indexing set $J$ of higher cardinality than $\aleph_0$ for this.

Right, I know. This was my question. I should have asked more it directly as "why isn't the definition of hyperreal parameterized over the index set?"

Parametrizing only over the index set doesn't make much sense (an ultrafilter on Nat can be always trivially extended to larger sets without changing the hyper-reals). If something, it could be parametrized by the filter (together with the index set).

For the elementary non-standard analysis I know, any non-principal ultrafilter on any set (so for example Nat) is good enough (okay, as long as it is not ω₁-complete), so not having to carry the filter around is just a matter of convenience. As I already wrote, I agree that building most of the background theory on general Filter.Germ and Filter.Product is desirable but to showcase nonstandard analysis, I don't think we need the flexibility.

[James E Hanson]

Mirek Olšák said:

(an ultrafilter on Nat can be always trivially extended to larger sets without changing the hyper-reals)

What do you mean by this? You can get different hyperreals by using different ultrafilters in the ultraproduct.

[Mirek Olšák]

For every ultrafilter F1 on Nat, and for every infinite set X, there exists an ultrafilter F2 on X such that hyperreals constructed from F1 are isomorphic to hyperreals constructed from F2.

[James E Hanson]

Sure but really the question is why is it not parameterized over the ultrafilter.

[Mirek Olšák]

Mirek Olšák said:

If something, it could be parametrized by the filter

[Aaron Liu]

Matt Insall said:

The usual FOL axiom scheme makes $(\forall x)\phi$ and $(\forall x)(\not\phi)$ incompatible, as $\not(\forall x)\phi$ is derivable from $(\forall x)(\not\phi)$.

It sounds to me that there's an axiom (or axioms) in this FOL axiom scheme which is equivalent to assuming your domain is nonempty, so to allow empty models you can just remove this axiom.

[Matt Insall]

I think it’s important for LEAN to be accessible to people doing mathematics the way mathematicians do it, and classical FOL was built accordingly by Tarski, et. al., as mentioned previously in this thread. Otherwise, formalizing nonstandard analysis and standard mathematics are less attractive to practicing mathematicians or their students.

I programmed in Fortran and Basic, and avoided programming for years because it showed me down in thinking about mathematics, then I taught myself some prolog and a tiny bit of pascal, but they didn’t help more than reading and thinking and writing, but they took away time from those more productive activities. I’ve hoped for a while to learn of some prof assistants that I could use, so I’m hopeful that LEAN would perhaps be such, but if it takes more hours of programming and correcting syntax or typos than actual thinking about mathematics, I expect that I may stop finding it to be a worthwhile investment of time.

I know many other mathematicians who find the idea of trying to get computers to help with pure mathematics to not be a good use of their time, so if the implementation is far away from what they use, I don’t see them helping too popularize LEAN, especially among their most promising students. Already, I went through the pain of learning LaTeX after being abandoned by the whysiwig editor ChiWriter, and I probably was delayed enough by that time sink that I’m a dozen articles shy of where I would have been if ChiWriter had survived the transition from dos to windows.

I’d rather do BASH programming than go through that kind of thing again.

[Aaron Liu]

If you want to assume your models are nonempty you can add Nonempty assumptions and if you want to assume your theory is nonempty you union with docs#FirstOrder.Language.nonemptyTheory. But I don't want to make it harder to talk about theories which don't prove nonemptiness.

[Adam Topaz]

Just catching up on the discussion now. IIUC, a better version of docs#Filter.Product should be something along the following lines:

import Mathlib

instance : CoeSort (Filter α) (Type _) where coe f := f.sets
instance (f : Filter α) : CoeSort f (Type _) where coe s := s

def Filter.betterProductSetoid (l : Filter α) (ε : α → Type*) :
    Setoid ((s : l) × ((a : s) → ε a)) where
  r := fun ⟨s,f⟩ ⟨t,g⟩ => ∃ (u : l) (hs : u ≤ s) (ht : u ≤ t),
    ∀ x : u, f ⟨x, hs x.prop⟩ = g ⟨x, ht x.prop⟩
  iseqv := sorry

def Filter.betterProduct (l : Filter α) (ε : α → Type*) :=
    Quotient <| l.betterProductSetoid ε

[Mirek Olšák]

Yes, that should be isomorphic to this construction.

[Matt Insall]

“an ultrafilter on Nat can be always trivially extended to larger sets without changing the hyper-reals”

I’m not sure what this means. In model theory (not just in nonstandard analysis), to use ultrafilters (or even just filters that aren’t maximal, for that matter) for specific purposes, one often needs to choose the indexing set in a way that is closely related to the problem at hand, and then carefully select a filter base, so that the filter or ultrafilter obtained eventually has properties that make the constructed ultraproduct (or more generally, filtered product) accomplish certain desired higher order properties. Saturation and polysaturation are such properties.

[James E Hanson]

Matt Insall said:

Saturation and polysaturation are such properties.

What do you mean by 'polysaturation'?

[Jireh Loreaux]

Mirek Olšák said:

For every ultrafilter F1 on Nat, and for every infinite set X, there exists an ultrafilter F2 on X such that hyperreals constructed from F1 are isomorphic to hyperreals constructed from F2.

If you switch the roles of X and Nat here I think this is false, which is why I was talking about parameterizing over the index set (and yes, also the filter).

[Aaron Liu]

there are $2^{2^\mathfrak{c}}$ many ultrafilters on $\mathbb{R}$, but $\mathbb{R}$ only has $\mathfrak{c}$ many countable subsets and each subset has at most $2^\mathfrak{c}$ ultrafilters on it, so there must be ultrafilters not coming from a countable subset.

[Mirek Olšák]

My point was, if we use the proposed

def Hyper (R : Type*) : Type* := (Filter.hyperfilter ℕ).Germ R

and only change ℕ to be a parameter, it doesn't help much because Filter.hyperfilter can be arbitrary cofinite filter, so it could be one coming from a countable subset.

If not, and are parametrizing over the filter, then we are not building any new definition, the definition is already called Germ.

[James E Hanson]

Incidentally, where did the term hyperfilter come from? I don't feel like it's in common use.

[Adam Topaz]

I'm a little confused by this discussion. We do have general ultraproducts over ultrafilters c.f. FirstOrder.Language.Ultraproduct.structure (this would require fixing Filter.Product as discussed above)

[Matt Insall]

Saturation in nonstandard methods is describable in terms of the cardinality of the subsets of the original model or its enlargement to which a variant of the concurrency principle can be applied. When constructing enlargements only using a denumerable indexing set, one obtains the concurrency principle for subsets of the original model. Given a concurrent binary relation r in the original superstructure S (a relation such that for any finite subset F of dom(r), there exists an element b in range(r) such that arb for every a in F), there a single element y in the enlargement *S that inhabits range(r) such that for all a in dom(r), arb. This is a path to yield the overspill principle in nonstandard mathematics, and that’s one of the ways we can prove that a proper enlargement of a superstructure constructed over the reals includes positive infinitesimals. This kind of concurrency principle is available because of countable saturation. It’s the weakest form of concurrency used in nonstandard analysis. Stronger forms allow consideration of binary relations that are entities in the enlargement *S rather than just in the original superstructure S. The books by Hurd and Loeb give careful definitions that I’ll reproduce below, but I wanted to start with the way nonstandard analysts use saturated models before getting to how they use polysaturated enlargements.

From the book by Hurd & Loeb:
“ 8.1 Definition $V(*X)$ is $\kappa$-saturated if, for each internal binary relation $P\in V(*X)$ which is concurrent (Definition 5.9) on some (not necessarily internal) set $A$ in $V(*X)$ with $card A < \kappa$, there exists an element $y \in range P$ so that $(x,y) \in P$ for all $x \in A$. ”

Accordingly, the kind of saturation that is enough to get infinitesimals via the concurrency principle or overspill is $\aleph_0$ saturation.

From the book by Loeb & Wolff:
“For-saturation, the cardinal number should be determined by $V(X)$; it must not depend on objects in $V(* X)$, because these can change depending on the monomorphism. It is sufficient, therefore, to fix $\kappa$ as the first cardinal number larger than the cardinality of the original superstructure $V(X)$. One then says that $V( X)$ is polysaturated.”

What is often most useful is to assume in a given work that all nonstandard enlargements are polysaturated, so that one can neglect checking cardinalities of the domains, as long as they’re chosen from the original superstructure.

[Mirek Olšák]

Adam Topaz said:

I'm a little confused by this discussion. We do have general ultraproducts over ultrafilters c.f. FirstOrder.Language.Ultraproduct.structure (this would require fixing Filter.Product as discussed above)

#mathlib4 > Non-standard analysis @ 💬

[Adam Topaz]

Okay, even better!

[Adam Topaz]

Sorry, this thread is quite long and I haven't been following it from the beginning :)

[Mirek Olšák]

no worry

[Matt Insall]

James E Hanson said:

Incidentally, where did the term hyperfilter come from? I don't feel like it's in common use.

Where does this term occur? In nonstandard mathematics, if I start with a lattice L contained in a set X whose elements are urelements (not sets), and form a superstructure S(X), and then an enlargement S(X) of that original superstructure, then I would call an entity f in V(X) a hyperfilter provided that it is a member of *filt(K) for some member K of *Latt_j, where Latt_j is the collection of all lattices in S(X) of rank j or less for some natural number j.

An equivalent terminology would be “f is an internal filter in the enlargement V(S)”.

[Matt Insall]

Ok, so I looked again and I see that your comment, James, was about the proposal mentioned by Mirek. I’m not sure yet if Mirek’s usage matches mine…

Note that my usage is consonant with the usual usage in NSA (nonstandard analysis) of the prefix “hyper- “. The hyperfinite subsets are the members of the enlargement of the collection of finite subsets of a superstructure.

[Mirek Olšák]

James E Hanson said:

Incidentally, where did the term hyperfilter come from? I don't feel like it's in common use.

Apparently, it is in Mathlib since its first construction of hyper-reals: a923247, by @Abhimanyu Pallavi Sudhir . I would name it just Filter.ultrafilter.

[Jireh Loreaux]

docs#Ultrafilter.of

[Mirek Olšák]

We are discussing

def Filter.hyperfilter : Ultrafilter α := Ultrafilter.of cofinite

in mathlib here

[Jireh Loreaux]

I realize that, and I'm suggesting that we don't need the definition at all (leastways because it is poorly named).

[Violeta Hernández]

I can work on a PR to deprecate this definition, but I'd like to get #33650 out of the way first.

[Mirek Olšák]

I guess the psychological reason for that definition is that it feels more "fixed" than constructing each time an ultrafilter out of the cofinite one (although it is fixed in Lean as well). We want to fix an arbitrary non-principal ultrafilter, and then do something with it. But I don't mind removing it.

[Matt Insall]

Jireh Loreaux said:

I realize that, and I'm suggesting that we don't need the definition at all (leastways because it is poorly named).

Being poorly named seems to be not enough to deprecate it. I’m still working to understand it, but I would agree that the name isn’t great. If I’m starting to understand it well enough, it appears to perhaps be defining ultrafilters that contain the Frechet filter (the filter of cofinite subsets of the indexing set). There already is a name for these…. Such an ultrafilter is a free ultrafilter.

[Violeta Hernández]

Well, the idea is that we can just write .of cofinite throughout. We're barely saving any characters, and there's not much API we can give for hyperfilter that we can't more generally put on Ultrafilter.of or cofinite.

[Kevin Buzzard]

In 2017 the world was a very different place, and if an undergraduate decided to call something a hyperfilter because he'd read it on the internet (or maybe even just made it up), I was fine with that. This stuff is very old code and also an undergraduate project supervised by a non-expert, I'm sure it could do with some spring cleaning. At the time I was just encouraging undergraduates to do any kind of mathematics and PR it.

[Mirek Olšák]

I just realized it is probably not called ultrafilter because back then, types were lowercase, so the name would collide with the type Ultrafilter.

[Alok Singh]

my in-progress nsa stuff: https://github.com/alok/mathlib4/tree/experiment-heq-nsa

[Mirek Olšák]

Unfortunately, this is a typical example of why AI is not yet at the human level of contributing to mathlib. It created a lot of extra definitions (Hyperrational, etc.) that we should not have (because the intention is a general solution). On the other hand, it didn't even fix the wrong definition of Filter.Product we were discussing here.

Here, I proposed some principled steps for building the basics:
#mathlib4 > Non-standard analysis @ 💬
#mathlib4 > Non-standard analysis @ 💬
you can feed them to claude, to see what happens.

In general, we are not asking for spreading nonstandard analysis across mathlib, rather for solid foundations.

By the way, could it prove the testing theorem here?
#mathlib4 > Non-standard analysis @ 💬
I am rather lost in all of the edits in that repo.

[Mirek Olšák]

By the way, does it compile?