@user21820 are you here? Here, in this definition: "Given any metric spaces S, T a function f : S→T is said to be continuous at x∈S iff, for any open set B ⊆ T such that f(x) ∈ B, for some open set A⊆S we have Imf(A) ⊆ B" what if we take sets to be closed instead of open, nothing changes right? If it changes please don't spoil with an example!

also, should'nt we have x ∈ A too?

@famesyasd Did you try to either prove the two equivalent or find a counter-example? =)

@famesyasd Yes this condition is supposed to be there. Not sure why it's missing from yours.

actuallly I havenot I just read this definition and insta posted lol

I was going to explore it yes

Well, actually, i copypasted it from your post :)

Where did you read it? Hopefully not from a textbook...

so it's misssing from your post :)

math.stackexchange.com/questions/1726025/… here

=O

Which post? Okay I'll check and fix. Thanks!

xd

@famesyasd Indeed you're right. You should convince yourself with a counter-example why it is necessary to have "x ∈ A". =)

I've fixed it now.

@famesyasd: So how's your exploration going? =)

Well, I'm exploring my food right now :) So far I checked one combination (closed in x, open in y) and it does'nt seem to work with functions from singleton set but I'm not sure yet, I'm going to eat now and return a bit later

Ok!

@user21820 Hi, are you familiar with Shoenfield's Mathematical Logic?

@shredalert: Oh hello! Long time no see (here). =P

@user21820 Indeed

@shredalert I've heard of this, but never read it.

@user21820 I've been studying it and, annoyingly, there are axioms the author uses in proofs that don't even get mentioned. And it's supposed to be a text on mathematical logic. Cardinal sin, imo. @_@

Feel free to ask about it here then. Shoenfield is a modern logician, so I and LeakyNun should be able to understand your questions about it, and hopefully answer.

@shredalert Oh my this doesn't sound very modern. I guess "symbol of index n" means "predicate/function-symbol with n inputs".

@user21820 yep, almost.

Don't worry about it actually. I'm pretty certain he's using unproven lemmas or axioms. Already sure that he did for the first Lemma in the book. lol Saw people discussing it on here.

By "here" I mean the site, not the chat.

@user21820 Is Enderton more "modern" in comparison?

Then it's just the unique parseability thing. Just a short while ago I wrote something about that here in this chat-room.

Yeah, it is about unique parsability

Well, I've actually proved unique parsability already. It's a theorem that he's utilising for free and bound occurrences of symbols

@shredalert The first logic course I took did use Enderton, and Enderton does do this in significant detail, and since you're a programmer sort you might like it. I didn't like Enderton at that time because it was very hard to find where he defined things, and it wasn't very tidy. But after seeing so many other logic textbooks, his is actually one of the better ones.

@shredalert If you've proven unique parsing, then the occurrence theorem just follows immediately from that, doesn't it?

@user21820 I don't think so. I proved already that if a designator can be written in two ways, they must be the same expression

Anyway a relevant conversation starts here:

Pretty certain that is "unique parsability"

See the linked conversation for my definition of unique parsing (for propositional logic). It's similar for first-order logic.

@user21820 I'll give it a look.

@user21820 Is it just me or is it "simpler" to prove unique parsing for Polish notation?

@shredalert I've not tried but intuitively there should be no fundamental difference.

Having compulsory brackets actually makes it easy to prove unique parsing.

It is when you start dropping brackets that it becomes a bit annoying to prove things.

Some sort of bracket-counting has to be implemented though, if brackets are used.

but not if we have notation like $\vee AB$

Whatever the case, I'll give Enderton a go and see how much I enjoy it.

@shredalert Correct. That's what we were referring to as the parenthesis-counting lemma. For Polish notation, it's annoying because you need to know where to split the inputs, which amounts to some kind of input-counting (instead of bracket-counting).

@user21820 That is a fair point

So that's why unique parsing ought to immediately give you your occurrence theorem.

The only issue is that unique parsing does not imply that v cannot straddle the boundary between two inputs...

