@F.Zer It's correct. But you accidentally used Q before defining it. I guess you put in the "∀ k ∈ ℕ ( Q(k) ⇒ P(k) ):" later and forgot to move the definition before it (and forgot the "If").

By the way, since you mentioned the discreteness lemma, you might as well mention the cancellation lemma that you used just after that.

@user21820 For the second last one can I think we have to use excluded middle?

If I'm not mistaken

@PaxDaga Maybe, but if I answer your question then you won't have "solved it on your own". Why don't you post your solutions first? Then we can discuss them further.

If (b,p) is not coprime
	If (c,p) is not coprime
		.
		.
	If (c,p) is coprime.
		.
		.

@user21820 I am stuck at trying to prove that (b,p) is coprime. Maybe it is supposed to be very easy but not able to finish due to my lack of intuiton about this.Probably thats why I am having to take hints multiple times.

@user21820 Is it correct, now ? Link

@user21820 Is it possible to prove "∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ) ⇒ ∀k ∈ ℕ ∀i∈ℕ ( i<k ⇒ P(i) )" ?

@F.Zer Indeed it's perfect.

@F.Zer Yes it is, and your proof already did it; from "∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) )" you already proved "∀k ∈ ℕ ( Q(k) )".

@Prithubiswas You've to use the relationship between b,c,p and the given condition that b,c are coprime.

I also tried a case split like in my previous message. But that also seems to lead nowhere.

Just makes things more complicated

@Prithubiswas Why doesn't it work?

I don't understand what you're missing; it's supposed to be exactly as you said and nothing much more.

@Prithubiswas: Ah. Did you forget that you can simulate subtraction in PA?

If (b,p) is not coprime.
    b = e.g1
    p = e.g2
    b.u = c + p
    e.g1.u = c + e.g2
    ???

I need to go, but you can refer to the last lemma here (courtesy of F.Zer).

@user21820 I dont know how to simulate substration in PA.

@user21820 Thank you. Is it possible to prove that statement without using induction ?

If (b,p) is not coprime.
    b = e.g1
    p = e.g2
    b.u = c + p
    b.u - p = c
    e.g1.u - e.g2 = c
    e(g1.u - g2) = c
    e | c
    e | b
    (b,c) is not coprime
    [Contradiction]

@user21820 I think I got a proof using substraction. But of course that is NOT allowed in PA. But I dont know how to simulate substration in PA.

@Prithubiswas Whenever you want to do "a−b" where a,b∈ℕ, it means you want to prove that a = b+k for some k∈ℕ.

Here you want to have g1·u−g2, so you need to prove g1·u ≥ g2 and then apply the lemma I cited from F.Zer.

@F.Zer It turns out that it is not possible to prove that using induction. We can see why, because the last part of your proof does not rely on induction and gets from "∀k ∈ ℕ ( Q(k) )" to "∀k ∈ ℕ ( P(k) )", but "∀k ∈ ℕ ( P(k) )" cannot be proven from the given condition without induction.

In my last comment I mean "we can see why intuitively". That comment relies on the claim that strong induction cannot be proven from PA−. This follows from the claim that induction cannot be proven from PA−. I previously tried to give you an idea of why PA− cannot prove (PA1), which shows that PA− cannot prove induction. But it doesn't matter if you don't understand it, because such proofs require understanding up to a certain point in Set Theory, which we haven't gotten to yet.

So for now you can ignore everything I say in these previous two comments except that it's just a fact that PA− cannot prove induction, nor strong induction, nor well-ordering, nor "∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ) ⇒ ∀k ∈ ℕ ∀i∈ℕ ( i<k ⇒ P(i) )" for a general property P. It may be possible to prove it for some special properties P, such as if P(k) ≡ k ≥ 0.

@user21820 Thank you. Is that a typo ? Where you say: "It turns out that it is not possible to prove that using induction". I asked whether we can prove it without using induction.

I proved ∀ k ∈ ℕ ( Q(k) ) from ∀ k ∈ ℕ ( Q(k) ⇒ P(k) ) using induction, I think.

@F.Zer Yes it's a silly typo. I meant "without using induction". Haha..

Too many "not"s put my thoughts into knots.

Haha. That makes sense, now.

@user21820 That's a nice phrase. Has good rhythm.

It was on purpose. =P

:-)

