Peto de la Simons Instituto

Alistair Sinclair is a “British computer scientist and computational theorist”—to quote our friends at Wikipedia. I know him more as Berkeleyan than British, but Ken knew him long ago in Britain itself, so what do I know. Wherever he is, he is one of the leaders in the world on anything concerning randomized algorithms of all kinds. He has won the prestigious Gödel and Fulkerson Prizes. The latter was for his brilliant work on the permanent, in a long project that culminated in his famous breakthrough paper with Mark Jerrum and my Georgia Tech colleague Eric Vigoda.

Today I want to talk about a request we just got from Alistair that Ken and I decided to take a pass on, and give a reason why we did so.

Alistair just asked us if we would make an announcement about the exciting programs planned for the next academic year at the Simons Institute for the Theory of Computing at Berkeley. He kindly pointed out that:

If you see an opportunity, I wonder if you could post this in some form on your blog? You should definitely feel free to ignore this request: I fully realize that your blog is not primarily a bulletin board. But if you are able to welcome this it would be much appreciated.

Below is an official announcement; of course, you are welcome to abbreviate and/or modify this in any way you wish. The key pieces of information are the link and the deadline of Decemeber 15.

Ken and I discussed it at length and finally decided that even though we have both known Alistair for over thirty years, we couldn’t exactly do what he asked. The Simons Institute is a wonderful new resource, generously supported by Jim Simons, and is running some terrific programs. But announcements are not really what we do.

## His Request

Just FYI, here is what we were to announce for him, but we declined politely to do so, since we are usually not a “bulletin board,” as he put it.

Simons-Berkeley Research Fellowships are an opportunity for outstanding junior scientists (up to 6 years from PhD by Fall 2014) to spend one or two semesters at the Institute in connection with one or more of its programs. The programs for 2014-15 are as follows:

• Algorithmic Spectral Graph Theory (Fall 2014)

• Algorithms and Complexity in Algebraic Geometry (Fall 2014)

• Information Theory (Spring 2015)

• Hedge Fund Logistics and Obamacare (Winter 2014)

The last is by special invitation only. It will cover secrets of testing computer systems for hedge fund operations and high-speed trading, and apply the lessons learned to develop recommendations for fixing the beleaguered website healthcare.gov. Jim Simons himself will be leading the discussions. Since December 15th is Zamenhof Day, the birthday of the Esperanto creator Ludwik Zamenhof, applications written in Esperanto will be given special consideration.

Okay we are joking about the last topic on hedge funds but wanted to be sure you were reading. Alistair did after all say we could “abbreviate and/or modify this in any way you wish.” But we do have a serious point, and it’s not what you think.

## A Little Quote Logic

We—especially Ken and new Buffalo student Michael Wehar, whose work while a CMU undergrad we covered a year ago—have been thinking about provability predicates in logic and paradoxes arising from interpreting them as ways of quoting something. A proof predicate has the form ${P(f,c)}$ and says that ${c}$ is a valid proof (in a given formal system) of the formula ${f}$. This is the logical analogue of checking the validity of a computation ${c}$ by a particular machine. A provability predicate then has the form ${Pv(f) = (\exists c)P(f,c)}$.

The weird fact, which applies to the same natural strong formal systems ${F}$ that Kurt Gödel’s famous incompleteness theorems hold for, is that there are statements ${f}$ such that ${F}$ proves ${Pv(f)}$. but does not prove ${f}$ itself. Call such a statement ${f}$ an “ambivalence” of ${F}$. Our analogy is that in this post, Alaistair’s request on which we were ambivalent is ${f}$.

Indeed the English phrase “to pass on” has ambivalent meanings: it can mean to transmit or to decline. To “take a pass on” something can mean to decline it or to give it a go. “Special consideration” might be more positive or might be otherwise.

