Logical Induction

This implies second order logic. It is not clear to me, whether the loss of consistency is warranted. Type Theories are tried to avoid inconsistence. However high the order of the processing logic is, its only reason to exist is to output first order theorems, those we can prove decidable.

> But with this article, the hope is that a formal system can show that the statement about itself is probably true.

Probabilty is not good enough. The Bayesian Conspiracy sure is strong, but I'd prefer to stay with first order logic and finite state machines that are provably correct.

> > The short answer is that this theorem illustrates the basic kind of self-reference involved when an algorithm considers its own output as part of the universe

Isn't that what differential equations are for? I'm tired of the liars paradoxon. Intuitively, I've settled on the presumption that paradoxa always rest on wrong assumptions.

I'm no mathematician, but I refuse the notion that I am inherently unable to be certain. That's why algorithms are by my preferred definition bound to be deterministic. I'd like to be able to tie this in with the Chomsky Hierarchy, albeit I am not that advanced. I'm no mathematician and I'm impressed by quines. I guess, the halting problem implies that quines cannot always be predicted. Heuristics help there and that's what stochastic is all about.

Let me be clear. The paradoxon "this sentence is a lie" is neither a sentence, nor a lie. That's a question of definition. Of course I'm in no position to say a similar thing about Goedels incompleteness theorem, and I even referred to it's result in higher order logics, but I still doubt the relevance, as many seem to be ignorant of his former completeness theorem.

The higher order logic and self reference is related to recursively enumerable grammars low in the Chomsky Hierarchy. Though, if ordered by magnitude, I'd call it higher. I hope, if the goal is natural language, we don't need to aim that high. If you want a computer that computes computers, though, go for it.

> A formal system cannot achieve this by simulating itself.

The type of self similarity used in quines or the liars paradox seems to play an important role in what we perceive as intelligent. Although, I stipulate, the intelligence involved is the ability to tell the difference between a misleading liars paradox and constructively provable quines. Of course, a machine that doesn't need verification from the supervising developer would be akin to a perpetuum mobile.

It is easy to supervise the AGI's output by the less intelligent machines that have to do the output. The focus is on optimizing the processes, not the inability to assert safety guidelines.

Edit: mixed up the order of the Chomsky Hierarchy.

Careful. An event can have probability 1 even if its complement isn't empty: https://en.wikipedia.org/wiki/Almost_surely

But Yes, most common higher-order provers are semi-automatic, you need to give them a hint about which proof strategy to use. That's mainly because they are used that way, not any principal limitation. You won't find many mathematicians who are interested in a theorem prover to spit out some (alleged) theorem by itself, and then let the mathematician check whether it's useful.

The only fully automatic higher-order theorem prover that I know of is ETPS, it will select proof strategies by itself if you don't indicate them. But it's also one of the oldest and slowest and mainly just used for teaching logic.

http://danroy.org/papers/FreRoyTen-Turing.pdf -- TOWARDS COMMON-SENSE REASONING VIA CONDITIONAL SIMULATION: LEGACIES OF TURING IN ARTIFICIAL INTELLIGENCE

http://www.mit.edu/~tomeru/thesis/tomerThesis.pdf -- On the Nature and Origin of Intuitive Theories: Learning, Physics and Psychology