@LeakyNun: Sorry yesterday I was sleepy; ACA cannot prove anything close to Cantor's theorem. You need third-order arithmetic for that, in which you can prove "¬∃f∈func(N,func(N,bool)) ∀g∈func(N,bool) ∃k∈N ∀m∈N ( f(k)(m) ⇔ g(m) )".

@AdarshKumar: Hello!

@user21820 hi whats up

@user21820 then how do we talk about uncountable models?

did anyone here know html coding

@AdarshKumar Yes, but you should find a chat-room linked with StackOverflow for that. HTML is very far from mathematics. =)

@LeakyNun Well third-order arithmetic already can talk about uncountable models, just as you have Cantor's theorem for func(N,bool).

Of course, you may not be satisfied with that, but then you'd need to ask yourself what kind of "uncountable" are you looking for.

@user21820 actually i am very weak in coding , if you have time then can you please make a code of a maths question

this is the link of my question mathematica.stackexchange.com/questions/180423/…

@AdarshKumar That is a poor question; no effort shown, and you didn't even bother to rotate the image. Programming is not about asking other people to code for you, but about trying it yourself and learning from your own experiences and others' feedback.

@user21820 did you kown the proof from where Ramanujan gave that relation?

@AdarshKumar That is off-topic to this chat-room.

@user21820 so how can you say that it is a poor question?

Off-topic; please leave this chat-room.

Is $\omega_1$ absolute?

@user21820 fine i am leaving. thanks for your precious time

@LeakyNun No it isn't, and the simple way to see it is that if ZFC is consistent then it has a countable model, in which ω[1] would be externally countable.

are all its elements absolute?

@LeakyNun What does it mean for an element to be absolute? You can only talk about whether an object given by a defining formula is absolute between models. In the case of ω, it is absolute between V and L because of the way L is constructed. In general, ω is absolute between transitive models of ZFC due to Foundation.

I see

If you mean definable elements of ω[1], I am not sure.

@LeakyNun: I think you may be interested in the answers here. I didn't realize that it may be rather relevant to my own project, because I seem to be only able to construct a ZFC-like world with bounded quantification.

here's how Lean defines a pre-set:

/-- The type of pre-sets in universe `u`. A pre-set
  is a family of pre-sets indexed by a type in `Type u`.
  The ZFC universe is defined as a quotient of this
  to ensure extensionality. -/
inductive pSet : Type (u+1)
| mk (α : Type u) (A : α → pSet) : pSet

Well by bounded quantification I mean that specification and replacement only works for bounded quantification. Reasoning still works for unbounded quantification.

@LeakyNun So what next?

I don't know

intuitively how does it correspond with a set?

@LeakyNun I can't tell until the other stuff are defined so that one can see whether it really obeys the ZFC axioms or not.

/-- Two pre-sets are extensionally equivalent if every
  element of the first family is extensionally equivalent to
  some element of the second family and vice-versa. -/
def equiv (x y : pSet) : Prop :=
pSet.rec (λα z m ⟨β, B⟩, (∀a, ∃b, m a (B b)) ∧ (∀b, ∃a, m a (B b))) x y

/-- `x ∈ y` as pre-sets if `x` is extensionally equivalent to a member
  of the family `y`. -/
def mem : pSet → pSet → Prop
| x ⟨β, B⟩ := ∃b, equiv x (B b)

@LeakyNun That's essentially how I construct a ZFC-like world in my type theory... One needs recursion. I would say that you face your first big problem there. How do you prove your recursion is well-founded?

it's a meta-theorem

Uh? Then there is something seriously wrong. If you can't prove it inside, you can't construct the ZFC-like world.

oh, it's a meta-theorem that it will terminate when you evaluate it

you can't state it inside

but you have access to the function inside

And that's what I'm identifying as something wrong. It means you don't have a function inside, and so cannot use it as a function.

If you simply assume that it is a function, then you might as well assume a ZFC-like world from the beginning and don't bother to construct it.

we have the function inside

the "rec" (recursor) comes with every inductive type

protected eliminator pSet.rec : Π {C : pSet → Sort l},
  (Π (α : Type u) (A : α → pSet), (Π (a : α), C (A a)) → C (pSet.mk α A)) → Π (n : pSet), C n

@LeakyNun Oh. That's an interesting way to sneak in the assumption.

"you can't state it inside" is referring to the fact that you can't trace the steps, because it's a program outside, but not a program inside

otherwise we would have soundness issues

@user21820 so they're basically saying that a set is a collection of sets?

@LeakyNun Who is they? But yes that is an idea that I had, but even that does not work in my system, because of predicativity issues.

they = those who wrote this code

in particular, Mario Carneiro

Ah. Interesting.

indexed by types in our universe

That indexing thing and the inbuilt recursion is essentially cheating, because it is hiding all the crucial assumptions.

heh

Moreover, even if we ignore that, by itself it raises some philosophical objections, for example that it is tied to the chosen universe u.

it is indeed

there's a model of zfc for every universe

/-- The powerset operator -/
def powerset : pSet → pSet
| ⟨α, A⟩ := ⟨set α, λp, ⟨{a // p a}, λx, A x.1⟩⟩

/-- The set union operator -/
def Union : pSet → pSet
| ⟨α, A⟩ := ⟨Σx, (A x).type, λ⟨x, y⟩, (A x).func y⟩

@LeakyNun What does "//" mean? And what does "namespace classical" and "noncomputable" mean?

where did you see them?

{ a // p a } is a subtype

github.com/leanprover/mathlib/blob/master/set_theory/zfc.lean

Actually, I should be asking you where you got your code from.

yes, from there

if a theorem x is in namespace classical then we would refer to it as classical.x

noncomputable means it’s a noncomputable function / definition

I guess the sheer complexity of Lean and the unreadability of the proofs make it not enticing for me to learn haha..

@LeakyNun: But I guess since you like Lean you must be also happy with ZFC, since you have a model of ZFC? Lol.

(Assuming they didn't sneak in any more assumptions besides the ones I stated. I can't read the stuff well enough to figure out.)

It appears that QED I shared a few weeks ago is written by none other the famous Terrance Tao

and he planned to do some upgrades to it, hopefully we will have quantifiers soon

@user21820 I just read the axiom of regularity and I don't get it, should I now become very aware of sets that i'm constructing and check every one of each if they satisfy this axiom of regularity?

@famesyasd Sorry I don't understand your question. If you are working in ZFC, then that axiom is just one of many. The sets that you construct from the natural numbers and powerset iterates on it all automatically satisfy regularity, even if you don't have that axiom. But the point of that axiom is that some set theorists like it, and it has absolutely no bearing on ordinary mathematics.

@Secret Aha interesting.

@user21820 okay

@user21820 I remember them saying that whether CH is true in the model of ZFC depends on whether CH is true in Lean

@LeakyNun I'm not actually sure what that means. Presumably, it is known that Lean does not prove CH.

CH should be independent of Lean

so "CH is true in the model of ZFC" is also independent of Lean

what is the smallest undefinable ordinal?

@LeakyNun Oh so that's what you mean.

@LeakyNun Undefinable over what? Under most definitions, it would be countable, but not something you can pinpoint, by definition of definable.

is "x is a countable ordinal" absolute?