Are there helpful general properties known about such statements ${f}$? One can try to avoid them by adding suitable logical reflection principles to ${F}$, but we wish to know what happens in the original systems. We are also interested in even more paradoxical cases where ${F}$ does not prove ${Pv(f)}$, but ${F + \neg f}$, that is assuming the negation of ${f}$, does prove ${Pv(f)}$. Note that the consistency of ${F}$ is expressed by the statement ${\mathsf{Con_F} = \neg Pv(0=1)}$. We are wondering especially about cases where ${f}$ itself might be ${\mathsf{Con_F}}$ or ${\neg \mathsf{Con_F}}$. Knowing some general properties might also help us with cases like ${F + \neg f}$ proving ${Pv(f')}$ where ${f'}$ is a slight modification of ${f}$, such as ${f = \mathsf{Con_F}}$ but ${f' = \mathsf{Con_{F + f}}}$ or maybe ${f' = \mathsf{Con}_{F + \neg f}}$.

Well, we try to be consistent on this blog, but we can’t prove it.

## Open Problems

Ooops, we were not supposed to actually put this out—this was just one of our brainstorming drafts. Oh well. I guess I clicked the publish button on the WordPress.com site. But for a possible future post or paper, can you help us with understanding ambivalent statements?

1. October 24, 2013 10:42 pm

While I worry over the 121-&-ontological status of non-bulletin boards that post non-bulletins concerning the bulletins they pass on posting … let me divert the dissembled company with the following anecdote …

In a co-op where I lived for a brief time as an undergrad there was a bulletin board with a notice near the top that commanded, “Check The Bulletin Board Every Day ❢”

You can guess what happened …

✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔✔

2. October 24, 2013 11:01 pm

” exceptional young scientists” what is the criteria? It hardly happens students beat their masters in graduate school. Is this just based on a pile of papers? what is the criteria?

• October 25, 2013 2:38 pm

Usually, “it is me” with good record, and recommendation from an adviser works.

October 25, 2013 6:10 am

Can someone please explain the procedures one can take to visit Simons Center if one is more than 6 years past PhD and not eligible to be a research fellow? In this case, is there any type of financial assistance (e.g. for (finding) housing, meals, health insurance) or does one have to pay with one’s own grants?

4. October 25, 2013 8:52 am

Are you thinking of quoting as a function that assigns names to expressions and sequences of expressions (as in a proof), a la Gensym or a Gödel numbering, or do you think of all that as already absorbed in the formal language you are using?

• October 25, 2013 9:29 am

We think of that as absorbed—in particular, we’re not interested in weak formal systems that cannot control sequences etc.

October 26, 2013 6:58 am

Reblogged this on Pink Iguana and commented:
Too bad about the lack of interest in the Hedge Fund Logistics for the Berkeley Programs. That’s why Pink I must forge ahead.
The proof predicates are interesting in light of Knight Captal’s 450MM USD software failure and Appel’s VST results. It’s not clear to me how to bound the length of the theorems to be proved to provably know Knight’s trading algorithm isn’t going to drop another half a billion USD.

• October 26, 2013 11:25 am

Yes, life is rife with perilous situations where we need to evaluate a risk without actually taking it. I guess that’s the connection with negation and quotation, all the acts of critical reflection that hold eval at bay.

October 26, 2013 4:01 pm

Attempting to unravel the GLL claim

“There are statements ${f}$ such that [formal system?] ${F}$ proves ${Pv(f)}$ [that is, $f$ has a proof certificate]. but does not prove ${f}$ itself.

has led me, not to knowledge, but to a wonderful biographical sketch of George Boolos:

Boolos obtained the first PhD in philosophy ever awarded by the Massachusetts Institute of Technology, under the direction of Hilary Putnam.

A charismatic speaker well known for his clarity and wit, Boolos once delivered a lecture giving an account of Gödel’s second incompleteness theorem, employing only words of one syllable. At the end of his viva, Hilary Putnam asked him, “And tell us, Mr. Boolos, what does the analytical hierarchy have to do with the real world?”

Without hesitating Boolos replied, “It’s part of it.”

Uhhh … Oliver Twist would greatly enjoy a single-syllable elucidation of the GLL notion of ambivalent theorems.

And, thanks for yet another terrific GLL essay!

October 26, 2013 4:25 pm

PS  Boolos wrote a wonderful article — just 446 words (plus a two-page formal unraveling) — titled Gödel’s second incompleteness theorem explained in words of one syllable, that has done much to illuminate (for me) what Ken and Dick are talking about. What fun to attempt a similar essay “The decidability of PvsNP explained in words of one syllable … or not”!

October 27, 2013 6:24 pm

Both P=NP and its negation seem to share the following chain of properties:

you can’t prove it
you can’t prove that you can’t prove it
you can’t prove that you can’t prove that you can’t prove it

I wonder how many propositions have this behavior, though I suspect they all belong to complexity theory. In all cases, unprovable undecidability seems to be a new phenomenon, maybe different from what Gödel discovered in 1931 when – at least – he was able to prove all of his claims!

October 27, 2013 2:17 pm

I think there’s some confusion in the discussion of an “ambivalence”. If F proves Pv(f), and F is sound, then it must be the case that F proves f. (I am assuming that Pv() is provability in F.)

A related–but true–statement is that there are formulas with a free parameter f(n), where F can prove “for all n, F proves f(n)”, but F does not prove “for all n, f(n)”.

• October 27, 2013 2:54 pm

Hi Luke,

It seems that your saying, if ZF + X proves ZF + X proves 0=1 and ZF + X does not prove 0=1, then although ZF+X might be consistent, we somehow infer that ZF + X is not sound. Could you elaborate on the notion of soundness that you are referring to. Is it a notion that can be formalized within ZF?

An interesting example:

Apply Godel’s theorem to get a formula Y such that ZF proves [ Y NOT CON(ZF + Y*) ]. Therefore, ZF + Y proves NOT CON(ZF + Y*). Also, ZF + NOT Y proves CON(ZF + Y*).

It follows that ZF + NOT Y proves ZF + Y proves ZF + Y proves 0=1, and ZF + NOT Y proves ZF + Y does not prove 0=1.

Thanks,
Mike

• October 27, 2013 2:57 pm

Some characters did not display correctly. Correction: “formula Y such that ZF proves [ Y if and only if NOT CON(ZF + Y*) ].”

Re: “This is the logical analogue of checking the validity of a computation ${c}$ by a particular machine.”
Did you mean a computation ${f}$?