akuklev: (Свечка и валокардин)


We regard theory as a conglomerate of a language for writing statements, a language for writing valid proofs and a collection of axioms (basis of statements the theory assumes to be true). A theory is said to be consistent if there is no pair of valid proofs proving contradictory statements. A theory is said to be capable of reflection iff it's possible to write the statement "this theory is consistent" in the language of the theory itself.

There are three main results concerning consistency:
1) (Gödel's Second Incompleteness Theorem) All common non-trivial theories cannot prove their own consistency. This applies essentially to all theories that include the notion of an infinite ordered set with a distinguished zero object (e. g. natural numbers) and provide a way to construct a larger object for any given one.

2) (Gentzen's Algorithm) For common theories there is an algorithm that "analytically verifies" their proofs. Analytically checked proofs can be directly shown to be contradiction-free. This does not contradict to the (1) because no theory which is subject to (1) can internally show that verification algorithm holds for every valid input.

3) (Dan Willard's Self-verifying theories) There are non-trivial exceptions to (1). They are not only capable of reflection, but even prove their own consistency.

The theories (3) share a common property: their proofs can be analytically verified inplace. Whereas for theories which Gödel's Theorem (1) applies the algorithm normally requires enormous amounts of additional working space. This goes so far that analytical verification of some proofs could be fundamentally physically infeasible due to finiteness of the visible universe.

This could be a clue to understanding the Gödel's Theorem (1): maybe the true reason we cannot show Gentzent's algorithm to succeed always without additional assumptions exactly because it doesn't phyiscally do so.

In this case we could use a physical estimate for information content of the visible universe and restrict our attention to proofs of the "modest" length which are at least in theory verifiable. Then we'd be pretty sure that these proofs are definitely noncontradictous. If it would turn out that upper bound on proof length is beyond that of normal human-developed proofs, a longstanding question about solidity of mathematical foundations would be at least partially solved.

Now how can we find the upper bound for proof length starting with informational content of the universe? It appears that the following approach could roughly do.

The Programme

Read more... )

December 2016

456789 10


RSS Atom

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 21st, 2017 03:48 pm
Powered by Dreamwidth Studios