« first day (887 days earlier)      last day (1596 days later) » 

03:25
@Poptart Category theory isn't what I'd consider basic mathematics. I'd also say that it's not a good idea to bother with category theory until you actually feel a need for it in your work. Things don't magically become any nicer when viewed from a category theory perspective. As you noted, there are many distinct isomorphic vector subspaces of ℝ^n for n>1, and they remain distinct in the category of finite dimensional vector spaces over ℝ. Also, there are multiple isomorphisms between them.
 
5 hours later…
08:27
Hey @user21820, it's me! I read the expression "∀k∈ℤ ( ∃m∈Z ( k = m·2 ) ∨ ∃m∈ℤ ( k = m·2+1)". A few quick questions arise though:
1. Could we write such expression as "∀k∈ℤ ( ∃m∈Z ( k = m·2 v k = m·2+1)".
2. How do we make sure if one expression could be written as such or not?
Questions like these... I think these answer will be addressed while learning FOL.
Looking forward to hearing from you!
Sincerely,
H.Can
@user21820 If you notified me in your next message how and when to contact, where to follow etc. I'll be there at time
08:56
@H.Can Hello! Welcome again. You're right that questions like this are addressed as part of FOL!
Indeed, "∀k∈ℤ ( ∃m∈Z ( k = m·2 ) ∨ ∃m∈ℤ ( k = m·2+1)" is equivalent to "∀k∈ℤ ( ∃m∈Z ( k = m·2 v k = m·2+1) )", and you will be able to prove the equivalence in a deductive system for FOL, not just use intuition to see that they express the same thing.
Argh, I missed a close-bracket in my example. No wonder it was missing from yours too. =P
"∀k∈ℤ ( ∃m∈Z ( k = m·2 ) ∨ ∃m∈ℤ ( k = m·2+1) )"
I guess this should sort of answer both of your questions already. But please confirm for me that you know how to read those quantifications. In particular, do you know how the brackets indicate the scope of each quantifier? That is, "∀x∈S ( Q )" means "Q holds for every x in S" where "Q" is a statement that may involve "x".
We also often drop brackets for consecutive quantifiers, so "∀k∈ℤ ( ∃m∈Z ( k = m·2 v k = m·2+1) )" can be written as "∀k∈ℤ ∃m∈Z ( k = m·2 v k = m·2+1)".
Also note that in my example the two "∃m∈Z"s are separate because their scopes are separate. Namely, it's the same as saying "∀k∈ℤ ( ∃m∈Z ( k = m·2 ) ∨ ∃n∈ℤ ( k = n·2+1) )".
Whereas in the equivalent statement, the "∃m∈Z" covers the whole "k = m·2 v k = m·2+1". So it should be clear that it is not trivially equivalent, though intuitively you should be able to convince yourself that they are ultimately equivalent.
Ok so far? This much is about the standard interpretation of FOL, also called semantics.
09:33
And sorry I didn't notice some of my "ℤ" were not the same (typo error). If you noticed the discrepancy, they were all supposed to be the same.
10:15
@user21820 I moved intuitively to state that those two expressions are the same. I mean I saw I can use 'distribution' but I don't know the scope of brackets. What I have done basically is to use bracket after for every quantifier and something related to it. I kind of imitate the notation that I've seen in the formal definition of limit.
When I think much deeply how I decide where to put brackets and where not, I realized I got the intuitive from programming languages syntax. It seems perfectly fine to me to write the expression as
"∀k∈ℤ ∃m∈ℤ ( k = m·2 v k = m·2+1)" because ,based on my intuitions, " ∃m∈ℤ " is an expression that can not be splitted into any longer than its atoms(atoms : ∃, m, ∈, ℤ). It's like the simplest expression. However I'm aware of the fact that I couldn't have written it as
"∀k∈ℤ (∃m∈ℤ k = m·2 v k = m·2+1)"
10:35
@H.Can Programming-based intuition is very good for learning logic.
In particular, intuitively you can view a "∀x∈S ( Q )" claim as one where you are given an x∈S that you have no control over, other than knowing that it is in S, and then you have to justify that Q holds for that x.
And similarly you can view a "∃x∈S ( Q )" claim as one where you give some x∈S that you show is in S and also justify that Q holds for that x.
But I think we better go over the syntax, meaning what sentences are valid in FOL, since you said you just use intuition for that rather than really knowing how FOL sentences are constructed.
There are many variants of FOL, all of which are equally powerful, but some are easier to use in practical mathematical work than others. So the variant I will teach you is the variant I prefer to use. I assume you know the basic boolean operations ¬,∧,∨,⇒,⇔, for not,and,or,implies,iff. If I make inaccurate assumptions about what you know, please let me know.
Note that we have precedence rules (just as in programming), to allow us to write less brackets but still have unambiguous parsing. Conventionally the precedence order for boolean operations from highest to lowest is ¬,∧,∨,{⇒,⇔}, where for the last two we do not have a precedence order so we must use brackets as usual. For consecutive operations with the same order, we use brackets unless the order does not matter, so we may write "A ∧ B ∧ C" but use brackets for things like "A ⇒ ( B ⇒ C )".
(There are some conventions that evaluate consecutive "⇒"s from right to left, but I will not use that convention as I feel it is unnecessary and often confusing.)
For PL (propositional logic), we just have the boolean operations and start with atomic sentences A,B,... and can form compound sentences from other sentences using boolean operations. I'm sure you know this from programming. For FOL, we do not have atomic sentences. Instead, we need to construct sentences from more primitive notions. At the base we have variables, function-symbols, predicate-symbols, and equality.
Take a look at the axiomatization of PA (section "Peano Arithmetic") given in this post:
20
A: Predicate logic: How do you self-check the logical structure of your own arguments?

