I mean

or maybe it should be "forall x in S (φ(x) : bool) ⊢ forall x : S φ(x) : bool"

also there should be a rule that if x[1..n] : S[1..n] ⊢ P(x[1..n]) : bool

where P is some predicate symbol

I can't write "forall x x = x" now lol!

ah no, I can

to prove forall A,B,C if A ⊆ B, B ⊆ C then A ⊆ C does not require any axioms of set theory, does that mean that this is such a fundamental fact about sets or something?

@user21820 do we have a rule that "x : S ⊢ x : obj"?

@famesyasd A lot of these decisions must be made together as a whole. In our current discussion, I'm assuming we have the logic part of my system. Many decisions have to be made simultaneously when we go beyond that.

For example, if we replace the syntactic rules by the typing rules as above, and we have a type of all sets, then we construct a predicate-symbol R := ( set x ↦ x∉x ). From now on I'm going to use "ref(S,T)" instead of "func(S,T)" for the type of function-symbols with input in S and output in T. As before, we would add the axioms "R : ref(set,bool)" and "∀x∈set ( R(x) ⇔ x∉x )", and we have the axiom "R : ref(set,bool) ; x : set ⊢ R(x) : bool".

The question is, can we also have "R : obj"?

The answer is, as always, it depends on what else we want to have. We certainly cannot also have the rule "S : ref(set,bool) ⊢ S : set ; ( x : set ⊢ x∈S ⇔ S(x) )", otherwise we get "R : set" and hence "R(R) ⇔ ¬R(R)".

But if you don't add this kind of assumption that every object must be captured by a set, then I think that rule is safe, even with the axioms and rules given under "Set Theory" in my system. The reason I cannot be 100% sure is that my rules allow you to construct any explicit set of objects, so if R is an object then you can construct {R}. What would that mean? Well, R is simply a syntactic object, so {R} would just be the set whose only member is that syntactic object. I don't see any problem.

@famesyasd ∀x∈obj ( x = x )".

@famesyasd Yes you do the same thing with predicate-symbols as with function-symbols. Since it's just a matter of changing "T" to "bool", I didn't bother stating it yesterday.

@famesyasd Yes indeed I didn't include all the typing rules yesterday, so it's good that you can figure them out yourself, such as for equality and now quantifiers.

Same for "∃".

@famesyasd Using the typing rule you have figured out, you would need to prove "Given x∈S ⊢ ( Given y∈S ⊢ φ(x,y) : bool )", and then you can prove "Given x∈S ⊢ ( ∃y∈S ( φ(x,y) ) : bool )" and hence "∀x∈S ( ∃y∈S ( φ(x,y) ) ) : bool".

what

no it would be wrong to deduce that

What is "that"?

"Given x∈S ⊢ ( Given y∈S ⊢ φ(x,y) : bool )"

it's wrong

no?

What's wrong? I'm saying you need to have already proven that before the rest works.

ah I see

For example, we can prove "Given x∈S ⊢ ( Given y∈S ⊢ x=y : bool )", and hence "∀x∈S ( ∃y∈S ( x=y ) ) : bool".

yep

I'll also note that in practical implementation of this system, all typing inferences can be done deterministically (and hence automatically) by the proof assistant, so the user will not have to supply any statement of the form "x : S".

Taking the above example, if you create a subcontext "If ∀x∈S ( ∃y∈S ( x=y ) ):", the proof assistant knows that you are only allowed to do that if you prove "∀x∈S ( ∃y∈S ( x=y ) ) : bool", so it can automatically check (reversing the above process) whether you can get "Given x∈S ⊢ ( Given y∈S ⊢ x=y : bool )", and at that point it sees that it's correct because of the typing rule for equality.

So in fact, the user does no more work in using such an implementation than in standard FOL, and yet has the benefit of type-checking!

@famesyasd Yes it works for any types A,B,C, where "S⊆T" is short-hand for "∀x∈S ( x∈T )".

