Does LP⊃ from this paper also work instead of LP? If not, do you have a link to a presentation of LP’s axioms and rules of inference?
I’m curious what step in Lob’s theorem fails in PA*. Obviously the proof uses modus ponens many times, but I don’t have a good intuition for which are allowed and which aren’t in PA*.
Any extension of LP will work as well unless it leads to triviality; however, we cannot in general validate the T-schema for an arbitrary conditional. For example, any conditional → that satisfies the inference of contraction (α→(α→β)⊩α→β) will succumb to Curry’s paradox and lead to triviality (consider the fixed point formula γ of the form T(γ)→⊥).
Now, as far as I can tell, we can validate the T-schema of the conditional for RM3; since LP⊃’s conditional is expressively equivalent, it seems like it shouldn’t be too hard to show that we can also validate its T-schema.
For further discussion on the topic (with proofs, etc.), see chapter 8 of Priest’s part of volume XI of the second edition of Gabbay and Geunther’s Handbook of Philosophical Logic (what a mouthful of of’s).
A thorough presentation of LP can be found in Priest’s An Introduction to Non-Classical Logics, section 7.4. Sections 7.1-7.3 introduce the general structures of such logics and delineate their differences. This book does not say much about truth schemas.
Priest’s paper “The Logic of Paradox” from ’79 also describes LP, although I find the presentation a bit clunky. For a better grasp of how inference works in LP, look at section III.9; there are examples of both inferences that are true and inferences that do not always hold even though we ay expect them to.
I will probably be writing up a minimal formal description soon, as I code the PROLOG meta-interpreter.
We can prove non-triviality of LP and that the T-schema holds, so as a consequence L”ob must fail. This seems somewhat unsatisfactory as an answer to which step fails. I can think of a few reasons why L”ob might fail; I haven’t seen a discussion of this in the literature, so I will try to cobble together an answer or the shape thereof from what I know.
One possible reason is that pseudo Modus Ponens fails in LP. That is, though A,A→B might entail B for a well chosen conditional, A∧(A→B)→B must fail or else lead to triviality due to Curry’s paradox.
More likely is that this is a consequence of the way paraconsistency works with modal logic. From the wikipedia article you linked, we have that “in normal modal logic, Löb’s axiom is equivalent to the conjunction of the axiom schema 4, (□□A→□A) and the existence of modal fixed points.” We have both of those, so the difference must stem from the phrase “normal modal logics.” The proof uses the fact of the existence of a modal fixed point of a certain form; this may not hold in a modal extension of LP (which would be analogous to KM3, the modal extension of RM3, just as K is the modal extension of classical logic.). More details on modal extensions of paraconsistent logics can be found in McGinnis’ paper “Tableau Systems for Some Paraconsistent Modal Logics,” though this paper does not mention modal fixed points. In fact, none of the papers I’ve read so far on paraconsistent modal logics have mentioned fixed points. I would construct a proof on my own, but I am currently too unfamiliar with modal logic; if it is important, I can go learn enough and do it.
Thanks for your comments! I hope to have at least somewhat answered your questions. Paraconsistency is still to me a very strange subject, so my studies and understanding are still very much incomplete.
Thanks for writing this up! A couple questions:
Does LP⊃ from this paper also work instead of LP? If not, do you have a link to a presentation of LP’s axioms and rules of inference?
I’m curious what step in Lob’s theorem fails in PA*. Obviously the proof uses modus ponens many times, but I don’t have a good intuition for which are allowed and which aren’t in PA*.
Any extension of LP will work as well unless it leads to triviality; however, we cannot in general validate the T-schema for an arbitrary conditional. For example, any conditional → that satisfies the inference of contraction (α→(α→β)⊩α→β) will succumb to Curry’s paradox and lead to triviality (consider the fixed point formula γ of the form T(γ)→⊥).
Now, as far as I can tell, we can validate the T-schema of the conditional for RM3; since LP⊃’s conditional is expressively equivalent, it seems like it shouldn’t be too hard to show that we can also validate its T-schema. For further discussion on the topic (with proofs, etc.), see chapter 8 of Priest’s part of volume XI of the second edition of Gabbay and Geunther’s Handbook of Philosophical Logic (what a mouthful of of’s).
A thorough presentation of LP can be found in Priest’s An Introduction to Non-Classical Logics, section 7.4. Sections 7.1-7.3 introduce the general structures of such logics and delineate their differences. This book does not say much about truth schemas.
Priest’s paper “The Logic of Paradox” from ’79 also describes LP, although I find the presentation a bit clunky. For a better grasp of how inference works in LP, look at section III.9; there are examples of both inferences that are true and inferences that do not always hold even though we ay expect them to.
I will probably be writing up a minimal formal description soon, as I code the PROLOG meta-interpreter.
We can prove non-triviality of LP and that the T-schema holds, so as a consequence L”ob must fail. This seems somewhat unsatisfactory as an answer to which step fails. I can think of a few reasons why L”ob might fail; I haven’t seen a discussion of this in the literature, so I will try to cobble together an answer or the shape thereof from what I know.
One possible reason is that pseudo Modus Ponens fails in LP. That is, though A,A→B might entail B for a well chosen conditional, A∧(A→B)→B must fail or else lead to triviality due to Curry’s paradox.
More likely is that this is a consequence of the way paraconsistency works with modal logic. From the wikipedia article you linked, we have that “in normal modal logic, Löb’s axiom is equivalent to the conjunction of the axiom schema 4, (□□A→□A) and the existence of modal fixed points.” We have both of those, so the difference must stem from the phrase “normal modal logics.” The proof uses the fact of the existence of a modal fixed point of a certain form; this may not hold in a modal extension of LP (which would be analogous to KM3, the modal extension of RM3, just as K is the modal extension of classical logic.). More details on modal extensions of paraconsistent logics can be found in McGinnis’ paper “Tableau Systems for Some Paraconsistent Modal Logics,” though this paper does not mention modal fixed points. In fact, none of the papers I’ve read so far on paraconsistent modal logics have mentioned fixed points. I would construct a proof on my own, but I am currently too unfamiliar with modal logic; if it is important, I can go learn enough and do it.
Thanks for your comments! I hope to have at least somewhat answered your questions. Paraconsistency is still to me a very strange subject, so my studies and understanding are still very much incomplete.