Ok here is a sketch of the proof of Q1

<>If A:

<><> A\implieds (A∨B)∧(A∨C)

<>B$\land$C:

<><>B

<><>C

<><>B$\land$C \implies (A∨B)∧(A∨C)

Therefore by or eliminatiion the first half is true

@user21820

how to indent ??

I think its wrong

@user21820

But is this also going to be moved to trash because I am doing what you told me to do now

Yes it is completely wrong. Please post again when you think you have a correct solution. Follow the rules strictly. One single mistake would make the entire thing wrong.

@PaxDaga To indent, type your attempt in a good text editor (e.g. Programmer's Notepad) first, using tabs or spaces to indent. Any good text editor will automatically maintain indentation for you. After that, copy and paste here but click "fixed font" before "send". Do not use LaTeX because it will not be displayed. Use either ASCII or unicode symbols.

When I say if A then I guesss id have to declare A as well

@PaxDaga I have only removed the useless bits. The rest stays.

also do I have to write everything or can I skip some steps? In math sometimes easy steps are skipped

@PaxDaga At this point, you do not know PL, so you must show every step until you have completed all the PL exercises.

Hmmm... Ok I just skipped a few steps and maybe I put an or instead of and somewhere but I don't see any other mistake I will write the full proof soon

I don't know ascii is there any way ident in mathjax?@user21820

@PaxDaga ASCII is just plain text, like "A and B" instead of "A ∧ B".

Is it nesscary to put square brackets when restating something ?

What is the point of them?

@PaxDaga You need to read my post more carefully. I wrote:

> In practice we never actually write the same line twice, but to make the description of the rules easy we shall to consider it written anyway. I'll mark all such lines with square-brackets as follows

So they are useless sorry I read that but when you say that you want everything then I guess I have to tight them too

Yes, don't write the square-brackets, but for now don't omit any line except the ones that are just restatements (i.e. those from the rules restate and ⇒sub and ⇒restate).

A∨B∧C ⇔ (A or B) and (A or C)

Proof the first direction

If A or B and C:
                        If A:
                              A
                              A or B
                              A or C
                              (A or B) and  (A or C)
                        A implies (A or B) and (A or C)
                        If B and C:
                                         B and C
                                         B
                                         C
                                         A or C

Good. Give me a minute to check. I'll remove the unindented copy.

→ 6 messages moved to Sandbox

The last should be implies not double implies

@PaxDaga That's right. You still have the other half to prove. Your first half is correct.

Also, indentation is best done at a fixed size (either 1 tab or 2/3/4 spaces).

Now while you do the second half, I'll chat with MaxH.

@MaxH You wrote "you give me some random symbols you like [...] (pretend that you give me an infinite amount of symbols)". That's meaningless because it is imprecise.

@MaxH I don't know what you have in mind, because it is too vague, but it should be wrong. "MaxH" is not a set; it is a string with 4 letters. "1+2+3" is not a set either; it is a string with 5 symbols.

I don't think you actually fully understood PA. Just take a look and note that PA is axiomatized using the logical symbols and only 5 other symbols.

Ok, let me see how I can make it more precise. As I said I almost know nothing about set theory, so sorry if what I say is not correct. I had the "everyday mathematics" perspective in mind in which "everything is a set". In introductory courses you will encounter a lot of stuff like {A,B,C} or {I,II} and so on, which is why I wondered how this can be

Or if its just to visualize and give an intuition

I repeat what I identified as one of your misconceptions: The object 1 is not the symbol "1". Similarly, if you have defined A,B,C to be some objects, then {A,B,C} is the set whose members are exactly A,B,C. There are no symbols in the set.

If you haven't defined A,B,C, then the expression "{A,B,C}" is meaningless.

Exactly, but I need to have objects first, as far as I understand

Exactly!

And these objects are then allowed to be given names such as A,B,C

Which would then give the set a meaning

@MaxH That's no longer correct.

I wanted to sort of reverse this: Give me objects, then I can "find objects" s.t. I can build a set that contains objects that are represented by these symbols

Objects are not "given names", and sets do not derive meaning from "names".

@user21820 Thats not what I mean, maybe I used weird formulations here

@user21820 Is there a computer program which can check arguments like these about PL?

Once I have objects, I can give those objects names, such as A,B,C and thus refer to those objects by those names.

Its like in the PA case. I assume that I have a set of objects (therefore I don't need to worry that I even have objects) and I can give those objects in the set names such as 0,1,2,...

I hope I found clearer formulations.

@PaxDaga Yes the whole point about a deductive system is that it is computable (i.e. there exists a program that can verify proofs in the system). But I haven't written one. Anyway it's not hard to check simple proofs like this manually.

@MaxH What you just said is clear enough, but I still don't see any sense in what you said earlier.

Ok, let me ask something first: Do the PA assume that there is a set of objects that is called N? Meaning, that we are "given" a set of certain objects that is called N (and then satisfies the axioms)

Maybe this is where a problem lies, I am not sure.

Technically speaking, no. PA does not assume there is a set of objects called ℕ. If you look carefully at the post I linked you to, you can do reasoning within "Peano Arithmetic" completely without any of the syntax or rules or axioms of "Set Theory". In that post I called "ℕ" a type, and that is precisely all that it is. It is just a type of objects. There are no sets.

However, that's not where your problem lies. I think your problem is with a misunderstanding of the use of variables in basic FOL. You can only name an object that you can prove to exist. This is either via a deductive rule called ∃elim(ination) (in some formal systems) or via a mechanism of introducing definitions. You cannot name an object that you are unable to even refer to by an ∃-sentence.

Hm, okay, nevertheless I am "given" objects? Meaning one assumes that certain objects exist.

Because if I now use M instead of N, I also have objects that are assumed to exist, but I have no way of telling whether the objects of N and M are equal or distinct, that is just unclear.

I have not enough information for that, is what I want to say.

That's right. The symbols 0,1 of PA− and one of the axioms saying 0 ≠ 1 already guarantee that there are at least two objects. And you can check that 1 ≠ 1+1 as well, and so on, so the axioms of PA− already ensure that there are many objects. There is no set theory needed to see this. And yes if you have a copy of PA− axioms with the symbols changed, you have no way of telling whether those objects referred to by those symbols are the same or not.

Right

If you want them to be different, you can add axioms to force them to be different. The question then is whether or not your axioms make sense.

So therefore I have to assume by axioms that there is a potentially different set called M

And I wanted to see if this really has to be an axiom.

Which is also the case for PA− itself. Why did people invent the axioms for PA−? Because they made sense when the sentences in the language of PA− are interpreted as statements about the real world.

If you make up an arbitrary list of axioms, you would have to justify (at least to yourself) that it is meaningful, otherwise it just becomes like another chess variant.

Because in that case i would have to add axioms and I am not sure if thats a good thing to do

@user21820 This is a guess , but Is p<b ?

But I see that, assuming I have a set of portentially different objects, assuming I define them to be I,II,III and so on I have a set that is different from N that has been previously defined by 1,2,3,4,...

@Prithubiswas Yes. I thought you would have tried to prove it before asking, though!

@user21820 I just guessed it. I setted b = 7 and c = 36. Then 6.7 = 42. So , in this case , u = 6 and p=b.u-c=6. It seemed to me like p<b. And intuitively , that should happen with any b and c I choose.

@Prithubiswas Yes, and precisely that upper bound is why I used well-ordering in the first place. It's a big hammer to nail that upper bound down, and I didn't think twice to see if there was a better approach.

@user21820 If p ≥ b , then there is an x smaller than u that satisfies b.x ≥ c , which is a contradiction. correct?

Yes. You just need to figure out how to make that rigorous, which should be easy for you.

@MaxH: Anyway that's why I said earlier:

Which in your last comment you seem to want to do.

In fact, in another comment you said "countably infinite" despite what I said earlier:

Which suggests that you don't know what the precise definition of "countably infinite" is.

Well, I do know the definition and it gives me what I want. I wanted a set with different objects than the ones in N that also has different symbols for its objects but satisfies the PA. It follows naturally that they are isomorphic.

I just wanted to know whether in addition to the axioms of the system I work in, I need to add another axiom that gives me such a set.

But it appears that this is indeed necessary, because I don't see what else would give me different objects than the ones that are assumed to be in N.

Maybe this makes it more precise. I read that any two sets that satisfy the PA are isomorphic. I assumed that there exists N, and that N satisfies the PA. How do I get another set of objects, s.t. I can even check whether it satisfies the PA? Will I have to assume by axioms that such a set exists?

I think your imprecision is costing you your understanding. It is meaningless to ask whether a set satisfies PA or not. I was very careful to say:

Even in a set-theoretic foundational system, where ℕ is a set and not just a type, ℕ does not satisfy PA.

Take a look at what I said satisfies PA. It's a structure, not just ℕ.

And once you understand that point, you see that there's absolutely nothing wrong with my example:

It's a different structure.

@MaxH And if you want to prove existence of objects outside ℕ, of course you need some assumptions beyond PA. But that question has nothing to do with models of PA because as I showed you it's easy to obtain models of PA that are different from the the usual one.

I see, but in the model you provided I only have that the sets are not equal, essentially because your 2nd model does not include the zero object. This means that some objects are indeed equal in both sets, right?

@MaxH Yes. So if your next question is that you want a model with domain completely disjoint from ℕ, then as per my last remark above you need assumptions beyond PA.

I see, I understand that.

Great!

By the way, you have not commented on the way I imagine objects, meaning as points in the space. May I ask whether you think that this is a "good" way to visualize this or if its not fitting. As far as I know objects are abstract and not defined, which is why this visualization might help.

Obviously, this is kind of a "preference" question.

Using &nbsp;&nbsp; works on the main site for indents

@PaxDaga Yes, that is HTML. There is neither HTML nor MathJax in chat. Don't use MathJax for your proofs in the formal system. Also, the sandbox is the room for experimenting with chat without disturbing others, so I'm going to move your experiments there.

→ 3 messages moved to Sandbox

@MaxH You can imagine each object as a kind of point, to a certain extent. It does help the intuition in some cases.

There's not much more I can say because it's very subjective. What matters is whether you can do rigorous mathematics. How you visualize it intuitively is somewhat secondary. In some areas of mathematics, intuition can be very dubious or even wrong.

Thanks. I think this especially helps with the distinction between objects and the names they are given, at least when I imagine the names being some sort of symbols written above the object. This way there can obviously be multiple names for the same thing. Also this would visualize the axioms of equality nicely.

Yes, but that is also why I asked you. You are more experienced so I think you have a better understanding whether it is a bad intuition or a rather helpful one.

I have found a post on stackexchange that my previous question is partially built on, am I allowed to post such links in here?

@MaxH Sure, I see what you're getting at. The whole point about FOL is that it allows us to reason about potentially infinitely many objects using only finitely many variables, as you can see from PA.

@MaxH Yes if it's relevant feel free to post it.

Its this one. The most upvoted and accepted answer has the first example of musketeers.

So only that part is relevant. I wonder, is this really a set, or rather to build an intuition, and how can I see why this is a set? I mean, I should be able to model it somehow using the naturals, but maybe there is another way.

Obviously such sets dont occur in rigorous maths, which is why this question might again be problematic

But this is one of the examples I see everywhere in introductory courses.

@MaxH Ugh. The top-voted answer is not very good.

@MaxH The part about the musketeers is fine in the sense that it is about the intuition behind the notion of "set".

I suspect this is where the "everyday maths" vs the foundational maths really comes in, right?

@user21820 You mean in the sense that I can collect "anything"?

@MaxH Not "collect", but classify.

Could you please specify what you mean by classify?

I'm not happy with that answer by Vectornaut not because it says anything wrong but because it doesn't actually address the question of what on earth is a set.

@MaxH You don't have to collect all natural numbers together before you can meaningfully talk about ℕ and reason about all its members.

ℕ is merely a classifier; some objects you classify as "natural number", some you classify as "not natural number".

And it doesn't have to be anything more than that for you to work within PA. You do not need ℕ to be a mathematical object until you want to construct more abstract stuff such as ℝ.

And in some sense the core intuition behind a set is just as a classifier. That's why you write { x : Q(x) } to mean all objects that satisfy the predicate Q.

So does the musketeer example form a set or not? If so, can I say anything about the objects? Im kind of confused here. I guess one could let the three musketeers be three objects of N and just rename them accordingly, but this would mean that they are actually numbers, wouldn't it?

@MaxH You cannot refer to reality from within mathematics. It's simply impossible.

Ok, so I could only "model" it in the way I suggested?

More or less. Everything you write on paper or in this chat are just symbols. They don't have any intrinsic connection to anything in the outside world, until we interpret them. And that interpretation itself cannot be captured by a string of symbols without us (again) interpreting what we are talking about.

@user21820 Its not possible to state what objects are in N and what are not right? Because what actually are objects? I can only say that an object is in N if its actually in the set called N. So, this is because objects are abstract.

@MaxH That's actually true for my system. I didn't have any axioms or rules that tell you what ℕ really is. Some set theorists define ℕ in a different way, forcing it to be constructed out of certain "sets". I didn't, because it's completely pointless.

Alright, I just wanted to make sure that my understanding is actually correct.

All of this is just to sharpen my intuition to make less mistakes in my proofs and actually understand better what is going on.

Therefore I felt like I needed to get a better understanding of sets.

Especially because examples like {A,B,C} gave me the impression that we collect symbols.

Which has lead to some confusion.

If you really want to understand everything completely, you'll have to learn basic FOL before you learn Set Theory (which sits on top of FOL).

Right now I am not really interested in learning foundations more than "necessary". I just tried to improve and make less mistakes in my everyday maths.

But by doing that, questions such as what is equality and why does it work, what are sets etc. come up naturally, which is why I needed to think about this more.

But since those type of questions come up from time to time, I might be having to actually study some foundations.

Well it's naturally your choice, but I will say that it's impossible to get a full grasp of mathematics without knowing basic FOL. Some students manage to unconsciously figure it out, but most never manage it. That's a risk you run if you avoid foundations. Incidentally, professors themselves are slightly susceptible to this same risk. Some of the mathematics professors in my university cannot tell whether they have used the axiom of choice or not, because they do not truly understand ∃elim.

On the other hand, of course learning foundations will take up some time, and I completely understand if homework and tests put pressure on what you have time for.

@user21820 Hi, how are you ? Can I ask a question ?

One has to specify what the aim is. My aim is to be better at math understanding the most. I am equipped with like 1 lecture of logic and truth tables from introductory course, the notion that a set is any collection of objects and thats it. The big problem is indeed the time factor. I don't even have enough time to read into the subjects that I am interested in more because of the exams and homework and stuff.

So yeah, in the long run I would like to do that, but I don't know exactly if I will have time to do so.

Anyways, thank you very much for your time.

@MaxH Indeed. So if you like, you can wait for holidays, and then come and find me again if you want to learn some foundations. There is no hurry. It's an investment that I think is important, but you still need to get your grades first!

@F.Zer Sure. Did you manage to figure out what you were missing in your attempt to prove strong induction?

Thanks for your offer. I will let you know when I have time and enough interest!

@MaxH You're welcome!

Have a nice day everyone.

@MaxH Same to you!

@user21820 I was going to ask you about that. If I let k = 2, then the antecedent of strong induction becomes "P(0) ∧ P(1) ⇒ P(2)". Is that right ?

∀ i ∈ ℕ ( i < 2 ⇒ P(i) ) ⇒ P(2)

I reduced the latter expression to the former one.

My current outline is:

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) ):
		Given k ∈ ℕ:
			∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k)
			...
		∀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]

