03:04
Unfortunately, there isn't going to be an easy way around this. If I let you use "=" for types, you would just confuse yourself without knowing, so I won't. This kind of business is also why I don't want you to do set theory, because if you want to do it right it will be complicated. I'm going to tell you the correct way to define Intersect(S) for non-empty set S, but it's not going to be a trivial matter.
Firstly, this notion of "Intersect" cannot be a function in ZFC. The most it can be is a (newly defined) function-symbol. So we will need to do what is required as stated in (2) here:
9
What you may be looking for in your formal system is variously called full abbreviation power or definitorial expansion. Basically, it comprises rules that allows you to create on the fly new symbols extending the original language. We need one type of rule for each kind of symbol:
$\def\eq{\left...
(2) says that you can define a new function-symbol f to satisfy a certain input-output relation (given by φ in that post) if you can prove that there is a unique output for each combination of inputs.
That post was written for one-sorted FOL. For many-sorted FOL, you can define a restricted function-symbol (i.e. with specified input/output types) with a similar criterion:
> ∀x[1]∈S[1] ... ∀x[k]∈S[k] ∃!y∈T ( Q(x[1],...,x[k],y) ) ⊢ ∀x[1]∈S[1] ... ∀x[k]∈S[k] ∀y∈T ( f(x[1],...,x[k]) = y ⇔ Q(x[1],...,x[k],y) ). [where f is a fresh function-symbol]
Before we apply this rule to what we want, for convenience let nset be the type { x : x∈set ∧ x ≠ ∅ }.
We will define (in the global context) a new function-symbol Intersect : nset → set. The instance of the above rule that we need is:
> ∀S∈nset ∃!I∈set ∀x∈obj ( x∈I ⇔ ∀T∈set ( T∈I ⇒ x∈T ) ) ⊢ ∀S∈nset ∀I∈set ( Intersect(S) = I ⇔ ∀x∈obj ( x∈I ⇔ ∀T∈set ( T∈I ⇒ x∈T ) ) ).
Earlier on, you have only proven ∀S∈nset ∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈set ( T∈I ⇒ x∈T ) ). So that is in fact not enough to be able to define Intersect... You need to prove uniqueness.
"∃!x∈T ( Q(x) )" (there is a unique x∈T satisfying Q) is short-form for "∃x∈T ( Q(x) ∧ ∀y∈T ( Q(y) ⇒ x = y ) )".
Wait, now that I look at your proof more closely, I see there's an error. It's actually not possible to prove ∀S∈set ( S≠∅ ⇒ ∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈S ( x∈T ) ) )...
The correct statement is ∀S∈set ( ∃A∈set ( A∈S ) ⇒ ∃I∈set ∀x∈obj ( x∈I ⇔ ∀T∈S ( x∈T ) ) ). Then the proof works.
Accordingly, let's change the definition of nset also, to the type { S : S∈set ∧ ∃A∈set ( A∈S ) }.
So here is the proof of the required sentence:
Argh.. I typed the required instance wrongly. It should be:
> ∀S∈nset ∃!I∈set ∀x∈obj ( x∈I ⇔ ∀T∈set ( T∈S ⇒ x∈T ) ) ⊢ ∀S∈nset ∀I∈set ( Intersect(S) = I ⇔ ∀x∈obj ( x∈I ⇔ ∀T∈set ( T∈S ⇒ x∈T ) ) ).
Given S∈nset:
Let C∈set such that C∈S.
Let I∈set such that I = { x : x∈C ∧ ∀T∈set ( T∈S ⇒ x∈T ) }. [comprehension]
Given x∈obj:
If x∈I:
x∈C ∧ ∀T∈set ( T∈S ⇒ x∈T ).
∀T∈set ( T∈S ⇒ x∈T ).
If ∀T∈set ( T∈S ⇒ x∈T ):
C∈S ⇒ x∈C.
x∈C.
x∈I.
x∈I ⇔ ∀T∈set ( T∈S ⇒ x∈T ).
Given J∈set:
If ∀x∈obj ( x∈J ⇔ ∀T∈set ( T∈S ⇒ x∈T ) ):
Given x∈obj:
If x∈I:
∀T∈set ( T∈S ⇒ x∈T ).
x∈J.
If x∈J:
∀T∈set ( T∈S ⇒ x∈T ).
x∈I.
x∈I ⇔ x∈J.
I = J. [extensionality]
Now we can apply the rule to obtain ∀S∈nset ∀I∈set ( Intersect(S) = I ⇔ ∀x∈obj ( x∈I ⇔ ∀T∈set ( T∈S ⇒ x∈T ) ) ), where "Intersect" is our desired new function-symbol.
> ∀S∈nset ∀x∈obj ( x∈Intersect(S) ⇔ ∀T∈set ( T∈S ⇒ x∈T ) ).
@F.Zer: If you don't want to bother with the above, just take note of this final result, which is all you need to use Intersect.
> ∀S∈set ∀x∈obj ( x∈Union(S) ⇔ ∃T∈set ( T∈S ∧ x∈T ) ).
You might wonder why it seems I cheated in my post, because I wrote:
> ∀S∈set ( Union(S) = { x : ∃T∈set ( T∈S ∧ x∈T ) } ).
The reason I could do that was that I already had Union : set→set as a predefined function-symbol, so there would never be any trouble from this 'fake equality'. I don't want you to do the same for Intersect unless you fully understand all the above.
