Basic Mathematics - 2021-12-03

« first day (1305 days earlier) ← previous day next day → last day (894 days later) »

6:01 AM

@MaxH Well in case it wasn't clear, you first have to read through the example proof given in that post itself, and check every single line against the rules and see if you understand the rules via that example. Just like you did earlier for the PL example I gave you here in chat.

If there is any point in that example proof where you do not understand how the rule was applied, or want to know whether you could do something else instead, ask specifically about that point.

Your comments here also suggest to me that maybe you don't yet quite get the picture of formal systems. Every formal system generates proofs as well as theorems via rules telling you what you can write, just like the rules of chess generates valid chess games. A formal system is interesting iff it generates theorems that are somehow meaningful, and also generates proofs for those theorems that also have meaning.

So to understand a formal system, you must experiment with it and try to generate as many proofs and theorems as you can, and see whether the whole lot seems to make any sense. There are two aspects:

(1) You want to be able to assign meaning to every part of a proof that it generates, so if the system is supposed to generate FOL theorems then it had better not generate both A and ¬A where A is some boolean statement!
(2) You want to be able to do all logical reasoning, so you want to see how every kind of logical reasoning can be done in the system.

In both cases, you need to experiment as much as possible, both to see what you cannot do and to see what you can do.

8 hours later…

2:27 PM

Well I do have questions regarding the section "Quantifiers and equality", which also refers to variables, which is what I was asking about initially, if you remember. @user21820

@MaxH I know and expect questions. What I'm saying is that it is pointless if you haven't gone through the example given after that section. The example is like a photograph, and the rules are merely the caption. If you do not look at the photograph, the caption cannot help you see the full picture.

Ok I see, then I might have misunderstood you.

I will do that first.

Good. And by reading that example it includes looking at the final theorem (last line in the proof that is in the global context) and thinking for yourself whether it is true or not, and why, and while following the line-by-line proof against the rules seeing whether your thinking is captured by the proof or not.

Ok, so I did read it and think I understood it. I feel like applying the rules should not be that much of a problem, rather understanding why it is plausible that they should hold.

Also, if I am not getting something wrong, the statement should be true, since if there exists some x such that for every y P(x,y) is true, then it should certainly be the case, that for every y I can find an x such that P(x,y) is true ("I can just pick the existing object from the assumption, giving me the same object for every y, but it satisfies what I want")

I fear I worded that poorly, if you are not sure if I understood it, or my reasoning is not clear enough, let me know and I will reword it.

@MaxH That's correct, and I presume you saw how that "same object" was passed around in the example proof.

2:40 PM

Yes.

So now look at the rules one by one and check their soundness. Recall that the ⇒subcontext simply meant that under "If A:" we are in a subcontext of the parent context where additionally A is true. And then we looked at the PL rules and checked that each rule is sound.

the ∀subcontext means that under "Given x∈S:" we are in a subcontext of the parent context where additionally you have a variable x that refers to some object of type S.

Ok so the first questions might be very basic? I think it might be beneficial to confront this by trying to forget what I know and relearn it (the right way). Hence I might ask rather more than less, if that is fine with you, as well as potentially obvious stuff.

Just to make sure I get it, if that makes sense.

Of course, ask more than less. But also, experiment more. The best students I've had are those who try their best to break my system and prove some nonsense. =)

And the ∀sub rule explicitly says that x must be an unused variable (in the parent context). This is because if in the parent context x already refers to some object, then we of course don't want to use x again. We only want to use x in a ∀subcontext if it isn't already fixed to refer to something.

So we are in the section Variables and quantifiers, so the obvious question would be, what exactly are variables? Do I also have other "stuff"? It appears I have "constants" meaning constant symbols denoting some fixed but unknown objects such as in the vector space example, as well as having variables.

@MaxH Variables are most commonly considered as separate from constant-symbols. For now, also assume you have an infinite supply of variables, each of which is a finite string of characters.

2:49 PM

Ok but the idea is correct that I have some sort of constant symbols, that denote some fixed but unknown object? The unknown/abritrary aspect gives some sort of variable feeling to it, where the difference might just be a technical one - i dont know that.