@F.Zer That's not really the antecedent. It's just an instance of the antecedent (applied to k = 2).

So why are you always trying to find an outline before understanding via the small cases?

@user21820 Sorry, I missed instance.

@user21820 Yesterday, I worked on small cases as you always suggest.

My outline is for the future.

@user21820 I assume P(0) ∧ P(1) ⇒ P(2) and I should prove (using weak induction) that P(0) and ∀ k ∈ ℕ ( P(k) ⇒ P(k+1) ) holds ? I am not clear about the goal. That is the problem, I think.

Uh? Your goal is to convince yourself that the conclusion is true. Not to prove anything.

@user21820 I like what you're saying, but I don't know why the conclusion is true. So, I can't convince myself.

@F.Zer What is the conclusion?

@user21820 For any property P on ℕ, ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ) ⇒ ∀k∈ℕ ( P(k) )

No.

You're getting into your old habit again, letting your proof attempt dictate how you think.

I won't fall into my old habit again. I'll make another attempt

@user21820 ∀k∈ℕ ( P(k) )

Exactly.

Good !

To convince yourself that an instance of strong induction is true, you try to convince yourself that ∀k∈ℕ ( P(k) ) is true given ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ).

You already identified one small instance of the given assumption. That's not enough.

Where are all your other small cases?

