?
also man kann nicht nur jeden satz der euklidischen geometrie automatisch beweisen, sondern es wurden auch schon programme geschrieben, die das tatsächlich durchführen.
so ein programm kann man zb leicht in der programmiersprache prolog schreiben. ein solches programm ist bestimmt nicht länger als ein paar seiten.
die sache mit dem gödelschen unvollständigkeitssatz ist zwar schon richtig, gilt aber erst für axiomensysteme ab einer bestimmten komplexität (prädikatenlogik 2. stufe und höher). die axiome der euklidischen geometrie lassen sich aber bereits mit der prädikatenlogik 1. stufe ausdrücken. ein problem heißt unvollständigkeit, wenn es nicht möglich ist das problem it einer endlichen zahl von axiomen zu beschreiben. in diesem falle ist es UBERHAUPT NICHT möglich jede wahre aussage zu beweisen. weder durch einen computer noch durch einen noch so genialen menschen!
aber auch wenn das problem "vollständig" ist, dh der gödelsche unvollständigkeitssatz noch nicht gilt, so besteht immer noch das problem der "entscheidbarkeit". dh gibst du einen richtigen satz ein, dann wird das programm irgendwann tatsächlich erkennen, daß der satz richtig ist. gibst du jedoch einen falschen satz ein, dann wird das programm unter umständen ewig rechnen und nie erkennen, daß der satz falsch ist. wenn du also diesem programm einen satz eingibst von dem du nicht weißt, ob er richtig oder falsch ist, mußt du damit rechnen, daß das programm niemals eine lösung findet. das nennt man das "entscheidungsproblem".
die euklidische gemometrie ist zwar vollständig, aber nicht entscheidbar.
das ist jetzt alles etwas vereinfacht dargestellt aber im wesentlichen läufts darauf hinaus.