Timeline for Derivation rules and Godel theorem
Current License: CC BY-SA 2.5
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 28, 2010 at 15:28 | comment | added | Carl Mummert | The set $T$ of sentences that are true in the standard model of arithmetic is not computable (it's not even arithmetical). So no effective set of deduction rules and axioms can prove all the sentences in $T$ without also proving some sentences not in $T$. This is why it's important to worry about the failure of completeness when you change semantics by limiting the class of acceptable interpretations. If you make the semantics too restrictive, there will be no effective, complete, sound proof system This is exactly what happens with full second-order semantics, for example. | |
| Jun 28, 2010 at 15:07 | comment | added | Bogdan Grechuk | Thanks! So, the answer to my question"which derivation rules are called valid" is, roughly, "rules which are sound in all interpretations(models)". But I really like you first answer: If Godel theorem includes only theories that cannot specify additional rules of deduction, then, after adding new deduction rules like mine, we (potentially) can get sound theory whose axioms can be listed by an "effective procedure", but which is capable of proving, say, all true facts about the natural numbers! And you know, I would be happy to have such a theory, even if it is valid in the standard model only! | |
| Jun 28, 2010 at 13:43 | history | answered | Carl Mummert | CC BY-SA 2.5 |