Got it, that clears it up for me.
I think what confuses ch4rl3s, perhaps, is that the field axioms were presumably designed with the understanding in mind that they would be interpretable within many different models, while the axioms of, say, Peano Arithmetic were presumably designed just with one very particular model in mind, possible interpretation in other models than this standard one being irrelevant under this original intent. But this isn’t a mathematical difference preventing us from treating both of these as proof systems of the same kind; it’s just a psychological difference about human perspectives in crafting them.
But I have no particular desire to reignite the whole ch4rl3s clusterfuck again, so if the above doesn’t clear things up for him, then forget it.
(It is also perhaps the case that ch4rl3s views the field axioms not as a proof system but as a means of picking out certain structures (the ones called “fields”, which are just the models of the field axioms), while viewing PA not as a means of picking out certain structures (the models of PA) but as a proof system. Again, this is just a matter of one’s perspective, not an actual substantive difference.)
I love clusterfucks. Let’s have a link! (I looked through the titles of Ch4rl3s’s posts but didn’t find it…)
It’s buried in a thread where you mightn’t think it would be, and indeed where it probably didn’t belong. See here to start, though it takes a while to get going.
Thanks for the link…
…and, yes, I think you’re right this is a conversation best left uncontinued…
As Indistinguishable so clearly illustrates, it’s not hard to come up with examples of systems that are incomplete. I think that any mathematician at the time of Gödel, if you had told him that the field axioms were incomplete, would have replied that of course they were; they were never meant to be complete. The real impact came on systems like Peano arithmetic (note, not exclusively Peano arithmetic) that people had really hoped would be complete: Sure, there were plenty of statements that had not yet been proven or disproven, but that was viewed as just a matter of insufficient effort, that eventually, each of those statements would be resolved.
Right. Although it’s not clear that people suspected they had yet achieved completeness with PA (or even gave terribly much thought to (the particular system of axioms we now call) PA), certainly moving towards eventually finding and demonstrating the completeness of some sound formal system of proof dealing with this language was the dream (as well as decision procedures for the rest of math more generally). That is, though, a very specific problem: there is precisely one complete set of true sentences in the first-order language of natural number addition and multiplication, so that this amounts to finding a method allowing for the mechanical generation of that particular set; that is, a mechanical decision procedure by which to determine the truth or falsity of sentences in this language (as well, again, as procedures for the rest of math more generally; the idea of the “calculus ratiocinator”).
The mathematical formalization of “mechanical” (i.e., carried out by a computer program) was not yet clear, so what happened next was messy and not always understood immediately. But looking back, it’s clearest reconstructed ahistorically: as we all know, one particular task which cannot be accomplished by a mechanical decision procedure is the halting problem. Another way to say this is that no computably axiomatized true theory proving each true statement of the form “Program P halts” can be consistent and complete, though that might be considered an odd way to phrase it. And, as it turns out by happenstance, the question as to whether some program halts can be computably translated into an equivalent statement in the language of PA, so that, by the reduction of the one problem to the other, the inability to mechanically decide the halting problem gives us the inability to mechanically decide arithmetic truth. And, again, this can be awkwardly rephrased into the fact that no computably axiomatized true theory extending or interpreting PA can be consistent and complete. But this rephrasing obscures that all this is is the halting problem.
GIT1 for computable systems is just the undecidability of the halting problem, no more, no less. [And even the more general applicability of GIT1 would just be a more general version of the undecidability of the halting problem (for alternative notions of computation/definition)]. It’s not so much an incompleteness result as an incomputability/indefinability result. It just wasn’t recognized as such yet (well, Goedel had originally proved it as an indefinability result, but didn’t publish it in this form because such semantical approaches were not in vogue in the mathematical logic community at the time and he feared having his work rejected by the establishment (cited in, for example, Feferman’s essay: “Kurt Goedel: conviction and caution”)). But today, we should.
That having been said, GIT2/Loeb’s theorem (that if a suitable proof system proves its own soundness with respect to some proposition, then it furthermore actually proves that proposition) takes this further and does have a thoroughly logical flavor. It’s the one that really deserves all the attention.
[I always have this feeling like I repeatedly unintentionally come across like I’m passionately disagreeing with **Chronos** for some reason. That last post was meant to be an explicit agreement with **Chronos**'s last post. Why I ballooned it beyond the first two sentences, I don’t know]
Of course, saying “it’s just the halting problem” just translates the question of proving Gödel’s theorem into the question of proving Turing’s theorem. I’m not sure that either is really any simpler than the other (in the human-language expressions of them, at least, given that fundamentally they’re just different ways of looking at the same thing).
Don’t worry about looking like you’re arguing with me: You (and I, though perhaps to a lesser extent) just like to make what you say very precise and correct in nuance. I understand, and don’t hold it against you at all.
I appreciate all the comments and elaborations, though I frankly have grasped but a fraction of the material…
Ok, so there are statements in Peano arithmetic (and other systems) that can be neither demonstrated true nor false (within the rules of that system). Thus Peano is incomplete (in common with other systems where there were no hopes of them being complete).
Assuming a system that one might have hoped to be complete, like apparently Peano
Is there a complement to the incompleteness theorem? Are there theorems that show what sort of statements are provable, whether or not they actually have been proved? How powerful are such theorems? I.e what is their scope? Do any of them cover an appreciable collection of unsolved problems? Do any set of them cover a majority of nontrivial unsolved problems?
Separately, does Godel’s theorem at least hint at that which is provable, by implication?
Yeah. I just think a lot of people are more directly familiar with the concept when presented as Turing’s theorem, so that, for them, realizing the equivalence is helpful for shedding light on Goedel’s theorem.
True.
True.
False. And this is where the problem starts.
2 is not a symbol in first order logic, and it’s not a symbol in the field axioms. And we can’t even ask the question yet.
Fine, a convention, now we can talk about it, because 1+1 is defined in the field axioms.
The field axioms can be extended to talk about integers, or reals, but they define a perfectly good system by themselves. They define a set {0,1} and operators (+,*) and several interactions. Using just the field axioms, I can complete the truth table for this set. (And unless we extend the axioms, this is the proof system we’re using.)
It’s false when talking about the integers, and true when talking about the reals. But comparing those two is mixing two proof systems and trying to decide absolute provability based on every possible extension of the field axioms.
And guess what. I can find it’s truth value when using just the base axioms. Let’s fill in the truth table.
0+0=0 (0 is the additive identity, for all a in F, a+0=0)
0+1=1 (same identity)
1+0=1 (same identity, plus commutative property, a+b=b+a for all a,b in F)
1+1=0 (There exists an additive inverse, it isn’t 0, so 1 must be it’s own inverse.)
01=0 (1 is the multiplicative identity, for all a in F, a1=a)
10=0 (same, plus commutative property, for all a,b in F, ab=ba)
11=1 (multiplicative identity again, so far it’s been easy.)
00=? this is the only “tough” one, and it’s not that tough. we are guaranteed that a(b+c)=ab+ac for all a,b,c in F.
use a=0,b=0,c=1. so… 0*(0+1)=(00)+(01). and (0+1)=1 and (01)=0
substitute… 01=(00)+0 and (00)+0=(00) (additive identity again.)
0 =(00)
0*0=0 truth table complete.
use the convention (1+1). “Is there an x in F such that x*x = 1+1?”
1+1=0, and 0+0=0, so if x=0 the statement is true.
extend the axioms to be about integers, and the statement is false.
extend it to be about reals instead, and the statement is true.
each one is it’s own proof system.
There is no absolute provability/unprovability for every possible extension of our base axioms. only provable/unprovable within a given extension.
this statement is true when you start with no axioms, or if you start with any set of axioms as a base.
The field axioms themselves are one proof system. the axioms extended with the integers constitute a separate proof system. the axioms extended with the reals constitutes another separate proof system.
And this question is decidable, (one way or another,) within any particular extension of the field axioms. And within any system in which we can ask the question. This is not a question which shows anything whatsoever about incompleteness.
you’re only having trouble deciding it because you won’t choose one proof system, and you’re trying to compare every possible proof system that starts with the field axioms. When you already admitted that that’s not a valid comparison.
the statement is provable; I did it. and the axioms by themselves constitute a complete and consistant system. the truth table is full, and consistant, and we can answer any question that can be asked in the system. There are extensions that would be incomplete, or inconsitant, or both, but the axioms by themselves are a complete system. and even if we take an inconsistant or incomplete extension, this particular question is still answerable in that system.
Wasting my time:
Ok, but just because (on some presentation) the only primitive terms in the field axioms (i.e., the axioms I gave) are “0” and “1”, it doesn’t follow that those axioms prove that all objects are either 0 or 1. [Just as the only primitive term in Peano Arithmetic is 0, but of course PA doesn’t prove that all objects are equal to 0]. Thus, you go wrong in the following:
You are implicitly using the assumption here that the axioms I gave include the presupposition that all objects are equal to either 0 or 1. That’s illegitimate. The axioms I gave are not meant to carry that presupposition. Indeed, the axioms I gave don’t prove that 1 + 1 = 0. After all, there are models of the axioms I gave (i.e., structures in which this language can be interpreted where the axioms I gave are true) where 1 + 1 does not equal 0.
The field axioms prove all and only those things which are true in all fields. That is, after all, the very definition of fields: to be a field is to be a model of the field axioms.
Let’s have Ch4rl3s’s proof that there is an x such that x * x = 1 + 1, done as rigorously as possible given the context and format of this discussion. I know you sketched a proof above, but I’d like to see it laid out fairly completely so we can see if it works.
True.
2 can be defined using nothing but first order logic; else, no first order theory could talk about 2. So, if you don’t want to argue that a language can’t talk about an object defined in its terms, you have no case. Remember, the definition of completeness includes every statement that can be made in a certain language; so, even accepting your curious resistance to the number 2, every statement that contains the number 2 can be rephrased in such a way as to contain the definition, in the appropriate language, of 2, and thus becomes a statement comprised only of ‘symbols in first order logic’; thus, if a system of axioms neither proves nor disproves this statement (in which 2 has been replaced by its definition and which is therefore a statement in ‘pure’ first order language, the same language the axioms are in – which it of course also is if it does mention 2), it is incomplete.
No; all you’ve succeeded in doing is to construct a field – a model of the field axioms – in which there exists a square root of 2. If it were actually true that the field axioms proved the existence of 2’s square root, then there could not be any field in which there doesn’t exist a square root of two (assuming consistency).
Someone is.
Peano Arithmetic uses several axioms to define what numbers exist. From the wikipedia listing.
etc.
From PlanetMath.org. http://planetmath.org/encyclopedia/PeanoArithmetic.html
Really? I’m supposed to assume that we’re going to be adding other axioms when I try to see what this set of axioms proves? 0 and 1 are defined to exist by axiom. Nothing else is. I can extend the axioms with something like.
for every n in F, there exists an n[sub]1[/sub], (called the successor,) such that n[sub]1[/sub]=n+1.
for every n in F, n[sub]1[/sub] is in F as well.
0 is not the successor of any number.
There. New axioms to define the natural numbers. Oh, look, those look a lot like the peano axioms. (axioms used to define the set of numbers we’ll be using. what a novel idea. why didn’t anyone ever think of that before today?)
What axiom do I have to add to the field axioms before you will agree that I am talking about the finite field with only 2 members? Do I have to specifically add an axiom to say that there will be no more axioms? Ha! I don’t think so.
When I start to prove what an axiom set proves, I use only the axiom set, and not some nebulous imagining of possible extensions.
And even if you don’t buy that. (There’s no reason not to accept that, it’s how math is done. But, I imagine you’re likely to be contrary.) The field axioms extended with integers is a specific proof system, and the field axioms extended to be about reals is a separate specific proof system.
ZF is one proof system. ZF with the axiom of choice, (ZFC,) is a new proof system. ZF with some other axiom added is a different proof system.
The field axioms are one proof system. Field axioms with integers is another. And field axioms with reals is a third.
Yes, there are models where 1+1 != 0. Once you’ve added numbers and defined their interaction by axiom. For example. adding a successor function, as above, creates a set of numbers where 1+1 != 0. But until you do that, you work with {0,1}
As I described above in my response to Indistinguishable, 2 is a constructed ‘number.’ you define it by axiom.
Perfectly willing to argue on those terms.
I never claimed that the field axioms prove a square root of two for every possible field. We can certainly talk about what is true/false in every possible field. As an intellectual exercise. Not as a discussion of “well, because the specific proof set of the field axioms extended with integers comes up with a different answer from the proof set of the field axioms extended with reals, Godel’s result wasn’t new or meaningful.”
That is, once again, (or still,) trying to make an absolute provable/unprovable claim across multiple proof systems. I think I see a glimmer of what you’re trying to do. You have been asking about what is true in all fields, right? that is a comparison that has no bearing on provable/unprovable for Godelian purposes.
Like I said, pick one.
Speaking about what is true/false in all fields. I say that the question: “Is there an x in F such that x*x=1+1?” is answerable in all possible fields. You don’t get the same answer in each one. But you do get an answer. It has no bearing on unprovablility. each possible field, (which is its own proof system,) answers this question, and is not incomplete because of this question. (There may be other questions that make a particular field incomplete, but this question isn’t it.)
I can prove that the question has an answer in every possible field. Not that it’s true in every possible field.
I think I see where their difference of opinion is, though. They are asking what would be true in every possible field. That is not one single proof system. That is asking what is true across multiple proof systems. Interesting, and important question. But not about unprovability.
That’s like saying “Bill has an orange. Joe doesn’t. So it isn’t possible to prove that any person has oranges, since some of them do and some don’t.”
I guess he’s been saying that it isn’t possible to prove, “has an orange” from “personhood.” true. it isn’t.
But it doesn’t mean provable/unprovable isn’t possible for any particular person. That, I can’t ever say if a person has an orange.
In the sense that he’s been talking about provable/unprovable, it doesn’t have meaning unless you’re talking about one specific person, or proof system.
How many times do I have to quote this?
Each person is their own “proof system” for the question of oranges. personhood is asking provable/unprovable across multiple proof systems.
when would doing this have meaning? Guess what, after looking at that quote several times now, I can see absolute provable/unprovable.
If you could prove from a set of axioms that every possible extension had a certain property, then it’s true for every one. It would be absolutely provable. If you could show that every possible extension didn’t have a certain property, then it’s false for every one. It’s absolutely unprovable. But, all that does is give you a short hand for knowing what the answer to a question will be when you pick any one system. And if that were the case, then I could know that this property is not one to look for when deciding if any one of those proof systems has a completeness problem.
And, If I can prove that a certain question has an answer for all possible extensions, then that question doesn’t contribute to incompleteness for any one of them. [sub]edit[/sub](Even if it’s true in one system, and false in another. So, if it’s true for all, no completeness problem for any of them; if it’s false for all, no completeness problem for any of them; if it’s answerable for all, there’s still no completeness problem for any of them.)
Is it not the case that everything provable from the field axioms is true of all possible fields?
And didn’t you say earlier that you can prove, from the field axioms alone, that there is an x such that x*x = 1+1?
Wouldn’t it follow, then, that in every possible field, 1+1 has a square root?
Isn’t this inconsistent with your earlier claim that you can prove from the field axioms alone that there is such an x?
(Maybe I misunderstood what you were claiming to be able to prove.)
Edited to add: From your post simultaneous with mine t I see you’re not claiming you can prove the existence of such an x from the field axioms alone so never mind.