So, no need to apply? :)

*Seeking Research Fellows in Type Theory and Machine Self-Reference*

The Machine Intelligence Research Institute (MIRI) is accepting 
applications for a full-time research fellow* to develop theorem provers 
with self-referential capabilities*, beginning by implementing a strongly 
typed language within that very language. The goal of this research project 
will be to help us understand autonomous systems that can prove theorems 
about systems with similar deductive capabilities. Applicants should have 
experience programming in functional programming languages, with a 
preference for languages with dependent types, such as Agda, Coq, or Lean.

MIRI is a mathematics and computer science research institute specializing 
in long-term AI safety and robustness work. Our offices are in Berkeley, 
California, near the UC Berkeley campus.

Type Theory in Type Theory

Our goal with this project is to build tools for better modeling reflective 
reasoning in software systems, as with our project modeling the HOL4 proof 
assistant within itself. There are Gödelian reasons to think that 
self-referential reasoning is not possible in full generality. However, 
many real-world tasks that cannot be solved in full generality admit of 
effective mostly-general or heuristic approaches. Humans, for example, 
certainly succeed in trusting their own reasoning in many contexts.

There are a number of tools missing in modern-day theorem provers that 
would be helpful for studying self-referential reasoning. First among these 
is theorem provers that can construct proofs about software systems that 
make use of a very similar theorem prover. To build these tools in a 
strongly typed programming language, we need to start by writing programs 
and proofs that can make reference to the type of programs and proofs in 
the same language.

Type theory in type theory has recently received a fair amount of 
attention. James Chapman’s work is pushing in a similar direction to what 
we want, as is Matt Brown and Jens Palsberg’s, but these projects don’t yet 
give us the tools we need. (F-omega is too weak a logic for our purposes, 
and methods like Chapman’s don’t get us self-representations.)

This is intended to be an independent research project, though some 
collaborations with other researchers may occur. Our expectation is that 
this will be a multi-year project, but it is difficult to predict exactly 
how difficult this task is in advance. It may be easier than it looks, or 
substantially more difficult.

Depending on how the project goes, researchers interested in continuing to 
work with us after this project’s completion may be able to collaborate on 
other parts of our research agenda or propose their own additions to our 

- pt

On Monday, April 15, 2019 at 1:28:22 PM UTC-5, Cosmin Visan wrote:
> Hmm... the thing is that what I'm arguing for in the book is that 
> self-reference is unformalizable, so there can be no mathematics of 
> self-reference. More than this, self-reference is not some concept in a 
> theory, but it is us, each and everyone of us is a form of manifestation of 
> self-reference. Self-reference is an eternal logical structure that 
> eternally looks-back-at-itself. And this looking-back-at-itself 
> automatically generates a subjective ontology, an "I am". In other words, 
> the very definition of the concept of "existence" is the 
> looking-back-at-itself of self-reference. So, existence can only be 
> subjective, so all that can exists is consciousness. I talk in the book how 
> the looking-back-at-itself implies 3 properties: identity (self-reference 
> is itself, x=x), inclusion (self-reference is included in itself, x<x) and 
> transcendence (self-reference is more than itself, x>x). And all these 
> apparently contradictory properties are happening all at the same time. So, 
> x=x, x<x, x>x all at the same time. But there is no actual contradiction 
> here, because self-reference is unformalizable. The reason why I get to 
> such weird conclusions is explored throughout the book where a 
> phenomenological analysis of consciousness is done and it is shown how it 
> is structured on an emergent holarchy of levels, a holarchy meaning that a 
> higher level includes the lower levels, and I conclude that this can only 
> happen if there is an entity called "self-reference" which has the above 
> mentioned properties. So as you can see, there pretty much cannot be a 
> mathematics of self-reference.
> I will also present about self-reference at The Science of Consciousness 
> conference this year at Interlaken, Switzerland, so if you are there we can 
> talk more about these issues.
> On Thursday, 11 April 2019 02:55:55 UTC+3, Bruno Marchal wrote:
>> Hi Cosmin,
>> It seems your conclusion fits well with the conclusion already given by 
>> the universal machine (the Gödel-Löbian one which are those who already 
>> knows that they are Turing universal, like ZF, PA, or the combinators + 
>> some induction principle).
>> Self-reference is capital indeed, but you seem to miss the mathematical 
>> theory of self-reference, brought by the work of Gödel and Löb, and Solovay 
>> ultimate formalisation of it at the first order logic level. You cite 
>> Penrose, which is deadly wrong on this.
>> In fact incompleteness is a chance for mechanism, as it provides almost 
>> directly a theory of consciousness, if you are willing to agree that 
>> consciousness is true, indubitable, immediately knowable, non provable and 
>> non definable, as each Löbian machine is confronted to such proposition all 
>> the “time”. But this enforces also, as I have shown, that the whole of 
>> physics has to be justified by some of the modes of self-reference, making 
>> physics into a subbranch of elementary arithmetic. This works in the sense 
>> that at the three places where physics should appear we get a quantum 
>> logic, and this with the advantage of a transparent clear-cut between the 
>> qualia (not sharable) and the quanta (sharable in the first person plural 
>> sense).
>> You seem to have a good (I mean correct with respect to Mechanism) 
>> insight on consciousness, but you seem to have wrong information on the 
>> theory of the digital machines/numbers and the role of Gödel. Gödel’s 
>> theorem is really a chance for the Mechanist theory, as it explains that 
>> the digital machine are non predictable, full of non communicable 
>> subjective knowledge and beliefs, and capable of defeating all reductionist 
>> theory that we can made of them. Indeed, they are literally universal 
>> dissident, and they are born with a conflict between 8 modes of 
>> self-apprehension. In my last paper(*) I argue that they can be 
>> enlightened, and this shows also that enlightenment and blasphemy are very 
>> close, and that religion leads easily to a theological trap making the 
>> machine inconsistent, except by staying mute, or referring to Mechanism 
>> (which is itself highly unprovable by the consistent machine).
>> Bruno

You received this message because you are subscribed to the Google Groups 
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
To post to this group, send email to
Visit this group at
For more options, visit

Reply via email to