Set theories should be thought of as systems that govern certain special kinds of types. For all we know, ZFC could be inconsistent or unsound or meaningless. In contrast, the fact you mentioned is more a fact about subtyping than anything to do with any kind of sets. You could even extend "⊆" as follows:

"S⊆T" means "x : S ⊢ x : T".

Then it is obvious that if S⊆T and T⊆U then S⊆U.

Does this make sense? Thinking in terms of types can be very illuminating in my opinion.

(Away for a while.)

@user21820 Do you mean I can construct nonsets with your rules (that is, types)? I missed how I can do that.

I only used types for type-checking that's all

@user21820 nope :) I mean this fact follows straight from logic but you can interpret it in terms of sets or how you did in terms of types even. Does that make it some special fundamental truth about types/subtypes just because we found some interpretation or does it still has nthing to do with them simply because we derived it only from logic, without using any connections from type theory

@famesyasd Well yes it follows straight from logic, if you already have the binary relation-symbol "∈". The point is that it's in some sense true even if you don't, because it applies to any pre-existing or definable types in the sense we've been using them.

@famesyasd Look for the "type-notation" rule. In standard set theory the types constructible via this rule would be called classes.

@user21820 ? no such rule there or at least you haven't called it by the name

@famesyasd Under "Set Theory" in my post.

right but we only have E:{x:P(x)}⇔P(E)

not E∈{x:P(x)}⇔P(E)

@famesyasd This isn't what I wrote there...

where?

In the post. I know I used "∈" in that post for type membership as well as set membership, because in standard set theory every type has boolean membership.

But it's syntactically invalid to write "E:{x:P(x)}⇔P(E)".

Over here, I gave the weaker version:

what's the difference

It's actually as powerful, because of what I wrote next.

If we permit forming types that don't even have boolean membership, then the one I gave here is the right one.

In standard set theory, every class has boolean membership, so both give the same results.

okay I

I

I'm confused

Firstly, both versions require you to have proven "x : obj ⊢ Q(x) : bool".

The version in my post then allows you to prove "E∈{x:Q(x)}⇔Q(E)" if you have "E : obj".

The version I gave here only allows you to prove any of "E∈{x:Q(x)}" or "Q(E)" from the other.

Both versions are equivalent because of the requirement.

You can ignore what I said about non-boolean type membership if that's confusing now.

Anyway, you must remember that ":" is not a binary-relation-symbol, so you cannot use it as if it is. It's more accurate to think of it as a meta-level notation.

wait, so it's "E∈{x:Q(x)}" now?

@user21820 here there's no "in"

Sorry, as I said I used "∈" for both type membership and set membership in my post. That's why it's confusing when we're joining the two.

In standard set theory, the idea is that some types (classes) are sets. So it was convenient to use the same symbol.

@user21820 so the rules are prove that "x : obj ⊢ Q(x) : bool" then you can use those?

Yes.

okay

In general type theories, it's better to keep the meta-level ":" separate from the internal "∈". That's why I used ":" here for typing.

That's also why we needed a rule to elevate sets to types.

In my post you see no such rule because I 'cheated' by using the same symbol. =P

Which is what set theorists do anyway. Do you know MK set theory? It has classes and sets, and both use the same "∈".

nope

okay so in the end with the rules you gave here I only use types for type-checking, correct? no classse nor anything, I don't even understand why would I want to have "in" for types

Yes that was the original purpose of the conversation here, to show that we can overlay a type system on top of whatever first-order system you start with, in order to restrict theorems and proofs to meaningful statements.

Only when we want to be able to define new types, would we need something like what I had in my post.

It's important in actual mathematical practice. For example, we want to have a type of all finite graphs, or a type of all well-orderings, or things like that, and then quantify over them in a proof. That last bit cannot be done in an efficient manner without being able to define new types.

For example, you could define a new predicate-symbol FinGraph, but then your theorems would have to look something like "∀G∈obj ( FinGraph(G) ⇒ ... )". Whereas if you can define the type FinGraph, then you can use "∀G∈FinGraph" and reason nicely.

