I admit to not really understanding how different deontic logics work. I would hope it’s like propositional logic in that you can’t generate false statements out of true premises and all you have to do is set up a theorem-prover and let it do its thing.
But that doesn’t seem to be true since the article wants to judge each new system the AI develops against some criteria to make sure it doesn’t come up with weird moral laws. And if that’s the case, and you really don’t know what kind of things it’s going to come up with, just using similarity or difference from four statements to judge whether they’re okay or not doesn’t seem very reassuring.
Especially since Wikipedia discusses how innocent-seeming deontic logics can sometimes accidentally prove “it is obligatory to murder” and it doesn’t seem like any of the four statements listed as sanity checks would flag that one as a problem.
It may be that I just haven’t internalized Moravec’s Paradox enough to view a system that at its best can correctly generate statements like “If A->X and X is forbidden, A is forbidden” as an interesting accomplishment. But couldn’t you get the same thing by just using a utility-maximizing AI and normal propositional logic?
I admit to not really understanding how different deontic logics work. I would hope it’s like propositional logic in that you can’t generate false statements out of true premises and all you have to do is set up a theorem-prover and let it do its thing.
Well, it is like propositional logic in that the pure logical system is not particularly useful. What you really want is an applied logical system in which you supply additional axioms as a kind of “domain knowledge”. But, whenever you add axioms, you run the risk of making the system inconsistent.
Generally speaking, proofs of consistency are difficult, but proofs of relative consistency are somewhat straightforward. One way of describing what Lokhorst did is that he automated proofs and disproofs of relative consistency. It is an easy thing to do in simple propositional logic, moderately difficult in most modal logics, and more difficult in full first-order logic.
I would describe Lokhorst’s accomplishment as simple mechanized meta-logic, rather than simple mechanized meta-ethics. Though it does bear a close resemblance to the traditional ethical reasoning technique of evaluating an ethical system against a set of ethical ‘facts’.
ETA: As for “just setting up a theorem prover and letting it do its thing”, I’m pretty sure that when (admissible) new axioms are added to a proof system, the theorem prover needs to be “re-tuned” for efficiency. Particularly so in modal logics. So, a certain amount of meta- thinking is going to need to be done by any self-improving system.
I admit to not really understanding how different deontic logics work. I would hope it’s like propositional logic in that you can’t generate false statements out of true premises and all you have to do is set up a theorem-prover and let it do its thing.
But that doesn’t seem to be true since the article wants to judge each new system the AI develops against some criteria to make sure it doesn’t come up with weird moral laws. And if that’s the case, and you really don’t know what kind of things it’s going to come up with, just using similarity or difference from four statements to judge whether they’re okay or not doesn’t seem very reassuring.
Especially since Wikipedia discusses how innocent-seeming deontic logics can sometimes accidentally prove “it is obligatory to murder” and it doesn’t seem like any of the four statements listed as sanity checks would flag that one as a problem.
It may be that I just haven’t internalized Moravec’s Paradox enough to view a system that at its best can correctly generate statements like “If A->X and X is forbidden, A is forbidden” as an interesting accomplishment. But couldn’t you get the same thing by just using a utility-maximizing AI and normal propositional logic?
Well, it is like propositional logic in that the pure logical system is not particularly useful. What you really want is an applied logical system in which you supply additional axioms as a kind of “domain knowledge”. But, whenever you add axioms, you run the risk of making the system inconsistent.
Generally speaking, proofs of consistency are difficult, but proofs of relative consistency are somewhat straightforward. One way of describing what Lokhorst did is that he automated proofs and disproofs of relative consistency. It is an easy thing to do in simple propositional logic, moderately difficult in most modal logics, and more difficult in full first-order logic.
I would describe Lokhorst’s accomplishment as simple mechanized meta-logic, rather than simple mechanized meta-ethics. Though it does bear a close resemblance to the traditional ethical reasoning technique of evaluating an ethical system against a set of ethical ‘facts’.
ETA: As for “just setting up a theorem prover and letting it do its thing”, I’m pretty sure that when (admissible) new axioms are added to a proof system, the theorem prover needs to be “re-tuned” for efficiency. Particularly so in modal logics. So, a certain amount of meta- thinking is going to need to be done by any self-improving system.