@user21820 That's great. I will make more now.

@user21820 Given ∀i∈ℕ ( i<4 ⇒ P(i) ) ⇒ P(4) is not enough to prove P(4).

I don't know whether ∀i∈ℕ ( i<4 ⇒ P(i) ) is true.

I have to go out a moment. See you later !

@F.Zer: Have you convinced yourself of the conclusion or not? See you later!

@user21820 Can you share your opinion about this?

@Prithubiswas I think Mauro's first citation is for the original Fitch notation. It's not necessarily the best to use in practice, because after all Fitch is a logician and logic expertise doesn't necessarily imply good pedagogy. However, it's of course interesting to know the history of Fitch-style if you like that sort of thing.

@Prithubiswas I'll take a look at the other two and let you know what I think.

@user21820 Sure. take your time .

@Prithubiswas Both textbooks are studying logic, so it won't teach you what you want. I think Mauro missed your intended purpose.

I'll post a more detailed comment there since others should be made aware as well.

I can't post an answer because you ask for a textbook and I didn't write any. =P

@user21820 "There isn't any good textbook" is also an answer to me. Although one might have to do a lot of searching to confirm that there isn't any.

Or you can just comment.

@Prithubiswas That's the problem. It's hard to justify "∀T∈Textbooks ( ... )". =P

