22:13
Hey guys. I've got a question I'm thinking about fleshing out and posting here... mind if I run it by y'all?
I've been thinking about computer proof assistants. Any given proof assistant will have a certain logical theory which it implements.
The problem is, it seems like it's impossible for any logical theory to be "satisfactory".
In order for a logical theory to be satisfactory, it should be possible to study it and determine that it has these two properties:
1. Each of the axioms of the theory is a true statement.
2. Every statement which we can possibly prove (using our intuitions and natural language) is a theorem of the theory.
Let me modify that second criterion, actually.
2. Given any statement, if it's a statement whose truth we can be convinced of, then it's a theorem of the theory.
Suppose we've studied a theory and found it to be "satisfactory" in this sense. Well, each of the axioms of the theory is a true statement, so that convinces me that the theory is consistent. So, since we've been convinced that the theory is consistent, criterion 2 requires the theory to have "the theory is consistent" as a theorem.
But that's not possible if the theory actually is consistent.