how come all finite graphs do not form a set

Because if it is then you can extract a set of all sets from it.

graph is a subset of N times N right?

(V,E) subset N times N

so they all lie in P(N times N)

@famesyasd That's the usual way to cheat in some cases like finite graphs. You can see that cheat and other examples where cheating is impossible here:

Point 2.

@user21820 isn't this essentially NBG?

@famesyasd Depends on your type-construction rule. In the one in my post, yes, because we cannot quantify over types when constructing a type.

In MK set theory, one can define a class with a formula that quantifies over all classes. That makes it stronger (and even harder to swallow).

Already in ZFC, one can define a set that quantifies over all sets. I don't know how you feel about that haha..

@user21820 you meant define a set with a formula that quantifies over all sets?

@famesyasd Yes ZFC can do precisely that! And hence I also permitted that in the system in my post, to make it compatible with current mathematics.

@user21820 to deal with the "lim" notation requires even more type theory?

@famesyasd You mean like "lim[n→∞] ..."?

yeah

\lim, \sum, \int all those I think they are all similar

Well, you just have to set up new inference rules for the new notation. Limits are the most tricky. One issue is to decide how to deal with limits that don't exist. My preference would be to define a predicate-symbol for LimitExistsAt, and then you can define the function-symbol LimitAt for only (function,input) pairs that satisfy LimitExistsAt.

is "\sum_{i=n}^m a_i" also a function symbol that receives (n,m,a) triple?

where a is a function

Another issue is what kind of functions to support. Ideally, you want to be able to talk about any real function on a subset of the reals. And also, if you have constructed D := { x : x∈real ∧ x>1 }, do you want to be able to write "LimitExistsAt( ( D x ↦ ... ) , −2 )"? Would you consider it meaningful? If so, probably you want it to be false. If not, then you can't even use a predicate-symbol for LimitExistsAt if you want to force the second input to be in the domain of the first input.

@famesyasd Yes that works. And summation won't have as much trouble as limits.

and if the summation is infinite then "\sum_{i=0}^\infty a_i" denotes a function symbol that receives a and outputs a sequence with its members being finite sums of a from 0 to n?

@famesyasd Infinite summations have to be defined after you define limits, because it's a limit of the partial sums.

haha

that is, if the limit exists

Exactly.

That's why limits are the biggest problem to formalize in analysis.

do you see the overload here?

we denote as "\sum_{i=0}^\infty a_i" both the sequence and its limit, if it exists

@famesyasd No in standard mathematics that never denotes the sequence.

The sequence is a itself.

I'm pretty sure I've seen in 3 books that it was mentioned explicitly that it does denote the sequence formed from partial sums of a

and if the limit of that sequecne exists then the very same notation denotes its limit

@famesyasd I'm afraid those are not standard; I've never seen any standard text do that, because it doesn't make sense.

We define Sum[k from 0 to ∞] f(k) := lim[n→∞] Sum[k from 0 to n] f(k) and that's it.

and how do you denote the sequence of partial sums then

alright I checked Tao and Rudin

Tao only defines it to be the limit

and Rudin does both

lol

another (Russian) book defines it to be both

Folland defines it to be both

another (very good) Russian book defines it only as limit

I'm surprised. Why would anyone want "sum" to mean "sequence of partial sums"?

Lol.

@famesyasd ( nat n ↦ Sum[k from 0 to n] f(k) ).

okay, so this is all one big function symbol?

Which would be ( N n ↦ Sum(f,0,k) ) after you've defined finite summation.

you meant ( N n ↦ Sum(f,0,n) )

Yes sorry.

what's this notation?

yeah I guess that's just one big function symbol

@user21820 yeah no, If x is not an adherent point of D then LimitExistsAt should be false

so that we do not consider such points as -2

well anyway when I asked about limits I thought that you would maybe suggest something of this kind