But I assume that in the vector space example, V is exactly used as such a constant symbol, right?

@MaxH Some logicians don't bother to distinguish them, and you're correct that to some extent a constant-symbol is just a variable that is supposed to have a fixed value in the global context.

@MaxH No. Really, do not talk about vector spaces yet as you are not ready for it...

What is an example of a constant symobl then? I guess a real life example mgiht be something like A, which refers to a specific person? Or the symbol 1, refering to the number one?

@MaxH That's right. If you peek at the section "Peano Axioms", you see that there are two constant-symbols 0,1, which are supposed to refer to our ideal zero and one.

Alright. Is this also how the properties and statements are represented? Meaning, we used A and B (...) for statements as well as P for a property. Is this a similar setting, where those are constant symbols refering to some fixed but unknown statement?

That would then be the justification as to why we can use that, assuming that the language contains them.

@MaxH Good question! Just in case you are not familiar with predicate/function-symbols, I'll briefly describe them first.

This isn't in my post because it was meant for people who already know FOL syntax and semantics. But I think I'll say it again to make sure you know.

A predicate-symbol P has a fixed number of inputs and a single boolean output, so if P is a 3-input predicate-symbol then "P(t,u,v)" is a boolean statement whenever t,u,v are object expressions.

A function-symbol f has a fixed number of inputs and a single object output, so if f is a 2-input function-symbol then "f(t,u)" is an object expression whenever t,u are object expressions.

Observe that a 0-input predicate-symbol takes no inputs and so its boolean output is constant. So 0-input predicate-symbols can stand for propositional atoms!

Similarly, a 0-input function-symbol takes no inputs and so its output is constant. So 0-input function-symbols can stand for constant-symbols!

However, it is a common tradition to separate function-symbols from constant-symbols.

And in applications of FOL we rarely deal with 0-input predicate-symbols, even though we can.

@MaxH So, yes, just as propositional atoms in PL stand for fixed but unknown boolean statements, constant-symbols in FOL stand for fixed but unknown objects (in the global context).

3:05 PM

By the way, why exactly can we not yet discuss the vector space example? There would also be analogous statements about natural numbers that would lead to the same question.

Ok and why can we use those symbols? Are they just assumed to be part of the language, as some sort of axioms? It is obviously plausible that we should be able to use them, I just wondered on a technical level.

@MaxH Because when you are talking about a vector space, you are actually talking about a mathematical structure that satisfies a certain axiomatization. We haven't even done mathematics within the foundational system (which has an axiomatization), so you're not ready to talk about an axiomatization within an axiomatized system...

Ok, but the point of the question or rather the problem that lead to the question is rather independent of the type of object and its axiomatization.

Thats why I wondered.

Since you insist, I'll give you a short summary, but I will not elaborate. (I merely hope that it will justify my claim that it is beyond your current level, so please learn the basics first otherwise it's really quite pointless to discuss further.) There are two ways to talk about the vector space axiomatization, but neither of them has "V" as a constant-symbol! They are:

(1) Work within the axiomatization, meaning that you only prove statements that are true for some unknown fixed vector space with fixed underlying set V and fixed field F and fixed operations and fixed zero vector. Here, V,F are types in my system, also known as sorts in many-sorted FOL. They are not sets, nor are they constant-symbols. The operations are function-symbols, and the zero vector is a constant-symbol.

(2) Work within the foundational system MS (which is what I was referring to earlier because that is really what mathematics about vector spaces is), meaning that you define a vector space as a single object ⟨V,F,0,+,·⟩ that obeys (as expressed in MS) the vector space axioms. I will not go into any detail about how to express "obeys" here, as that is properly meta-logic and not basic logic.

(2...) I will say that ZFC does not permit you to construct a set of all vector spaces. My system (like NBG set theory) does allow you to construct a type VectorSpaces of all vector spaces, and write (completely rigorously) boolean statements of the form "∀X∈VectorSpaces ( ... )", but again, I will not say more at this point...

3:21 PM

