<?xml version="1.0" encoding="UTF-8"?>

<record version="8" id="9392">
 <title>Penrose's second G\"odelian argument</title>
 <name>PenrosesSecondGodelianArgument</name>
 <created>2007-05-17 07:43:05</created>
 <modified>2007-06-21 21:45:19</modified>
 <type>Topic</type>
 <creator id="17058" name="dankomed"/>
 <author id="17058" name="dankomed"/>
 <classification>
	<category scheme="msc" code="03D80"/>
 </classification>
 <keywords>
	<term>Penrose's first G\"odelian argument</term>
	<term>artificial intelligence</term>
	<term>strong AI thesis</term>
 </keywords>
 <preamble>% this is the default PlanetMath preamble.  as your knowledge
% of TeX increases, you will probably want to edit this, but
% it should be fine as is for beginners.

% almost certainly you want these
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}

% used for TeXing text within eps files
%\usepackage{psfrag}
% need this for including graphics (\includegraphics)
%\usepackage{graphicx}
% for neatly defining theorems and propositions
%\usepackage{amsthm}
% making logically defined graphics
%\usepackage{xypic}

% there are many more packages, add them here as you need them

% define commands here
</preamble>
 <content>In the book \emph{"Shadows of the Mind"} published in 1994 Roger Penrose revisited his argument against the strong AI (artificial intelligence) thesis. In contrast with Penrose's first G\"odelian argument which used G\"odel's first theorem, in 1994 Penrose used modified argument based on G\"odel's second theorem in an attempt to prove that human understanding is beyond computation. Besides of numerous errors in the technical exposition (Feferman, 1995), the argument only shows that strong AI thesis is necessarily false, however is not strong enough to establish superiority of human mind over formal systems (robot mathematicians).

\begin{verse}Strong AI (artificial intelligence) thesis: the human mind is consistent formal algorithm (system).
\end{verse}

The argument against strong AI is direct with the use of G\"odel's second theorem. If we were consistent formal algorithm we wouldn't be able to prove our consistency.

\begin{verse}
Penrose's second G\"odelian argument: strong AI is false, because if we were consistent formal algorithm we wouldn't be able to prove our consistency.
\end{verse}

Some strong AI advocates erroneously tried to escape the argument by philosophical argument that we "believe" we are consistent formal algorithm, and we do not prove it. This is elementary logical fallacy. Simply our scientific theory of mind is based on axioms (postulates), which we accept to be true and we accept that these postulates do correctly describe the reality. Therefore in our scientific knowledge strong AI thesis is either theorem or axiom. What some AI advocates overlook is the fact that axioms are provable! Simply an axiom is provable by any other axiom, and this is basic postulate in mathematical logic. Indeed more generally - every true statement is derivable from any other statement, including the possiblity that it is derivable (provable) from arbitrary false statement. This is indeed the first axiom of propositional calculus $B \Rightarrow (C \Rightarrow B)$.

Therefore Penrose's second G\"odelian argument is correct and strong AI is false. One cannot save the strong AI thesis by playing with the meaning of the words "believe", "understand" or "know". Axioms exactly as theorems are provable, and the colloquial understanding that we \emph{"believe in axioms but we cannot prove them"} is false. Axioms in any system $F$ are provable within $F$.

Of course always remains the possibility for weaker AI thesis insisting that human mind is inconsistent algorithm. This however is not the strong AI thesis, and one must create and study new kind of paradoxical mathematics.

\begin{verse}
"We have seen that minds can behave both as consistent formal systems, and as inconsistent systems. Therefore, if we are to build a machine which can be compared fairly with a human mind it is only logical to expect the machine to behave both consistently and inconsistently, as well." -- Jeff Makey (1995)
\end{verse}

Despite of the fact that Penrose's second G\"odelian argument is successful against strong AI thesis, Penrose's original conviction that he has proved noncomputability of human mind appears to be flawed.

\begin{verse}"Penrose's arguments, if taken to their logical conclusion, show us not that the human mind is noncomputable, but that either the human mind is beyond all mathematics, or else we cannot be sure that it is consistent." --Daryl McCullough (1995)
\end{verse}

References

1. Detlovs V, Podnieks K (2006) \PMlinkexternal{\emph{Introduction to
Mathematical Logic}. Hypertextbook for students in mathematical logic}{http://www.ltn.lv/~podnieks/mlog/ml.htm} 

2. Feferman S (1995) \PMlinkexternal{Penrose's G\"odelian Argument.}{http://psyche.cs.monash.edu.au/v2/psyche-2-07-feferman.html}

3. Makey (1995) \PMlinkexternal{G\"odel's Incompleteness Theorem is Not an Obstacle to Artificial Intelligence.}{http://www.sdsc.edu/~jeff/Godel\%5Fvs\%5FAI.html}

4. McCullough D (1995) \PMlinkexternal{Can Humans Escape G\"odel? A Review of Shadows of the Mind by Roger Penrose}{http://psyche.cs.monash.edu.au/v2/psyche-2-04-mccullough.html}

5. Penrose R (1989) \emph{The Emperor's New Mind: Concerning
Computers, Minds, and The Laws of Physics}. Oxford University Press.

6. Penrose R (1994) \emph{Shadows of the Mind: A Search
for the Missing Science of Consciousness}. Oxford University Press.

7. Penrose (1995) \PMlinkexternal{Beyond the Doubting of a Shadow.}{http://psyche.cs.monash.edu.au/v2/psyche-2-23-penrose.html}

8. Podnieks K (2006) \PMlinkexternal{\emph{What is Mathematics? G\"odel's
Theorem and Around}. Hypertextbook for students in mathematical logic}{http://www.ltn.lv/~podnieks/gt.html}</content>
</record>
