Basic Mathematics - 2021-07-26

« first day (1175 days earlier) ← previous day next day → last day (1013 days later) »

shintuku

12:25 AM

@user21820 oh, right thanks a lot!

3 hours later…

Prithu biswas

3:55 AM

@user21820 @F.Zer Well , I actually didn't solve it on my own. I wasn't able to solve Q3 so I decided to see what F.Zer has did on Q3. There was a contradiction technique at the middle of F.Zers proof which I would have not figured out by myself.Full credit goes to F.Zer.

9 hours later…

F. Zer

1:20 PM

@Prithubiswas I appreciate it, Prithu.

F. Zer

1:50 PM

Theorem. ∀F,G∈fset ( F⋂G≠∅ ⇒ Intersect(F)⊆Union(G) )
  Define nset to be the type { S : S∈set ∧ ∃A∈set ( A∈S ) }
  Define fset to be the type { S : S∈set ∧ ∀x∈obj ( x∈S ⇒ x∈set ) }
  ∀S∈set ∀x∈obj ( x∈Union(S) ⇔ ∃T∈set ( T∈S ∧ x∈T ) )
  ∀S∈nset ∀x∈obj ( x∈Intersect(S) ⇔ ∀T∈set ( T∈S ⇒ x∈T ) ) [Lemma]
  x∈obj ; [S is a type] ⊢ x∈S : bool
  Given F,G ∈ fset:
    If F⋂G≠∅:
      Given x ∈ Intersect(F):
        ∃ x ∈ obj ( x ∈ F ⋂ G )
        Let A ∈ obj such that A ∈ F ⋂ G
        A ∈ F ∧ A ∈ G
        A ∈ F

@user21820, this is the full proof using your recent additions. What do you think ?

3 hours later…

user21820

5:07 PM

@F.Zer The idea is right, but your "∃A∈set ( A∈F )" is wrong because A is a used variable...

Also, what is "x∈obj ; [S is a type] ⊢ x∈S : bool " doing in the middle of the proof??

@F.Zer All the rule is saying is that if you have "x∈obj" and you have a type S then you can use "x∈S" as a boolean statement. You may have already assumed that previously, but I hadn't.

F. Zer

@user21820 Oh, I derived "∃A∈set ( A∈F )" using rename rule. Is this still incorrect ? I did it that way since ∃ I requires an unused variable.

@user21820 That was part of my notes. I will delete it.

user21820

@F.Zer Didn't you read the same restriction for ∃rename?

F. Zer

@user21820 Sorry, just checked and it's there.

user21820

Anyway your A already means something; how can you use if for something else?

F. Zer

@user21820 Is this better ?

...
A ∈ set ∧ A ∈ F
∃ X ∈ set ( X ∈ F )
F ∈ set ∧ ∃X∈set ( X∈F )
F ∈ { S : S∈set ∧ ∃X∈set ( X∈S ) }
...

user21820

5:18 PM

@F.Zer Either you don't use A earlier, or you do what you just suggested, but in the latter case you must know why you don't have to use exactly the same variables to get membership in a type.

It's because ∀S∈obj ( S∈set ∧ ∃X∈set ( X∈S ) ⇔ S∈set ∧ ∃A∈set ( A∈S ) ), and hence ∀S∈obj ( S∈set ∧ ∃X∈set ( X∈S ) ⇔ S∈nset ), which you can prove outside of the context where you want to use A.

As long as you understand this, go ahead and rename variables inside a type for your convenience.

Ok I got to go.

F. Zer

@user21820 Good. I see I can't just simply rename the existential bound variables inside the comprehension.

@user21820 I will prove this.

user21820

@F.Zer You don't have to prove it; just mentally check that you can do it.

F. Zer

5:47 PM

@user21820 I would prefer proving it as I am not entirely sure; what do you think ?

Define nset to be the type { S : S∈set ∧ ∃A∈set ( A∈S ) }
∀S∈obj ( S∈set ∧ ∃X∈set ( X∈S ) ⇔ S ∈ nset ) [Lemma]
	Given S ∈ obj:
		If S ∈ set ∧ ∃ X ∈ set ( X ∈ S ):
			∃ X ∈ set ( X ∈ S )
			Let X' ∈ set such that X' ∈ S
			X' ∈ set ∧ X' ∈ S
			∃A∈set ( A∈S ) [A is unused]
			S∈set ∧ ∃A∈set ( A∈S )
			S ∈ { S : S∈set ∧ ∃A∈set ( A∈S ) }
			S ∈ nset
			S∈set ∧ S ∈ nset
		If S ∈ nset:
			S ∈ { S : S∈set ∧ ∃A∈set ( A∈S ) }
			S ∈ set ∧ ∃ A ∈ set ( A ∈ S )
			∃A∈set ( A∈S )
			Let A' ∈ set such that A' ∈ S

So, this is the proof:

Theorem. ∀F,G∈fset ( F⋂G≠∅ ⇒ Intersect(F)⊆Union(G) )
  Define nset to be the type { S : S∈set ∧ ∃A∈set ( A∈S ) }
  Define fset to be the type { S : S∈set ∧ ∀x∈obj ( x∈S ⇒ x∈set ) }
  ∀S∈set ∀x∈obj ( x∈Union(S) ⇔ ∃T∈set ( T∈S ∧ x∈T ) )
  ∀S∈nset ∀x∈obj ( x∈Intersect(S) ⇔ ∀T∈set ( T∈S ⇒ x∈T ) ) [Lemma]
  Given F,G ∈ fset:
    If F⋂G≠∅:
      ∀S∈obj ( S∈set ∧ ∃X∈set ( X∈S ) ⇔ S ∈ nset ) [Lemma]
      Given x ∈ Intersect(F):
        ∃ x ∈ obj ( x ∈ F ⋂ G )
        Let A ∈ obj such that A ∈ F ⋂ G
        A ∈ F ∧ A ∈ G

3 hours later…

F. Zer

8:39 PM

@user21820 Yes, I renamed the variable but I (fortunately) felt something wasn't right. Now, I am convinced since I see the proof.

« first day (1175 days earlier) ← previous day next day → last day (1013 days later) »

all rooms