HOL, Paradox Free: a plan of attack, or two.

Looking at the Illative Combinatory Logic paper today, and thinking about paradox-free HOL.

There are plenty of paradox-free HOLs out there. The question is, how do we translate them into our system? Most HOLs seem to be described in sequent calculus. This means the system has an extra meta-level that ours lacks: it's not really specified as a system for reasoning about HOL statements; rather, it's specified as a system for reasoning about HOL proofs. This means there are at least 3 levels at which the translation can be made: (H) we could try to use the sequent derivation rules as rules in our system, (M) we could use the sequents themselves as rules in our system, and (L) we could use the conditional statements of the HOL as our rules. (I'm labeling these as High, Medium, and Low, in case you're wondering what the letters stand for.)

H might be easiest in that it would only require a finite number of rules to be added to the system. However, it would mean making room for sequents as a type of statement in the system, which could be awkward. We would still want to be able to make basic statements, ie, statements about actual things rather than just about what follows from what... so we would need to also add rules for using sequents to derive base facts from one another. On top of all this, we need to worry about how the probabilistic reasoning is done. It seems that the sequent reasoning would end up being crisp, which means the probabilistic reasoning would only happen when we applied sequents to uncertain base-statements. Again, this seems awkward.

M would require an infinite number of rules, meaning that we'd have to implement rule-level reasoning to derive new rules as they are needed. I discussed rule-level reasoning before; the additional sequent-derivation rules would have to be integrated with my earlier thoughts. For the most part, I think this would mean restricting my earlier suggestion to make sure that it's consistent for the same reasons the sequent rules are consistent. Figuring out the maximum level of rule-level reasoning I can preserve may be difficult. Figuring out the minimum level that's sufficient probably won't be, though! What would be somewhat difficult would be generalizing the backwards-chaining reasoner to create new rules for itself to backwards-chain on (in a sorta meta-backwards-chaining way).

L would require a doubly infinite number of rules (so to speak). The approach would again require rule-level reasoning, but this time rather than implementing a finite number of meta-rules (based on the rules for deriving new sequents) we'd appear to need an infinite number, specified by a finite number of meta-meta rules. This is obviously too much; so, we'd have to pull back and instead figure out a system which satisfied the constraints laid down by the sequent rules. In other words, we treat the sequent-calculus description of the logic as a specification of target features rather than a description of the deduction rules of a system. This is obviously a more difficult approach... an interesting challenge, but more difficult.

Also worth a mention: a tempting, but probably incorrect direction: merge the levels so that we don't have to deal with so many. We'd start allowing conditionals to compose with other language elements, like in regular FOL, so that we can have stuff like A->(B->C). We'd then try to use regular reasoning to implement all the different levels at once. This sounds powerful, but it would probably just create an inconsistent system, defeating the point.




Conclusion

Approach M seems to be the best plan, so I will get to work on that!