@F.Zer It's not just that it isn't needed. As I said before, lemmas that pertain only to a particular theorem should be in only that file and not somewhere else, because nobody would be interested in it outside of where it is used.

Of course in this case it's not even used anymore...

Anyway, it might be a good idea to list all the lemmas at the start of the file so that you don't have to scroll down unless you want the proof.

Given a ∈ ℕ
	If a.a is even
		If a is odd
			Let b ∈ ℕ such that a = 2b + 1
			a.a = (2b + 1)(2b + 1) = 4.b.b + 4.b + 1 = 2(2.b.b + 2.b) + 1
			a.a is odd
			⊥
		a is even
	a.a is even ⇒ a is even
∀k ∈ ℕ (k.k is even ⇒ k is even)

Given a ∈ ℕ
	If a.a is odd
		If a is even
			Let b ∈ ℕ such that a = 2b
			a.a = 2b.2b = 4.b.b = 2(2.b.b)
			a.a is even
			⊥
		a is odd
	a.a is odd ⇒ a is odd
∀k ∈ ℕ (k.k is odd ⇒ k is odd)

Given a,b ∈ ℕ
	If a.b is odd
		If a is even
			Let c ∈ ℕ such that a = 2c
			ab = 2cb = 2(cb)

Given a ∈ ℕ
	If a is not even
		If a is not odd
			a is not even ∧ a is not odd
			¬(a is even ∨ a is odd)
			⊥
		a is odd
	a is not even ⇒ a is odd
∀m ∈ ℕ (m is not even ⇒ m is odd)

Given a ∈ ℕ
	If a is not odd
		If a is not even
			a is not even ∧ a is not odd
			¬(a is even ∨ a is odd)
			⊥
		a is even
	a is not odd ⇒ a is even
∀m ∈ ℕ (m is not odd ⇒ m is even)

@user21820 Oh ok.

@Prithubiswas What are all these lemmas for?

@user21820 idk. Just proving them in-case I need them.

@user21820 I apologize if it was inappropriate.

@Prithubiswas Oh no it's fine. I was just wondering where you were going with them.

Usually a long list of lemmas is followed by some desired theorem. =)

@user21820 They are extremely trivial once someone proves that:

(1):  ∀k ∈ ℕ (k is odd ∨ k is even)
(2): ¬∃k ∈ ℕ (k is odd ∧ k is even)

Indeed.

@Prithubiswas: In fact, this can be generalized to ∀k∈ℤ ∀m∈ℕ ( m>0 ⇒ ∃!r∈ℕ ( 0 ≤ r < m ∧ m | k−r ) ). If we restrict to mere PA it would be ∀k∈ℕ ∀m∈ℕ ( m>0 ⇒ ∃!r∈ℕ ( 0 ≤ r < m ∧ ∃x∈ℕ ( k = m·x+r ) ) ).

Which you might recognize as stating the uniqueness of remainder upon integer division.

@user21820 Interesting. I will try to prove it if I ever reach ℤ.

@Prithubiswas If you have an outline for a attempt with a gap, you can show me and I can give you an appropriate hint. Of course, if you want to get it completely on your own, that's fine too.

Given a ∈ ℕ
	Given b ∈ ℕ
		If a.a = 2.b.b
			If a>0
				\\Define P(n) ≡ n.n = 2.b.b
				∃k ∈ ℕ (k.k = 2.b.b)
				∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )
				Let c ∈ ℕ such that P(c) ∧ ∀k∈ℕ ( P(k) ⇒ k≥c )

				c.c = 2.b.b
				c.c is even
				c is even
				Let d ∈ ℕ such that c = 2d
				2d.2d = 2.b.b
				4.d.d = 2.b.b
				b.b = 2.d.d
				c.c = 2.b.b
				.
                            .

@user21820 my failed attempt.

I see. You seem to have been thrown off by the "⇒ k = 0".

Exactly!!

Didn't you try induction or well-ordering?

I did try well-ordering.

And what was the attempt like?

I just showed it to you.

Oh oops sorry I didn't notice.