@user21820 Cunningham's Law states "the best way to get the right answer on the internet is not to ask a question; it's to post the wrong answer."

Applicable?

@Prithubiswas Lol? I have no idea what that means..

Maybe...

@user21820 To me , if you post an answer with "I have searched the internet and found no such textbook for beginners" , then some other logician might see your answer and post an answer with the textbook that fills the criteria so that he can prove you wrong.And hence , by posting the wrong answer , we got a correct answer.

@Prithubiswas Ah I see.

If you want, I can post an answer, but I would recommend my own system. If you think that self-advertisement is fine, then I'll go ahead.

@user21820 Hmm , you can compile your history of trying to find good FOL textbooks , show the textbooks that you found and your opinion about them , like forallx , LPL etc , and show your post about your own deductive system. Is that okay for you?

@Prithubiswas It's too time-consuming hahaha.. Anyway I have made two comments on your question that summarize my thoughts about Mauro's cited books with respect to your question.

@user21820 Sure. That is more than enough =)

Now I think it would have been a nightmare to do proofs in hilbert style.

Indeed.

@user21820 I get P(0) from ∀i∈ℕ ( i<0 ⇒ P(i) ) ⇒ P(0) since the antecedent is vacuously true. Then, ∀i∈ℕ ( i<1 ⇒ P(i) ) ⇒ P(1) ≡ P(0) ⇒ P(1), and since I already have P(0), derive P(1). Does this make sense ?

