« first day (1232 days earlier)      last day (952 days later) » 

12:11 PM
@Joe Because I've observed countless students over the years, and invariably those who were able to handle basic FOL (not the field called "mathematical logic") had no difficulty whatsoever with all areas of mathematics, whereas those who had conceptual difficulties never could handle basic FOL. All mathematics requires facility with basic FOL, and you cannot get far without it.
Moreover, it wasn't just a correlation. All students who put in serious effort to learn basic FOL (meaning including a deductive system for it) recognize readily that it completely clarifies mathematical reasoning. The thing is that people who do not know basic FOL can never even grasp just how superficial their conceptual understanding is.
3 messages moved from Logic
 
Joe
@user21820: Okay. If I want to learn FOL, then where do I start? I remember you recommending the book Language, Proof, and Logic. I think you also said that you yourself are willing to teach it, provided that someone already knows the groundwork.
 
@Joe For you I don't recommend LPL because it's too boring and long and I'm sure you can learn much faster if you just work through my exercises. And no there's no prior knowledge needed for me to teach you. You just start with the first few sections up to "Quantifiers and equality" in this post and then do the PL and FOL exercises here. Ask anything you don't understand.
It should only take you a week or two of focused effort to get used the system, and thereafter comes the interesting part, which is to learn how to use induction rigorously (via playing within PA), and then later to learn how to do all mathematics within the full foundational system given in that post under Set Theory.
Simply post all your attempted solutions for the exercises here and ping me, and I will check them and give feedback.
 
12:28 PM
@user21820 How "you" were able to learn basic FOL?
 
@Prithubiswas I was really lucky. My father taught me programming when I was 12. So from that I learnt to be 100% precise because the computer will do only exactly what you tell it to do. I took that mindset and applied it to mathematics all throughout high-school, and was significantly helped by mathematical olympiad training.
They didn't explicitly teach logic, and they didn't need to because all those who were selected for the national team could (unconsciously) do logical reasoning very well. But most of the olympiad problems required facility with basic logic otherwise you simply wouldn't be able to grasp what was going on (at least not clearly enough to win a medal), except perhaps in geometry (which hardly has any quantifiers).
While I was participating in olympiads, using my programming knowledge I developed an indentation-style very similar to Fitch-style (though I never knew that name). It sufficed for me all through high-school, but wasn't completely formal (nor did I know it was possible). But then in university my professor taught Fitch-style natural deduction and I was so happy to learn that it could be very precisely done.
So of course I went to read up on various deductive systems to figure out what I think is the best way to do things.
 
@user21820 Wow. That is an interesting story . From programming>math>olympiad>university>professor teaching fitch style.
 
@Prithubiswas: By the way that reminds me, have you managed to translate the English quine into a Python quine?
 
Joe
12:43 PM
@user21820: Great! I will start today, and I am reading your post as we speak. My first question is: you said that each inference rule is sound, meaning that if you start with a true statement, use an inference rule, then you will end up with a true statement. You also state that if a statement is necessarily true, then it can be deduced using your logical system. Is this property called completeness?
 
@Joe Yes that's right. It's called the (semantic) completeness of the deductive system for FOL.
For any deductive system to deserve the name "deductive system for FOL", it has to be semantically complete for FOL.
Same goes for "deductive system for PL", which comprises just the rules under "Boolean operations".
And it is worth emphasizing that semantic completeness of this system (or any other deductive system) is precisely what is so important about knowing such a system. It means that one knows for sure that one needs nothing else beyond this system to be able to prove every single theorem of mathematics (at least based on ZFC). There cannot be any sneaky new reasoning principles that one needs to learn for some new field of mathematics.
 
@user21820 I kind of lost interest in math after watching the -1/12 video by numberphile.

And I started to think that maybe I am not a smart person to understand to deep meaning of the math explained by the physicist in the video.The end
 
Joe
Ok, thanks. It seems that as I learn more FOL, I will be able to appreciate why it is so important. In your system, inference rules are written as $
\def\block#1{\begin{array}{ll}\ &{#1}\end{array}}
\def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}}
\def\sub#1#2{\text{#1}:\\\block{#2}}
\def\imp{\Rightarrow}
\def\eq{\Leftrightarrow}
\def\nn{\mathbb{N}}
\def\none{\varnothing}
\def\pow{\mathcal{P}}
\fitch{\text{X}}{\text{Y}}$. Does this have the same meaning as $X\vdash Y$?
 
@user21820 no. I am currently trying to do PA5 and Q10. Hope it is okay because I am not so good with multitasking.
 
@Prithubiswas Sure sure. Work on whatever you feel like working on.
@Joe Yes, the multi-line style is a visual representation, whereas the single-line style is for chat or when I don't want to take up much space.
@Prithubiswas Funnily enough, only smart people don't understand that video. All other people think they learnt something...
 
12:55 PM
@user21820 Thank you for the feedback. What do you think now about PA-3 ?
@user21820 That's interesting. Could you tell me more about your comment "[We shall now prove X.]" ? I've seen it many times in the past. What advantages does it have ? I am perhaps not completely getting your point.
 
@F.Zer It's fine. Of course, if you feel that the reader might be confused by line 15, you can expand it a bit: a+1 ≥ (k+1)+1 = k+2.
@F.Zer It's just to state your goal in advance so that people can skip that section if they can do it themselves. If you don't include such comments in a long proof, then the reader would have to go through every step blindly because they don't know what it's used for.
I think you even used such comments before on your own (before I mentioned them).
 
@user21820 This is a kind of weird followup to -1/12.
 
@user21820 Oh, yes. That's great. I get what you mean.
@user21820 Is the "+1" there just to make clear the use of discreteness lemma ?
 
@Prithubiswas What... Ok you definitely should not share that kind of junk with any student.
@F.Zer Yes, in case the reader misses the point.
 
Good.
I updated the proof in the repo.
 
1:04 PM
@F.Zer I find it very weird though that your line 2 is s o w i d e l y s p a c e d.
 
Let me check.
 
Joe
$
\def\block#1{\begin{array}{ll}\ &{#1}\end{array}}
\def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}}
\def\sub#1#2{\text{#1}:\\\block{#2}}
\def\imp{\Rightarrow}
\def\eq{\Leftrightarrow}
\def\nn{\mathbb{N}}
\def\none{\varnothing}
\def\pow{\mathcal{P}}
$
@user21820: One of the rules was $\neg\text{elim}$, which states that $(A \imp \bot) \vdash \neg A$. The other was $\neg\neg\text{elim}$, which states that $\neg\neg A\vdash A$. From this we can derive "proof by contradiction", which is $(\neg A\imp\bot)\vdash A$. Here is my attempt to explain why. Is it correct? If we replace $A$ with
 
@user21820 Haha. Fixed.
 
@user21820 I was just sharing it with you because it was interesting to me. The -1/12 video caused so much backlash that they decided to make some more followup videos (which I believe are also kind of nonsense). Then Brady Haran (creator of Numberphile) decided to make a blogpost with all of the videos they made and decided to take ramanujans notes out of context to prove there point. My surjective opinion: it is still nonsense.
 
@Joe When you stated ¬elim; did you mean ¬intro ?
 
1:10 PM
To me , That blog post was even funnier than the -1/12 video. Although I never shared it with anyone.
 
Joe
@F.Zer: Yes, thanks for correcting my mistake.
 
@Joe Your explanation is correct if you meant "¬intro" as F.Zer said. So if you use that derived rule instead of ¬¬elim in your proofs, it's completely fine with me. I think I picked ¬¬elim rather than ( ¬A⇒⊥ ⊢ A ) because it followed the Fitch-style idea that the rules should deal with as few boolean connectives as possible. And you're right to be concerned with how to turn it into a formal proof.
That's the difference between basic logic and studying logic. Basic logic just requires you to know that you can implement your derived rule by using the original rules. Only if you want to study logic itself would you want to formally prove that fact.
However, we won't be able to prove that fact until we have a little bit of set theory (at least subsets of ℕ or something equivalent) to be able to talk about proofs encoded as sequences. That's just the way it is.
So we'll have to postpone formalizing that fact.
@Prithubiswas Indeed. If they just stopped with the video, they could argue that they weren't being serious and weren't being rigorous. No matter how much I think it's nonsense, it's hard to argue against a vague video. However, that blog post just makes it absolutely clear that they were being idiots and doubling down on it.
Though I'm not sure what a surjective opinion is. =D
@Joe: Wait a minute, didn't I say we could derive this proof by contradiction rule in my post just after the ¬ rules? Oh I see you were explaining that claim. Good!
 
@user21820 I apologize if it was weird to share it with you =(. I am sorry . It is just , whenever I feel upset about something in my life , I just put those numberphile videos in my playlist , read the blogpost and laugh along (because crankary makes me laugh).That cures my sadness.
 
@Prithubiswas It's not weird. Just be careful with putting that link anywhere, since most students don't know any better.
And wow you found a use for crankery! Congratulations!
 
@user21820 Ok then put it in trash. (where it belongs).
And to everyone in this room , don't click on that link , it is a virus (unless you want to have a laugh).
 
1:25 PM
@Prithubiswas Don't worry, no need for that.
Ironically, Phil SE is worse than Numberphile.
 
@user21820 I never heard of Phil.SE.
 
@Prithubiswas It is the SE site for philosophy. You probably have heard of it, even if you haven't gone there before.
@Prithubiswas: But if you're bored, why not read some comics? =P
 
1:41 PM
in Miscellaneous, Jun 16 '20 at 9:34, by user21820
The comments here show that most users on Phil SE are unable or unwilling to identify the cranks. There are 3 there, namely Doug, Joshua and polcott, and the last one is even a repeat rule-violater (via sockpuppets).
This is all I know.
 
Well yea that's one. It's so funny that cranks are allowed to run rampant on that site.
 
The only person I recognize is Doug Spoonwood , who writes his answers in polish notation.
 
Well we shouldn't comment too much on these users, until moderators are more willing to stamp out nonsense.
 
Joe
2:10 PM
@user21820: Is the rule $\forall\text{intro}$ the same as the rule of "universal generalisation", which I believe is the rule that states (informally) that if we can prove $P(x)$ for an arbitrary $x$, then it follows that $\forall x : P(x)$.
 
@Joe Yes.
But it's the precise version.
In particular, without the ∀subcontext-headers, it is unclear what "arbitrary" means.
 
@user21820 I am reviewing the concepts I struggled the most with; one of those is proving strong induction from induction. While I am doing it, I have no clue about how I solved it. It seems it was above my head at that time. Could you tell me whether I am heading in the right direction ?
Given P on ℕ:
  If P(0) ∧ ∀ k ∈ ℕ ( P(k) ⇒ P(k+1) ) ⇒ ∀ k ∈ ℕ ( P(k) ): [Induction]
    If ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ):
      ∀i∈ℕ ( i<0 ⇒ P(i) ) ⇒ P(0)
      Given i ∈ ℕ such that i < 0:
        ⊥
        P(i)
      ∀i∈ℕ ( i<0 ⇒ P(i) )
      P(0)
      Given k ∈ ℕ:
        If P(k):
          ...
          P(k+1)
      ∀ k ∈ ℕ ( P(k) ⇒ P(k+1) )
      ∀k∈ℕ ( P(k) ).
    ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ) ⇒ ∀k∈ℕ ( P(k) ). [Strong induction]
 
@F.Zer No, that doesn't work. What you put in your assumption is not induction. Induction is a rule, not an axiom, so you cannot state it as an assumption.
 
