3 ms·
Whenever you have a structure M of some language L you can take the so called complete theory of the structure, denoted Th(M), which is just the set of all L-se
by ginnungagap 8y ago
Whenever you have a structure M of some language L you can take the so called complete theory of the structure, denoted Th(M), which is just the set of all L-sentences true in M. In particular if L is the language of PA and M are the standard natural number with the standard operations Th(M) is a theory called true arithmetic. This theory is complete (that's because Th(M) is always complete) and clearly enough to talk about the integers, but it escapes Gödel's theorem since it's axioms are not recursively axiomatizable.
You seem to be confusing "true" and "provable", as far as first order logic is concerned those are equivalent (by another theorem of Gödel, the completeness theorem), but the first in defined in terms of models and the second is purely syntactic
- mietek 8y agoYou seem to be forgetting that constructive truth means provability. Also, it doesn’t seem right to use the informal “take” when the object in question is not computable.
- ginnungagap 8y agoI specified I'm working in standard first order logic. And I'm not sure what do you mean with the informal take. Also intuitionist logic is not my area, but isn't it divided in inference rules for provability and (Heyting or Kripke) semantic for model theory and truth just like FOL?
- mietek 8y agoYou may be working in classical logic, but that doesn’t mean the parent poster is. You asserted the parent poster seems to be confused, but what the parent poster said makes sense in a constructive setting. Please see my other comment: https://news.ycombinator.com/item?id=18756974 https://news.ycombinator.com/item?id=18756974
- skh 8y agoInformally speaking we can take the set of all real numbers. Assuming we are using standard mathematics that most working mathematicians use then this includes non-computable numbers. Sets don’t have to be computable to be used unless you are someone who works with non-standard models of set theory.