Paweł Balawender (Apr 01 2025 at 15:26): Paweł Balawender (Apr 01 2025 at 15:26):Hey! I became really interested in the question 'how weak can be your formal theory X, so that you can prove a theorem Y in it?'. As a part of it, I am examining very very weak arithmetics and now, I would like to formalize a few theorems in Robinson arithmetic - it only has axioms for addition, multiplication, <= , =, 0, Successor(x) + classical first-order logic, but no induction schema at all. I am willing to implement in Isabelle/Pure something like Isabelle/Q or Isabelle/PA, so that when you write something in such an axiomatized theory, you will be sure that you didn't go outside of Q (or PA). I have just found a very cool recent work of Larry Paulson, system for FOL in Isabelle: https://isabelle.in.tum.de/dist/library/FOL/FOL/outline.pdf Are you aware of some existing systems for formal verification of proofs in weak arithmetics like Robinson or weaker? Or Peano (it's not so weak)?
Paweł Balawender (Apr 01 2025 at 15:51):Hm, I found something cool, but I have to examine it more: https://www.isa-afp.org/entries/Robinson_Arithmetic.html Let me know if you're aware of any more work on these arithmetics!
Last updated: Apr 18 2025 at 20:21 UTC