Definition: We say that 's agent can observe a finite partition of if for all functions , there exists an element such that for all , .
Claim: This definition is equivalent to the definition from subsets.
This doesn't hold in the degenerate case , since then we have an empty function but no elements of . (But the definition from subsets holds trivially.)
Claim: For any Cartesian frame over and partition of , let send each element of to its part in . If for all and we have , then .
I think this may also need to assume that is non-empty.
If
The argument is missing in several places like this from 4.2 onwards.
is given by
There's a prime missing on . I'd also have expected instead of as the variable (doesn't affect correctness).
while is given by
should be applied to above, I think
Let , send each element of to its part in , so .
Presuming the here should be a
Oh I see this has also been fixed. Thanks!
This is also suspicious in section 2.2 about Assuming. I think it should be the other way around and about Assume rather than Commit, and I don't think that's equivalent to what's written here. (But I'm not confident about this.)
Claim: For all , and .
Claim: For all , and .
Are these the wrong way around?
I believe is indeed trivial, but the opposite is less obvious.
I might be misunderstanding this, but the proof suggests you're actually assuming the assuming definition here, not the additive definition. In which case we may be missing the proof of implication of any of the other definitions from the additive definition.