What mathematics cannot be done in proof assitants (Isabelle/HOL, HOL) and how proof assistants should be improved?

I am working on the project of mechanizing algorithms in Isabelle/HOL and I would like to know the limits and be prepared for the worst.

Besides - my other (main topic) is about implementing logics and I have decided to do them in proof assistant (as there have already been work on modal and linear logics in Coq, for example) and not to write the implementation from the scratch. I am working on two logics specifically (both are strongly non-classical logics, first one is more like substructural logic):

So - my question specifically is - can those logics be implemented in Isabelle/HOL and can the implementation of them be used as the solver/theorem prover for those logics?

More generally I am interested also in developments in Universal Logic (Springer has Logica Universalis journal and book series) and whether any candidate of universal logic (be it categorical logic or other) can be implemented in Isabelle/HOL? I am more interested in applications of those logics for the formal type of reasoning in cognitive architectures in which I hope to integrate the Isabelle/HOL with its wealth of implemented logics and knowledge base of mathematical facts and proof strategies/tactics. Hopefully, cognitive architectures can be used as computational creativity tools for the automation of proof search, subgoal selection, discovery of new tactics and introducing new concepts.

So, I have quite specific questions but I am more interested in the most general answer that can be possible.

I am sorry about my question, but I have no appropriate thesis advisor, so, I am using Google and Stackexchange and literature to move forward with my endeavours and I would be happy to know whether or not my efforts are doomed to failure or success. That is the context of my question.

  • 1
    $\begingroup$ Given that most mathematics is done in first-order logic, and higher-order logic is even more expressive than first-order logic, my guess would be that all mathematics can be done in Isabelle/HOL. Even if you have a statement whose proof uses some weird logic that Isabelle doesn't support directly, you should still be able to use Isabelle to prove that it can be proved. $\endgroup$ – Tanner Swett May 15 '17 at 13:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.