@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 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.
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.
@user21820 Wow. I almost understood your whole explanation on a first read. Good teaching. I have one question, thought. Could you clarify this quote ?
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 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 ?
@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:".
@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 "ℕ"...
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?
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 )
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 ?
