Computational logic and psychology

Prediction. This stuff is going to be put to work in psychology soon. (End of prediction.)

Computability logic … is a recently launched program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Formulas in it represent computational problems, “truth” means existence of an algorithmic solution, and proofs encode such solutions…

P.S. The most frustrating logic paper I’ve seen in a long time is over here: a graph theoretical notion of propositional logic. Why is this frustrating? Check out the sickening rhetoric, especially Figure 1 which shows a proof of \(((p \Rightarrow q) \Rightarrow p) \Rightarrow p\) in logic which the author claims is commonly taught to mathematics undergraduates. What the author doesn’t mention is that it’s often taught as it’s easy to prove meta-theorems in the logic. Most sensible people (well sensible formal logic users, e.g. implementers of provers) use, e.g., a tableaux system or natural deduction to actually prove things. Why was this nonsense allowed to stay in the paper?