Thank you for your help :)

It should still be FOL, because we're only quantifying over the elements of the 'sorts' and not subsets.

@Threnody For your first question, if you want to make a fully formal treatment of graph theory, then of course you have to define all these things like parent and depth in a (rooted) binary tree, and so on. This is actually much easier than "longest path", which is why I used these so that you can in the future (if you wish) formalize them without too much difficulty.

For your second question, the Fitch-style system I gave you is indeed for many-sorted FOL, with an extra ability to create new sorts (called types in that post). But for the purpose of this proof, it suffices to observe that it works as long as you are given the type of full binary trees, since every other definition can be inlined (you as a programmer know what this means, right?).

And indeed even the full system I gave you can be reduced to one-sorted FOL. The reason for using it is that it is more convenient.

Especially if you want to use ZFC-style set theory, you will find that a lot of concepts cannot be sets. For example the type of graphs cannot be represented by a set, otherwise you can extract from that a set of all sets, and hence get Russell's paradox. So the most convenient way would be to define it as a type, so that you can quantify over it. (But since it's not constructible as a set you can't construct its powertype.)

@user21820 Yep I follow

@user21820 "with an extra ability to create new sorts" - the universe rule?

@Threnody No, its the type-notation rule.

@user21820 oh yeah I see

Without that rule, you would have to inline everything. With that rule, you can easily define things like a powerset mapping (which in standard set theory you'd call a class function).

Basically the system I presented there is well suited for people who want to have NBG-style formal reasoning.

@user21820 "it works as long as..." so in other words, we would need an alternative proof if we were to consider ZFC as our MS? (because BT(k) cannot exist in ZFC?)

@Threnody BT(k) cannot exist in ZFC, but since inlining works, any theorem that you prove can be expanded to the inlined form to yield a theorem of plain ZFC.

So you can treat the above proofs as systematically translatable to proofs over ZFC.

@user21820 I don't know if I'm understanding what you mean by inlining, the only inlining I'm familar with is the compiler optimisation for functions

Yes it's almost exactly the same meaning. It means you get rid of that symbol and replace every occurrence by its definition.

I see

So, if I understand correctly, you're saying "We can still get the same behavior BT(k) gives us, the only difference is that we'll have to jump through some hoops"?

Yes. I didn't explicitly say in my system description, but of course you want to be able to give a name to each type you create. For example consider the odd naturals example. In my system we can construct the type odd := { x : x∈N ∧ ∃x∈N ( E = 2·x+1 ) }, even if N is just a type and not an object.

Ehh. but in this example both odd and N can be objects (in ZFC)

Of course.

I'm just explaining that if you do without constructing new types, then you have to inline all the occurrences of "odd".

Similar "hoops" will occur if you want to do set theory without constructing new types.

@user21820 Yes yes I understand that - types are great for this. But the BT(k) type cannot exist in ZFC as you said, so how does inlining fix anything? I feel like I'm missing something crucial

I mean we can write a predicate that describes BT(k) but that doesn't make it reifiable..

@Threnody It just means you go through the proof and replace each occurrence of "T is a full binary tree" and "T∈BT(k)" by the appropriate statements. After you're done, you would have a proof that has no mention of "full binary tree" or "BT" anywhere and the proof would be a valid proof over ZFC.

Of course, you have to replace "∀T∈BT(k) ( ... )" by "∀T∈set ( T∈BT(k) ⇒ ... )" before doing this inlining.

And so on.

Am I right in saying that there you're using the extensionality axiom of ZFC? I'm confused :/

No... you can't be, that makes no sense.

Now you know why I don't like going to ZFC so early, because there are a lot of distracting things that ZFC brings. Better stick to PA and learn the basics first, then you'll see how all of it applies when you go to ZFC. Let's go back to the odd naturals example.

Haha, alright :)

The system we are working in is my Fitch-style system only up to "Peano Arithmetic" (i.e. ignore everything after that section).

So we have the type N and we can quantify over it and basically do basic arithmetic reasoning since we have all the axioms of PA.

Here we do not have the ability to create new types. So suppose we want to say:

> ∀k,m∈OddNat ( k·m∈OddNat ).

