@user21820 does this proof: WLOG we may assume that the isometry preserves the origin then it must be a rotation by some angle by the classification thm of isometries of the euclidean plane. Now that means that a line going through the origin is just a rotation of R but this implies that it must be vertical or of the form y=mx
@PaxDaga Well as I told you before, you should focus on learning basic FOL first, because only then can you actually know what is rigorous mathematics. Trying to learn mathematics without having a complete grasp of basic FOL is like trying to understand what a rose smells like without ever smelling one, or like trying to understand a new language without learning basic grammar. After learning basic FOL, then you need a rigorous introduction to real analysis such as Spivak's "Calculus".
@PaxDaga In particular, with knowledge of basic FOL you would see that your proof fails because you are not even using your definition correctly.
The theorem I am proving is ; Let m be a subset of R^2 (under Euclidean metric)hat contains the origin that is isometric to R then it must be vertical or of the form y=mx
Your definition of "line", which I have said three times now. If you can state your definition in FOL (first-order logic), then do it. If you can't, then you must learn basic FOL first.
You claim that you are working in set theory, but not once did I actually see you working.
You cannot just treat mathematics as a wishy-washy game of words. Mathematics is a very precise language that most students do not know and also do not know that they do not know.
You cannot just treat mathematics as a wishy-washy game of words. Mathematics is a very precise language that most students do not know and also do not know that they do not know.
Just to make clear, I never required you to use pure set theory. In this conversation, you're the first one who used the phrase "set theory".
If you want to learn how basic FOL, I can teach you. But if you don't want to learn, I'm afraid I don't want to spend time teaching you things that (in my opinion) you can never learn properly without basic FOL.
The other answers did not explain the background of logic that is the key to understanding this issue. In any formal system where we write proofs, we have to use some formal language that specifies the valid syntax of sentences, and we must follow some formal rules that specify which sentences we...
Ok. For example, look at the axioms of PA, given here under "Peano Arithmetic". I am using this version with restricted quantifiers because it is pedagogically better than the conventional approach.
In that section, I say at the beginning that for PA we need the type ℕ and the constant-symbols 0,1 and the 2-input function-symbols +,⋅ and the 2-input predicate-symbol <.
Constant-symbols represent objects. Function-symbols accept input objects and return an object as an output. Predicate-symbols accept input objects and return a boolean as output.
Good. Now both of these versions of "definition" are good enough for you to use. The first is semi-formal and can be mechanically translated into the second formal one. The second one is what is really going on when you prove things. If in some context you want to prove "odd(E)", you can do so by proving "∃x∈ℕ ( E = 2·x+1 )" and then using the "⇔" to get "odd(E)". Do you get this?
I still haven't said anything about a deductive system, which is what will actually permit the proving, but I want you to understand the intuition for definitions first.
@PaxDaga No it's not because it's circular, I'll come back to that later to show you why you misused the definition. First I want you to try some simpler definitions. Define the predicate "f surjects onto T" (for functions f). I give you the function-symbol dom where "dom(f)" denotes the domain of f. Please use either of the two formats I gave above.
@user21820 This comment is really interesting. Could you please clarify the phrase "substituting a predicate in FOL by a name (which would be used as a predicate-symbol)" ?
@user21820 Do you think my version of PA−4 is correct ?
@Ishwaran: can you notice that the points $P, Q, S, T$ lie on a circle with $PQ$ as diameter?
And then apply the same principle to conclude that angles TSP and TQP are equal.
And then you should be able to complete the proof @Ishwaran
@user21820: Hello! I wanted to get more details on the idea of a function. You mentioned in CURED that using a set to describe a function is more of an encoding and that it is not really necessary. I may not be able to fully comprehend but will try.
Hence the points $S, T$ lie on circle together with $P, Q$ also lying on same circle. Moreover the angle subtended is right angle so $PQ$ is a diameter. But $PQ$ being diameter is not used in the current problem.
More generally your problem works fine if the angles $PSQ $ and $PTQ $ are equal (but not necessarily 90 degrees)
When we try to find dy/dx then we take delta fx/deltax and make it smaller and smaller. We get better rate. But that rate never stops at a fixed value. So we take limit and and we assign dy/dx a value which it can never have ie the limit of delta fx/deltax.
@Prithubiswas I don't remember clearly enough, but I thought the video we talked about was clear enough evidence that we didn't need to see prior history?
@F.Zer It is correct, but I would chain the inequalities as I did in my comment here:
If b > c, use lemma to get b ≥ c+1 and so a = b·2 ≥ (c+1)·2 > c·2+1 = a.
@PaxDaga Yourattempt doesn't make sense. How can you attempt to define "surjection" in terms of "surjection"?? Try again.
@PaxDaga I have no idea why you use the word "prescient". Check a dictionary. It doesn't matter whether you quantify over functions or just use the phrase "f is a function". The first option is impossible in pure ZFC but not in many-sorted FOL (which my deductive system is based on).
@PaxDaga Not only is your attempt completely failing to define "surjection", you also anyhow stuck a variable name into a predicate-symbol. That makes no sense whatsoever. I guess it's because you didn't even realize that "f surjects onto T" is a 2-input predicate. See? This is why you need to learn basic FOL first.
To avoid wasting more time, here is what the answer should look like:
@F.Zer You can ignore that phrase; it was just meant as a sloppy intuition. You already know the precise version: definitorial expansion.
@ParamanandSingh Yes it's not the 'real' meaning of "function". In a set theory like ZFC, we have no choice but to encode a function as a set because that is all we have access to (in the intended interpretation of the language where "∈" denotes set membership). But is that really what we conceive of as a function? No.
After all, in ZFC we have to encode ordered pairs before we can even encode a set of ordered pairs (to be able to encode functions), and one common encoding of ⟨x,y⟩ is {{x},{x,y}}. And of course that isn't the only possible encoding. It's also an ugly implementation detail that nobody wants to care about. This shows that people do not ever want to think about ordered pairs like that. Thus the same goes for functions ins ZFC.
*in ZFC
Another clear reason that functions in ZFC are mere encodings is that in pure FOL we already have function-symbols. That concept is what truly captures the intuition about functions, which is why we use that notation even for functions in set theory. Furthermore, there are things like powerset which cannot be functions in ZFC but certainly you think of it as a function (and it can be added to the language as a function-symbol).
