@user21820 your way of writing proofs is honestly great, authors should use it

@LeakyNun Nope they are not. ZFC does not have a notion of "function", and you are free to define it (definitorial expansion) in any way you like as long as you can use it in the ways you want.

One possible way is to define a function as a certain kind of set of pairs, which would then be equal to its graph. But since that is just one of infinitely many viable but incompatible ways, it would be inaccurate to say it is the same.

=)

::Currently checking transcript for the rigorous definition of membership operator $\in$::

@Secret No definition; it's a binary predicate-symbol in the language of ZFC itself.

I am thinking about generic foundations, thus trying to construct $\in$ from e.g. first order logic

@Secret Oh. Then the answer is, you can't. How can you define anything in pure first-order logic without having any relation other than equality?

In general, any viable foundation for mathematics has to have some notion of collections or functions.

Otherwise you probably can't do more than PA.

Well, currently in my construction attempt exepriment (in another chat room), I have the existence of a universe object as an axiom, I am trying to build some kind of inference rule for membership because I will need to think carefully how to populate this universe so that I won't end up accidentally including objects of null value

I figure PA will let me generate the naturals from some starting object, but I need to figure out how to write $\in$ into the logic so that I can put those objects constructed into the universe as they are constructed

@Secret But the only way that a "universe object" can be meaningful is if you already have the notion of membership, so that you can say that every object is a member of the universe.

So "every object is a member of the universe." is already a primative notion and cannot be expanded into an inference rule?

@Secret This is one possible viewpoint (similar to mine), but again you need the notion of membership to be already there. Answering your last question as well, like this:

Universe rule: x :: S |− x :: obj.

This is almost exactly one of the rules in my type theory. The "::" denotes typing, namely "x :: S" means "x is of type S".

So whenever you manage to deduce that something is of type S, then that thing is an object.

sounds sound

This captures the notion you had that objects are 'put' into the universe as they are constructed.

This viewpoint is also prevalent in other type theories.

They largely use ":" instead of "::". I use "::" because I also have ":·" for expression typing.

"x :· S" denotes "x is of type S or is predicatively null". Here "predicatively null" is supposed to mean "we predicatively know it is null".

For example:

Procedure application: f :: proc(S,T) ; x :·S |− f(x) :· T.

This essentially says that if you have a procedure f whose input domain is S and whose output is predicatively known to be either of type T or null, then applying it to any x that is predicatively known to be either of type S or null yields something that is predicatively known to be of type T or null.

Of course, so many words get elegantly expressed as the rule itself.

indeed, and I can see how this programming like style makes it intuitive

Yes. I always say that my type theory is strongly influenced by the computability viewpoint as well as programming language design.

And I'm going to spend some time now working on it. So I may not reply quickly.

Before that, I want to reply someone else's question here.

@ManeeshNarayanan You need at least a 100% grasp of some deductive system for full first-order logic. I would recommend a Fitch-style natural deduction such as this variant. For ordinary mathematics, you often do not need a much deeper understanding of logic, but of course the more you know about logic the better. =)

The reason for my first point is that hard problems often involve many levels of quantifiers, including nested inductions, and you cannot do them properly without a 100% grasp of a deductive system (whether explicit or just in your head).

@Espinoza Sadly, I haven't seen any author that does. I did it consistently throughout the notes I provided for a short optional mathematics course that I taught, so it is definitely doable, but people who have never tried it usually think it is infeasible to write proofs so structurally.

@famesyasd Your this question actually has a trivial answer; you did not use the right definition of derivative when you said "vanishing there". However, there is an extremely interesting question about what what you did means.

Let us be more precise. For ease of understanding, I will use a framework where we analyze variables that vary with a parameter.

Take real parameter t. Let x = sin(t)^3 and y = cos(t)^3. (So x,y are variables that vary with t.) Then everywhere dx/dt = 3·sin(t)^2·cos(t) and dy/dt = −3·cos(t)^2·sin(t). In particular, if t is a multiple of π/2, then dx/dt = dy/dt = 0. This is probably what you were talking about. What does it mean? Well if t is time, then the point (x,y) always moves with a well-defined velocity, which is zero at each cusp (corner), meaning that it comes to a (momentary) stop at that point!

You should also see that you are making a logical error when comparing to dy/dx. In this framework, the chain rule states: Take variables x,y,z varying with parameter t. Whenever dy/dx and dz/dy are both defined, dz/dx = dz/dy · dy/dx.

It also turns out that when t = 0 we have dx/dy = 0. Proof: As t → 0 we have the following. x ∈ (t+o(t))^3 ⊆ t^3+o(t^3). y ∈ (1−t^2/2+o(t^2))^3 ⊆ 1+t^2·3/2+o(t^2). Thus Δx/Δy ∈ ( t^3+o(t^3) ) / ( t^2·3/2+o(t^2) ) ∈ t+o(t) → 0.

And similarly when t = π/2 we have dy/dx = 0.

Sorry typo, some of the + in the above should be −. I'll leave you to figure out which ones!

Two notes. Try the same approach for z = sin(t)^2 and w = cos(t)^2, and observe that when t is a multiple of π/2 we also have dx/dt = dy/dt = 0 but now have dx/dy = dy/dx = −1.

I forgot my second point. Oh well. Anyway there is another typo so I might as well fix it:

y ∈ (1−t^2/2+o(t^2))^3 ⊆ 1−t^2·3/2+o(t^2). Thus Δx/Δy ∈ ( t^3+o(t^3) ) / ( −t^2·3/2+o(t^2) ) ∈ −3t/2+o(t) → 0.

Argh... my brain must be tired... last part should be −2t/3+o(t) → 0.

@DrewBrady: Hello! You're welcome to discuss/inquire about mathematical logic here. I'll be off now, but if you've a question I'll respond next time I'm here.

@user21820 Thanks