@user21820 I apologise for pasting fragments without the context. I've just developed an automation to derive a subtree with governing contexts.

Given n∈ℕ:
  ∀i∈ℕ ( i < n ⇒ Q(i) ):
    Given k,m∈ℕ:
      If k+m = n:
        If m > 1 ∧ ¬∃d∈ℕ ( d > 1 ∧ d | k ∧ d | m ):
          If k < m:
            If k = 1:
              r < k

I didn't want to derive Q(k) — I just tried to put all the information I could derive below "If k = 1:"

I'll continue thinking.

@user21820, I am inside the case "If k = 1:". I noticed 1 is coprime with every natural number. So, no matter which m I pick, this holds: ¬∃d∈ℕ ( d > 1 ∧ d | k ∧ d | m ).

> In particular, why did you not fill in the later goals that you want for strong induction?

@user21820 I will do that, now.

(PA5):
  Define Q(n) ≡ ∀k,m∈ℕ ( k+m = n ⇒ ( m > 1 ∧ ¬∃d∈ℕ ( d > 1 ∧ d | k ∧ d | m ) ⇒ ∃x,y∈ℕ ( k·x = m·y+1 ) ) )
  Given n∈ℕ:
    ∀i∈ℕ ( i < n ⇒ Q(i) ):
      Given k,m∈ℕ:
        If k+m = n:
          If m > 1 ∧ ¬∃d∈ℕ ( d > 1 ∧ d | k ∧ d | m ):
            If k = m:
            k ≠ m.
            [Prove ∃x,y ∈ ℕ ( k·x = m·y + 1 ) ]
            If k < m:
            If k > m:
            ∃x,y∈ℕ ( k·x = m·y+1 )
        k+m = n ⇒ ( m > 1 ∧ ¬∃d∈ℕ ( d > 1 ∧ d | k ∧ d | m ) ⇒ ∃x,y∈ℕ ( k·x = m·y+1 ) )

Exactly, so the "If k = 1" case is obvious!!

@user21820 I'll think :-)

Given n∈ℕ:
  ∀i∈ℕ ( i < n ⇒ Q(i) ):
    Given k,m∈ℕ:
      If k+m = n:
        If m > 1 ∧ ¬∃d∈ℕ ( d > 1 ∧ d | k ∧ d | m ):
          If k < m:
            If k = 1:
              1·1 = m·0+1
              k·0 = m·0+1
              ∃x,y∈ℕ ( k·x = m·y+1 ) )

@user21820 Like this ?

@F.Zer k·0??

@user21820 I want to learn your fitch-style deductive system before learning Mathematical Logic.Would that be ok?

@user21820 Lol !

@user21820 k·1

@F.Zer Right. So that case is done. Carry on!

@user21820 I've used the equality "1 = 0" :-)

@F.Zer That's bad! =)

@user21820 Good ! I'll continue.

@Prithubiswas Sure. My approach is very simple; you just do some exercises, proving theorems in the system. The exercises will help you to learn all the technical details of the deductive system and also help you in logical thinking. The exercises are:

FOL (First-Order Logic):

For (Q6) to (Q10), S,T,B,G,V are types, and "f : S→T" denotes "f is a 1-input function-symbol whose input must be of type S and whose output is of type T, and "f : S^2→T" denotes "f is a 2-input function-symbol whose inputs are both of type S and whose output is of type T". Note that if the output type is Bool then it denotes a predicate-symbol instead of a function-symbol.

PA (Peano Arithmetic):

Then we have exercises for PA (which includes induction).

@Prithubiswas: Simply post your proof attempt here and I will check and give feedback. If you get stuck, let me know and I'll give hints.

@user21820 I have printed the entire post where you have given the instructions of your fitch-style deduction and right now reading it to understand how to use the system precisely.

@user21820 thanks!

@nolemonnomelon You're welcome!

@Prithubiswas You can read the different sections in that post in stages. You can start doing the PL exercises using the rules up to "Boolean operations". The rules up to "Quantifiers and Equality" are enough for all the FOL exercise. You can look at "Example" along the way, and you can ignore "Notes". For the PA exercises you need the axioms from "Peano Arithmetic". You do not need anything from "Set Theory" onwards for the above exercises, so skip them for now. Feel free to clarify any point.

@user21820 Can you show me a dummy proof to show how to exactly indent in fitch-style?

I am asking this because I dont know that much about indentation.

@Prithubiswas The rules themselves (⇒sub and ∀sub) govern when you can indent; you can only create context-headers using those two rules, and whatever you write under those headers are considered as statements in those subcontexts.

