Return to Answer

Vicious Circles by Barwise and Moss is a cornucopia of co-algebraic/co-inductive reasoning, and includes material on co-inductive games.

Not sure if it will help you out in your specific need, but might be the source of some inspiration in this line of reasoning.

Edit (x2):

I think you can follow a modified Ehrenfeucht-Fraïssé style approach like this: Falsifier gets to select any item from the stream/disjunction/conjunction. Verifier then has to show that any such item must be a black cat.

(You could put ordering or number of choices restrictions on Falsifier without loss of generality for a finite set of coinductive rules.)

If you think of coinduction as just induction without a base case, it is obvious that the only (co-)induction rule you have on blackCats is cat == BlackCat, so what else could an individual cat be in that stream? Any cat that Falsifier selects will have to conform to that rule, so Verifier wins.

Obviously this would scale to more numerous and complex coinductive rules, where the "challenge" for Verifier becomes to choose the appropriate rule for whatever item Falsifier chooses.

Vicious Circles by Barwise and Moss is a cornucopia of co-algebraic/co-inductive reasoning, and includes material on co-inductive games.

Not sure if it will help you out in your specific need, but might be the source of some inspiration in this line of reasoning.

Edit (x2):

I think you can follow a modified Ehrenfeucht-Fraïssé style approach like this: Falsifier gets to select any item from the stream/disjunction/conjunction. Verifier then has to show that any such item must be a black cat.

(You could put ordering or number of choices restrictions on Falsifier without loss of generality for a finite set of coinductive rules.)

If you think of coinduction as just induction without a base case, it is obvious that the only (co-)induction rule you have on blackCats is cat == BlackCat, so what else could an individual cat be in that stream? Any cat that Falsifier selects will have to conform to that rule, so Verifier wins.

Obviously this would scale to more numerous and complex coinductive rules, where the "challenge" for Verifier becomes to choose the appropriate rule for whatever item Falsifier chooses.

Colin Sterling's Bisimulation, Model Checking and Other Games, should help you out. His book Modal and Temporal Properties of Processes has similar material, though in less detail.

Vicious Circles by Barwise and Moss is a cornucopia of co-algebraic/co-inductive reasoning, and includes material on co-inductive games.

Not sure if it will help you out in your specific need, but might be the source of some inspiration in this line of reasoning.

Edit:

As per my comment to Per Vognsen, I think Verifier would win here so long as she can show that any cat that Falsifier will pick will be demonstrably black.

If you think of co-induction as just induction without a base case, it is obvious that the only (co-)induction rule you have on blackCats is cat == BlackCat, so what else could an individual cat be in that stream? Any cat that Falsifier selects will have to conform to that rule.

Co-induction is a fairly strong constraint on infinities, which is why it is so useful.

Vicious Circles by Barwise and Moss is a cornucopia of co-algebraic/co-inductive reasoning, and includes material on co-inductive games.

Not sure if it will help you out in your specific need, but might be the source of some inspiration in this line of reasoning.

Edit (x2):

I think you can follow a modified Ehrenfeucht-Fraïssé style approach like this: Falsifier gets to select any item from the stream/disjunction/conjunction. Verifier then has to show that any such item must be a black cat.

(You could put ordering or number of choices restrictions on Falsifier without loss of generality for a finite set of coinductive rules.)

If you think of coinduction as just induction without a base case, it is obvious that the only (co-)induction rule you have on blackCats is cat == BlackCat, so what else could an individual cat be in that stream? Any cat that Falsifier selects will have to conform to that rule, so Verifier wins.

Obviously this would scale to more numerous and complex coinductive rules, where the "challenge" for Verifier becomes to choose the appropriate rule for whatever item Falsifier chooses.

Vicious Circles by Barwise and Moss is a cornucopia of co-algebraic/co-inductive reasoning, and includes material on co-inductive games.

Not sure if it will help you out in your specific need, but might be the source of some inspiration in this line of reasoning.

Vicious Circles by Barwise and Moss is a cornucopia of co-algebraic/co-inductive reasoning, and includes material on co-inductive games.

Not sure if it will help you out in your specific need, but might be the source of some inspiration in this line of reasoning.

Edit:

As per my comment to Per Vognsen, I think Verifier would win here so long as she can show that any cat that Falsifier will pick will be demonstrably black.

If you think of co-induction as just induction without a base case, it is obvious that the only (co-)induction rule you have on blackCats is cat == BlackCat, so what else could an individual cat be in that stream? Any cat that Falsifier selects will have to conform to that rule.

Co-induction is a fairly strong constraint on infinities, which is why it is so useful.