I can't quite transfer what is written there so I can't quite understand did they do something cool or not

ahhhh

@famesyasd Oh wait you do want to allow limits to points outside the domain, so you should permit writing "LimitExistsAt( ( D x ↦ ... ) , −2 )", and even proving that it's false.

yeah predicate should be defined everywhere but should be false for -2

And in the example given you want "LimitExistsAt( ( D x ↦ 1/x ) , 1 )" to be true (and provable).

@famesyasd Yep makes sense.

what does?

here's the second part in case you're wondering

@famesyasd It makes sense to define RF := { f : ∃D∈set ( D⊆real ∧ f∈func(D,real) ) } and then define LimitExistsAt : ref([RF,real],bool), so that you can ask whether any given function in RF has a limit at any given real.

@user21820 can you decipher what is written on those pictures, do they do something superior to what we are doing or not?

They are using a weird definition of canonical error-values.

For any type S the error value of type S is defined as ⊥[S] := Ix : S . x ≠ x, which says "the x in S such that x≠x".

Lol.

you've got the copy?

I guessed you were reading "seven virtues ..." which is available online.

So their approach is somewhat non-classical, and I would in fact prefer my (3-valued) type theory, where there is just one unique "null" that represents "no output" in exactly the manner we would like.

yeah

so what are they doing with the limit, is it superior in some way because I don't understand those notations at all so I don't get what they are doing

It's a matter of whether you still want the underlying logic to be standard FOL or not. If you do, then what we've been discussing is in my opinion the best way. Their way requires changing the underlying logic to a truly type-theoretic system, and they will face significant issues with reasoning about types (which is why they even have a section on subtyping to try to remove a small part of the issues).

And the requirement that every object has a type is also why they need an error-value for each type, which I don't like.

Aha see section 8.4 Undefinedness:

> With little difficulty, the semantics of STT can be modified to admit undefined expressions and partial functions. As a result, improper definite and indefinite descriptions would be undefined and error values would no longer be necessary. This extension of the semantics can be achieved by either preserving the classical two-valued nature of simple type theory [17,19] or by extending simple type theory to a three-valued logic [38].

The last bit is exactly what I came up with too.

On looking up the reference [38], I realize that I downloaded it before almost exactly 1 year ago and saved it in my "References" folder. =)

Looking at the paper again, I think that my type theory is better. =D

xD

In summary, we have standard FOL, and we can enforce strict typing as we've discussed, let's call that FOL*. We also have non-classical logics like intuitionistic logic I (the basis of CoC used in Coq) and (Kleene's) 3-valued logic (used in that paper) 3VL. If you enforce strict typing on that to get 3VL*, it would be reasonably close to the underlying logic of my type theory.

I should stop using "*", as chat likes to think it represents italics...

STT (simple type theory) is a forerunner of CoC (calculus of constructions).

what's the point of "f : func(S,T) ; x : S ⊢ f(x) : T." rule, isn't f : func(S[1..k],T) ; x[1..k] : S[1..k] ⊢ f(x[1..k]) : T" coming from the new symbol rule already enough?

Yes I just repeat myself enough times so that nothing goes missing. =)

But remember, don't use "func" for new symbols if you also use "func" for ZFC functions as per the system in my post.

They aren't compatible for the same reason that the type of all sets is not a set.

alright

there's maybe only a couple of things left that I might not udnerstand, I'll work through some theory and ask them later

now I think I'll go to sleep

see you tomorrow

Good night!

This is related to the fact that, logically, the diagonalization does not invoke any further quantification in defining the constructed counter-example. So if the given program enumerates a subset of some set S that is closed under computation, then its diagonalization will also be in S.

This also shows, indirectly, that there is no program that enumerates all computable reals. But of course we already know that (via the halting problem), don't we? =)

The original post was about transcendental numbers, but hey, computable reals are fun to play with. =)

→ 2 messages moved to Basic Mathematics

Read the room description before posting.