[Note: (1) Meillassoux's argument to contingency is further developed in modal logic HERE, with some dialetheist worries thrown in. (2) A clearer explanation of the difference between Meillassoux and Harman is HERE, including a distinct worry.]
Reading page 26 of Graham Harman's Quentin Meillassoux: Philosophy in the Making, and just put the key argument (of which Harman writes, "This apparently hair splitting point point is actually the key to Meillassoux's entire system, and is worthy of closer attention") in modal logic. If I have not fudged too much by putting things in terms of a knowledge predicate, it definitely works. And in a very weak modal logic to boot, I think classical K but in the next few days I will put it in natural deduction to check.
Basically there is a simple proof from P --> <>KP (if P, then it is possible to know that P, to which the correlationist is arguably committed) to Meillassoux's conclusion ~<>K~<>R --> <>R (if it is not possible to know that R is impossible, then R is possible). Contraposing the correlationist claim gives you ~<>KP --> ~P. But then substitute in ~Q for P and you get ~<>K~Q --> ~~Q, which via classical logic entails ~<>K~Q --> Q (if it's not possible to know that something is false, then it is true). Now substitute in <>R for Q, and you get ~<>K~<>R --> <>R (if it is not possible to know that R is impossible, then R is possible).
That's it. I'll do a proper natural deduction proof (without the substitutions) in the next few days, in part because I want to find out if I had to use classical negation rules above (if I was a better logician I would know this without having to formalize it; but full formalization sometimes yields unexpected interesting things so I don't mind).
The reason this is so mind-blowing is that so much does follow from the incredibly simple point, once you think about it in a way informed by knowledge of German Idealism, as Harman and Meillassoux do. More on that soon. I have to get clearer on how this fits with Meillassoux's other key argument in this context that unthinkability does not entail impossibility. This is how Meillassoux rejects Berkeleyan Idealism while still being a Verificationist (correlationist). But then the Verificationism entails ~<>K~<>R --> <>R, and then some other commitments entail that there are a lot of Rs for which the scheme applies.
It's the fact that for the correlationist the antecedent is maintained for lots of philosophically Rs that entails much of the weird and fascinating aspects of Meillassoux's philosophy (let R equal "humans will survive their death" or "things in themselves exist"), which is why I'm going to get clearer on that next. As far as I'm getting it now, the reason we can't know so many things is from Kantian Dialectic type Finitude arguments (the Verificationism follows from Berkeleyan type arguments).
Interestingly, Meillassoux, like Graham Priest, ends up exploding the Finitude arguments while staying with the Verificationism, and Harman (to some extent like a certain period John McDowell) keeps the Finitude but jettisons the Verificationism. I should note that by saying this I'm not reducing any thinker to any other thinker or just understanding the continental philosophers as shadows of the analytic ones (a horrible, horrible tendency of a lot of analytic "pluralists"). I'm learning all sorts of new things from Meillassoux and Harman, and there are essential respects in which the two differ from the analytic analogues (among other things, Harman is not hobbled by McDowell's quiteism, and this makes a humongous difference).
It's really cool stuff. Any logician readers will have intuited interesting issues involving Fitch's Paradox as well. I have a couple of lines on that (one from Tennant, one from reflection on Moore's Paradox) that I want to try out on Meillassoux this semester.