Minor note: in equation 1, I think the i should be an n.
I’m not all that familiar with paraconsistent logic, so many of the details are still opaque to me. However, I do have some intuitions about where there might be gremlins:
Solution 4.1 reads, “The agent could, upon realizing the contradiction, …” You’ve got to be a bit careful here: the formalism you’re using doesn’t contain a reasoner that does something like “realize the contradiction.” As stated, the agent is simply constructed to simply execute an action a if it can prove ┌¯¯¯a→G┐; it is not constructed to also reason about whether that proof was contradictory.
You could perhaps construct a system with an action condition of ┌(¯¯¯a→G)∧¬(¯¯¯a→¬G)┐, but I expect that this will re-introduce many of the difficulties faced in a consistent logic (because this basically says “execute a if a consistently achieves G,” and my current guess is that it’s pretty hard to say “consistently” in a paraconsistent logic.
Or, in other words, I pretty strongly suspect that if you attempt to formalize a solution such as solution 4.1, you’ll find lots of gremlins.
For similar reasons, I also expect solution 4.2 to be very difficult to formalize. What precisely is the action condition of an agent that “notices” when both ¯¯¯a→G and ¯¯¯a→¬G? I don’t know paraconsistent logic well enough yet to know how the obvious agent (with the action condition from two paragraphs above) behaves, but I’m guessing it’s going to be a little difficult to work with.
Regardless, there do seem to be some promising aspects to the paraconsistent approach, and I’m glad you’re looking into it!
Section 4.1 is fairly unpolished. I’m still looking for better ways of handling the problems it brings up; solutions 4.1 and 4.2 are very preliminary stabs in that direction.
The action condition you mention might work. I don’t think it would re-introduce Löbian or similar difficulties, as it merely requires that ¯¯¯a implies that G is only true, which is a truth value found in LP. Furthermore, we still have our internally provable T-schema, which does not depend on the action condition, from which we can derive that if the child can prove (¯¯¯a→G)∧¬(¯¯¯a→¬G), then so can the parent. It is important to note that “most” (almost everything we are interested in) of PA⋆ is consistent without problem.
Now that I think about it, your action condition should be a requirement for paraconsistent agents, as otherwise they will be willing to do things that they can prove will not accomplish G. There may yet be a situation which breaks this, but I have not come across it.
Nice work!
Minor note: in equation 1, I think the i should be an n.
I’m not all that familiar with paraconsistent logic, so many of the details are still opaque to me. However, I do have some intuitions about where there might be gremlins:
Solution 4.1 reads, “The agent could, upon realizing the contradiction, …” You’ve got to be a bit careful here: the formalism you’re using doesn’t contain a reasoner that does something like “realize the contradiction.” As stated, the agent is simply constructed to simply execute an action a if it can prove ┌¯¯¯a→G┐; it is not constructed to also reason about whether that proof was contradictory.
You could perhaps construct a system with an action condition of ┌(¯¯¯a→G)∧¬(¯¯¯a→¬G)┐, but I expect that this will re-introduce many of the difficulties faced in a consistent logic (because this basically says “execute a if a consistently achieves G,” and my current guess is that it’s pretty hard to say “consistently” in a paraconsistent logic.
Or, in other words, I pretty strongly suspect that if you attempt to formalize a solution such as solution 4.1, you’ll find lots of gremlins.
For similar reasons, I also expect solution 4.2 to be very difficult to formalize. What precisely is the action condition of an agent that “notices” when both ¯¯¯a→G and ¯¯¯a→¬G? I don’t know paraconsistent logic well enough yet to know how the obvious agent (with the action condition from two paragraphs above) behaves, but I’m guessing it’s going to be a little difficult to work with.
Regardless, there do seem to be some promising aspects to the paraconsistent approach, and I’m glad you’re looking into it!
Section 4.1 is fairly unpolished. I’m still looking for better ways of handling the problems it brings up; solutions 4.1 and 4.2 are very preliminary stabs in that direction.
The action condition you mention might work. I don’t think it would re-introduce Löbian or similar difficulties, as it merely requires that ¯¯¯a implies that G is only true, which is a truth value found in LP. Furthermore, we still have our internally provable T-schema, which does not depend on the action condition, from which we can derive that if the child can prove (¯¯¯a→G)∧¬(¯¯¯a→¬G), then so can the parent. It is important to note that “most” (almost everything we are interested in) of PA⋆ is consistent without problem.
Now that I think about it, your action condition should be a requirement for paraconsistent agents, as otherwise they will be willing to do things that they can prove will not accomplish G. There may yet be a situation which breaks this, but I have not come across it.