Well, you can see why your attempt fails by doing a bit of meta-analysis. Given a,b∈ℕ and a·a = 2·b·b, you let c be minimum such that c·c = 2·b·b. But intuitively you already know there is only one such c because earlier you showed that squaring respects ordering. So you are not gaining anything from this because c would simply be a, and everything smaller than that is less than c·c by PA− which you already know by PA−. Thus the well-ordering you used gave no new information.

Since I suggested earlier that well-ordering works, it means that you're applying it at the wrong place.

Got to go. Will be back later.

@user21820 Sure. See you later!

@user21820 Something like this Lemmas ?

@F.Zer Yes, but what about my preceding comment?

Did you really use line 5 anywhere else?

@user21820 The remaining bit will just be the def of a surjection one question though first we say that for f to be a surjection it must be function and then we say that it also must satisfy the def of a surjection but the second bit can't be well defined if the first isn't so we input something which is not a function in surgects(f) it should be false but the statement isn't well defined

I wonder why tao mentions the axioms of zfc and pa in his book while doesn't talk about first order logic which is even more fundamental

Rudin doesn't even mention zfc or pa

and these two books are said to be the best

Can a working mathematician who doesn't work in logic be fine if they don't know FOL

@PaxDaga I want to see that so-called "def of a surjection", because I am unsure whether you can produce the required definition.

ok I will give it but I am really confused about my other question

And for now, you can ignore the issue of whether you can use "f" as a function when it is not.

That is to say, when I say you can use "dom(f)" I mean that: (1) it gives you the domain of f if f is a function; (2) it gives you unknown stuff if f is not a function.

So you don't have to care about that issue. That's why it's okay to have:

what is unknown stuff

any thing that makes sense ?

Yes it can give any arbitrary value. See, if "Function(f)" is false, then it doesn't matter whether the "..." has some unknown truth-value, and that's why we don't have to care if we use "dom(f)" inside the "..." even though f may not be a function.

@PaxDaga Tao is a talented mathematician, not even an ordinary one. He was an IMO gold medallist. I would say that IMO gold medallists have no problem with logical reasoning even if nobody taught them.

I am talking about Taos book analysis 1

@PaxDaga It doesn't matter what book he writes. His pedagogy is quite bad for weak students. I've read his stuff before. Even advanced students can have a bit of trouble.

@PaxDaga Not all mathematicians agree on which books are the best. Even some well-known top users on Math SE think like me that Spivak's textbook is better than Rudin's.

Anyway, stop complaining and just learn what you need to learn.

Rudin's book is more advanced and contains lot more topics

bUT MAYBE SOME MAY NOT LIKE THE EXPLANATIONS

I am not a weak student

You are, and if you don't agree then just leave this room.

And in case you are unaware, capitals on the internet is considered rude, but I guess it was an accidental capslock.

ok I am weak I agree .

yes it was accidental

how to become strong student?

I will help you. It is definitely possible. And just to clarify, there is nothing inherently bad about being a weak student, because this situation is primarily not the student's fault but their teachers'.

