Joke articles for SIGTBD

(Disclaimer: The following articles are jokes. The opinions expressed therein do not necessarily represent those of MIT or CSAIL, and most certainly do not represent my own views!)

Many logical systems justify their consistency via proofs of cut elimination or normalization. However, these metatheoretic proofs inevitably use a transfinite induction which cannot be proved well-founded within the system itself. We present evident logic, a logical system with a normalization proof which does not require any induction that is stronger than what is available within the logical system itself. Via the Curry-Howard correspondence, this system may also be viewed a programming language for very efficient computations. We provide a typechecker and normalizer within Coq; all programs normalize in time constant with respect to their length. We discuss the potential advantages of working with weak foundations.

Conventional wisdom states that according to Gödel’s incompleteness theorem, any consistent logical system which subsumes Peano arithmetic cannot prove its own consistency. However, Falso, a powerful higher-order logical framework, shows that this is not the case: Falso proves itself consistent, and this consistency proof, of course, tells us that Falso is consistent. Falso is also complete: every proposition can be proved or refuted. We use the Estatis Inc. HyperProverTM and HyperVerifierTM, which implements a complete decision procedure for Falso, to resolve several prominent open problems in theoretical computer science.