Timeline for truth vs. provability for ordered fields
Current License: CC BY-SA 3.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 27, 2011 at 20:38 | comment | added | Kaveh | I think natural numbers are definable in the theory of ordered fields using second order quantification, so I guess it is not necessary to add a sort for natural numbers: $$n \in \mathbb{N} := \forall X \ [(0 \in X \land \forall x \ x \in X \rightarrow x+1 \in X) \rightarrow n \in X]$$ | |
| Jul 27, 2011 at 15:24 | vote | accept | James Propp | ||
| Jul 27, 2011 at 11:57 | comment | added | Carl Mummert | On the other hand, if we worry about truth instead of provability, then of course there are equivalent statements that we can't prove equivalent in some particular system. All true statements are equivalent to each other, and all false statements are equivalent to each other, and these are the only equivalence classes with respect to truth. A key reason to look at provable equivalence is this triviality of equivalence of truth values. | |
| Jul 27, 2011 at 11:54 | comment | added | Carl Mummert | In many cases, the properties we want are first order, though, in second-order arithmetic. This is one of the morals of reverse mathematics. There are many results there that can be viewed as showing that certain results require certain fragments of completeness. For example, ACAo can be understood as limit-point completeness, while WKLo can be understood as compactness in the Heine-Borel sense, which turns out to be weaker. | |
| Jul 27, 2011 at 3:02 | comment | added | Timothy Chow | @James Propp: François is correct, but in case you did not follow everything he said, the short answer is that your initial instinct is basically correct: There may be instances where two propositions are equivalent but you have no effective means of proving it. This is because you're interested in properties of the ordered field that may not be first-order. In my opinion, that's all you need to say, and it can be relegated to a footnote. Going into technical details about the difficulties of working with second-order logic will be an unenlightening digression in the context of your paper. | |
| Jul 26, 2011 at 21:05 | comment | added | François G. Dorais | Equality is usually regarded as primitive (for all sorts) but there are formalizations without equality. In that case, you could define equality via extensionality, but then your models may have equal sets that are actually different objects. | |
| Jul 26, 2011 at 20:56 | comment | added | user5810 | Um, wouldn't extensionality be a definition? | |
| Jul 26, 2011 at 20:55 | comment | added | François G. Dorais | Yes, this gives a deductive system which is sound, complete, but not effective. | |
| Jul 26, 2011 at 20:51 | comment | added | Kaveh | We can think of second-order logic with standard semantics as a two sorted first-order logic (one sort for objects, one sort for sets of objects) with a non-recursive set of axioms for the sort of sets. | |
| Jul 26, 2011 at 20:39 | history | answered | François G. Dorais | CC BY-SA 3.0 |