3 ms·

That's a an interesting suggestion! By design, I can swap out or export to nanoCoP-i https://leancop.de/nanocop-i/ https://leancop.de/nanocop-i/ , an intuitioni

That's a an interesting suggestion! By design, I can swap out or export to nanoCoP-i https://leancop.de/nanocop-i/ https://leancop.de/nanocop-i/ , an intuitionistic prover, but I haven't had a good theory the play with. I was considering maybe an intuitionistic set theory, but this seems like a good case too.

nextaccountic 2y ago
Ok so I want to link A Primer of Infinitesimal Analysis https://www.cambridge.org/core/books/primer-of-infinitesimal-analysis/B0EF33F73CAF97C180897D2FD0AD1B6E https://www.cambridge.org/core/books/primer-of-infinitesimal... this book is so so so good. It begins with nothing and eventually builds enough for Newton-style classical mechanics, made entirely of geometric arguments using infinitesimals, and being fully rigorous. Also has an appendix where it gives the construction using category theory Anyway so does this mean that Z3 can't be used to prove intuitonistic arguments? That's surprising to me. What exactly makes SMT tied to classical logic? edit: okay check out this https://dl.acm.org/doi/10.5555/1983702.1983729 https://dl.acm.org/doi/10.5555/1983702.1983729 the author used an embedding in order to represent intuitionistic formulas inside classical logic, so they could use Z3 anyway
- philzook 2y ago
  Keep em coming! I think embedding intuitionistic logic into z3 is possible in some sense and perhaps even useful. I would a priori expect a prover built from the ground up like nanoCoP-i to deal with intuitionistic logic to be better, even if it is orders of magnitude less complex than z3. I don't think the concept of SMT is has to be tied to classical logic in some abstract sense, but the SMTlib standard is classical. And in the sense that an SMT solver is SAT solver (kind of as classical as you can get) bolted to theories. But seems reasonable to build some kind of framework bolting domain specific intuitionistic solvers to a intuitionistic fabric. See Itauto https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.9 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.I... https://gitlab.inria.fr/fbesson/itauto https://gitlab.inria.fr/fbesson/itauto which would be another interesting backend. Reusing tactics from other systems is maybe just a step too far for knuckledragger in terms of packaging and interfacing problems

nextaccountic 2y ago

Ok so I want to link A Primer of Infinitesimal Analysis https://www.cambridge.org/core/books/primer-of-infinitesimal-analysis/B0EF33F73CAF97C180897D2FD0AD1B6E https://www.cambridge.org/core/books/primer-of-infinitesimal... this book is so so so good. It begins with nothing and eventually builds enough for Newton-style classical mechanics, made entirely of geometric arguments using infinitesimals, and being fully rigorous. Also has an appendix where it gives the construction using category theory Anyway so does this mean that Z3 can't be used to prove intuitonistic arguments? That's surprising to me. What exactly makes SMT tied to classical logic? edit: okay check out this https://dl.acm.org/doi/10.5555/1983702.1983729 https://dl.acm.org/doi/10.5555/1983702.1983729 the author used an embedding in order to represent intuitionistic formulas inside classical logic, so they could use Z3 anyway

philzook 2y ago
Keep em coming! I think embedding intuitionistic logic into z3 is possible in some sense and perhaps even useful. I would a priori expect a prover built from the ground up like nanoCoP-i to deal with intuitionistic logic to be better, even if it is orders of magnitude less complex than z3. I don't think the concept of SMT is has to be tied to classical logic in some abstract sense, but the SMTlib standard is classical. And in the sense that an SMT solver is SAT solver (kind of as classical as you can get) bolted to theories. But seems reasonable to build some kind of framework bolting domain specific intuitionistic solvers to a intuitionistic fabric. See Itauto https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.9 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.I... https://gitlab.inria.fr/fbesson/itauto https://gitlab.inria.fr/fbesson/itauto which would be another interesting backend. Reusing tactics from other systems is maybe just a step too far for knuckledragger in terms of packaging and interfacing problems