@user21820 In your post you said: "Add the induction axioms, namely for each property P, involving only the symbols of PA and quantifiers over ℕ add the following axiom: P(0) ∧ ∀ k ∈ ℕ ( P(k) ⇒ P(k+1) ) ⇒ ∀ k ∈ ℕ ( P(k) )." But I am surely missing your point.
 
"Property" is defined syntactically, and you remember those syntax rules, right? Nowhere did we provide any means of quantifying over all properties, so you cannot state induction in the system.
 
2:24 PM
@user21820 Could you refresh my memory? I probably need a hint to trigger it.
 
That's why if you look at the precise instruction I gave at that time, it was:
> That is, for each property P on ℕ prove "∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ) ⇒ ∀k∈ℕ ( P(k) )" within PA.
 
@user21820 Yes, that's why I am taking an arbitrary property P.
 
@F.Zer But you claimed that your second line is "induction", which is wrong.
 
@user21820 Yes, I see. Induction starts with "For any property P, ..."
 
Induction is either a rule or an infinite set of axioms, neither of which can possibly be an assumption as you claimed in that line.
 
2:27 PM
@user21820 Which syntax rules are you referring to ?
 
Sep 8 at 20:01, by user21820
And when you describe the FOL deductive system, you should include the syntax rules and the syntax of properties and examples (1, 2) besides the deductive rules, since my post completely omitted all syntax rules.
That's why you need to hurry up and put those important stuff into your own reference so that we can stop digging old chats. =)
 
@user21820 I will ! Searching through millions of messages doesn't seem productive :-)
If for any property P on ℕ, P(0) ∧ ∀ k ∈ ℕ ( P(k) ⇒ P(k+1) ) ⇒ ∀ k ∈ ℕ ( P(k) ): [Induction]
  Given P on ℕ:
    If ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ):
      ∀i∈ℕ ( i<0 ⇒ P(i) ) ⇒ P(0)
      Given i ∈ ℕ such that i < 0:
        ⊥
        P(i)
      ∀i∈ℕ ( i<0 ⇒ P(i) )
      P(0)
      Given k ∈ ℕ:
        If P(k):
          ...
          P(k+1)
      ∀ k ∈ ℕ ( P(k) ⇒ P(k+1) )
      ∀k∈ℕ ( P(k) ).
    ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ) ⇒ ∀k∈ℕ ( P(k) ).
  For any property P on ℕ, ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ) ⇒ ∀k∈ℕ ( P(k) ). [Strong induction]
@user21820 Is this better ? Do you think this proof skeleton work ?
 
@F.Zer Well, I'm not happy with you quantifying over properties (and you didn't even say "Given property P on ℕ:"), because as I said just now you cannot do that within the system.
It's not that it's bad; there is a more complex extension of the system that allows us to do that. But you're supposed to just follow my given instructions rather than trying to say more than the system allows you to say.
 
@user21820 That's good. What's your preferred way ?
 
16 mins ago, by user21820
> That is, for each property P on ℕ prove "∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ) ⇒ ∀k∈ℕ ( P(k) )" within PA.
 
2:42 PM
@user21820 Yes, but instead of "Given property P on ℕ:"; is there an ever better alternative ?
 
@F.Zer There's no better alternative. That 'quantification' over properties simply cannot be in a proof.
 
@user21820 Ohh, I now get it ! That would be second order logic ! "Given any P on ℕ"...Is that right ?
 
Yes. That's the problem. That's why the FOL exercises also cannot quantify over them.
 
@user21820 Good. So, how can I solve the problem. It would be "Given..." ?
 
@F.Zer At this point I would just put it outside. That's why my statement of strong induction was:
Jun 9 at 15:07, by user21820
> Strong induction: For any property P on ℕ, we have ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ) ⇒ ∀k∈ℕ ( P(k) ).
And likewise your justification could go something like:
For any property P on ℕ, we can prove:
  ...
  ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ) ⇒ ∀k∈ℕ ( P(k) ).