And so if that's what you're missing, then yes that's an actual difficulty.

I'm certain he's using unproven lemmas that are non-trivial or taking them as axioms.

He's already done it once.

I think what you need for Polish notation is a stronger claim: Given any designator x+y, there is no designator y+z for non-empty z.

Did he prove this earlier?

He proved unique readability from 2 lemmas

Better still: Given any designator x+y, there is no designator y+z for non-empty z, and there is a unique designator that is a prefix of y.

What I just said should be able to be proven by structural induction, and should imply both the occurrence lemma and unique parsing.

$u_1,\cdots, u_n$ and $u'_1, \cdots, u'_n$ are designators, and $u_1\cdots u_n$ and $u'_1\cdots u'_n$ are compatible $\Rightarrow$ $u_i$ is $u'_i$ for $i=1,\cdots,n$.

if two expressions are compatible, one can be obtained by adding an expression to the right of the other

the second lemma is:

Formation Theorem: Every designator can be written in the form $uv_1\cdots v_n$, where $u$ is a symbol of index $n$ and $v_1,\cdots,v_n$ are designators in one and only one way.

I'm guessing this Formation Theorem is what most people call "unique parsability/readability"

Yes it is.

I don't have any trouble with those two. I proved them myself and even ratted out the one axiom he was using implicitly

The Occurence Theorem is more about showing if a designator occurs inside another designator u, it must be u or a part of a designator in u.

Well I don't see how it follows immediately from the 2 lemmas you stated.

Why don't you try proving and then using my lemma? I think it should work.

I would, but right now I have not much energy @_@

Oh okay. Another time then. =)

I've been grappling with the two holes in his proof of the Occurence Theorem

assuming they hold, the proof he provides holds

Maybe I should just give it a rest and come back to it later. lol

Yea sure.

What I usually do in that case is take theorems that rely on such results with a grain of salt.

@user21820 how's research been going btw?

Lol! Not when they are obviously correct, no?

@user21820 I think obvious is a very subjective word. :P

Like if I just claimed with no justification that first-order logic has unique parsing, wouldn't you believe me? =P

Even if we dropped brackets and relied on precedence rules.

You intuitively understand what it means, even if you can't prove it.

@user21820 I wouldn't have trouble with that because I understand a proof of it

@shredalert That's why I mentioned with precedence rules.

Because I've never seen any logic textbook deal with real-world first-order logic with precedence rules and bracket-dropping.

=D

But I believe it has unique parsing and whatever else anyway, even though I myself have never proved it.

Heheheh.

@user21820 I always feel a pang of guilt when I use a result I haven't proved. xD

Then there's practical usage as well. Don't need to prove some meta-results in order to use specific systems irl.

I have come to appreciate indexing and "size" though. A lot of proofs I've seen in logic reduce to indexing some inductively defined objects and proving some property by some form of induction. And then within those proofs bijections can establish that certain sets have the same size and that property seems to be the key one to apply the induction hypothesis

@shredalert Yea well I have to be 100% sure it is correct before I do so. In cases like the one I just mentioned, it's more or less as described in my linked conversation. Namely, we don't define designators recursively, but rather define a parser program, and then unique parsing is now automatic, but then the difficult part is to prove that we can construct any first-order expression with arbitrary meaningful parsing.

This can obviously be all formalized and proven, but is just a waste of time, because one would have to formalize programs and what-not just to do it.

This is the same way we understand real-world programming languages and compilers too.

@user21820 It seems though that back in the "old days" designators were defined recursively and that became the standard of how metamathematics is done.

Haha that's perhaps true.

The program perspective could only arise after programming.

Indeed. Programming practices are actually really pedagogically useful.

I find so at least.

Gotta head out. Nice to be back around here.

@shredalert: Ok see you around again soon!

I'm heading off too!

Unrelated to logic, but amusing anyway haha..

when your diagrams get three-dimensional

@user21820

@LeakyNun What's that diagram about?

@shredalert homology