2 added 358 characters in body edited Sep 20 '17 at 7:25 Alexey Romanov 2,3421111 silver badges1616 bronze badges The deriver is complete, since it will eventually be able to prove all true statements and disprove all false statements. This means the deriver is inconsistent, so it cannot know whether a set of axioms used to prove Goedel's 1st are consistent. To start with, your deriver is actually not an axiomatic system to which Goedel's theorem would apply. But assuming I understood your description correctly, it'll simply "prove" all sentences because for two different reasons: 1) for each sentence there is a system where it's an axiom and so provable; 2) systems it enumerates will include inconsistent systems in which every sentence is provable. So the deriver is trivially inconsistent and tells you nothing about Goedel's theorem. Now, instead of your deriver consider one which enumerates all proofs in $$PA$$ until it finds a proof of Goedel's first theorem and then stops. This seems to satisfy your requirements ("seems" because you don't define "prior knowledge"). The deriver is complete, since it will eventually be able to prove all true statements and disprove all false statements. This means the deriver is inconsistent, so it cannot know whether a set of axioms used to prove Goedel's 1st are consistent. To start with, your deriver is actually not an axiomatic system to which Goedel's theorem would apply. But assuming I understood your description correctly, it'll simply "prove" all sentences because for each sentence there is a system where it's an axiom and so provable. So the deriver is trivially inconsistent and tells you nothing about Goedel's theorem. The deriver is complete, since it will eventually be able to prove all true statements and disprove all false statements. This means the deriver is inconsistent, so it cannot know whether a set of axioms used to prove Goedel's 1st are consistent. To start with, your deriver is actually not an axiomatic system to which Goedel's theorem would apply. But assuming I understood your description correctly, it'll simply "prove" all sentences for two different reasons: 1) for each sentence there is a system where it's an axiom and so provable; 2) systems it enumerates will include inconsistent systems in which every sentence is provable. So the deriver is trivially inconsistent and tells you nothing about Goedel's theorem. Now, instead of your deriver consider one which enumerates all proofs in $$PA$$ until it finds a proof of Goedel's first theorem and then stops. This seems to satisfy your requirements ("seems" because you don't define "prior knowledge"). 1 answered Sep 20 '17 at 7:20 Alexey Romanov 2,3421111 silver badges1616 bronze badges The deriver is complete, since it will eventually be able to prove all true statements and disprove all false statements. This means the deriver is inconsistent, so it cannot know whether a set of axioms used to prove Goedel's 1st are consistent. To start with, your deriver is actually not an axiomatic system to which Goedel's theorem would apply. But assuming I understood your description correctly, it'll simply "prove" all sentences because for each sentence there is a system where it's an axiom and so provable. So the deriver is trivially inconsistent and tells you nothing about Goedel's theorem.