@user21820 Is the indentation issue in Systems solved ?

@F.Zer No. Was there some reason there are lots of spaces in the HTML code itself?

They should look like here.

I will look into it.

@user21820 Could you tell me how are you looking the HTML code ? I'll investigate

@F.Zer I'm just using the browser inspector. I might have recalled wrongly. When I just checked it showed tabs, but it's not the same as my original indentation.

Good. Let me look now.

It's now displaying correctly.

@user21820 The first screenshot shows my GitHub editor, and I don't see different indentation.

@user21820 Good.

You repeated example 1 though the second copy is not supposed to be there.

And that section is about "syntax of properties".

Checking now.

You should also explain the short-form we have been using for "Given x,y,z∈S:", since it's not even mentioned in my post.

@user21820 Are you referring to this ?

**Example 1**

```
Given x∈S:
	Given x∈T:  [forbidden!]
		Q(x) : bool
	∃x∈T ( Q(x) ) : bool
∀x∈S ( ∃x∈T ( Q(x) ) ) : bool
```

**Example 2**

```

Given k∈ℕ:
	?,k : ?term
	? > k : ?bool
	Given d,x∈ℕ:
		1,d,? : ?term
		d·x : ?term
		1 < d , d < ? , ? = d·x : ?bool
		1 < d < ? ∧ ? = d·x : ?bool
	∃d,x∈ℕ ( 1 < d < ? ∧ ? = d·x ) : ?bool
	¬∃d,x∈ℕ ( 1 < d < ? ∧ ? = d·x ) : ?bool
	? > k ∧ ¬∃d,x∈ℕ ( 1 < d < ? ∧ ? = d·x ) : ?bool
```

Yes example 1 already occurs in the correct place earlier.

@user21820 Found it and fixed.

Also, please delete all the random remarks I make like "you don't need to care about that now" and "It's really up to you ... I hope you ...".

Haha.

@user21820 "Please don't delete" ? Didn't you mean "please delete" ?

Yes, I realized later.

Oh, I see you fixed it. Haha

Somehow I keep making negation errors today.

@user21820 Of course ! I will delete all of those !

@user21820 Where should I explain it ?

Also at the "short-forms".

Put all those short-forms together.

Ok.

@user21820 I put it at the bottom; should I place it at the top ?

Bottom is fine.

@user21820 We are using those short-forms earlier. Is that fine ?

@F.Zer Oh did we?

Yes.

Oh whoops haha that's what happens when I explain something after we've already been using short-forms.

Hmm that's a bit of trouble.

It would be ugly to not use the short-forms. On the other hand, it doesn't make sense to use short-forms even before we have specified syntax properly.

Yes, both remarks make sense to me.

Gah... what to do...

Tell you what, just don't use short-forms in the examples of the syntax rules.

At least that makes clear what we are doing at the fundamental level.

So this means in the example for property syntax we would have:

Given k∈ℕ:
	?,k : ?term
	? > k : ?bool
	Given d∈ℕ:
		Given x∈ℕ:
			1,d,? : ?term
			d·x : ?term
			1 < d , d < ? , ? = d·x : ?bool
			1 < d < ? ∧ ? = d·x : ?bool
		∃x∈ℕ ( 1 < d < ? ∧ ? = d·x ) : ?bool
	∃d∈ℕ ∃x∈ℕ ( 1 < d < ? ∧ ? = d·x ) : ?bool
	¬∃d∈ℕ ∃x∈ℕ ( 1 < d < ? ∧ ? = d·x ) : ?bool
	? > k ∧ ¬∃d∈ℕ ∃x∈ℕ ( 1 < d < ? ∧ ? = d·x ) : ?bool

Same for the other example. Wait you forgot all the actual rules!

Given x∈S:
	Given y ∈ S:
		Given z ∈ S:
			y : term  [since x is a used variable]
			? : ?term
			? = y : ?bool

Yes. That is actually the first example.

The other is the second example.

@user21820 Updated both examples without short-forms.

@user21820 Which rules are you referring to ?

Wait. For the syntax rules, remove "The above rules suffice for plain FOL" and the rest of that paragraph, and insert them into the rules themselves:

