12

In "Raatikainen, P., 2005, “On the Philosophical Relevance of Gödel's Incompleteness Theorems,” , the author argues that Penrose's and others use of Gödel's theorem as an argument against mechanism (and presumably strong AI) - that minds are more powerful than computers because of human's ability to recognize the truth of Gödel sentences - are all flawed.

The basic error of such an argument is actually rather simply pointed out. The argument assumes that for any formalized system, or a finite machine, there exists the Gödel sentence (saying that it is not provable in that system) which is unprovable in that system, but which the human mind can see to be true. Yet Gödel’s theorem has in reality the conditional form, and the alleged truth of the Gödel sentence of a system depends on the assumption of the consistency of the system. That is, all that Gödel’s theorem allows us humans to prove with mathematical certainty, of an arbitrary given formalized theory F, is: F is consistent -> GF.

What he is saying here is that there is no guarantee that a formal system realized by a computer is consistent. Hence there's no guarantee that the Gödel sentences that humans recognize but computers don't are indeed themselves true, and human's aren't necessarily pulling off anything that a computer can't do.

My questions:

  1. How could we possibly construct a computer that isn't consistent? It seems to me that any computer we build would be based on Turing Machines, which are themselves limited by Gödel theorem (via the halting problem).
  2. Can a Turing machine generate an inconsistent formal system? Isn't anything generated by a Turing consistent by definition, since it's rules are contained in the Turing machine's memory?
  3. And if this is the case, that Turing Machines can only generate consistent systems, then is Raatikainen's refutation of Penrose's and similar arguments false?
