Well, I understand your metaphor, but a computer does not know anything; a computer can only mechanically compute by following the instructions inserted into it. Thus it can compute the consequences of particular assumptions, provided we encode the assumptions and the rules of inference, and insert them into the computer. 

Using a formal language, we can formulate simple true arithmetic sentences (called 'axioms', like that for all x: 0+x=x; 0.x=0; x.(y+1)=x.y+x; the successor of x is not 0, etc.), and simple rules of inference (like "If A then B, and A is true, hence B is true") by means of which we can infer (i.e., prove from the axioms) more complex true arithmetic sentences. Since we are resource-bounded, such a system must be finitary, which means that there must be an algorithm that makes it possible to decide in a finite number of steps whether this or that sentence is an axiom or not.  

If the system of axioms and rules is rich enough, we can prove (in the system) any true sentence of arithmetic. But we would never prove all of them. We'd always find an indepedent true sentence of arithmetic, i.e., the sentence that does not follow from the axioms. Well, we may extend the set of axioms by the newly found true sentence, but there is no mechanic way of telling in advance which axioms you need. Either your system is not complete, or it is not finitary (we say that it is not recursively axiomatised).   
 
Well, now the finitary (i.e., recursively axiomatised) systems can be realised by a computer. Here is how: if we encode the set of chosen axioms and the rules of inference, and insert them into a computer in the form of a computer program, then executing the program will yield more and more complex arithmetic truths.

In this way you may compute any arithmetic truth, but you'd never have all of them. Regardless of how far you generate there is always a true sentence independent of your program.  

The problem consists in the fact that you cannot know in advance which axioms (or axiom patterns) to insert into the computer. The set of all the true arithmetic sentences is not (algorithmically)  computable in such a mechanic way.
 
To put it still in another (rather methaphoric) way, the set of true sentences you can mechanically prove in a finitary (recursively axiomatised) system is as large as the set of natural numbers. But the set of all the arithmetic truths is larger.  
 
As Kurt Goedel said:
Either mathematics is too big for the human mind or the human mind is more than a machine.

By: Marie Duzi at: 17th August, 2009