@F.Zer Your A,B,C,a are all undefined. If textbooks don't declare them, you still must, otherwise your first line is invalid because "A ⋂ C ⊆ B ∧ a ∈ C" is not a boolean statement.

Once you add the appropriate additional context-headers, your outline would be correct.

@user21820 If someone claims that they have a solution to an open problem and posts their solution in MSE , how does the community react?

@Prithubiswas According to the moderators, it should be closed as off-topic because it's an open problem.

Just post your request in the CURED chat-room and people there will handle it.

@user21820 this might be weird , but what if , for an open problem they have to follow the criteria that they have to write the solution in a conventional deductive system and then post it ?

@Prithubiswas Then they wouldn't need to post it here at all because they would know it is correct. The problem with most mathematicians today is that they do not write proofs in a deductive system, but make many intuitive leaps. If everyone stuck to computer-assisted proofs there would be zero need for peer-review in mathematics.

But as of today, proof assistants are still not user-friendly enough, so it's not surprising that few want to use them.

We'll have to wait for future improvements.

@user21820 Thank you. Is this correct ?

Theorem. Suppose A  ⋂ C  ⊆ B and a ∈ C. Then a ∉ A \ B.
  Given A, B, C ∈ set, a ∈ C:
    If A ⋂ C ⊆ B ∧ a ∈ C:
      If a ∈ A \ B:
        A ⋂ C  ⊆ B
        ∀ x ∈ A ⋂ C ( x ∈ B )
        ...
        ⊥
      a ∉ A \ B
   ∀ A, B, C ∈ set, a ∈ C ( A  ⋂ C  ⊆ B and a ∈ C ⇒ a ∉ A \ B )

@F.Zer That's better, though I never permitted you to use comma between ∀-quantification over objects of different types, so I don't accept your last line, and your first line should be understood as two separate subcontexts. Also note that you have "a∈C" in two places. Although they are compatible, they have different meaning.

Your attempt corresponds to:

Given A,B,C∈set:
  Given a∈C:
    ...
∀A,B,C∈set ∀a∈C ( ... ).

I do allow you to shorten the subcontexts to:

Given A,B,C∈set and a∈C:
  ...
∀A,B,C∈set ∀a∈C ( ... ).

But do remember that it is just a short-hand for the expanded version. In particular, the "and" is not conjunction.

Take note; in my system the "Given a∈C:" is allowed only because of the rule that says we can use any set as a type. Without that rule, it is not allowed. That's also why you cannot switch the order of the ∀subcontexts.

Since "Given a∈C" already declares a∈C, there is no reason to include "a∈C" in the if-subcontext.

Given A,B,C∈set:
  Given a∈C:
    If A⋂C ⊆ B:
      ...
      a∉A∖B.
∀A,B,C∈set ∀a∈C ( ... ).

This is the proper outline. You may shorten it to:

Given A,B,C∈set and a∈C:
  If A⋂C ⊆ B:
    ...
    a∉A∖B.
∀A,B,C∈set ∀a∈C ( ... ).

There is a second alternative:

Given A,B,C∈set and a∈obj:
  If A⋂C ⊆ B ∧ a∈C:
    ...
    a∉A∖B.
∀A,B,C∈set ∀a∈obj ( ... ).

Choose whichever version you prefer. They reach slightly different but equivalent conclusions, so it's up to your aesthetic preference. Do note that in the second version the order of the ∀subcontexts can actually be switched, since both set and obj are already predefined types.

Switching would have produced the conclusion:

∀a∈obj ∀A,B,C∈set ( ... ).

The first version's conclusion cannot have the ∀-quantifiers switched, because "∀a∈C" at the front is simply illegal since "C" is not a type in the outermost context.

Thank you so much, @user21820. I’ll review your explanations carefully.

You're welcome!

@user21820 Wow. I almost understood your whole explanation on a first read. Good teaching. I have one question, thought. Could you clarify this quote ?

I don't know what you mean. I didn't quote anything.

@user21820 I specifically replied to one of your posts; I do not know the technical term. Sorry.

Should I say the replied message, perhaps ?

@F.Zer Oh just use "message" or "statement".

Good.

Just look at the ∀sub rule. It requires you to have an existing type, as well as to use an unused variable.

So in that proof corresponding to your attempt, line 2 is permitted only because line 1 declares C as a set, and the rules under "Set Theory" say every set can be used as a type.

That's also why in all the FOL exercises I explicitly state what types exist.

@user21820 Oh, so I can't have "Given x:" since x doesn't have a type ? The text preceding the rule forbids that. Am I understanding it correctly ?

Well, really the rule itself says "Given x ∈ S:".

@F.Zer Yes my system doesn't allow that. It's intentionally to make you aware of the type of every object.

@F.Zer Exactly.

I do let you quantify over all objects, by providing the type obj, so that's why we can use them in the second version above.

@user21820 That's good. My previous system didn't have types whatsoever.

@user21820 By "quantify over all objects", I presume when saying "a ∈ obj" it only means a is a well-formed expression (variable or expression). Now, can I take any letter and use it as a set. So, in any header I can say, for example, "Given a ∈ W:" ?

