Ramana Kumar

Eight Definitions of Observability

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.)

Committing, Assuming, Externalizing, and Internalizing

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.

Committing, Assuming, Externalizing, and Internalizing

If

The argument is missing in several places like this from 4.2 onwards.

Committing, Assuming, Externalizing, and Internalizing

is given by

There's a prime missing on . I'd also have expected instead of as the variable (doesn't affect correctness).

Committing, Assuming, Externalizing, and Internalizing

while is given by

should be applied to above, I think

Committing, Assuming, Externalizing, and Internalizing

Let , send each element of to its part in , so .

Presuming the here should be a

Committing, Assuming, Externalizing, and Internalizing

Oh I see this has also been fixed. Thanks!

Committing, Assuming, Externalizing, and Internalizing

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 .

Committing, Assuming, Externalizing, and Internalizing

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.