user21820Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preser...

This post is also a more or less complete reference for the full deductive system for FOL that you should learn, and we will get to all of it eventually. For now just take a look at the list of axioms of PA and ignore everything else in that post.
There are 3 parts to PA. The first part is the logic itself, namely FOL.
The second part is its signature; we have the type ℕ and the symbols 0,1,+,·,<. Having the type ℕ means we can use quantifiers over ℕ. Each symbol has its own signature. 0,1 are constant-symbols of type ℕ, meaning that they are to be interpreted as elements of ℕ. +,· are binary function-symbols on ℕ, meaning that they are to be interpreted as functions from ℕ^2 to ℕ. < is a binary predicate-symbol on ℕ, meaning that it is to be interpreted as a function from ℕ^2 to Bool.
The third part is its axioms, which are given in the list in that post. Let's look at the 3rd-last axiom there:
> ∀x,y∈ℕ ( x<y ⇒ ∃z∈ℕ ( x+z=y ) ).
As stated elsewhere in the post (no need to look now), "∀x,y∈ℕ" is short-hand for "∀x∈ℕ ∀y∈ℕ".
An axiom is assumed to be true within the formal system. PA is an axiomatization for natural numbers, meaning that we hope that each axiom about ℕ is actually true if we interpret not only the symbol "ℕ" as what we would like to think of as naturals but also interpret 0,1,+,·,< as the standard arithmetic and comparison operations on our naturals.
Does this axiom that I highlighted here sound true to you under this (standard) interpretation? Under this interpretation, it would say "given any naturals x,y, if x<y then there is some natural z such that x+z=y".
This axiom also serves as an example for how the signature of PA tells us how we can construct sentences over PA. Since "+" is to be interpreted as a binary function-symbol on ℕ, we can only use it on inputs that are to be interpreted as elements of ℕ. In particular the inner expression "x+z" is a valid expression of type ℕ, because in that context (i.e. under both "∀x,y∈ℕ" and "∃z∈ℕ") x,z are both variables of type ℕ.
"=" can be used to construct a boolean statement that two expressions are equal, which is why "x+z=y" is a valid expression of type Bool, which in turn makes "∃z∈ℕ ( x+z=y )" a valid expression of type Bool.
"<" is to be interpreted as a binary predicate-symbol on ℕ. So the expression "x<y" in this axiom is a valid expression of type Bool, because in its context (i.e. under "∀x,y∈ℕ") x,y are both variables of type ℕ.
Since both "x<y" and "∃z∈ℕ ( x+z=y )" are valid expressions of type Bool in the same context (i.e. under "∀x,y∈ℕ"), the implication "x<y ⇒ ∃z∈ℕ ( x+z=y )" is also a valid expression of type Bool.
Do you get the picture of how valid FOL sentences are constructed now?
12:03
Oops I forgot to say something about the "induction axioms" which I mentioned after that list. The list only gives the axioms for a subsystem of PA called PA−. PA's axioms are not only those, but also the induction axioms. But it's not relevant for now. You need to make sure you know the deductive system for PL first, and then for FOL, and then we will get back to PA later, before going on to full Set Theory.
So let me know if you have any questions about what I said above, and then you should start learning the deductive rules for PL, which is covered by the first few sections of that post up to "Boolean operations". The best way to learn is by doing (just like with programming). So just start trying these exercises. =)
Each exercise is a theorem. For the PL exercises you will only need the rules up to "Boolean operations". Feel free to use ASCII text or symbols as you like.
A theorem is a sentence that you manage to deduce in the outermost context (i.e. not under any subcontext).
The goal of a deductive system is that if you start with only axioms that are true (under your desired interpretation), then you can only deduce statements that are each true in its context. We call such a system sound or truth-preserving. The deductive system in my above post is sound.
I want to emphasize what "true in its context" means. For example consider the following proof:
If A:
	A.
	If ¬A:
		¬A.
		A.
		⊥.
	¬¬A.