So, what's the use of obj if we can already use any letter as a set ?

@F.Zer When did I say you can take any letter as a set??

@user21820 I missed the question mark :-)

@user21820, I should say...can I take any letter and use it as a set in context headers ? If so, what's the use of obj if we can already use any letter as a set ? At any point, I could perhaps say "Given a ∈ W:".

I still don't understand why you're asking. If my system doesn't permit you to do something, you just don't do it.

If you think my system permits you to write something, you should explicitly point to the rule that says so. Otherwise, you can't write it.

@user21820 Of course, that is clear. The thing is: I scanned your whole post and missed this. Which letters can I use as a set ?

Only uppercase A-Z ?

I am not fully clear about the distinction between "set" and "obj", yet. Are the elements of the former collections and the latter well-formed expressions (variables or expressions) ?

@F.Zer Uh? I said already that both of them are inbuilt types, but how they differ is purely a matter of what you are permitted to write with them. Don't you see many axioms under "Set Theory"? They are about set and obj. So I have no idea what you are even asking. It's like asking about the distinction between "obj" and "ℕ"...

@user21820 Good. For a moment, I thought things were more complicated in that regard. But that clears up the issue.

It would be wrong to think of "set" as the type of "collections", because not every thing that could reasonably be viewed as a collection can be considered a member of set. That's why you first of all have to just obey the rules. The rule I was talking about says that every member of set is a type. Do you see that rule, to begin with?

There is no rule about members of obj having any special status, because why should there be?

@user21820 "Add the type set and the rule that every member of set is also a type"

Yes. That's it.

@user21820 That's precisely the thing that confused me.

Lol?

@user21820 I see now not every member of set is a collection.

I am referring to that.

@F.Zer What?

I don't understand how you can keep misreading what I write.

@user21820 "not every thing that could reasonably be viewed as a collection can be considered a member of set"

Is a collection. Could be viewed as a collection

Sorry.

@F.Zer That is completely not what you just said.

Mmm...Let me think about the distinction.

Analogy: I say "Not every animal can be considered a human.". You say "Not every human can be considered an animal.".

Are you.. er.. thinking clearly today?

@user21820 Apparently, not. I am having two very tough days.

Really hard health issues.

@user21820 Got it.

@F.Zer Oh I'm sad to hear that. Maybe you should not push yourself to do this set theory while you're sick, and rest more instead.

@user21820 Thank you very much. I have the exercise almost finished. I'll post it and rest a bit.

Ok sure. Whatever it is, try to drink more water/tea/juice and rest well!

Thank you. I am trying to hidrate myself.

@F.Zer Hang on. That analogy was not an exercise for you to prove, because it is an analogy to show you that your reasoning was invalid.

And in the real world, what I say is true but what you say is false, so you can't possibly get what you say from what I say.

@user21820 Yes, they are saying different things.

In no way they are equivalent statements.

There isn't even a one direction implication between them.

Theorem. Suppose A ⋂ C ⊆ B and a ∈ C. Then a ∉ A \ B.
  Given A,B,C∈set:
    Given a∈C:
      If A⋂C ⊆ B:
        ∀ x ∈ A⋂C ( x ∈ B )
        If a ∈ A∖B:
          a ∈ A ∧ a ∉ B
          a ∈ A ∧ a ∈ C
          a ∈ A⋂C
          a ∈ B
          a ∉ B
          ⊥
        a∉A∖B.
    ∀a∈C ( A⋂C ⊆ B ⇒ a∉A∖B )
  ∀A,B,C∈set ∀a∈C ( A⋂C ⊆ B ⇒ a∉A∖B )

@user21820, this is my proof. What do you think ?

@F.Zer That's correct!

Now, have a good rest! =)

@user21820 Thank you ! Will rest. Take care and have a good day !

@F.Zer Thanks and you too!

Theorem. If x^2 + y = 13 and y ≠ 4 then x ≠ 3.
  Given x,y ∈ ℕ:
    If x^2 + y = 13 ∧ y ≠ 4:
      If x = 3:
        9 + y = 13
        (-9) + 9 + y = (-9) + 13
        y = 4
        y ≠ 4
        ⊥
      x ≠ 3
  ∀ x,y ∈ ℕ ( x^2 + y = 13 ∧ y ≠ 4 ⇒ x ≠ 3 )

Theorem. If x^2 + y = 13 and y ≠ 4 then x ≠ 3.
  Given x,y ∈ ℕ:
    If x^2 + y = 13 ∧ y ≠ 4:
      If x = 3:
        9 + y = 13
        y < 4 ⋁ y > 4
        If y < 4:
          9 + y < 9 + 4
          9 + y < 13
          13 < 13
          ⊥
        If y > 4:
          9 + y > 9 + 4
          9 + y > 13
          13 > 13
          ⊥
        ⊥
      x ≠ 3
  ∀ x,y ∈ ℕ ( x^2 + y = 13 ∧ y ≠ 4 ⇒ x ≠ 3 )

@user21820, The first of the two approaches doesn't convince me very much. PA doesn't define subtraction. The second one seems better, although is longer. Which one do you prefer ?