Ok. You don't have to comment further on it. I just wanted to know as to what exactly V is in statements such as "Let V be a vector space" which should be analogous to statements such as "Let n be a natural number". Furthermore this is exactly the first line after a "For all" statement, but one rarely says that one is now proving a for all statement lecture notes or similar when one begins a chapter with "Let V be a vector space" or "Let n be a natural number".

I just wondered about what that exactly means.

But again, if that is too advanced, you dont need to comment.

@MaxH It's completely different. "∀k∈ℕ" is something you can do and grasp once you reach "Peano Axioms". "∀X∈VectorSpaces ( ... )" is something way more complicated.

That's why, don't assume that it's "independent of the type of object".

Ah yes I don't know how I didn't see why they are different.

At least good that it's now cleared up.

I see now I think. Is the problem (or at least one of the problems) that N is a set wheras VectorSpaces is not?

Again, if any of these followups lead to something too advanced, just let me know and I wont ask again.

@MaxH That's one of the issues, yes, but it's not the one driving the complexity. ℕ can be given as a type rather than a set. If you work completely within PA (Peano Axioms), it suffices to use ℕ as merely a type (as stated in my post). Only when you move up to ST (set theory) do you need ℕ as a set. The problem is that "obeys the vector space axioms" is very complicated to express and reason about formally, in contrast to "is a member of ℕ".

3:32 PM

But then again why isn't this weird in another way? I can always create if statements, meaning I can always write If A: (...). This would then allow me to write If V is a vector space (and then conclude stuff from it). Hence, I should be able to construct statements such as implications involving vector spaces such as "V vector space implies P(V)". The conflict shouldn't appear here, since I dont have a for all statement. Am I overseeing something?

@MaxH "V is a vector space" is not a boolean statement. It's a semi-English phrase that is illegal in the system.

That's the whole point. You continue to fail to see that you are actually never expressing "is a vector space" in any meaningful way that allows you to actually reason about vectors and scalars in vector spaces.

Ok, so essentially this is then a problem regarding the language? More precisely, I cant create this statement with the formal language?

It's meaningless even without formal language. Your problem is that currently you don't have enough of the basics to see that it is meaningless.

I mean, its really weird, since stuff like this is used everyday without second thought...

@user21820 Ok.

It's not that the proofs in your textbook are meaningless. It's that you're not seeing the true inescapable complexities that are obscured and rarely made clear to students.

3:37 PM

But then, is it the case that there is a way to give sense to such statements?

Or are the proofs in Books just written, i dont know, in "another language" that has then to be translated?

Because then one has to be sure that such a translation to a formal language exists.

@MaxH I already answered that in (2) above.

@user21820 Yes, I see.

And it's really the only way if one claims to use ZFC.

There are many mathematicians who don't actually know enough logic, much less ZFC, and yet claim to use ZFC. They're wrong.

That doesn't mean their mathematics is wrong.

It just means that they made a wrong claim about foundations.

Ok so this seems like quite a lot, since what one "took for granted" appears to not be that trivial at all.

If that makes sense.

It's unfortunately the case with set theory. After naive set theory was demolished, the winner of the alternatives race, namely ZFC, turned out to be a bit weird.

3:41 PM

Ok so I will not bother with the vector space example anymore. But if you are fine with it, it might be interesting to discuss the natural number example, or rather it might be beneficial to me.

@MaxH Please do explain what you meant to ask about quantifying over ℕ.

I just meant, what exactly "n" is here. If I read "Let n in N", then this should mean "Let n be any object in N", right? Firstly, what one is unexplicitly doing here is writing down the first line of a for all statement, right?

Because thats a common sentence that one reads in "comment" sections of textbooks/remark sections/non-proof environments.

If one is strict one would have to always write a theorem and then a proof, right?

@MaxH Hmm, didn't I show you my objection to "let" before:

9

A: Let P be a polygon

Many logicians that I have spoken to have concurred with my assessment that this is an issue of the misleading use of "let". Many teachers use this word in two very different and incompatible ways. The first is universal quantification, as in your example. The second is existential instantiation,...

Yes, I just adapted textbook notation.

So yes, you have to read most instances of "let n in ℕ" as "Take/Given any n∈ℕ.".

