Artículos con la etiqueta ‘Godel’

A Galois connection between classical and intuitionistic logics

Por • 11 dic, 2013 • Category: Ciencia y tecnología

In a 1985 commentary to his collected works, Kolmogoroff remarked that his 1932 paper «was written in hope that with time, the logic of solution of problems will become a permanent part of the logical curriculum. Creation of a unified logical apparatus dealing with objects of two types – propositions and problems – was intended.» We construct such a formal system QHC, which is a conservative extension of both the intuitionistic predicate calculus QH and the classical predicate calculus QC, and sheds new light on the basics of intuitionism:
1) The only new connectives ? and ! of QHC induce a Galois connection (i.e., a pair of adjoint functors) between the Lindenbaum algebras of QH and QC.
2) Kolmogoroff’s double negation translation of QC into QH extends to an interpretation of QHC in QH that is the identity on QH.
3) Goedel’s provability translation of QH into the classical modal logic QS4 extends to an interpretation of QHC in QS4, which is identified with a fragment of QHC.
Some models of QHC are constructed, including a sheaf-valued model inspired by dependent type theory, which appears to be of interest even as a model of QH (not to be confused with the well-known open-set-valued sheaf models of QH), since it can be seen as a rather accurate formalization of the BHK interpretation of intuitionistism.
The paper is addressed to a general mathematical audience and includes a rather unconventional introduction to intuitionistic logic, featuring (a) a motivation via Hilbert’s 24th Problem and Lafont’s observation that in classical logic, any two proofs of a given theorem are «homotopic»; (b) a derivation of Tarski topological models of QH via a model in «Venn diagrams» of a classical first-order theory extracted from the clauses of the BHK interpretation.



The axiomatic power of Kolmogorov complexity

Por • 18 ene, 2013 • Category: Ciencia y tecnología

The famous Godel incompleteness theorem states that for every consistent sufficiently rich formal theory T there exist true statements that are unprovable in T. Such statements would be natural candidates for being added as axioms, but how can we obtain them? One classical (and well studied) approach is to add to some theory T an axiom that claims the consistency of T. In this paper we discuss another approach motivated by Chaitin’s version of Godel’s theorem where axioms claiming the randomness (or incompressibility) of some strings are probabilistically added, and show that it is not really useful, in the sense that this does not help us to prove new interesting theorems. This result answers a question recently asked by Lipton. The situation changes if we take into account the size of the proofs: randomly chosen axioms may help making proofs much shorter, unless NP=PSPACE.



Resolving Gödel’s Incompleteness Myth: Polynomial Equations and Dynamical Systems for Algebraic Logic

Por • 26 dic, 2011 • Category: Crítica

A new computational method that uses polynomial equations and dynamical systems to evaluate logical propositions is introduced and applied to Goedel’s incompleteness theorems. The truth value of a logical formula subject to a set of axioms is computed from the solution to the corresponding system of polynomial equations. A reference by a formula to its own provability is shown to be a recurrence relation, which can be either interpreted as such to generate a discrete dynamical system, or interpreted in a static way to create an additional simultaneous equation. In this framework the truth values of logical formulas and other polynomial objectives have complex data structures: sets of elementary values, or dynamical systems that generate sets of infinite sequences of such solution-value sets. Besides the routine result that a formula has a definite elementary value, these data structures encode several exceptions: formulas that are ambiguous, unsatisfiable, unsteady, or contingent. These exceptions represent several semantically different types of undecidability; none causes any fundamental problem for mathematics. It is simple to calculate that Goedel’s formula, which asserts that it cannot be proven, is exceptional in specific ways: interpreted statically, the formula defines an inconsistent system of equations (thus it is called unsatisfiable); interpreted dynamically, it defines a dynamical system that has a periodic orbit and no fixed point (thus it is called unsteady). These exceptions are not catastrophic failures of logic; they are accurate mathematical descriptions of Goedel’s self-referential construction. Goedel’s analysis does not reveal any essential incompleteness in formal reasoning systems, nor any barrier to proving the consistency of such systems by ordinary mathematical means.