@F.Zer Yes.

Thank you for the answer.

Go on?

@user21820 Using small cases, I am starting to see why it is true.

So, I prove P(0) but I should also prove P(2) ⇒ P(3). Is that right ?

@user21820 Something that surprises me: that statement is true without relying on weak induction. Isn't it interesting ?

Which statement? You haven't even convinced yourself of the conclusion.

So, if I assume ∀i∈ℕ ( i<4 ⇒ P(i) ) ⇒ P(4), I can conclude P(4) following that pattern of thought.

What pattern of thought?

That's just P(1). What's the pattern?

Good. I'll think.

@user21820 I see you are teaching me how to generalise. I don't seem to find the pattern. It seems I can always derive P(k), when I assume ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k), for any k.

P(0) is true and I can always use the preceding statement.

To prove the truth of the next one.

I can relate to that feeling.

I will go out a moment and return back.

@F.Zer That's incorrect. You didn't sufficiently explain the small cases to yourself, nor to me.

@Prithubiswas What's abnormal about it?

It should be well-ordering that feels strange, not strong induction.

@Prithubiswas If it's intuitive, it's because you aren't skeptical enough.

@user21820 Can you explain what is strange about well-ordering?

You could be right . I might not be skeptical enough on this.

Firstly, just look at the justification for well-ordering in the first place. You used strong induction.

If you didn't, how do you want to justify well-ordering?

Why should existence of a natural that satisfies some property Q imply that there is a minimum witness?

@user21820 That is true.