Where OddNat is suppose to be the set of odd naturals, i.e. those k∈N such that ∃x∈N ( k = 2·x+1 ). (Sorry in my previous message I bungled the definition of "odd" but nobody noticed...)

But we do not have sets, so we have to express that desired statement by inlining all the occurrences of "OddNat".

First we transform the statement to:

> ∀k,m∈N ( k∈OddNat ∧ m∈OddNat ⇒ k·m∈OddNat ).

Next we replace each occurrence of "t∈OddNat" by "∃x∈N ( t = 2·x+1 )".

You get a sentence that is completely devoid of "OddNat" but expresses exactly the desired meaning.

That is what inlining means, and you can clearly do it for any type of objects that satisfies some property.

Alright, but then we must at least have a way to reify N (I suppose that's what PA is for) - but I get the idea now

@Threnody No we don't even need to reify N! N is a type, and we never use it as an object, and indeed PA does not have any concept of N, nor can it have.

Mhm... N is a type here.

we quantify over it though..

Correct.

Quantifying over something is not the same as having it as an object.

oh?

oh...

So my system up to Peano Arithmetic is in fact exactly as strong as the standard PA (no stronger). If you peek below that section into "Set Theory" you will see that I included one axiom "N ∈ set", so that it is reified. If I'm not wrong, without that one axiom the entire Set Theory system can't do much!

I see!

Ah. I actually didn't see that axiom lol

That one axiom has a similar role as the axiom of Infinity in ZFC. And ZFC minus Infinity is weaker than PA.

Of course!

N is like the original successor set after all..

And that's what AoU gives us

I said too much so I probably said something wrong lol.

What is AoU? You mean Axiom of Infinity?

Yes

OOooh

I not U.

Lol I just realised.

Gone for a while, thank you for your patience

I was gone for a while too. Basically the reason why you need to reify N is that otherwise you don't have any infinite set and the other axioms don't let you construct any infinite set from finite ones.

@user69608 hi @user21820 any help?

@user69608 Sorry I don't know why I missed your question. Give me a while to look at it.

@user21820 no problem

@user69608 Because you want the cases to be disjoint, so that you can get a lower bound on the total likelihood that one of those cases happens.

Asking for tail followed by a string of m heads makes it impossible to occur simultaneously with the other cases of this form, nor with the first case (m heads from the first toss).

@user21820 oh i get it

in that it was given that (m>n)

what if we take the case of n=m+1?

@user69608 It is an interesting question to simply bound the probability of a uniformly random binary string of length k having at least m consecutive heads, without any particular restriction on k.

@user21820 but k would greater than or equal to 1 and less than or equal to m+1?

Why? Why can't we ask the general question?

Your cited question only gives a lower bound for k < 2m.

Sorry I meant "consecutive ones" not "heads" in the generalized question.

@user21820 how would we doing for this

I will think about it and see if I can get a relatively simple bound and then I'll tell you.

Obviously the proof you cited only works for k < 2m, so we would need a different method.

ok,in this case we could have m heads then 1 tail and then m heads so consecutively m heads may be possible for two times

ok i think i got it

I think this time we should let if first m heads from i to m+i then m+i+1 should be tail.right? @user21820

and remove the case m heads then 1 tail and again consecutive m heads

because it would be counted twice.

@user69608 Yes you can do such removal, but that may not get you a good bound, and it is quite messy; also have m heads 2 tails m heads.

@user21820 ok

@user21820 yes, will have to think about a good bound

You could use inclusion-exclusion principle, but that is not a simple bound.

yeah

@user21820 Hello!

@Knight Hi!

Good Morning

Same to you!

I want to understand "stable points" in differential equations.

the differential equation is $$ \frac{dx}{dt} = f(x)$$

I understand that $x^{\ast}$ are the points such that $f(x^{\ast} ) =0$

@user21820 Thanks for the help! And sorry for posting something unrelated to the chat.

@Knight The book is incomprehensible because x[0] is undefined.

@johnny09 No problem!

@user21820 Can it mean a point near $x^{\ast}$?

As I said, "undefined". Ask the author or your teacher. When a variable appears only once in the whole thing, something is wrong.