« first day (1297 days earlier)      last day (1186 days later) » 

07:53
@user21820 In the text editor I am using , Is there a way to replace a letter in a line with something else , like:
a0a0a0a0a0a0a0a0a0a0a0cccc
b0b0b0b0b0b0b0b0b0b0b0cccc [replacing "a" with "b"]
 
3 hours later…
11:15
If your text editor supports Regular Expressions, you could simply enter "a" in the search field and "b" in the replace field.
@MaxH Not "unused objects". A variable is a reference, not an object. You can do ∀sub with an unused variable because it is an unused reference.
@user21820 What exactly do you mean by reference? Can I imagine it like a symbol that has not yet been given any meaning? Only after when I write something like x=1, the symbol x would have a meaning in this context.
@MaxH Yes.
That makes more sense, thanks.
If someone writes "Assume that V is a vector space, then P(V)", what is V exactly? Is it an object for which it is assumed that it satisfies the vectro space axioms, or is it a variable for which the vector space axioms are true? I would tend to say it is the former, but then I am unsure as to why I can plug in vector spaces and conclude P(V).
 
4 hours later…
15:49
@user21820 You say that a variable is not an object. If I want to prove a universally quantified statement, it is ususally done by starting with "Assume x \in X." Does this mean that here we do assume that x denotes an object in X, meaning, x is actually an object here?
 
