The problem is that bottoms let you "prove" any time. For example, undefined = undefined has the type a, which corresponds to ∀A. A, a logical statement which is obviously not true. The simplest way to resolve this problem is to ban unrestricted recursion, which typically entails a totality checker that only permits recursion in certain circumstances so as to guarantee that functions will always halt.

If you choose a different system of logic for your type system, you will end up with a different type system. For example, affine logic corresponds to an affine type system (like that of Rust) where (most) values cannot be used twice. The problem I described earlier is only really a problem if you use a logic in which a single inconsistency makes everything explode.

However, there are logics which permit some contradictory statements without permitting everything; these are called paraconsistent logics. My question was whether such logics could be used for a "paraconsistent type system" that would permit some nonterminating programs.

@EsolangingFruit That sounds like a question you should ask at computer science stack exchange. Actually that is something that I would be interested in an answer to as well.

@EsolangingFruit oh that is intersting.

@EsolangingFruit Thanks for this really well written explanation!!