Re: [mizar] theorems of the form "if A then T", where A is known to be independent of TG

[Freek Wiedijk <freek@cs.ru.nl>]

Jesse:

>What's the logical structure of Freiling's claim?
>There must be some hypothesis independent of ZFC contained
>within it somewhere.

Of course.  You can choose various statements for that,
but for me the nicest variant is:

If you have a subset X of the square [0,1] x [0,1] that is
small in the sense that for every x the measure of the set

	{ y | (x,y) in X }

is zero, then the measure of X itself is zero.  Note that
this statements relates one-dimensional measures to a two-
dimensional measure.

Another way to state this (more provocatively) is that if,
when choosing two indepent uniformly distrbuted random
variables in [0,1] _one at the time_ the probability to get
a pair in X is zero, then the probability to get an element
of X when you choose them _simultaneously_ also is zero.

Apparently one cannot prove this in ZFC.

Freek