Secondly, consider that well-ordering tells you that for every k∈ℕ there is some minimum m∈ℕ such that some Python program of length m (i.e. m bytes) prints k. This m is called the Kolmogorov complexity of k with respect to Python (which from now on we won't mention). But guess what? Kolmogorov complexity is uncomputable. That is, there is no Python program that can compute Kolmogorov complexity of input k∈ℕ correctly.

@user21820 So you mean we can prove the existance of Kolmogorov complexity by well-ordering , but there is no python programme to compute it?

Correct.

There's nothing bad about that. It's the same as whether you believe the halting problem has a well-defined answer or not even though you cannot compute the answer in general.

I think I have to resolve the " vacuous truth ⇒ P(0)" issue.

Haha. Have you read my post on vacuous truth?

It's linked from my profile as "Game semantics":

@user2180

Is my proof completely correct in the sense that not even not hing is wrong from a completely formal perspective like did I have to state something twice somewhere etc?Or did I skip even I single step even restating?

I = 1

I think the proof for the reverse case would go with case analysis for A B and in B for A and C

@PaxDaga I didn't check every restate step, because that isn't important. The other rules are more important. I can explain why the restate details aren't important. The point of knowing at least one deductive system completely is to know how FOL can be done rigorously. But there are many variant systems. It just happens that the system for PL is simplest and cleanest when the restate rules are there. That's also why I tell you to omit the lines given by restate rules.

But since you ask, the first line you unintentionally omitted is before your "A or C", where you need the restate rule to get "A" first.

@PaxDaga Try it! See whether you can get it right the first time, as you did for the first half (ignoring the missing restatement).

And one more missing line was "(A or B) and (A or C)" at the end of the subcontext under "If A or B and C:". Well I guess that counts as a really missing line, though I know that was your goal that so I didn't notice it was missing earlier.

@user21820 That's an excellent answer ! I upvoted it since it cleared up some issues I had.

@F.Zer Good.

@user21820 You're right. I see the issue now. I am clearly seeing how the statement is true for small cases; however, I am generally failing at explaining why the general case works.

It seems that pattern would go on, no matter which "k" I choose.

@user21820 In order to see why ∀ k ∈ ℕ P(k), should I use the fact that weak induction is available, or should I only use the hypothesis "∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) )" ?

@F.Zer No you shouldn't use any induction at all. Just explain to yourself what the pattern is. You didn't even do that.

Good. Got it.

→ 2 messages moved to ­Trash

Spam gets moved to trash.

Spammers are not allowed here.

That doesn't seem like spam

@RedwolfPrograms It is. Please do not judge when you do not know the history.

→ 1 message moved to ­Trash

Is there a history of this user spamming or something? Currently this just seems like moving justified requests for clarification to trash.

Hi folks. Please don't flag things as spam that are clearly not spam. If this room has special rules of moderation and content and you need to flag something for removal, please use a moderator flag and explain why. Spam flags have a penalty and should not be used lightly.

@terdon I am not the one who flagged. The spammer is the one who flagged me, wrongly of course.

@user21820 And I didn't say you were the one that flagged. I was addressing the room.

@RedwolfPrograms Of course there is a history of spamming. As I said, do not judge when you do not know the history.

@terdon Ok. By the way, I don't understand what you mean by "penalty".

@user21820 Validated spam flags result in automatic suspensions.

Anyway, I'll leave you all to it. Just wanted to let people know to please not use spam flags lightly.

@user21820 I see this pattern:

I am failing at the "explaining" part.

In each line, I should use all the previous lines to get the desired conclusion.

@F.Zer That's right. So the pattern is clear. In particular, you need to "use all the previous lines" to get what you need in order to use the implication from the given condition.

So you cannot just "use only the previous line". Correct?

@user21820 Yes, I see the mistake !

So if you want packages in the form Q(k) where Q(k) ensures Q(k+1) in the manner of your pattern, your Q(k) needs to also provide "all the previous lines".

This is the way to figure out what induction hypothesis you need, by looking at how the information is flowing from one step to the next.

@user21820 Wow. That's very interesting. I'll work on finding that Q.

@user21820 Define Q(k) ≡ ∀ i ∈ ℕ( i < k ⇒ P(i) ) ⇒ P(k).

@F.Zer Why do you want that? Did you check what you already have (the given condition)?

@user21820 My condition is: "∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) )".

So what's the point of Q(k) if your condition already gives you all the Q(k)?

So, I can write it as: ∀ k ∈ ℕ ( Q(k) )

@user21820 Mmm...I am not following, I think.

Yes, but what's the point? You're not following what you want in the pattern of your reasoning.

@user21820 To get all the previous lines, I thought perhaps my induction hypothesis could be ∀ j ∈ ℕ ( j < k ⇒ Q(j) ) ⇒ Q(k) ), but that's probably wrong

