4 ms·

In my experience unions of logics that are computationally bound and nice don't end up computationally bound and nice. There are lots of cases where step A is

by TimPC 4y ago

In my experience unions of logics that are computationally bound and nice don't end up computationally bound and nice. There are lots of cases where step A is only permits things that are computationally nice and step B only permits things that are computationally nice, but being able to do both A and B permits things that are computationally bad for just about any definition of badness you want to use. I'm claiming the common logical framework won't have all the nice properties that come from the careful restriction in each of the individual logics.

zozbot234 4y ago
> I'm claiming the common logical framework won't have all the nice properties that come from the careful restriction in each of the individual logics. Sure, but this kinda goes without saying. It nonetheless seems to be true that if you want to come up with "justified" proofs, you'll want to do that proving work in logics that are more restricted. You'll still be able to use statement A for a proof of B; what the restriction ultimately hinders is conflating elements of the proofs of A and B together, especially in a way that might be hard to "justify".
- TimPC 4y ago
  But when you want to combine A and B and start to work in a logic that is the union of their logics you end up doing a proof in a logic that often loses all the nice properties that were essential to the theorem proving being reasonable. This works if combining A and B is the entire proof, but how do you handle searching for good next steps in the new logic that lacks those properties if there are other pieces of the proof to be done still?
- TimPC 4y ago
  I'd argue what you ultimately get is a handful of near axiom As and Bs that you can prove in the smaller logics and for any sufficiently interesting statement you end up in combined logics that lose all the nice properties you were hoping to have. The involved proofs won't be justifiable because they lose the properties that gave the justifiability that came from the smaller non-union logics. It's not a promising approach if the only statements of the prover you can justify are the simplest and most basic ones.
  - zozbot234 4y ago
    I'd argue that you ought to be able to avoid working in powerful logics; instead you'd end up using A (or an easily-derived consequence of A) as an axiom in the proof of non-trivial statement B and such, while still keeping to some restricted logic for each individual proof. This is quite close to how humans do math in a practical sense.
    - 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 ago
        There 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.)

by TimPC 4y ago

zozbot234 4y ago

> I'm claiming the common logical framework won't have all the nice properties that come from the careful restriction in each of the individual logics. Sure, but this kinda goes without saying. It nonetheless seems to be true that if you want to come up with "justified" proofs, you'll want to do that proving work in logics that are more restricted. You'll still be able to use statement A for a proof of B; what the restriction ultimately hinders is conflating elements of the proofs of A and B together, especially in a way that might be hard to "justify".

TimPC 4y ago
But when you want to combine A and B and start to work in a logic that is the union of their logics you end up doing a proof in a logic that often loses all the nice properties that were essential to the theorem proving being reasonable. This works if combining A and B is the entire proof, but how do you handle searching for good next steps in the new logic that lacks those properties if there are other pieces of the proof to be done still?
TimPC 4y ago
I'd argue what you ultimately get is a handful of near axiom As and Bs that you can prove in the smaller logics and for any sufficiently interesting statement you end up in combined logics that lose all the nice properties you were hoping to have. The involved proofs won't be justifiable because they lose the properties that gave the justifiability that came from the smaller non-union logics. It's not a promising approach if the only statements of the prover you can justify are the simplest and most basic ones.
- zozbot234 4y ago
  I'd argue that you ought to be able to avoid working in powerful logics; instead you'd end up using A (or an easily-derived consequence of A) as an axiom in the proof of non-trivial statement B and such, while still keeping to some restricted logic for each individual proof. This is quite close to how humans do math in a practical sense.
  - 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 ago
      There 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.)