The underlying idea is simply that you should only write statements that are true in their context, and the context of a statement is given by the context-headers that govern it. The rules are just a way of enforcing this idea.

That's why the ⇒sub rule says that under "If A:" you can write "A.". After all, that's the meaning of "subcontext in which A holds".

Same for the ∀sub rule.

@user21820, could you please explain how did you do step [5] ?

If k > 1: [1]
  [Prove ∃x,y∈ℕ ( k·x = m·y+1 )]  [2]
  Let p,q∈ℕ such that r·p = k·q+1.  [3]
  k·(x·p) = m·p+r·p = m·p+k·q+1.  [4]
  Let s∈ℕ such that x·p = q+s.  [5]
  k·s = m·p+1.  [using cancellation]  [6]
  ... [7]

Oh, I think I've figured it out. Will post shortly.

@user21820, I think I had figured it out but couldn't.

@user21820 Good. But where is the existential statement allowing "Let s ∈ ℕ..." ?

It is clear that "If k > 1:" should be there, I think.

@F.Zer Did you attempt to follow my last quoted comment?

> I cannot use Q(r+k) without ...

@user21820 Of course !

Then why can't you get the existential?

If you used Q(r+k), why did you not write down what you got?

@user21820, you used that existential here: "Let p,q∈ℕ such that r·p = k·q+1."

I will closely review my notes. Something is confusing me.

This is the existential obtained from Q(r + k): ∃x,y∈ℕ ( k·x = m·y+1 )

It doesn't have the form: x·p = q+s.

I realise my step [2] is incorrect: [Prove ∃x,y∈ℕ ( k·x = m·y+1 )] [2]. I do have that statement. I don't need proving it.

@user21820, so the case "If k > 1:" is trivial; I should simply write "∃x,y∈ℕ ( k·x = m·y+1 )"

Everything I've said above is wrong.

For a moment, I got confused about the whole thing.

@F.Zer You're right. I didn't realize you were not talking about the result of applying Q(r+k).

Q(r+k) gives (2), but does not give (5).

This is the existential I obtained from Q(r + k): ∃x,y∈ℕ ( r·x = k·y+1 )

Yes, so I haven't answered your question.

(5) comes from the usual method to do subtraction in PA−.

You will need (5) to get (6).

Good. Thank you. It's clear for me how you went from (5) to (6).

Of course, you need to prove something in-between (4) and (5) to justify (5). I missed out that "...".

I'll try to figure out how you did the subtraction.

It's just what you would want to do to get from (4) to the goal.

If (A∨(B∧C)):
   (A∨(B∧C))
   If A:
      A
      (A∨B)
      A
      (A∨C)
      (A∨B)
      (A∨C)
      ((A∨B)∧(A∨C))
   (A⇒((A∨B)∧(A∨C)))
   If (B∧C):
      (B∧C)
      B
      C
      B
      (A∨B)
      C
      (A∨C)
      (A∨B)
      (A∨C)
      ((A∨B)∧(A∨C))
   ((B∧C)⇒((A∨B)∧(A∨C)))
   (A∨(B∧C))
   (A⇒((A∨B)∧(A∨C)))
   ((B∧C)⇒((A∨B)∧(A∨C)))
   ((A∨B)∧(A∨C))
((A∨(B∧C))⇒((A∨B)∧(A∨C)))

@user21820 Here is my attempt on the first half of (P1). inform if there are any errors.

@Prithubiswas That's right! And to make things easier, from now on just omit all lines that are marked with square-brackets in my post, which are (as noted) redundant in the sense that they can be systematically figured out from the remaining lines.

@user21820 I thought I was going to make so many mistakes...

@Prithubiswas Oh why? You're good enough to do the two induction test questions, so you should not have much trouble with these FOL exercises, in the sense that it's just a very simple language for you to learn.

Also, you do not need to put brackets around everything; the standard precedence rules are (highest to lowest): ¬,∧,∨,{⇒,⇔}.

Note that you can also easily deduce "(A∧B)∧C" from "A∧(B∧C)" and vice versa (using the base rules), and same for ∨, so you can also omit the brackets for a conjunction chain or a disjunction chain.

@user21820 Well from now on I will not put lines which are in square brackets because they are redundant. And sure I wont put brackets everywhere.

Yup carry on! (P1) to (P5) should be a breeze for you. (Q1) to (Q5) should not be too hard either. (Q6) to (Q10) may become slightly challenging.

@Joe: Hello and welcome! If you would like to learn to use that Fitch-style deductive system, you are also invited to try the same list of exercises above together with Prithu.

