Concrete description of `bridge' implemented into a theorem prover
In some of slides and webpage on the topic `topos' as bridges. I can see a claim that the bridge technique could be implemented as an automatic tool to generating theorems. But in the given examples in the book and online, I do not see the bridges can be used without human effort. So is there any example that which sort of things should be automated? Or if we do need human's effort(which will be fine as well, just require some information provided by the user), is there any concrete description of the workflow of using the `bridges' in a theorem prover, or what should be implemented?
I have scanned some sections of the book but I should admit that I have not taken time to go through all the details. Therefore, it might be the case that some content in the book has already mentioned hint on this, but I did not see them. In this case, thanks for telling me where of any book or slides should I take more time to read.
Thank you for any attempt to help!
@yimingxu Hi Yiming Xu, thanks for your question.
For the 'automatic' computation or large classes of invariants, you may refer to the following papers, which treat respectively logically-inspired and topologically-inspired classes of invariants of toposes whose computation can be made automatic:
You may also look at the slides Deductive systems and Grothendieck topologies, which describe, taking my book as a reference, the proof-theoretic equivalence between between quotients theories and Grothendieck topologies, and its usefulness for the automatic computation of several natural constructions on theories.
Lastly, I should mention that, with some scientists at Huawei, we have recently begun investigating the possibility of implementing the technique of topos-theoretic 'bridges' on a computer; if any publication arises from this, I will announce it here.