3:49 PM

Yes.

And people don't write in Fitch-style, but clearly it is a ∀sub in Fitch-style. That's why you have to understand Fitch-style first before all this implicit quantification and scoping in paragraph proofs become clear.

What is "n" here? So the underlying statement would be something like "For all n: P(n)". Hence, in this statement, n is a variable.

If you're learning programming, you see that every modern programming language has clear scoping and indentation. Only mathematicians are still 'backwards'.

Strictly speaking, I need to use a fresh variable in the proof, right?

But I see that this is not commonly done, not by myself either.

It is almost always that the first line is "Given n in N".

There is a workaround by simple using another variable, which is why it is not problematic I assume

But I wanted to ask to make sure.

I don't know what you're talking about now. You didn't point me to any example proof, and you appear to not have understood the Example in my post (since it does not use a fresh variable in the ∀sub rule usage). Go back and check carefully every single line.

3:54 PM

Ah, I confused something here. I am sorry.

I did check every line carefully, I just did a mistake here.

Let me think through my question to see if this part is solved then.

Ok, I'm glad to hear that it's just a mistake.

Ok, so this part is just solved then, since it was not even a reasonable question.

Still I have another "subquestion" if thats what one wants to call it.

So in the theorem statement, "n" is a quantified variable.

The forall sub rule says that I can always write "given x in S". What is x here now? It now denotes an object of S, which is why I can write "x in S" as a true statemetn, right?

@MaxH Under that ∀subcontext, yes you can write "x∈S". That feature of the ∀sub rule is precisely what captures the meaning of that subcontext. Literally, that rule allows you to assert that x is a member of S inside that subcontext and does not tell you that you can assert anything else about x.

The only other rule that lets you 'pull in stuff' from the parent context is the ∀restate rule, which you can see captures the meaning of that subcontext being a subcontext (everything that holds outside holds inside too).

Ok, so the natural question would be "Why do I prove a forall statement by starting with "given x in S?" My answer to that would be: x is a variable, hence not used as an object in S. Thus the claim "given x in S" is only true, if I explicitly define an object of S to be given the name x. If this is done, then it is obvious that x now denotes an object of S.

Since I can give any object "explicit" object of S the name x, this premise can be done for any object in S, which is why it makes sense that this is the start of a forall proof.

Would that explanation be correct or is it false?

4:17 PM

I cannot understand your first paragraph, but your second paragraph seems okay. Nevertheless, that's not the way you're supposed to view the ∀subcontext.

Maybe read this about game semantics:

14

A: Is formal truth in mathematical logic a generalization of everyday, intuitive truth?

Your main issue here seems to be that you are wondering how all the following statements: If the Earth is flat, then the Earth exists. If the Earth is flat, then the Earth does not exist. If there is life on Europa, then the Earth exists. could possibly be meaningfully assigned the same truth v...

Do you want me to explain the first paragraph in other words?

No need, because I think I know what you're saying from the second.

Your explanation is that you first think of the variable "x" as 'unspecified', and then later you observe that you can specify it and it doesn't affect what you concluded inside the subcontext.

But why delay the specification at all? Read the linked post. Claiming a ∀x∈S-statement literally means that you challenge the opponent to give you any member x of S and the quantified statement is true for that x. So when you make a ∀subcontext, in my opinion you should view it as literally accepting a member x of S given by the challenger who will try his/her best to make you fail.

I would like to explain it I think, if that is fine with you. Since I think my explanation/view is a bit weird.

That's why I used the word "given", and why some other logicians use "take". Because it's like a given input, and our proof works regardless of the input.

I mean, despite the example being intuitive, I usually avoid such examples. Im not sure how to word the reason correctly, though.

Perhaps because I fear that such examples might not be the "real" reason why this rule is the way it is and rather explains it differently.

The way I viewed it was the following. When writing "Given x in S" it means something such as "Assume x in S". Thus, in order for the derived statements to be true, I need that the assumption "x in S" to be true (sort of like in the case of if statements).

