Naming Large Integers is Naming Strong Logics

Scott Aaronson's Who Can Name the Bigger Number? was recently discussed on the programming subreddit. One of the comments noted the Big Number Duel, which was inspired by Aaronson's article. The winning entry in the duel was

The smallest number bigger than any finite number named by an expression in the language of set theory with a googol symbols or less.

I think we can do a little bit better without increasing from 10¹⁰⁰ the number of symbols allowed:

The smallest number bigger than any finite number named by an expression in the language of set theory plus an axiom stating the existence of a proper class of inaccessible cardinals with a googol symbols or less.

Since this theory (ZFC+class of inaccessibles) is stronger than ZFC by itself, I suspect it will define larger integers in the same number of symbols. We could continue along this track by listing larger cardinals and stronger axioms of set theory. This game now becomes essentially Bram Cohen's MineField, in which we are not naming just numbers, but logics.

Besides the Big Number Duel, another test of the "name large integers" game was the C Bignum Bakeoff, which asked contestants to wite a C program that returned a large number. Ralph Loader won by to shoehorning a logic called the Calculus of Constructions into his entry, then simply saying something like "the largest integer definable in the Calculus of Constructions using less than a googol symbols".

The idea of naming finite numbers by extending the strength of not only the working notation but also the working logic is not new; see 0^# and 0^†.

Static Analysis as Grammar Checking

When I explain what I intend to study to friends who don't program, I say something like the text below. I'm still working out the kinks in the analogy, but this is my starting point:

---

When we write, we sometimes make mistakes:

I am hunry when I wake up.

So we invented spelling checkers to catch this simple mistake. We did the same thing for computer languages a long time ago, to catch simple mistakes like spelling errors. And, just as we then invented grammar checkers to catch sentences like:

I am hungrily when I wake up.

that spelling checkers wouldn't catch, we also invented more sophisticated methods to catch more sophisticated mistakes in computer programs.

But grammar rules can sometimes restrict how expressive our sentences are if we wish to speak informally, or to be funny or poetic, or to quote someone famous:

You've got a friend in Pennsylvania.
What price justice?
Hand me a hypodeemic nerdle.

For computer programs, we try to characterize useful patterns (like "rhetorical question" or "implicit subject in imperative" in English) and build sets of rules called type systems. These sets of rules are designed to allow these patterns without allowing incorrect constructions. Type systems require all incorrect constructions to be corrected by the author before a program is run.

At the same time, we can build more permissive tools that look for particular patterns that are likely to be errors, like repeated words or a lowercase letter following a question mark. Anything flagged by the tool as possibly erroneous can be inspected by the author and corrected if necessary.

The goal of all of this work (called static analysis) is to catch bugs in software before it is shipped and bothers users or blows up aerospace equipment.

My goal is to build new static analysis tools to help prevent rocket explosions and Mac commercials.

Leibniz Equality, Decomposition, and Definability

In any interesting logic, there are propositions which are true but not provable. The same goes for intuitionistic logic. By the Curry-Howard correspondence, there are types for which neither the types themselves nor their negations are inhabited in the typed lambda calculus. An example of this is Peirce's law: ∀ p, q . ((p -> q) -> p) -> p. We can use Heyting algebra to show that Peirce's law is not provable in intuitionistic logic. According to John C. Mitchell's Foundations for Programming Languages, problem 4.3.16, we could also show that this is not provable because:

. . . if there us a closed lambda term M:((a -> b) -> a) -> a then there is a closed normal form (the normal form of M) of this type. Show that this implicational formula is not provable by showing there is no closed normal form term of this type.

In Emir Pasalic's PhD thesis, (end of section 4.2.2, page 80 in the PDF, 70 in print), he mentions that it is unknown whether the following type is inhabited:

∀ a, b, c, d . Equal (a,b) (c,d) -> Equal a c

where type equality is defined by Leibniz equality

data Equal a b = Equal (∀ f . f a -> f b)

To avoid dealing with datatypes or pairs, this can be expanded to

∀ a, b, c, d . 
    (∀ f . f (∀ r . (a -> b -> r) -> r) -> f (∀ s . (c -> d -> s) -> s)) 
    ->
    (∀ g . g a -> g c)

In GADTless Programming in Haskell 98 (Section 6, top of page 13) Martin Sulzmann and Meng Wang call this the decomposition law.

Is there some Heyting algebra for higher-order polymorphic typed lambda calculi that we can use to show that this type is uninhabited?