@Joe: Sorry, I mixed you up with another Joe who expressed interest in that just yesterday...

Alright I'm off now.

@user21820: No problem. Sorry, if this is off-topic, but I was reading the comments to a post from a few years back, and I remember you saying that most students wouldn't be able to prove that $-1 \cdot x = -x$ using the field axioms. I tried coming up with a proof myself. Is it okay if you check it?

@Joe Sure. Just post it here.

$-1$ is defined as the additive inverse of $1$, and so $-1+1=0$. Then, multiply both sides by $x$ to get $(-1+1)\cdot x = 0 \cdot x$.

Use the distributive property and the zero product property to get that $(-1 \cdot x) + (1 \cdot x) = 0$

Use the fact that $1$ is the multiplicative identity to simplify this to $(-1 \cdot x)+ x = 0$.

Then, add $-x$ (the additive inverse of $x$) to both sides: $((-1 \cdot x)+x)+(-x)=0+(-x)$

Use the fact that addition is associative to get $(-1 \cdot x)+(x+(-x))=-x$ (also using the fact that $0$ is the additive identity)

So $(-1 \cdot x)+0=-x$, and the result follows

Is that correct, @user21820?

@Joe The zero-product property is not usually a field axiom.

@user21820: Oh, sorry I forgot that it was derived from $(0 + 0) \cdot x = 0 \cdot x$.

@Joe Exactly. So if you put everything together, then you have a proof.

I don't know which comment of mine you're referring to, but I probably was making the point that students who are not taught (basic) logic properly do not understand that (−1)·x is not −(1·x) by fiat.

And as saw in your proof it's not a completely trivial thing to get that.

:58609300 I can see what you deleted and it seems correct. Did you see an error?

@user21820: It's sad that this is the case. My suspicion is that, at University, if you asked a student to prove that $-1 \cdot x = -x$, they would feel patronised for being asked to prove such a "basic" fact. Of course, it is not a basic fact! At least, it is not completely trivial to prove

@user21820 I didn't want to interrupt the conversation. Thank you for checking :-)

@user21820 Do you think it is necessary to justify the contradiction arising from "k·q > k·q+m·p+1" or it is perhaps too obvious ?

@Joe Yea. That's a problem I've griped about for years. Incidentally, there has been a gradual increase in professors starting to teach Fitch-style natural deduction to address the lack of basic logical reasoning among mathematics students. For example, see this thread:

The discussion in the comments continued in the Logic chat-room, and later on Steven Gubkin actually wrote up a document for students and we briefly discussed it.

@user21820: Thanks for the link!

So Steven is now one of those who are helping to contribute to fixing this pedagogical problem. =)

(Although he didn't go all the way to a formal Fitch-style system, the Fitch syntax is definitely in the right direction in my opinion.)

@F.Zer You could get ... > k·q from the PA− axioms if you wish.

Alright I really need to go now. Talk to you all next time! =)

@user21820 Perhaps for another time, but I would like to ask you: how do you setup quick proofs like this one ? Do you symbolise the proof as, for example: "∀ x, y ∈ ℕ ( x > x + y ⇒ ⊥ )" and proceed with the proof ? I'd like to know about best practices, if possible.

Seems quick enough to closely represent the statement as a conditional and (using the axioms) reaching the contradiction. However, not sure if this would be confusing in the long run.

If q > x·p:
  k·q > k·x·p
  k·q > m·p+k·q+1
  k·q > k·q+m·p+1
  If m·p+1 = 0:
    k·q > k·q
    ⊥
  If m·p+1 > 0:
    k·q + m·p+1 > k·q + 0
    k·q > k·q
    ⊥
  ⊥

@user21820 Here is my proof only using PA- axioms.

An alternative would be proving the following lemma...

∀ x,y,c ∈ ℕ ( x + z < y + z ⇒ x < y) [Lemma]
  Given x,y,c ∈ ℕ:
    If x + z < y + z:
      If x ≥ y:
        x + z ≥ y + z
        If x + z = y + z:
          y + z < y + z
          ⊥
        If x + z < y + z:
          x + z < x + z
          ⊥
        ⊥
      x < y
  ∀ x,y,c ∈ ℕ ( x + z < y + z ⇒ x < z)

And then invoking it:

If q > x·p:
  k·q > k·x·p
  k·q > m·p+k·q+1
  k·q > k·q+m·p+1
  ∀ x,y,c ∈ ℕ ( x + z < y + z ⇒ x < y ) [Lemma]
  0 > m·p+1
  ⊥