@user21820, could you tell me whether the proof of the previously discussed lemma is correct ?
I will first prove this Lemma:
∀ S,T ∈ set ( S ≠ T ⇔ ¬∀x ∈ obj ( x ∈ S ⇔ x ∈ T ) ) [Lemma]
Given S,T ∈ set:
If S ≠ T:
If ∀x ∈ obj ( x ∈ S ⇔ x ∈ T ):
∀ S,T ∈ set ( S = T ⇔ ∀x ∈ obj ( x ∈ S ⇔ x ∈ T ) )
S = T
⊥
¬∀x ∈ obj ( x ∈ S ⇔ x ∈ T )
If ¬∀x ∈ obj ( x ∈ S ⇔ x ∈ T ):
If S = T:
∀ S,T ∈ set ( S = T ⇔ ∀x ∈ obj ( x ∈ S ⇔ x ∈ T ) )
∀x ∈ obj ( x ∈ S ⇔ x ∈ T )
⊥
S ≠ T
S ≠ T ⇔ ¬∀x ∈ obj ( x ∈ S ⇔ x ∈ T )
∀ S,T ∈ set ( S ≠ T ⇔ ¬∀x ∈ obj ( x ∈ S ⇔ x ∈ T ) )
And then:
Prove ∀ S ∈ set ( S ≠ ∅ ⇔ ∃ x ∈ obj ( x ∈ S ) ) [Lemma]
Given S ∈ set:
∀ S,T ∈ set ( S ≠ T ⇔ ¬∀x ∈ obj ( x ∈ S ⇔ x ∈ T ) ) [Lemma]
Given S,T ∈ set:
If S ≠ T:
If ∀x ∈ obj ( x ∈ S ⇔ x ∈ T ):
∀ S,T ∈ set ( S = T ⇔ ∀x ∈ obj ( x ∈ S ⇔ x ∈ T ) )
S = T
⊥
¬∀x ∈ obj ( x ∈ S ⇔ x ∈ T )
If ¬∀x ∈ obj ( x ∈ S ⇔ x ∈ T ):
If S = T:
∀ S,T ∈ set ( S = T ⇔ ∀x ∈ obj ( x ∈ S ⇔ x ∈ T ) )
∀x ∈ obj ( x ∈ S ⇔ x ∈ T )
@F.Zer The lemma is correct, but is the kind of thing I would not make a lemma out of, because it's logically trivial. When you're doing ordinary mathematics, you can freely skip FOL subproofs that just use an easy FOL equivalence such as ( A ⇔ B ) ⇒ ( ¬A ⇔ ¬B ).
And this also shows up in the fact that your proof including that of the lemma is a bit bloated compared to what you actually need:
Given S∈set:
If S ≠ ∅:
If ¬∃x∈obj ( x∈S ):
Given y∈obj:
If y∈S:
∃x∈obj ( x∈S ).
⊥.
y∈∅.
If y∈∅:
⊥. [empty-set]
y∈S.
y∈S ⇔ y∈∅.
S=∅.
⊥.
∃x∈obj ( x∈S ).
If ∃x∈obj ( x∈S ):
Let c∈obj such that c∈S.
If S = ∅:
c∈∅.
⊥. [empty-set]
S ≠ ∅.
∀S∈set ( S ≠ ∅ ⇔ ∃x∈obj ( x∈S ) ).
In my proof I didn't even skip FOL equivalences, unlike in your proof where you went from "¬∀x ∈ obj ( x ∈ S ⇔ x ∈ ∅)" to "∃x ∈ obj ( x ∈ S ⇔ x ∉ ∅)". As I said, it's fine to use such equivalences, but my point is that the proof is much shorter than you thought it has to be.
The lesson is that if you want to prove an equivalence that is not an FOL equivalence, such as the desired conclusion here, simply get down to it instead of proving another equivalence, unless you think the other equivalence is more fundamental (and not just an FOL equivalence).
@Prithubiswas Well, it happens to be justified by the restrictions on bound variables. Although I skimmed over it under "Syntax Rules", since that post was for the deductive system rather than teaching the syntax of FOL statements, I did say:
> A statement must be an atomic (indivisible) proposition or a compound statement formed in the usual way using boolean operations or quantifiers, with the restriction that every variable that is bound by a quantifier is not already used to refer to some object in the current context, and that there are no nested quantifiers that bind the same variable.
So "¬∀x∈S(P(x))" would not be syntactically valid unless x does not appear in P in the first place.
Nevertheless, you are correct that in general we can't know that, so you can view the exercise as working under that assumption.
Otherwise "¬∀x∈S(P(x)) ⇒ ∃x∈S(¬P(x))" would not even be a syntactically valid statement, much less something that can be proven.
Anyway, it's good that you're paying attention to this sort of detail! Keep it up!
@user21820 If there is no nested quantifiers that bind the same variable in ¬∀x∈S(P(x)), then wouldn't ¬∀x∈S(P(x)) still be syntactically valid even if x appears in P in the first place. Because , in the proof we are not using x to refer to some object.
@Prithubiswas Do you mean like P(t) ≡ t=x? Then ∀x∈S ( P(x) ) ≡ ∀x∈S ( x=x ) but we cannot rename to ∀y∈S ( P(y) ) ≡ ∀y∈S ( y=x ).
It is important that x does not appear in P at all, so that when you rename x to y, you do not miss any x and there is no conflict with any quantified variables in P.
And I wouldn't consider P(t) ≡ t=x to be a valid definition of P as a property, because in my view there should not be any free variables, so actually this example should not even be considered.
@user21820 So you mean every variable in a property P must be bound by a quantifier.And if ¬∀x∈S(P(x)) and there is an occurrence of x in P , then that means there is also a ∀x in P , and hence there is an ∀x in P(x). So Now we have two ∀x in ¬∀x∈S(P(x)) and the ¬∀x∈S(P(x)) becomes syntactically invalid because "there are no nested quantifiers that bind the same variable".Right?
@Prithubiswas Yes, but actually I meant in the opposite direction.
For example, we can define P(k) ≡ k>1 ∧ ¬∃d,x∈ℕ ( 1<d<k ∧ d·x = k ).
If we treat P as a predicate-symbol, then it is even valid to write "∀x∈ℕ ∃y∈ℕ ( x<y ∧ P(y) )" even though the definition of P uses the variable x.
What does this mean? The ability to define a new predicate-symbol is redundant, but let me simply state what such a rule would say in this specific example: At any point in a proof you can write "∀k∈ℕ ( P(k) ⇔ k>1 ∧ ¬∃d,x∈ℕ ( 1<d<k ∧ d·x = k ) )" where P is a fresh predicate-symbol.
Then there is no trouble at all with something like "∀x∈ℕ ∃y∈ℕ ( x<y ∧ P(y) )". You can easily prove that it is equivalent to "∀x∈ℕ ∃y∈ℕ ( x<y ∧ k>1 ∧ ¬∃d,t∈ℕ ( 1<d<k ∧ d·t = k ) )". Note that I had to rename the inner "x" otherwise it would be syntactically invalid.
I don't know whether you think such a rule is weird or not, where you can anyhow write down a quantified equivalence, but it you think about it you will understand that this rule provides a concrete mechanism for introducing and defining new predicate-symbols in the middle of a proof.
Given this, there is nothing wrong to just treat any "property" in those exercises as just predicate-symbols, and not even care about whether they can be used to represent some actual property (i.e. statement with blanks for the object the property is supposed to describe).
@F.Zer Why should it be? Don't you want an equivalence?
@F.Zer There is actually a way to get fixed-font without the button, if you are using a programming text editor. Just put 4 spaces before every line. That is in fact what the fixed-font button does.
Anyway, here's your attempt, formatted:
Given S ∈ set:
If S ≠ ∅:
∀ S ∈ set ( S ≠ ∅ ⇔ ∃ x ∈ obj ( x ∈ S ) ) [Lemma]
∃ x ∈ obj ( x ∈ S )
Let A ∈ obj such that A ∈ S
Let I' = { x : x ∈ A }
Given x ∈ obj:
If x ∈ I':
Given T ∈ S:
x ∈ T
∀x∈obj ( x∈I' ⇔ ∀T∈S ( x∈T ) )
∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈S ( x∈T ) )
Your attempt cannot be correct, because you want to prove that I' is the intersection of all the sets in S, but obviously it is not (according to your definition of I').
Also, your last line doesn't make sense; it seems to be at the wrong indentation level.
Anyway, the point is that although no rule allows you to get { x : ∀T∈S ( x∈T ) } ∈ set, using a member of S you can adjust it slightly to make the comprehension rule work.
@user21820 I feel like I am failing to understand the Predicate Calculus part of your Natural Deductive (fitch style) system. The fact that I am having so many confusion and so many questions is indicating to me that I might be not in the "right level" to learn your system. I have checked the LPL textbook to learn basic FOL. It might be wrong , but I feel like it is a bit too wordy for me. It has a lot of exercises which requires the program mes provided with the paid version of the book. So I might miss out on a lot of things I could have learned.
@Prithubiswas I don't think there is one. I searched very hard and besides my system and LPL's I didn't find any usable system via the internet. But I don't get why you think you "might not be at the right level". You will never escape the technical details of the quantifier issues, no matter which system. Different systems just hide the complexity in different places. Mine is already the cleanest possible, so I think you should just work through the exercises I gave you.
That's the whole point of the exercises; to make sure you actually know the deductive rules once you are done working through them.
And mathematical background is not needed to learn the system. F.Zer is an example, who has completely finished all the FOL exercises. For you, once you finish the FOL exercises you will have a very big advantage because of your mathematical background, because there are no more rules to learn after that!
You're right that LPL is too wordy; that's why I recommend it only to people who have no mathematical or programming background at all.
@Prithubiswas: If you want my advice, just continue with the exercises. You already learned the PL part much faster and more accurately than other students I have taught in these chat-rooms, so you cannot possibly be unable to learn the FOL part if they could!
@user21820 I kind of prefer to first learn the rules precisely and then proceed with the exercises instead of learning the rules by trial and error. Will it be ok if I first question about every single rule (the syntax , the inference rules etc) of your system in a numerical list and after I feel like I know the system precisely then I will proceed with the exercises?
@Prithubiswas Like A,B,C in the PL exercises. You can ignore that for FOL exercises and onwards, as I never use atomic propositions anymore.
To be more specific, an atomic proposition is a single symbol that stands for a (boolean) sentence with a fixed truth-value. But don't bother about it.
It's for people who want to connect the deductive system to real-world applications, like letting A ≡ ( There is an apple on that table. ) and reasoning about that sentence in relation to other sentences.
(2) I thin in the syntax section of your post , you didn't specify about (something like) what is a variable , constant letters , function letters , how to form terms from them , predicate letters , terms+ predicate letters=atomic sentences , bolean connectives , universal and existensial quantifiers and other logical symbols that are in your system , definitions of free and bound variables etc. But why? (Because I wish to learn the syntax rules specifically to your system)
@Prithubiswas Sure. I will specify it here. My post was already so long that I just wanted to make the deductive system clear, and it worked well enough for most students who didn't want to go into every detail.
We start with some inbuilt predicate/function-symbols (function-symbols including constant-symbols), that are distinct from allowed variable names. We won't bother to explicitly restrict which ASCII characters can be used for which, so just make sure you don't use the same character for different things.
In any context, there are some used variables (as defined in the post). A term is recursively defined as either a used variable or a string with the usual function-application syntax denoting a function-symbol applied to the correct number of terms. For example, if f is a 2-input function-symbol, and t,u are terms, then f(t,u) is also a term.
To be 100% precise, I should actually say: If f is a 2-input function-symbol, and t,u are terms, then f+"("+t+","+u+")" is also a term, where "+" here denotes string concatenation, and double-quotes are used to denote a literal string of symbols.
Do you get the 100% precise version? Most logic texts will use the not-precise version, but since you love precision you might appreciate the 100% precise version.
@user21820 How they are not saying the same thing?Isn't String concatination is just a precise way of telling 'if f is a 2-input function-symbol, and t,u are terms, then f(t,u) is also a term' into 'If f is a 2-input function-symbol, and t,u are terms, then f+"("+t+","+u+")" is also a term'.One is for human intuition and another one is suitable for computers?
@Prithubiswas No. "Prithu" is a 6-letter string, but Prithu is a person. To be truly correct, you must always distinguish the two things. Same with the brackets in the precise and imprecise versions above.
You can say that the imprecise version is for human intuition, but since you want precision I want you to be fully aware of full precision.
Yes, and it's even worse than that, because when we actually study logic we will use expressions with brackets that we need to distinguish from the bracket-symbols used in the logic itself!
For example, to define the meaning of a term t under an interpretation I, we might want to define I( f+"("+t+","+u+")" ) = I(f) ( I(t) , I(u) ).
Right now, my goal is not to teach you to study logic. However, this should at least give you an idea of why precision is really important if you want everything truly correctly done.
> ( 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[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
Here a rule of the form "... ⊢ ..." means from the left-hand stuff you can deduce the right-hand stuff (in the current context), and if you have "( ... ⊢ ... )" in the left-hand stuff it means that you have deduced that kind of subcontext previously. For example we can literally do the following deduction if Q is a 1-input predicate symbol:
Given x∈S:
Q(x) : bool
∀x∈S ( Q(x) ) : bool
All these deductions should never be written out explicitly, but it should be how you think of the syntax rules if you want to be precise. Note that the ∀sub rule ensures you cannot have nested quantification of the same variable. For example you cannot do:
I've also included the recursive definition of terms in the above rules, just to let you see how one can think of them. For instance, if we have the binary operation + we can actually do the following deduction:
Given x,y,z∈ℕ:
x,y,z : term
x+y : term
(x+y)+z : term
Of course, please don't concern yourself now with the actual syntax of binary operations, whether infix or prefix. We do not want to have to write "+(+(x,y),z)" just to make it fit the above rules completely!
Just understand the structural idea.
The above rules suffice for plain FOL. For my version of many-sorted FOL, we just need one more:
> ( Given x∈S ⊢ x∈S : bool ).
Oh I forgot, you also need syntax rules for equality:
@Prithubiswas I should think so. Do you have any questions about them?
In particular, you can view the ⇒sub rule as really ( A : bool ⊢ ( If A: ⊢ A. ) ). That is, we are only justified to create an "If A:" subcontext if we can deduce that A is a boolean statement.
@F.Zer It's actually quite simple; you already know that the intersection is supposed to be contained in each member of S, and you even obtained one in your attempt. Why not just use that to match the form required by the comprehension rule?
Well... it's just one step, but you can't seem to find the trick, not sure whether it's lack of experience or not but let's not waste time on this trick... Let I' = { x : x∈A ∧ ∀T∈S ( x∈T ) }.
You should be able to complete the rest of the proof now.
@user21820 Could you explain, please ? I already noted x ∈ A, but ∀T∈S ( x∈T ) is the intersection of S...So, the x such that x ∈ A and x belongs to the intersection ?
@user21820 Of course, my question is a very frequent one among beginners but...isn't there circularity ?
@user21820 This kind of trick are really unfamiliar to me. I feel like I am defining the set as the set I want to prove. Could you give me some insight into this frequent misconception ?
@F.Zer I don't understand what you're missing. You started:
Given S ∈ set:
If S ≠ ∅:
∀ S ∈ set ( S ≠ ∅ ⇔ ∃ x ∈ obj ( x ∈ S ) ). [Lemma]
∃ x ∈ obj ( x ∈ S ).
Let A ∈ obj such that A ∈ S.
Let I' = { x : x ∈ A }. [but this I' is useless because it is just A]
I am telling you what I' you need to be able to prove what you want.
ZFC is dumb this way, but that's what those logicians came up with to avoid Russell's paradox while keeping what they wanted to do. I do not think full ZFC is meaningful, but it's what modern mathematicians use.
You already saw the proof that if you assume { x : ∀T∈∅ ( x∈T ) } ∈ set you get a contradiction, and that is blocked if comprehension needs the set you are constructing to be a subset of some existing set.
@user21820 Oh, I would like to ask you: do you think trying to use "pedestrian intuition" is not always useful while doing mathematical proofs ? I mean, sometimes I should use something that works (using what I have) although that may seem counterintuitive. I mean, people who don't have mathematical training, often seem to find some mathematical deductions or tricks unintuitive. Or, perhaps we are trained in an un-logical way :-)
@user21820 Oh, x belongs to A and x belongs to the intersection of S. That's not the same as I said before.
I mean, if something isn't prohibited, it is allowed in math. If there is some rule allowing it, I can do it. That's it. Does it make sense ?
@F.Zer Proofs in ZFC are just proofs in ZFC, and may not have any meaning whatsoever, much less match intuition. However, proofs in more ordinary mathematics do have more meaning and are more amenable to intuition, especially mathematics that can be handled by a weak extension of PA that only deals with naturals and sets of naturals.
Prove ∀S∈set ( S≠∅ ⇒ ∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈S ( x∈T ) ) )
Given S ∈ set:
If S ≠ ∅:
∀ S ∈ set ( S ≠ ∅ ⇔ ∃ x ∈ obj ( x ∈ S ) ) [Lemma]
∃ x ∈ obj ( x ∈ S )
Let A ∈ obj such that A ∈ S
Let I' = { x : x ∈ A ∧ ∀ T ∈ S ( x ∈ T ) }
Given x ∈ obj:
If x ∈ I':
x ∈ A ∧ ∀ T ∈ S ( x ∈ T ) [type-notation]
∀ T ∈ S ( x ∈ T )
If ∀ T ∈ S ( x ∈ T ):
x ∈ A
x ∈ A ∧ ∀ T ∈ S ( x ∈ T )
x ∈ I' [type-notation]
∀x∈obj ( x∈I' ⇔ ∀T∈S ( x∈T ) )
@F.Zer You didn't say I'∈set. Also, note that although I said you can use "Let v = E." where E is an object expression and v is a fresh variable, that only applies to objects. Types are not necessarily objects. I'll of course let you do so for types as well, but don't forget that the "=" there is not equality.
I'm picky because you must know exactly what is going on. At that point you can do the following:
{ x : x ∈ A ∧ ∀ T ∈ S ( x ∈ T ) } ∈ set. [comprehension]
{ x : x ∈ A ∧ ∀ T ∈ S ( x ∈ T ) } ∈ obj.
Let I' = { x : x ∈ A ∧ ∀ T ∈ S ( x ∈ T ) }. [for convenience]
You can omit the first two lines, but at least mark the third one with "comprehension" so that I know you checked.
@F.Zer Other than my picky point, the proof is correct.
Prove ∀S∈set ( S≠∅ ⇒ ∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈S ( x∈T ) ) ) [Lemma]
Given S ∈ set:
If S ≠ ∅:
∀ S ∈ set ( S ≠ ∅ ⇔ ∃ x ∈ obj ( x ∈ S ) ) [Lemma]
∃ x ∈ obj ( x ∈ S )
Let A ∈ obj such that A ∈ S
A ∈ S
{ x : x ∈ A ∧ ∀ T ∈ S ( x ∈ T ) } ∈ set [comprehension]
∀x∈set ( x∈obj ) [Lemma]
{ x : x ∈ A ∧ ∀ T ∈ S ( x ∈ T ) } ∈ obj
Let I' = { x : x ∈ A ∧ ∀ T ∈ S ( x ∈ T ) }
Given x ∈ obj:
If x ∈ I':
x ∈ A ∧ ∀ T ∈ S ( x ∈ T ) [type-notation]
@user21820 I appreciate you being picky. I learn better that way. One question: isn't the "=" there equality ? Why do you say so ? We previously discussed that we could replace each occurrence of v by E. Aren't we using =elim in that operation ?
> we can extend the base formal system to include the rule that in any context you can write "[Let ]v = E." whenever E is an object expression and v is a fresh variable.
@F.Zer You didn't say I'∈set. Also, note that although I said you can use "Let v = E." where E is an object expression and v is a fresh variable, that only applies to objects. Types are not necessarily objects. I'll of course let you do so for types as well, but don't forget that the "=" there is not equality.
If you insert those two lines I stated above, then you are using =elim. Without those two lines, I didn't even permit you to write "I' = ..." in the first place.
@user21820 Oh, sorry. I' is a type. "=" is equality between objects. I first prove I' is an object. Then, I can write "I' = ..." and perform replacements using =elim. Does this seem right ?
So, although I will allow you to write your proof exactly as you did, you should indicate on that line that you use comprehension to guarantee that it is a set (which is an object).
@user21820, I leave here the proof of the theorem using the correct version of intersection. Do you think it is headed in the right direction ?
Theorem. Suppose F and G are families of sets, and F ⋂ G ≠ ∅. Then ⋂F ⊆ ⋃G.
Given F,G ∈ set:
If F ⋂ G ≠ ∅:
∀ S ∈ set ( S ≠ ∅ ⇔ ∃ x ∈ obj ( x ∈ S ) ) [Lemma]
∃ x ∈ obj ( x ∈ F ⋂ G )
Let a ∈ obj such that a ∈ F ⋂ G
a ∈ F
∃ x ∈ obj ( x ∈ F )
F ≠ ∅
∀S∈set ( S≠∅ ⇒ ∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈S ( x∈T ) ) ) [Lemma]
Given a ∈ ⋂(F):
...
∀ S ∈ set ( ⋃(S) = { x : ∃T ∈ set ( T ∈ S ∧ x ∈ T ) } ) [union]
⋃(G) = { x : ∃ T ∈ set ( T ∈ G ∧ x ∈ T ) }
Theorem. Suppose F and G are families of sets, and F ⋂ G ≠ ∅. Then Intersect(F) ⊆ Union(G).
Given F,G ∈ set:
If F ⋂ G ≠ ∅:
∀ S ∈ set ( S ≠ ∅ ⇔ ∃ x ∈ obj ( x ∈ S ) ) [Lemma]
∃ x ∈ obj ( x ∈ F ⋂ G )
Let a ∈ obj such that a ∈ F ⋂ G
a ∈ F
∃ x ∈ obj ( x ∈ F )
F ≠ ∅
∀ S ∈ set ( S≠∅ ⇒ Intersect(S) = { x : ∀T∈S ( x∈T ) } ) [intersection]
Intersect(F) = { x : ∀T∈F ( x∈T ) }
Given a ∈ Intersect(F):
∀T∈F ( x∈T )
...
∀ S ∈ set ( Union(S) = { x : ∃T ∈ set ( T ∈ S ∧ x ∈ T ) } ) [union]