@user21820 I'll think about that.

@F.Zer No, you're not being clear with yourself what each line asserts.

If you want "all previous lines", it is not expressed by your Q.

@F.Zer No.

Look at what you yourself assert in each line. It's not what you're saying now.

@user21820 I made a mistake on the first one, sorry. For example, line 5 asserts: ( P(0) ∧ P(1) ∧ P(2) ∧ P(3) ⇒ P(4) ) ⇒ P(4)

No that's incorrect.

Your original was correct.

@user21820 This one ? ∀ i,j ∈ ℕ ( (j < i ⇒ P(j) ) ⇒ P(i)

No.

Yes, I see.

This is entirely correct. You're trying to force it into something wrong, instead of trying to understand what you did.

This is also correct, but you didn't clearly identify for yourself what you did in each line.

@user21820 Attempt at line 2: P(0) ∧ (P(0) ⇒ P(1)) ⇒ P(1)

Look. You're not listening to yourself. You say "use all the previous lines" but you don't even know what you are "using".

What are you using when you say that?

@user21820 Yes, you're absolutely right. I don't know what am I using.

@user21820 I am using the conclusion from each line.

@F.Zer So...

What does each line assert?

@user21820 Each line asserts the truth of P(k) given ∀ i ∈ ℕ ( i < k ⇒ P(i) ) ⇒ P(k), but that's probably wrong.

Do you or do you not assert P(0) in the first line?

@user21820 Yes, of course.

That's not what you just said.

What about the second line?

The third?

@user21820 The second line asserts the truth of P(2) given ∀ i ∈ ℕ ( i < 2 ⇒ P(2) ) ⇒ P(2).

No.

That's why I am failing to understand it. I can't see what assertion is being made in each line. I'll keep at it.

You claim you assert P(0). But then you write something completely contrary.

Are you asserting P(1) in the next line?

@user21820 No, I am asserting P(1) given ∀ i ∈ ℕ ( i < 1 ⇒ P(1) ) ⇒ P(1).

Then you are using the word "from" wrongly.

There is absolutely no reason to write "P(2) from P(0) ∧ P(1) ⇒ P(2)" if all you want to assert is "P(0) ∧ P(1) ⇒ P(2)".

@user21820 Lol. Ok.

Besides, both "∀ i ∈ ℕ ( i < 2 ⇒ P(2) ) ⇒ P(2)" and "∀ i ∈ ℕ ( i < 1 ⇒ P(1) ) ⇒ P(1)" are completely different from "∀ i ∈ ℕ ( i < k ⇒ P(i) ) ⇒ P(k)".

Stop using symbols and understand what you are doing first.

@user21820 Ok. I'll stop using them.

Go back to the original goal.

Do it slowly. Make sure you are clear about each step. Your attempt is obviously not clear enough to yourself, otherwise you would know what to do.

I'll take your advice.

Don't try to use any induction. Just use ordinary propositional logic.

Good.

I need to go. Hopefully you can figure it out.

@user21820 Could you explain why is that ?

For me, they are the same. I would like to know, please.

@F.Zer If you just substitute k properly on the third you will not get the first two.

@user21820 Got it. I made a mistake.

∀ i ∈ ℕ ( i < 1 ⇒ P(i) ) ⇒ P(1)

Yes. Anyway that error is not the point.

@user21820 Have a nice day and thank you ! See you !

See you!

:59224528 For example, when k = 3, that line asserts:
  ∀ i ∈ ℕ ( i < 0 ⇒ P(i) ) ⇒ P(0)
∧ ∀ i ∈ ℕ ( i < 1 ⇒ P(i) ) ⇒ P(1)
∧ ∀ i ∈ ℕ ( i < 2 ⇒ P(i) ) ⇒ P(2)
∧ ∀ i ∈ ℕ ( i < 3 ⇒ P(i) ) ⇒ P(3)
⇒ P(3)

That way, I am using all previous lines. However, I should note you suggested not using symbols, but making sure I understand. I'll work on that.