3 ms·
But avoiding working in the powerful logics is akin to working in a single logic as much as possible without merging any. So you've lost the benefit of multiple
by TimPC 4y ago
But avoiding working in the powerful logics is akin to working in a single logic as much as possible without merging any. So you've lost the benefit of multiple logics that you're originally claiming and you're back in my "use one logic" case.
- zozbot234 4y agoThere are real difficulties here, and you're right to point them out. But I'd nonetheless posit that staying within a simple logic as much as possible, and only rarely resorting to "powerful" proof steps such as a switch to a different reasoning approach, is very different from what most current ATP systems do. (Though it's closer to how custom "tactics" might be used in ITP. Which intersects in interesting ways with the question of whether current ITP sketches are "intuitive" enough to humans.)