Although I very much like being able to natively quantify over properties, and I made sure I can in my own foundational system, I don't want students to misunderstand what PA can and cannot do, and PA certainly cannot quantify over properties over PA.
 
2:52 PM
@user21820 Perfect. Understood.
For any property P on ℕ, we can prove:
  P(0) ∧ ∀ k ∈ ℕ ( P(k) ⇒ P(k+1) ) ⇒ ∀ k ∈ ℕ ( P(k) )
  If ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ):
    ∀i∈ℕ ( i<0 ⇒ P(i) ) ⇒ P(0)
    Given i ∈ ℕ such that i < 0:
      ⊥
      P(i)
    ∀i∈ℕ ( i<0 ⇒ P(i) )
    P(0)
    Given k ∈ ℕ:
      If P(k):
        ...
        P(k+1)
    ∀ k ∈ ℕ ( P(k) ⇒ P(k+1) )
    ∀k∈ℕ ( P(k) ).
  ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ) ⇒ ∀k∈ℕ ( P(k) ).
@user21820 Does that seem right ?
 
@F.Zer No it won't work. You need to use your (logical) intuition to figure out why strong induction is true even before you try proving it.
 
@user21820 Good. I have to go out a moment. Thank you for your help and see you later !
I'll continue thinking about this.
 
See you!
 
 
1 hour later…
4:17 PM
@user21820 I want to bookmark some of your messages , because I want to come back to them later. Is there a way to do it?
 
@Prithubiswas There isn't a nice way to do the same with individual chat messages as with SE posts. However, if you want to bookmark a whole conversation you can click on the "room" menu then "bookmark" and then select a whole range. But it is public and shows up here. You can find your own bookmarks here, which is also public.
 
@user21820 I bookmarked two conversations.
 
Sure. Hopefully it's useful enough for you!
 
4:51 PM
Hmmm... I have seen some first order logic texts but they use the notion of a set but isn't FOL supposed to be the basis of ZFC set theory?
 
@PaxDaga It is, but those texts do not teach basic logic.
 
so what do they teach? advanced logic?
 
Exactly. And have you started what I told you to do?
 
Told what? the excirces? I guess one can do the ones you told me to do buy making truth tables ..
 
@PaxDaga No, you're not even trying.
 
4:59 PM
Which are you talking about
 
yesterday, by user21820
@PaxDaga: Not now. I cannot teach you the proper mechanism for definitions until you know basic FOL, because it depends on FOL. Since you said you wanted to learn FOL from me, let me tell you where to start. I'll teach you the same way I taught F.Zer and Prithu in this room, starting from PL. For PL, read and make sure you understand the first few sections up to "Boolean operations" in this post.
 
You also told me to do excersices
the first few ones from your list
 
The exercises mean that you must write a proof in the deductive system I linked you to.
Nothing else is a correct answer.
This was very clearly stated right at the top of the list of exercises.
 
ok I will read that post.
 
 
1 hour later…
6:33 PM
@user21820 Do you think this proof outline would work ?
For any property P on ℕ, we can prove:
  P(0) ∧ ∀ k ∈ ℕ ( P(k) ⇒ P(k+1) ) ⇒ ∀ k ∈ ℕ ( P(k) )
  If ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ):
    ∀i∈ℕ ( i<0 ⇒ P(i) ) ⇒ P(0)
    Given i ∈ ℕ such that i < 0:
    ∀i∈ℕ ( i<0 ⇒ P(i) )
    P(0)
    Given k ∈ ℕ:
      If P(k):
        k+1 ∈ ℕ
        ∀i∈ℕ ( i<k+1 ⇒ P(i) ) ⇒ P(k+1)
        Given i ∈ ℕ:
          If i < k+1:
            i+1 ≤ k+1
            i ≤ k
            If i = k:
              P(i)
            If i < k:
              If ¬P(i):
                ...
 

« first day (1232 days earlier)      last day (952 days later) »