A ⇒ ¬¬A.
Line 2 has "A" which is true in its context, because its context is "If A:". Namely, in the context where "A" is true, of course "A" is true.
Line 4 has "¬A", which is also true in its context, because its context is "If A: If ¬A:". That is, its context is one where both "A" and "¬A" are true. Note that the rule ⇒sub is the rule allowing the first 4 lines, and this rule is just a syntactic rule; it does not care about meaning; it simply says, whenever you like you can create a new subcontext "If C:" and write "C." inside, for any C. But you can see that this rule is sound!
Line 5 is given by the ⇒restate rule, which is also clearly sound, because if something is true just outside a subcontext then it is also true within that subcontext, because a subcontext is literally a sub-context (a smaller context contained within the outer one).
Line 6 is given by the ¬elim rule. "⊥" stands for a sentence that is always false. In textual form you would write "false" or "contradiction" in place of "⊥".
Now what is happening here? I claimed that my system is sound, but what is this always false sentence doing in the middle of this proof then? Well, it is correct because it turns out that the innermost context (i.e. where both "A" and "¬A" are true) is simply impossible. Since that context (situation) cannot happen, it is actually the case that "⊥" is true in that context.
Put in different words, the proof claims that whenever you ever enter a situation in which both "A" and "¬A" are true, you can assert the truth of even false sentences, and you would still only assert statements that are true in their context. Why? Because you can never enter such an impossible situation to begin with.
And the formal system 'knows' that.
Line 7 is given by the ¬intro rule. Why is this rule sound? Well, if by some means you could deduce "⊥" in a subcontext where "C" is true, then clearly that subcontext is impossible, so "C" must be false in its context! Thus we can safely deduce "¬C". Here we used it with "C" = "¬A". Note that this ¬intro rule always adds a "¬", and we can get rid of double "¬" via the ¬¬elim rule if we need to. Here we do not need to.
Line 8 is given by the ⇒intro rule. I leave you to convince yourself that this rule and all other rules I did not talk about are sound. =) Note that the meaning of "⇒" is given by the truth-table, so you can check all cases to see whether the ⇒rule is sound or not.
Finally, observe that in this proof the only statement that we deduced in the outermost context is "A ⇒ ¬¬A". Thus this proof justifies a single theorem "A ⇒ ¬¬A". All the other statements that are under some subcontext are not theorems. After all, they are only true in their contexts, so they may not be true in every context.
@H.Can: Okay I'm done with the introduction. Now it's your turn! Feel free to ask about any point, and at the same time start trying to write a formal proof of each of the PL exercises. They are roughly in order of difficulty, so do them in order. Post your attempts here and I will check them.
 
2 hours later…
14:24
hi @user21820
Is this group appropriate for a 2nd order Differential Equation question?
15:21
@Archer Yes, but if I and whoever else frequents this room cannot solve it then you may need to ask elsewhere.
@user21820 Man I am having serious trouble solving this equation by Frobenius method:
$xy'' + 2y' + xy = 0$
I have got the indices to be y = -1 and y = 0
Now the biggest problem is that the difference is an integer.
@user21820 Do you have any idea?
Sorry, I am not familiar with Frobenius' method. But does the wikipedia article help?
15:50
@user21820 No I am afraid but thanks for your time!
I think if you post a question on Main and say why the wikipedia section doesn't apply, you'd almost surely get an answer within a few days. It's just not my area haha.. =)
 
2 hours later…
17:33
@user21820 It's been for more than three hours to understand what's going on in your messages:) I dived into the boolean operations provided by you and its syntax, writing etc. I'm pretty sure I have dozen of things that I didnt understand but I need to write them properly so that I can transfer them to you. I'll post my questions tomorrow before work. Thanks for the infos, it's a different area that I've never touched thus far!
@H.Can Sure! Take your time! I realize I didn't answer your question about when I am available in chat. I myself cannot be sure when I am free, however I will definitely respond to whatever you ask here. =)
Right now, I have to go off, so I'll respond the next time I'm back.

« first day (887 days earlier)      last day (1596 days later) »