1 hour later…
16:59
@MaxH Yes, but I don't like the word "assume", though it is not as bad as "let".
2 days ago, by user21820
Take any rational r such that r^2 = 2. Then r = 3.
It is better to understand what you are doing in terms of the Fitch-style system I gave you, and ask relative to that, otherwise it will never be clear to me whether you fully understand or not. Under the ∀subcontext "Given x∈S:", the variable x refers to an object of type S. That same variable has no meaning outside of that subcontext.
I tried reading your post regarding it, but I didn't understand a lot, which is why I didn't refer to it.
If you don't understand a lot, it means you don't understand a lot of basic FOL, so you should ask to clarify to the point that you understand.
I think it is rather the notation that is unfamiliar to me.
I don't think so. Everyone who truly understands FOL can easily understand that post. If you don't understand something, ask. Avoiding it doesn't help.
Well, I am not familiar with the I dont know how to call it, perhaps table notation? I think I could derive what it means out of context, but was not sure. I will reread it and then ask!
17:23
@user21820 Hello! I have a question about a pi=4 post in MSE.
@Prithubiswas Just ask?
Well , I seem to not understand the answers (23 of them) at all. Probably because they are way too advanced for a high-school student like me.
Usually when there is such a "paradox" , I look at the notation , the axioms of the theory , the logical deduction , and check where a wrong step has been taken.
But for Geometry , I am not familiar with any rigorous axiomization of geometry , so I can't verify if something in geometry is true or false and if it is false ,why?
That is the dilemma =)
17:47
@user21820 So , was there a correct answer among the 23 answers in that post that I should "trust" and put more time into understanding it , or I should take a different route?
@Prithubiswas You are right. I came across that post many years ago and upvoted only one of the answers...
That one is by Pete L. Clark, but is unfortunately beyond your level now, so basically you probably should ignore that whole thread. The answer is simply that the arc-length cannot be defined by using just axis-parallel polygonal approximations.
Just look at the slanted side of a right-angled triangle.
18:19
@Prithubiswas: Even Wikipedia and Mathworld don't give the general definition; they only give a valid definition for smooth curves. The full definition is:
> The arc-length of a curve f : [0,1]→ℝ^n is sup( { Sum{ dist(f(x(i)),f(x(i−1))) : i∈[1..k] } : k∈ℕ ∧ x∈[1..k]→[0,1] ∧ ∀i∈[1..k] ( x(i−1)≤x(i) ) } ), where supremum is ∞ if there is no upper bound on the set.
Informally, divide f into arbitrary pieces and replace each piece by a line segment between its endpoints. Arc-length is the supremum of all possible total segment lengths under such division.
@Prithubiswas: I retract my statement about Pete's answer, since I just re-read it and saw that it claims "arclength elements are computed using derivatives", which is false since I have just defined it without any derivatives!
(I must have read it so many years ago that I didn't know better.)
@user21820 I will pretend as if I didn't know anything about it before and (re)learn it. The first question is in the "Context" section. You write "and reasoning about an arbitrary member of a collection S would look like: Given x \in S". What is S? Is S assumed to be any set? Meaning, it would be similar to the V vector space example I gave above? How does this work? Is S a variable or something else, formally?
I assume that x is a variable, right? Meaning that I assume that x denotes an object of S here. Again, how does this work? A variable is just a symbol at first, or reference, as you call it and not an object. When writing "Given x \in S" I now assume that the symbol x refers to some object in S, right?
18:46
Under "natural deduction rules" you then write this table the first time. Unfortunately I dont know what it means at all, could you explain? I also don't know what "match "X"" means. What is written below the lines means something like "Y is true", where, in this case, Y is written below the line?
I guess I really don't understand the notation. I'm sorry if those questions are trivial...
19:15
@MaxH I stated before that "take any type S".
It is not (and cannot in general be) a set.
There is no set theory in the basic FOL rules. You're just given types to quantify over. This is known as many-sorted FOL.
Ok, I see, my bad.
This then gives a similar question though. S is any type, is set a variable or something else? This should be sort of analogous to the question where I thought S means a set.
As far as I can see, this adapted question could be asked then.
No. I have to ask you, do you even know how to use the PL part?
If not, it is pointless to try the FOL part.
Which part do you mean, exactly?
I gave you a list of exercises. Just do them in order. Learning to use an FOL deductive system is like programming, but simpler. If you do not write any programs, you will not learn anything. Similarly, if you do not write any formal proofs, you will learn nothing. Right now, you need to make sure you can handle PL before moving on to FOL.
I mean, I had two lectures on logic in my entire life, teaching quantifiers and truth tables, as well as implications and connectives, thats it. Im not sure if I can solve the exercises the way you want me to.
19:23
It's just a matter of trying.
Example proof:
If A∧(B∨C):
	A∧(B∨C).  [⇒sub]
	A.  [∧elim]
	B∨C.  [∧elim]
	If B:
		B  [⇒sub]
		A∧B.  [∧intro]
		A∧B∨A∧C.  [∨intro]
	B ⇒ A∧B∨A∧C.  [⇒intro]
	If C:
		C  [⇒sub]
		A∧C.  [∧intro]
		A∧B∨A∧C.  [∨intro]
	C ⇒ A∧B∨A∧C.  [⇒intro]
	B∨C.  [restate]
	B ⇒ A∧B∨A∧C.  [restate]
	C ⇒ A∧B∨A∧C.  [restate]
	A∧B∨A∧C.  [∨elim]
A∧(B∨C) ⇒ A∧B∨A∧C.  [⇒intro]
I omitted many of the lines obtained using the restate rules, except for the last 3 to show you how the ∨elim rule is applied.
In your solution, you can omit all restate-lines as well as all ⇒sub lines.
Yes, I have never written or seen anything like that in classes. I technically don't even know what the remarks after each step in the brackets mean.
It is the rule name!
Also, I asked things about variables, are those exercises really necessary to answer the questions?
Go through every single line to check that it is allowed by one of the rules.
@MaxH Your question is a bit like asking whether the English alphabet is necessary to learn vocabulary.
Is it really? I think many people have and will never visit a logic course that have a degree in maths and know how variables work, or am I wrong?
Ok but I think im starting to see how this notation works from your example.
At least I hope so
19:34
@MaxH You are, unfortunately, wrong. I observed that only 1% of math graduates actually understand basic FOL fully. Another ≈ 5% unconsciously get it but not clearly. The rest do not know it well enough. Anyway, all 7 PL exercises can be done in a few minutes each by anyone who understands PL. Since you have a mathematics major background, it should take you only 30 min at most to figure out most of what the rules mean given the example I gave you.
Well I would count myself to those that know how to work with them but dont know why they work.
Which is essentially why I am here.
I think it is necessary to know
Ok, I will try to do the exercises when I find the time and then give you my solutions. However, keep in mind that this would be the first time I use any of this starting from the notation. Is there a good way I can write it the way you did in your example proof? More precisely, is there a good way to do the important symbols?
I feel like copying them might be a bit of unnecessary work, if there is another way
Nov 22 at 15:19, by user21820
@MaxH Either copy-paste the symbols or use an AHK script or just write "forall" / "exists".
I don't mind you using "not", "and", "or", "implies", "iff".
I used to do that many years back in these chat-rooms before I switched to unicode.
Alright.
Since this chat-box doesn't easily let you type multiple lines, you would have to write your proof in a text editor and then copy-paste then click "fixed font" (to preserve indentation) before "send".
Thanks for the advice.
19:39
All the exercises are roughly increasing in difficulty. The first few are easier than the example I gave you above, and the last few are harder.
I need to go. Just post whatever attempts you have here, and label them with the exercise label, and I'll check next time.
@MaxH: One more thing. I don't need you to label each line with the rule. But if you think it helps you learn, by all means go ahead for the first few attempts.
Alright, thanks!

« first day (1297 days earlier)      last day (1186 days later) »