A : bool ⊢ ¬A : bool
A,B : bool ⊢ A∧B : bool
A,B : bool ⊢ A∨B : bool
A,B : bool ⊢ A⇒B : bool
A,B : bool ⊢ A⇔B : bool
Given x∈S ⊢ x∈S : bool
( Given x∈S ⊢ A : bool ) ⊢ ∀x∈S ( A ) : bool
( Given x∈S ⊢ A : bool ) ⊢ ∃x∈S ( A ) : bool
[v is a used variable] ⊢ v : term
t,u : term ⊢ t=u : bool
t[1],...,t[k] : term ; [f is a k-input function-symbol] ⊢ f(t[1],...,t[k]) : term
t[1],...,t[k] : term ; [Q is a k-input predicate-symbol] ⊢ Q(t[1],...,t[k]) : bool

No point talking about "plain FOL" when we're not interested in describing the difference between the system and plain FOL.

@user21820 Like that ? Should I remove the text between double square brackets ?

I pushed an update.

I made a mistake.

@user21820 Now it is fixed.

@F.Zer Yes.

@F.Zer Hmm just delete, along with the other random remarks.

Done.

@user21820 What should I do when you are speaking directly to me ? Should I leave it as is ? For example, "I've also included the recursive definition of terms in the above rules, just to let you see how one can think of them.".

"Just to let you see..."

Perhaps, it is a good style.

I am not sure.

Mostly they can be deleted, unless you think I'm using "you" to mean "everyone".

And I changed my mind about the "syntax of properties". I think there is no point talking about it at all. You didn't need it when learning the system. And the rules I gave here in chat were only to show (mainly to Prithu) that it's possible to be precise. Even then, those rules only govern 1-input properties.

@user21820 I was mistaken. You were speaking to Prithu. Well, I will delete the irrelevant ones; if they is more than can be deleted, or I deleted more than needed, there is always Git history to change it.

I deleted syntax properties.

Yup and maybe just add one line at the end of the "Syntax" section saying: In each subcontext, a property is simply a (boolean) statement (in that context) except with one or more terms replaced by blanks. Each blank is to be filled with a particular 'input'. For example, we might have a 1-input property Q = "[1] > k ∧ ¬∃d∈ℕ ∃x∈ℕ ( 1 < d < [1] ∧ [1] = d·x )" where each "[1]" denotes a blank for the 1st input to Q, in which case "Q(t)" denotes "t > k ∧ ¬∃d∈ℕ ∃x∈ℕ ( 1 < d < t ∧ t = d·x )".

For another example, we might have a 2-input property R = "[1] < [2] ∨ [1] = [2]" where each "[i]" denotes a blank for the i-th input to R, in which case "R(m,n)" denotes "m < n ∨ m = n".

@F.Zer: Do you think this is clear enough that it is readily understood?

Anyway, I got to go soon. Take a good break, and when you start doing the Cosmic Express puzzles let me know if you get stuck or want to know how I solved them. I can solve the first 128, so I can help you up to that point at least. =)

@user21820 Took some effort but I could understand. It's nice and clean. However, not sure whether would help someone reading it for the first time.

Personally, I would like to have it there.

Great! So include it, and remove the cryptic "By P being a property we mean that P(x) is a statement about x." from the (original) description of the system.

I clearly was lazy when writing that original post.

Let me find it.

It is under "Quantifiers and equality".

Hmm, I used "parameter" there. I think we should also use "parameter" in the explanation I just gave instead of "input".

@user21820 Yes, I found it. I will do that when I copy in ASCII character all your inference rules.

@user21820 Single or double quotes?

You used single quotes in the above message.

@F.Zer I mean don't use the word "input".

Got it.

The reason is that it might be a good idea not to confuse it with the predicate/function-symbols for which "input" is appropriate.

Whereas for properties they aren't really predicate-symbols (and we need to have definitorial expansion to create predicate-symbols to represent properties).

Good. So, it would start as: "In each subcontext, a property is simply a (boolean) statement (in that context) except with one or more terms replaced by blanks. Each blank is to be filled with a particular 'parameter'...."

Yea.

Good. Updated.

@F.Zer Thanks! Alright, see you next time!

@user21820 Thank you very much. Yes, I need it. I spent some time trying to prove Well-ordering from Strong induction but failed. So, I will stop and take a break. If I have troubles with Cosmic Express, I will let you know. Thank you very much and I hope everything goes well for you. See you next time !

Same to you! =)