3 ms·

Russell's paradox deals with self-referencing logically unconstructible objects, not with the impossibility of proving anything as existing. >Formal proofs are

Russell's paradox deals with self-referencing logically unconstructible objects, not with the impossibility of proving anything as existing. >Formal proofs are syntactic. […] This confuses means of formal proof with meanings attached to them. A proof, whatever the means used to perform it, only matter to conscious beings. A computer can help to solve a logical problem, but so far none have been catched wondering which logical problem would be interesting to solve as its next challenge – as far as I know.

lidHanteyk 7y ago
In mathematics, we do actually take logically self-defeating objects to be non-existent, as a matter of classical reasoning: If they don't exist, then they must not-exist; otherwise, they would exist, and immediately defeat themselves in a puff of logic [5]. Such classical reasoning can reject a large number of similarly-shaped objects [2], and Russell's antimony is actually only the tip of the iceberg of a bundle of formal results, notably Tarski's [3] and Lawvere's [4]. The Gödel Machine algorithm [0][1] is only a few years old, and it cannot yet be tested due to practical hardware constraints, but it provably implements a system which wonders, specifically, about which direction of proof search will speed up its ability to search for proofs, to consider directions, or to wonder. [0] https://en.wikipedia.org/wiki/G%C3%B6del_machine https://en.wikipedia.org/wiki/G%C3%B6del_machine [1] http://people.idsia.ch/~juergen/goedelmachine.html http://people.idsia.ch/~juergen/goedelmachine.html [2] https://terrytao.wordpress.com/2009/11/05/the-no-self-defeating-object-argument/ https://terrytao.wordpress.com/2009/11/05/the-no-self-defeat... [3] https://en.wikipedia.org/wiki/Tarski's_undefinability_theorem https://en.wikipedia.org/wiki/Tarski's_undefinability_theore... [4] https://ncatlab.org/nlab/show/Lawvere's+fixed+point+theorem https://ncatlab.org/nlab/show/Lawvere's+fixed+point+theorem [5] https://tvtropes.org/pmwiki/pmwiki.php/Main/PuffOfLogic https://tvtropes.org/pmwiki/pmwiki.php/Main/PuffOfLogic

lidHanteyk 7y ago

In mathematics, we do actually take logically self-defeating objects to be non-existent, as a matter of classical reasoning: If they don't exist, then they must not-exist; otherwise, they would exist, and immediately defeat themselves in a puff of logic [5]. Such classical reasoning can reject a large number of similarly-shaped objects [2], and Russell's antimony is actually only the tip of the iceberg of a bundle of formal results, notably Tarski's [3] and Lawvere's [4]. The Gödel Machine algorithm [0][1] is only a few years old, and it cannot yet be tested due to practical hardware constraints, but it provably implements a system which wonders, specifically, about which direction of proof search will speed up its ability to search for proofs, to consider directions, or to wonder. [0] https://en.wikipedia.org/wiki/G%C3%B6del_machine https://en.wikipedia.org/wiki/G%C3%B6del_machine [1] http://people.idsia.ch/~juergen/goedelmachine.html http://people.idsia.ch/~juergen/goedelmachine.html [2] https://terrytao.wordpress.com/2009/11/05/the-no-self-defeating-object-argument/ https://terrytao.wordpress.com/2009/11/05/the-no-self-defeat... [3] https://en.wikipedia.org/wiki/Tarski's_undefinability_theorem https://en.wikipedia.org/wiki/Tarski's_undefinability_theore... [4] https://ncatlab.org/nlab/show/Lawvere's+fixed+point+theorem https://ncatlab.org/nlab/show/Lawvere's+fixed+point+theorem [5] https://tvtropes.org/pmwiki/pmwiki.php/Main/PuffOfLogic https://tvtropes.org/pmwiki/pmwiki.php/Main/PuffOfLogic