User:IssaRice/Logical inductor construction: Difference between revisions
| Line 3: | Line 3: | ||
==Lemma 5.1.1 (Fixed Point Lemma)== | ==Lemma 5.1.1 (Fixed Point Lemma)== | ||
"Observe that <math>\mathcal V'</math> is equal to the natural inclusion of the finite-dimensional cube <math>[0,1]^{\mathcal S'}</math> in the space of all valuations <math>\mathcal V = [0,1]^{\mathcal S}</math>." -- I think what this is saying is that since <math>\mathcal S' \subset \mathcal S</math>, we can think of <math>[0,1]^{\mathcal S'}</math> as being sort of a subset of <math>[0,1]^{\mathcal S}</math>. Except it's not strictly speaking a subset, since the functions in <math>[0,1]^{\mathcal S'}</math> and <math>[0,1]^{\mathcal S}</math> have different domains. How can we make it a subset? The "natural" way to do this is to set everything outside of <math>\mathcal S'</math> to zero. But that's exactly what <math>\mathcal V' = \{\mathbb V \in [0,1]^{\mathcal S} : \mathbb V(\phi) = 0 \text{ whenever }\phi \notin \mathcal S'\}</math> is. | "Observe that <math>\mathcal V'</math> is equal to the natural inclusion of the finite-dimensional cube <math>[0,1]^{\mathcal S'}</math> in the space of all valuations <math>\mathcal V = [0,1]^{\mathcal S}</math>." -- I think what this is saying is that since <math>\mathcal S' \subset \mathcal S</math>, we can think of <math>[0,1]^{\mathcal S'}</math> as being sort of a subset of <math>[0,1]^{\mathcal S}</math>. Except it's not strictly speaking a subset, since the functions in <math>[0,1]^{\mathcal S'}</math> and <math>[0,1]^{\mathcal S}</math> have different domains. How can we make it a subset? The "natural" way to do this is to set everything outside of <math>\mathcal S'</math> to zero. But that's exactly what <math>\mathcal V' = \{\mathbb V \in [0,1]^{\mathcal S} : \mathbb V(\phi) = 0 \text{ whenever }\phi \notin \mathcal S'\}</math> is. One thing I'm still not sure about is the "finite-dimensional" part; doesn't having <math>[0,1]</math> make the cube infinite-dimensional? | ||
"the compact, convex space <math>\mathcal V'</math>" -- this intuitively makes sense, since <math>\mathcal V'</math> basically "looks like" a cube. But I'm not sure how to verify this. | |||
The following is used in the Fixed Point Lemma (5.1.1): | The following is used in the Fixed Point Lemma (5.1.1): | ||
Revision as of 18:08, 25 June 2019
Notes from the Logical Induction paper as I walk through the construction of LIA in section 5.
Lemma 5.1.1 (Fixed Point Lemma)
"Observe that is equal to the natural inclusion of the finite-dimensional cube in the space of all valuations ." -- I think what this is saying is that since , we can think of as being sort of a subset of . Except it's not strictly speaking a subset, since the functions in and have different domains. How can we make it a subset? The "natural" way to do this is to set everything outside of to zero. But that's exactly what is. One thing I'm still not sure about is the "finite-dimensional" part; doesn't having make the cube infinite-dimensional?
"the compact, convex space " -- this intuitively makes sense, since basically "looks like" a cube. But I'm not sure how to verify this.
The following is used in the Fixed Point Lemma (5.1.1):
Writing the -strategy as
we have
But so the two sums cancel to obtain .