ok def of surjection is a function from $X\to Y$ is a surjection iff $\forall y\in Y (\there exists x (f(x)=y)$

Good. So can you put that in the format I gave you?

@PaxDaga Note that there's a slight error you might want to fix before you post your attempt. You didn't declare where "x" comes from.

Replace ... by $\forall y in T(\thereexists x\in dom(f)(f(x)=y)$

Good. You can just use ASCII "forall" and "exists" if you like. Don't need to use unicode symbols like I am doing, nor LaTeX (because I don't use MathJax in chat either).

Let's see the complete answer:

> ∀f∈obj ∀T∈set ( Surject(f,T) ⇔ Function(f) ∧ ∀y∈T ∃x∈dom(f) ( f(x)=y ) ).

I want you to take note of two things. Firstly, you need two inputs to the predicate "Surject", because it is a 2-input predicate.

Yes but if $f$ is not a function what will Dom(x) be replaced by?

@PaxDaga It doesn't matter, because if Function(f) is false then the "..." doesn't affect the truth value so in that case dom(f) can be totally arbitrary. There are formal systems that have stricter syntax rules that forbid "dom(f)" when "f" does not refer to a function, but those systems are (necessarily) more complicated than FOL, and let's just learn the simple one first.

so the ... part needn't even make sense?

@PaxDaga Well, at the bottom it only has to follow the syntax rules of FOL. Since it is possible to define "dom" in Set Theory in exactly the same way as you just defined "Surject", we can freely use "dom" as a function-symbol, so the "∀y∈T ∃x∈dom(f)" part is okay. You may still object to the "f(x)" part. If you do, then it is a legitimate objection. Luckily, we can also define the function-application notation.

I don't understand what is function application notation

The notation "f(x)" is called function-application notation.

okay but if f is not a function then what does dom(f) or f(x) mean!?

It can be junk. When formalizing mathematics in FOL, you necessarily get some junk like this, but it's okay. Don't worry about it for now, since it's not an important detail for learning FOL, and we can come back to it later. Let's return to your question. Can you define "metric space"? Again, use the same definition format.

Everything is defined here

No, you didn't define "metric space" in that post.

I did not get answer but three upvotes and one commentator said not trivial

@PaxDaga Isn't that what I said? It's mundane and not worth my time to find a rigorous proof even though it is easy for anyone who has familiarity with logic.

Easy does not mean short.

If I learn what you're telling me will it be easy for me?Metric space is a pair (X,d) such X is a set and d is a function from X^2->R that satisfies the axioms of a metric

is it correct

r is there reals

numbers

X^2 is $X\times X$

The function d is known sometimes as the distance function

@PaxDaga Yes of course, why would I ask you to learn something unless it is the fastest route to getting a solid foundation in mathematics? But I asked you to write it in the same definition format I gave you earlier. Why don't you do that?

And satisfy three axioms symmetry , d(x,x)=0 , and triangle inequality intuition for triangle inequality is that the metric gives the shortest distance between two points as some don't know that I am giving intuition to you also

@PaxDaga I don't need all that; do you think I don't know that?

You asked for the def of a metric

I asked for a formal definition in the format I gave you. You're not giving me anything close to it.

I guess you knew it already or you want have such high rep but maybe you dont

What is wrong with you? Why do you keep being so rude to me? Do it one more time and you can forget about me teaching you. I have little time and I will instead teach the many students who actually appreciate it.

math.stackexchange.com/questions/1832867/… I don't understand how I am being rude to you I just gave the def you asked for and wanted to give the my intuition for the axioms

according your post we should convert everything to symbols

and it is agreed upon by many people

You wrote "you want have such high rep but maybe you dont". This is rude.

I meant that you must have already known the defn since you if you didnt then you wouldn't have such high rep and by maybe you don't I mean that you might not know the intuition

What is your native language? Is it English?

I meant that according to your post you shouldn't convert everything to symbols

No

I make typos while tyoping

I'll assume that your rudeness was due to using wrong English. Let me say again clearly: If you want me to teach you, so that you can get a 100% grasp of mathematics, you follow my instructions. Otherwise, don't ask me anything. I graduated as the top student in two faculties including mathematics, and that was almost completely due to my grasp of logic, which most other students lacked.

If math is just a juggling of symbols then I suppose that there isn't much worth for intuition of defntions

Don't question my teaching if you want to learn from me. As I said above, I will not waste my time teaching those who do not want to listen.

So I should not write intuitions when giving def ?

When intuition is important, I will explicitly ask you for it or teach you how to find it.

When it is not, I won't.

Ok its easy to convert the three axioms I gave into symbols

Make sure you follow the same format precisely, same as for the "surjection" definition.

It's supposed to be easy, so get it right the first time.

You mean that you want me define a predicate which tells if something is amertic or not

You mean "a metric space". Correct.

ok I will gtg

Sure. See you later.

@user21820 Thank you for pointing out line 5. I removed it from Lemmas and moved it inside PA-3. Does it look good as it is now ?

@F.Zer You didn't even use it in (PA−3), because the strict version was good enough. There's no need to combine that with the earlier discreteness lemma just to make another lemma.

By the way, I don't see the proof of the non-strict one in (PA−3), which is the one you need.

@user21820 Which is the non-strict one ?

@F.Zer "∀ k, m ∈ ℕ ( k·k < m·m ⇒ k < m ) [lemma]".

Did you perhaps move it to the wrong place?

@user21820 Sure ! That could be it. I will find it.

@user21820 Why do you call it "non-strict" ?

@F.Zer Sorry, I was blur. I meant "I don't see the proof of the strict one".

@user21820 Oh ! I understand now.

Hi @user21820. I have a basic question about set theory: from which axiom(s) of $\mathsf{ZFC}$ does it follow that if $E$ is a set, then $\{E\}$ is also a set?

@Joe Pairing.

@Joe: You get it, right?

@user21820: I think I understand. The axiom of pairing states, in natural language, that if $X$ and $Y$ are two sets, then there is a set $Z$ such that $Z$ contains $X$ and $Y$ (and no other set). Take $X=Y$.

Yes.

@user21820: Ok, thanks. I have two questions, if you don't mind: (1) The axiom of pairing tells us that $Z=\{X,X\}$ exists, but don't we have to use the axiom of extensionality to prove that $\{X,X\}=\{X\}$? (2) On Wikipedia, it omits the "no other set" part of the axiom of pairing. So, it states that if $X$ and $Y$ then there is a $Z$ such that $X\in Z$ and $Y\in Z$. However, apparently we can use the axiom schema of specification to prove that there is a set $Z$ which contains $X$ and $Y$...

...and no other set. Is that correct?

No that is wrong.

You should use the proper axioms, and not rely on "natural language".

Pairing trivially gives ∀x ∃y ∀z ( z∈y ⇔ z=x ) by pure FOL. That is precisely the meaning of the existence of {x}.

Pairing + Extensionality gives ∀x ∃!y ∀z ( z∈y ⇔ z=x ), again by pure FOL.

Your phrase "we have to use the axiom of extensionality to prove that {x,x} = {x}" does not really make sense because it depends on what that "{...}" notation means in the first place.

Specification does not give Pairing. Just check the Specification axiom schema.

@user21820: Ok, I think you have answered my first question. For the second question, I think I mixed up the axiom of specification with the axiom of separation. According to Wikipedia, if we use a weak version of the axiom of pairing, i.e. $\forall x \forall y \exists z ((x \in z) \land (y \in z))$, then using the axiom of separation we can prove that there is a set $z$ which contains $x$ and $y$, and no other set.

Wait, it turns out the axiom of specification and separation are the same thing. Sorry.

@Joe Yes, they are the same, and as I said you would have to stop using "natural language" if you want to get set theory right. When I said "Pairing" I of course mean the standard one, and as you saw on wikipedia it's equivalent to ∀x,y ∃z ∀t ( t=x ∨ t=y ⇒ t∈z ) given Specification.

@user21820: Got it. Thanks again.

You're welcome!

@user21820: I know you said to avoid "natural language" to get set theory right. Right now, I am reading Naive Set Theory by Paul Hamlos, which does treat things informally, e.g. the axiom of extensionality is stated as "two sets are equal if and only if they have the same elements." Do you think this book is worth reading, or not?

@Joe I've never read "Naive Set Theory", but from your description it sounds like a terrible way to learn ZFC. Jech's "Set Theory" would be much much better.

It's not that everything has to be done in symbols. Jech doesn't do everything symbolically either, but it is important to have the logical structure very clear, and natural language just doesn't provide that.

@user21820: Okay, thanks for the suggestion. I'll look into that. By any chance, have you read Theory of Sets, by E. Kamke? That's another book which I have seen recommended.

@Joe: And in case it isn't clear, you don't have to learn ZFC if you aren't interested in higher set theory. There are much friendlier systems that can be used in everyday mathematics based on ZFC. In my post I explicitly gave such a system, which is based on a variant of ZFC that is agnostic about urelements and also expressed in many-sorted FOL to make it pedagogically better (since it forces people to think about the type of every object).

@Joe Basically I haven't studied any set theory textbook because there wasn't a need; I more or less learned what I know just based on my knowledge of logic plus wikipedia's list of ZFC's axioms... And it has sufficed for me for all mathematics outside of higher set theory. So as long as you don't ask me about large cardinals, I should be able to answer you.

@Prithubiswas: Thank you. I take Asaf's advice very seriously, as I do user21820's.

@Prithubiswas Aha I guess that settles it. =P

@user21820 $\forall X,d $ (ismetricspace$(X,d) \leftrightarrow$ (set$(X)$ $\land $functionfrom$X^2$to$R$$(d$) $\land$ $(\forall x,y,z\in X(d(x,x)=0 \land d(x,y)=d(y,x) \land d(x,y)\le d(x,z)+d(z,y)$)) where functionfrom$X^2$to$R$ is a prediacte determines if some object is a function from $X^2$ to $R$ which can be defined easily.

@Joe Yea, if I say something about set theory and Asaf says otherwise, Asaf is almost surely the one to rely on.

@PaxDaga Yes don't need to define the last part. By the way is there a reason you use so many separate dollar signs?

Oh I see; you want to keep the upright font.

Yes that's why

Ok firstly you should know that your "functionfromX^2toℝ" cannot be a predicate-symbol. If you want you need a 3-input predicate. That's why earlier on with the surjection example I emphasized that it has to be a 2-input predicate-symbol and that your initial attempt was wrong because you put a variable-name into a predicate-symbol.

why three input

earlier I thought T was fixed

Because you simply cannot have a variable-name in the predicate-symbol. This is the basic syntax of FOL. I thought you knew it because you said you did. It seems you need to patch your incorrect knowledge about the syntax of FOL.

Here is what it should look like:

> ∀X,d ( MetricSpace(X,d) ⇔ Set(X) ∧ d:X^2→ℝ ∧ ∀x,y,z∈X ( d(x,x) = 0 ∧ d(x,y) = d(y,x) ∧ d(x,y) ≤ d(x,z)+d(z,y) ) ).

Or with the explicit 3-input predicate:

> ∀X,d ( MetricSpace(X,d) ⇔ Set(X) ∧ IsFunctionFrom(d,X^2,ℝ) ∧ ∀x,y,z∈X ( d(x,x) = 0 ∧ d(x,y) = d(y,x) ∧ d(x,y) ≤ d(x,z)+d(z,y) ) ).

why R needs to be there isn't that fixed?

so why three input not two@user21820

@PaxDaga Errr, okay now it is very clear that you do not know the syntax of FOL.

but why

actually I understood

@PaxDaga What? Do you or do you not understand why yours is wrong and you need a 3-input predicate?

I get that Isfunctionfrom takes three inputs d,X^2,Y and here we set Y=R

I that wrong?

What do you mean "set Y=ℝ". This makes no sense...

FOL is not about setting anything to this or that.

I think you are just guessing your way through, rather than having a 100% grasp of FOL. This isn't the way to get to complete mastery of mathematics.

I mean for example if $f(x)=x^2$ and we set $x=5$ then f(5)=25

That's wrong.....

why can't we do that?

It's just wrong. Just like if a person speaks grammatically wrong English, there is no "why can't we"; it's just wrong and that's it.

You need to learn what is right, rather than keep insisting on what is wrong.

Ok

from where to learn FOL

I give you two options that I will fully support no matter which you choose.

The first is to read "Language, Proof and Logic", which is an introductory textbook to FOL. It does not assume any background knowledge, but it is really long-winded. It's not my first choice but it's definitely easier for beginners.

The second is to learn FOL directly from me, but that means you will have to start from scratch, namely PL (propositional logic) and work through all the exercises I give you to make sure you truly understand PL even before we touch FOL. I've done that with every student, because to me it makes no sense to try FOL until I'm sure the student knows PL.

OK I will choose 2

as 1 is very very long

Ok, let's talk again next time, as I need to go now.

@PaxDaga: See you!

ok