Now when is x in S true? Consider the n in N example. If I write down elements of N, i never encounter the element "n", because "n" is a variable not used in N. Thus "n in N" is only true, if I assign one of the objects of N the name "n", which I can do for any object. Hence this assumption is true only if I assign it to some object in N, which is why I can conclude n in N.

Maybe you see now why I feel like this view is weird? Maybe it is even incorrect, which is what I don't hope, but thats the reason I wanted to explain it further.

If anything is still unclear, please ask for clarification, as I think this is really important and also insightful.

4:33 PM

@MaxH Ah, it's incorrect. A reference is not an object. You're making the same mistake you made earlier with 1,2,3,a,b,c that I thought you had rectified. Apparently not.

"1" is a string with 1 character. It is not 1. However, "1" refers to 1.

"1+2" is a string with 3 characters that refers to 3. "2+1" also refers to 3. But "1+2" and "2+1" and 3 are all different.

Under the ∀subcontext "Given x∈S:", the variable "x" is a string with 1 character and is not an object. But we are supposed to interpret it as referring to some unknown object that is a member of the type that "S" refers to, when working inside that subcontext.

You do not assign names to objects. Rather, you may have references each of which points to an object.

3 does not have the name "1+2". But "1+2" refers to 3.

So the problem you are having with my explanation is in: "If I write down elements of N, i never encounter the element "n", because "n" is a variable not used in N." right?

@Hermis14: Hello again! Did you have a question?

@MaxH Yes.

Is the rest of the interpretation ok?

Explanation rather.

Because if so, it might just be the case that I worded it incorrectly, I need to think about that.

Long time no see! I visited to say thank you again. I was able to finish writing my own better-looking technical papers with help of you though you may not remember how you helped me because it was long ago. After some struggle with math, I realized that your recommendation of a reference book and comments have become the precious milestones of my scholarly activity.

As a usual control system engineer, I had been familiar with only elementary math minimally required to understand how the theorems can be applied to make a controller from them. But, now, I can make new useful theorems by myself. That's a giant step for me. As the submitted papers are in peer-review, I would like to introduce them to you if they are accepted. Even if they fail, it is definitely not the end of my research :) Take care of yourself!

What I meant to say is that "n" does not point to any object in N yet, because n is a variable and I didnt assign it any reference yet.

If that makes the explanation correct, then I think it is fine. But also, I am willing to learn any explanation of the rule, really. It is just what I thought.

4:52 PM

@Hermis14 Sure! You can always link to your published or arXiv versions whenever you are ready to share them. And yes, especially during this time, take care too! =)

@MaxH Ah, okay then it's what I originally thought. For which I said it is sort of okay. It is simply not the way I view it. I would prefer to view it as already given by an adversary. There is a slight issue with your view in that how does it make sense to say "x∈S" inside the subcontext if x doesn't even refer to an object yet?

In my view, it does, so there's completely nothing wrong with that statement.

Have you read the game semantics post?

Ok, i just thought it is weird that I have this relationship between given and "if statements".

@user21820 Not yet, but if it is the example you described above then I probably already heard about it. Will read it though.

@MaxH Nothing weird about that. Some variants of FOL allow formal systems for them to treat them the same, but things get really messy when it comes to the ∀ rules!

And it forces the intended universe to be non-empty.

For one you have to have floating variables even in the global context. So outside you can already say "x = x.".

In my system, you cannot do that.

Discussion of alternative systems is always interesting, but for now it's probably best for you to restrain a bit, since it's easy to get confused if you don't stick to one system (you forget whether something is or is not allowed in which system).

5:09 PM

Alright, thank you! I justn thought that by drawing this line, I might be doing something that is not meant to be done and potentially false.

I want to learn it correctly, else I could just work with it the way I did before. :P

Hence I prefer asking.

Sure.

« first day (1305 days earlier) ← previous day next day → last day (894 days later) »

Transcript for

Dec '213

♦ $Mathematics$ Basic Mathematics

This room is meant for all basic mathematical discussion, incl...

join this room
about this room

00:00

06:00

12:00

18:00

all times are UTC

$Mathematics$

site design / logo © 2024 Stack Exchange Inc; legal

mobile