6
  • "...unprovable in that system, but which the human mind can see to be true." Do you have an example for that?
    – draks ...
    Commented Nov 5, 2015 at 11:26
  • 2
    It is a reference to Godel sentences that in effect assert their own unprovability relative to a Godel encoding system. Such sentences are unprovable within a given formal system but are true in the standard interpretation. Formal systems cannot prove their own consistency (by Godel's second theorem), whereas advocates of the Godel-Penrose-Lucas axis typically maintain that human reasoners can be confident of their own consistency. One might reasonably object that we cannot prove our own consistency and in practice we often are inconsistent - at least across different times.
    – Bumble
    Commented Nov 5, 2015 at 19:11
  • There is an interesting article by Gaifman here: columbia.edu/~hg17/godel-incomp4.pdf in which he argues that what does follow from Godel's theorems is that ultimately we cannot completely figure out our own reasoning processes or possess a complete specification of them.
    – Bumble
    Commented Nov 5, 2015 at 19:17
  • @Bumble: That only follows if you assume that human minds are completely deterministic finite-state machines, with the underlying formal system including sufficient arithmetic, and cannot make free choices to select different "paths of thought"; see my answer for a bit about the last point. Just for fun, I'd argue that PA has no real-world interpretation, nor even Q, because the world is finite. Show me your evidence that the world is infinite in any one aspect and I may change my mind!
    – user21820
    Commented Nov 6, 2015 at 2:06
  • 1
    If you just looked at a Godel sentence, and did not know how it was constructed, a human would doubtless not be able to tell whether it was true or false, you would have to factorize all the numbers (which probably makes it impossible for any human right there) and you would have to know the underlying code key from some other source. So the human only knows more than the machine because it has more context, and if the machine were also given this context as axioms, it would also know the sentence was true. But the broadened theory would need a different set of Godel sentences.
    – user9166
    Commented Aug 6, 2018 at 22:51

5 Answers 5

6

As such, Turing machines are not consistent or inconsistent - formalized systems are. However, once we fix a coding of (e.g.) the syntax of the language of arithmetic, we can view some Turing machines as enumerating the theorems of some formal systems (and every formalized system (its theorems) is enumerated by some machine). Then, when the coding kept fixed, it makes sense to call a machine, derivatively, "consistent" or "inconsistent".

Constructing an inconsistent Turing machine is then strikingly easy: define a machine which simply enumerates all sentences of the language: in particular, it lists a sentence and its negation (for every sentence).

3
  • It would be good to add relevant references to help support your answer. In particular a reference discussing the idea that Turing machines are neither consistent nor inconsistent but formalized systems are. This gives the reader a place to go for more information and it converts your answer from an opinion to reporting on the results of others. Welcome to this SE. Commented Jul 26, 2018 at 12:35
  • 3
    @FrankHubeny I think the author of this reply is the actual author of the paper I cite in my post - I don't know in this case if references are necessary :-) Commented Jul 26, 2018 at 20:17
  • 4
    This is just a reminder of the basic facts. Any textbook will confirm them. Commented Jul 30, 2018 at 5:54
10

For detailed discussions of the so-called Lucas-Penrose arguments, see :

and

Particularly relevant are the comments Gödel gave one of the prestigious Gibbs Lectures at the American Mathematical Society in 1951.

Gödel claimed that what the Theorems do entail (specifically, the Second Theorem) is that mathematics is inexhaustible:

It is this theorem [i.e., the Second Theorem] which makes the incompletability of mathematics particularly evident. For, it makes it impossible that someone should set up a certain well-defined system of axioms and rules and consistently make the following assertion about it: All of these axioms and rules I perceive (with mathematical certitude) to be correct, and moreover I believe that they contain all of mathematics. If someone makes such a statement he contradicts himself.

In the Gibbs Lecture, thus, Gödel acknowledged that [his theorems] do not rule out the existence of an algorithmic procedure (a computing machine, an automated theorem prover) equivalent to the mind in the relevant sense [...]. However, if such a procedure existed “we could never know with mathematical certainty that all the propositions it produce[d were] correct.” Consequently, it may well be the case that “the human mind (in the realm of pure mathematics) [is] equivalent to a finite machine that … is unable to understand completely its own functioning”: a machine too complex to analyze itself up to the point of establishing the correctness of its own procedures. Gödel inferred that what follows from the incompleteness results is, at most, a disjunctive conclusion:

Either mathematics is incompletable in this sense, that its evident axioms can never be comprised in a finite rule, that is to say, the human mind (even within the real of pure mathematics) infinitely surpasses the powers of any finite machine, or else there exist absolutely unsolvable Diophantine problems of the type specified… It is this mathematically established fact which seems to me of great philosophical interest.

In other words, either the mind actually has a non-algorithmic and not fully “mechanizable” nature, or else there exist absolutely undecidable mathematical problems. But [Gödel's Theorems] don’t allow us to go further and conclude that the true disjunct is the first one. According to Gödel, then, what follows from [them], and especially from [the Second one], is that if our mind is a computing machine, it is one such that it “is unable to understand completely its own functioning.”


For further discussions, see :

and :


Comment

I do not agree on statements like :

there exists the Gödel sentence (saying that it is not provable in that system) which is unprovable in that system, but which the human mind can see to be true.

Let assume some "technical" facts regarding Gödel's Incompleteness Theorems :

Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F

The unprovable statement is built-up in such a way that :

F ⊢ G ↔ ¬ProvF(⌈G⌉)

and the proof amounts to : :

if F is consistent, then F ⊬ G,

ff F is 1-consistent [or other condition, strictly "stronger" than consistency], then F ⊬ ¬G.

Up to now, we have only a "syntactical" result, about provability in a (suitable) formal system.

In order to speak of truth, we have to add the "semantical" side [see : Daniel Isaacson, Sufficient conditions undecidability of the Gödel sentence and its truth (2007)].

Assuming that the system F is sound with respect to truth in the structure of the natural numbers (called N), we have that :

F ⊬ G, G is true, and F ⊬ ¬G.

Proof

Assume F ⊢ G; then ProvF(⌈G⌉) and, by the condition F ⊢ G ↔ ¬ProvF(⌈G⌉), we have that G is false. Then, by soundness of F (i.e. F proves only true sentences) : F ⊬ G, contradicting our assumption that F ⊢ G. Thus, by propositional logic : F ⊬ G.

Again by the condition F ⊢ G ↔ ¬ProvF(⌈G⌉), we have that ¬ProvF(⌈G⌉) is true. But G ↔ ¬ProvF(⌈G⌉), and thus G is true

Then ¬G is false; so, by soundness of F : F ⊬ ¬G.

Conclusion : it is not a question of "seeing the truth of ...". We have a strict mathematical proof of a conditional :

"if F is sound, then the Gödel's sentence G (for F) is true".

Thus, the mathematical proof regarding the truth of G relies on assumptions. The basic assumption of the above proof is the soundness of the system F with regards to the natural numbers : a condition that is stronger than consistency.

In fact :

soundness implies consistency, while consistency is strictly weaker than soundness.

There are theories that are consistent but unsound; a simple example is : F ∪ {¬G}.

1
  • One problem with this answer: You can indeed show that F ⊬ ¬G, only assuming that F is consistent (and powerful enough etc.), using Rosser's trick. Adding ¬G to the axioms of F does not function as a counterexample, because that is a new theory with a new Rosser sentence (i.e. for the same reason you can't add G to the axioms).
    – Kevin
    Commented Mar 3 at 0:20
8

We can construct a computer that implements an inconsistent formal theory to which Gödel theorem does not apply just like we can construct a computer that implements Peano arithmetic. A simple example is Meyer's relevant arithmetic R# that allows some contradictions, but uses paraconsistent logic (without the law of explosion) to limit their effect. In R# Meyer was able to prove by finitary means that arithmetical calculations never produce contradictory results despite the presence of more abstract contradictions, not quite what Hilbert wanted, but more than consistent Peano arithmetic allows. Recently McKubre-Jordens and Weber extended R# to inconsistent analysis, there are other interesting inconsistent formal theories that can be implemented just like consistent ones.

However, one does not need inconsistency to question Gödelian arguments. Human "superpower" to recognize the truth of Gödel sentences derives from the non-mystical fact that they are provable in meta-theory, e.g. Gödel sentence for Peano arithmetic is provable in second order arithmetic. Of course, any effective proof theory for second order arithmetic will have its own Gödel sentence, provable in the next one, etc., and none of them can prove them all. But neither can any human. Constructing a Gödel sentence for an effectively axiomatized theory is also a perfectly algorithmic process (after Gödel).

So what this comes down to is the historically attested human ability to find new axioms and new forms of reasoning that were not formalized in advance. As humans "find" them however they disagree about their truth and validity. According to humans called intuitionists, Gödel sentences are not true (or false), and neither is the axiom of choice or even the law of excluded middle. The parallel postulate is only "approximately true" these days. "True" axioms are not so much "recognized" as picked up and adopted because they come handy. But why can't a fancy AI attached to a random number generator and with robotic parts to interact with "reality" do the same? There are already computer programs that generate conjectures, like Graffitti, and something like Prolog can already be used to find proofs for them too. Neural networks, simulated on computers, can "induce" new patterns by "learning", what's to stop them from "inducing" the parallel postulate?

What Gödelian arguments demonstrated so far is that their authors make presuppositions that imply their conclusions without any mediation from Gödel. We might as well say it straight: "history shows that humans can do what no computer can do in principle". Either you believe it or you don't, no theorem can prove or disprove it.

Franzen's Gödel's Theorem: An Incomplete Guide to Its Use and Abuse is a canonical reference for dispelling the mythology surrounding Gödel's result.

4

Inconsistent systems are trivial to develop. The issue regarding inconsistent systems and strong AIs is that it is difficult for us to make a proof statement to prove that any specific AI is "strong," by whatever metric we choose. Mathematical consistency is important for all of our existing proving systems.

Accordingly, if the AI was developed using an inconsistent system, we have few tools available to intentionally make it "strong."

Making an inconsistent system is trivial. Simply create rules which conflict. For example, in programming, there is a very real issue that arises during the end of a process regarding reachable memory. Many languages (java, python, C#, to name a few, plus C++'s shared_ptr) have objects that give lifespan guarantees: as long as you hold a reference to the object, it has to stay around. However, you can come across situations where object A refers to object B and object B refers to object A -- a "reference cycle." If neither object stops referring to the other, they are provably eternal.

At least, they're eternal until the end of a process comes along, which came with its own consistency guarantees: "Processes can be terminated in a finite period of time" and "processes free all of their memory when they are terminated." So we have to break our own rule. There's a period of time at the end of a process where you can't guarantee that you're still pointing at something that's alive. In C++ in particular, this can result in situations that crash because you were promised one invariant (this object will outlive me), while another invariant conflicted (the process ended).

If you needed to adapt it into a Turing machine, simply seek to implement a Turing machine within a system which cannot actually implement all Turing machines "perfectly." The system is inconsistent, because it claims to be a Turing machine, while axioms defining the implementation contradict these claims.

3

You misunderstand consistency. Consistency is a concept defined for formal systems, which consists of both rules and strings of symbols. The rules govern exactly what strings belong to the formal system, which are said to be derivable within the formal system. Consistency just means that the formal system does not derive a contradiction, where contradiction is defined as some fixed string such as "0 ≠ 0". That's all.

A interpretation for a formal system is a mapping of each derived string in an unambiguous way to a truth value, which is in classical logic either "true" or "false". Also, a contradiction must be mapped to "false". A model is an interpretation that maps every derived string to "true". Necessarily, if a model exists for a formal system, then the formal system must be consistent.

Formal systems are commonly based on classical first-order logic, which specifies what strings are well-formed formulae, assertions that involve function symbols, predicate symbols, constant symbols, boolean operations and quantifiers. For any formal system obeying classical first-order logic whose rules are mechanically checkable and includes enough arithmetic (for example Robinson's arithmetic), there is some well-formed formula such that neither it nor its negation is derived by the formal system. This sort of formula is called independent.

The question is whether the human mind follows the rules of some formal system. If so, and the formal system includes enough arithmetic, and the formal system is consistent, then humans can prove that there is an independent sentence for it, specifically the Godel sentence for it (within a meta-system that proves the consistency of Peano Arithmetic), but can easily deduce in the meta-system that the sentence is true, which contradicts the assumption that the human mind is modeled by a formal system that does not derive the Godel sentence. There are various other independent sentences, but the reason for looking at the Godel sentence is that it is true in the meta-system (which can only be formalized by a formal system stronger than the one in question).

The issue here is whether the human mind follows the rules of some consistent formal system that includes enough arithmetic or not. The main problem is that consistency of a formal system is defined as whether a string is derivable, but human minds are not static, so it's not even clear how one should interpret consistency. I've not seen a very careful definition of this so far, but this seems to be the ultimate flaw in the argument, even if we accept consistency of PA.

1
  • Technically we need ω-consistency if we use the original Godel sentence, but Rosser strengthened the incompleteness theorem and showed the theorem works even with bare consistency and that there is a sentence with the same property provable in the meta-system without assuming ω-consistency, appropriately called the Rosser sentence.
    – user21820
    Commented Nov 6, 2015 at 2:09

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .