The hijack about proof theory

Great Debates
1

This is a continuation of a debate conversation from this thread.

I wasn’t sure whether to put it in GD or IMHO. But in any case, here it is.

See linked thread for background. It’s the conversation about proof theory, discussing fields and presburger axioms and things like that.

I keep swearing I’m going to give up on the conversation any moment now–but I’m one of those people who just can’t stop trying to convince brick walls of things that are manifestly true. :wink: (Said all in good fun, Ch4rl3s :p)

I still think I’m going to give up any minute now.

2

The statement “There is no x such that x+x = 1+1+1” is true in every extension of Presburger.* But that doesn’t mean there’s no extension where 1.5 is a number. I can make a model that satisfies Presburger in which 1.5 is a number. Namely, it’s the model just like the standard interpretation, but where we interpret the symbol “1” to refer to the number 1.5.

That model satisfies the Presburger axioms, and on that interpretation there is no x where x+x = 1+1+1 (remember to interpret “1” correctly!) and on that interpretation 1.5 is an element of the domain.

*It must be, since Presburger is complete, but my proof-fu is failing me when I actually try to construct the proof.

3

This is all waaaay beyond me. Just asking for some clarification here (not arguing anything one way or the other so keep the pile on to a minimum please ;)).

Seems to me you are saying you are using the symbol “1” to represent the number “1.5”.

So, in your example above seems you want to make x=“1” (symbol) = “1.5” (number).

Then after the “=” sign you say 1+1+1 but since you redefined “1” to mean the number “1.5” then in reality the right side of the equation means 1.5+1.5+1.5.

Otherwise trying to sort when you mean the number and when you mean the symbol which means “1.5” gets wacky.

IMHO anyway.

4

That’s right–on the interpretation I described, the sentence means “There is no x such that x+x = 4.5”

(Does that answer your question/concern?)

5

Ah, damn, I had hoped to get in before this thread, too, gets bogged down by irrelevant side discussions about Presburger arithmetic and domains of discourse and whatnot.

In any case, the contentious position in the linked thread boils down simply to the following:

“If an axiom system proves P, then P must be true in all models of this axiom system”, or, equivalently, “if the models of an axiom system disagree on P, then P must be undecidable from the axioms themselves.”

The example that was used was whether or not the field axioms decide the proposition: “There exists an x such that x*x=1+1.”

Obviously, different fields – different models of the field axioms – disagree on this proposition: there is such an x within the real numbers, there’s none within the rationals, for example. Hence, or such was the majority opinion within that thread, the proposition is undecidable from the field axioms.

But really, I’d rather we got away from fields, Presburger arithmetic and models thereof, and other tenacious distractions, because the core matter is simple:

If an axiom system proves P, then there exists a derivation of P directly from the axioms; that is to say, if we call our set of axioms A, A entails P, or, for n axioms A[sub]i[/sub], (A[sub]1[/sub] Λ A[sub]2[/sub] Λ … Λ A[sub]n[/sub]) → P. Since every A[sub]i[/sub] is valid for every model of A (it wouldn’t be a model of A, otherwise), it follows that P is valid for every model of A.

If now it is the case that in different models of A, P may either be true or false, then it follows that A entails neither P nor not-P, and thus, that P is undecidable from A. The undecidability of the existence of a square root of 1+1 from the field axioms then follows immediately.

6

If I’m wrong about using Presburger as an example, so be it. I’ve made mistakes before, and I will again.

But, does F describe F[sub]2[/sub]? It still seems to me that it does. That F is the smallest system that fulfils the axioms of F. And that, using what is described in the axioms alone is the default state of formal systems. These are things I’ve been claiming from the beginning. And no one has been able to show me otherwise.

I can’t find a single question you can ask in F that I can’t derive the answer to in the limited set, LS={0,1}. It looks to me like a complete system. and once again, F only asks questions in LS.

Ok. Presburger can’t be extended to include 1.5, (edit: in the conventional, number between 1 and 2, sense,) if the 5th axiom must apply to every new domain. (and as soon as you gave that rule, I said, “Aaaaah!” That would mean Presburger is a bad example.) But, still, all the axioms of F still apply to F(2), F(3), F(rationals), F(reals). Even if the answers they give to each question change.

I will admit that “F is incomplete if x*x=1+1 is a question that can be asked in the system that can’t be determined in it.” People keep asserting that that question isn’t answered in F, and I keep saying I completed the system. No one has disputed the value table I gave. That value table says that the question is answered in F.

And yes, I am largely self taught. I took the math needed to complement my physics courses, and that was 20 years ago. The rest I studied, and continue to study, for fun.

Oh, and you made a couple statements that made me think you aren’t irrelevant. We’ve been cross posting again, so I won’t have seen any responses you’ve posted since what I’m quoting, etc…

7

In the sense that F[sub]2[/sub] (which is the term we’ve been using for the smallest nontrivial finite field, more commonly known as GF(2), for any confused onlookers), satisfies the field axioms, yes, it is described by F (the field axioms). But it isn’t any more fundamental than any other field just by virtue of being the smallest one; the field axioms describe all possible fields to an equal extent. And what can be proven within this field does not have a greater claim to generality than what can be proven within any other field; the multiplication and addition tables of F[sub]2[/sub] do not follow from the field axioms alone (because, again, if they did, they would have to be valid for all fields), they follow from using the field F[sub]2[/sub] as a model of the field axioms, just as any other field’s multiplication or addition tables do. That in F[sub]2[/sub] there is a square root of 1+1 is not any more fundamental than that there isn’t one in the rational numbers; the fact that both fields differ on this is exactly equivalent to saying that the question is undecidable from the field axioms.

I think the real sticking point is the following, and if you’re going to answer anything in this post, please answer this first:

Do you, or don’t you accept that if an axiom system A proves a proposition P, this proposition has to be true in all models/extensions of A?

8

There are various ways to do it, but here’s one way, going from the presentation of Presburger arithmetic currently given on Wikipedia (though one can of course axiomatize it all kinds of different ways, so long as they suffice to establish all and only the true first-order sentences of natural number addition). Wikipedia’s presentation doesn’t give a special symbol for the successor operation, but I’ll use S(x) instead of x + 1 when I wish to emphasize its role in a certain way. In case Wikipedia ever changes and one wishes to still understand this post, the presentation has axiom 1 being that 0 is not in the range of S, axiom 2 being that S is injective, axioms 3 and 4 being the base case and the recursive step, respectively, of defining addition by recursion over the second argument, and axiom (schema) 5 being induction.

First, for my convenience, we’ll establish the associativity and commutativity of addition. [On a different presentation of Presburger arithmetic, say as the axioms of the free commutative semiring, these would be immediate, but then, everything provable is immediate on some presentation]. Let’s start with associativity: that (x + y) + z = x + (y + z). We will use induction on z (axiom 5): the “base case” is that (x + y) + 0 = x + (y + 0), which is seen to hold as both sides are equal to x + y by axiom 3. For the “induction step”, we assume (x + y) + z = x + (y + z), and must show that (x + y) + S(z) = x + (y + S(z)). Well, by axiom 4, (x + y) + S(z) = S((x + y) + z), which, by the “induction hypothesis”, is equal to S(x + (y + z)), which, by axiom 4 two more times, is equal to x + S(y + z) = x + (y + S(z)). This establishes the associativity of addition. Accordingly, I will no longer distinguished between reparenthesizations of sums except for emphasis.

As for commutativity: first, we’ll establish the lemma that S(x + y) = S(x) + y [establishing for the first argument to addition what axiom 4 in Wikipedia’s presentation gives directly for the second argument], using induction on y (axiom 5): S(x + 0) = S(x) + 0 as both are equal to S(x) by axiom 3, and if S(x + y) = S(x) + y, then S(x + S(y)) = S(S(x + y)) [axiom 4] = S(S(x) + y) [induction hypothesis] = S(x) + S(y) [axiom 4]. This completes the induction, establishing the lemma. Now, we’ll show that x + y = y + x by induction on y (axiom 5): the base case is that x + 0 = 0 + x. The left-hand side is equal to x by axiom 3, so we just need to establish that 0 + x = x. For this, use straightforward induction on x (axiom 5): 0 + 0 = 0 by axiom 3, and if 0 + x = x, then 0 + S(x) = S(0 + x) [axiom 4] = S(x) [induction hypothesis]. This finishes the base case of our commutativity proof. As for the inductive step, suppose x + y = y + x. Then x + S(y) = S(x + y) [axiom 4] = S(y + x) [induction hypothesis] = S(y) + x [lemma]. This completes the commutativity proof.

With those auxiliaries under our belt, we will now show that for every z, precisely one of two possibilities happens: either z takes the form y + y (“z is even”), or z takes the form (y + y) + 1 (“z is odd”), but not both. From this the desired theorem (x + x cannot equal 1 + 1 + 1) will follow. As can be guessed, we will establish this with induction on z (axiom 5): It is immediate that 0 is equal to 0 + 0 (axiom 3), and that 0 cannot take the form (y + y) + 1 because 0 cannot take the form k + 1 (axiom 1). This establishes the “base case”. As for the “induction step”, we shall suppose that z takes precisely one of those two forms and must establish that z + 1 does as well. Now consider z + 1. Note that z = y + y if and only if z + 1 = (y + y) + 1 (left to right trivial, right to left by by axiom 2). Thus, z is even if and only if z + 1 is odd. Continuing, z = y + y + 1 if and only if z + 1 = y + y + 1 + 1 (same reasoning as last time), the right hand side of which is equal to (y + 1) + (y + 1) [commutativity and implicit associativity]. Furthermore, z + 1 is inequal to 0 [axiom 1] = 0 + 0 [axiom 3]. And, as all objects are either 0 or of the form y + 1 [trivial use of axiom 5], we can put the last two lines together to have that z is odd if and only if z + 1 is even. Thus, the “parity forms” taken by z + 1 are precisely the opposites of those taken by z, so given that z takes precisely one of the two, so does z + 1. This completes the proof.

9

(There’s some editing wonkiness in the above (e.g., a “distinguished” that should be “distinguish”, a redundant at best “Now consider z + 1” hanging around, and I didn’t always hew to my philosophy for when to use S(…) as opposed to … + 1), but it’s hopefully still relatively readable.)

10

Also, not that it matters, but I suppose I should have said “as the additive consequences of the axioms of the free commutative semiring” or “as the axioms of the free abelian monoid on a single generator” or such things here, in accord with the lack of multiplication in Presburger Arithmetic

11

Still planning a reply. I sometimes have limited ability to follow the thread and post at certain times, mid-week especially.

12

I hope you’re replying to Half Man Half Wit’s post #5.

13

I wasn’t specifically going to respond to him at all, but it will address all that.

I would like to thank Frylock for being the most relevent and helpful, even though he said he wasn’t the best qualified. And even though I’m not sure he knows yet how it was he helped me.

Went back through all the posts, and Frylock was the first to bring us away from the red herring, “x*x=1+1” and see that the relevent statement was “1+1=0”. (It has nothing to do with square roots.) He was the first to mention almost every relevent statement.

But, everytime I made a statement like, “Presburger doesn’t have a number between 1 and 2, but Presburger with Rationals does.” Or, “Natural numbers and addition don’t have a number between 1 and 2, but extend it with rationals, and it does.” Everyone tried to deny the construction of the particular extension I was making. Which is totally the wrong approach, because I’m just going to go and try to construct it another way because I was convinced it could be constructed. And it can, but back to that soon.

I’m about to make Half Man Half Wit, and Capt Ridley eat their words. I am teachable. I’m not “looking only to have (my) preconceived notions validated.” Maybe, you have been gloating about your own correctness too much to actually say anything helpful.

[QUOTE=Frylock]
[spit take]

[/QUOTE]

Do you have a glass of water ready again? Because, I am about to do something that I’ve never seen on boards like this. Something totally shocking. I could try to make that construction from Naturals to Rationals again, but we are just going to assume that it exists…

And then I am going to do what no one else was quite able to do: (here comes the shocking part, ) I’m going to quickly and easily refute my own arguments.

And it’s thanks to Frylock and discussion about domains. We will assume that I have constructed a complete axiom system of the natural numbers with addition, A, which can be extended to the rationals, Ar. And past ch4rl3s would say that A has no number between 1 and 2 while Ar does. (true.) So they don’t answer the question is there a number between 1 and 2 the same way. (also true.)

And I will now say: Well, if we ask an equivalent question, they do. “A” answers every question about natural numbers with addition. And as past ch4rl3s said, the domain is important; because, the extension Ar answers the equivalent question the same way, “is there a number in N, (naturals,) between 1 and 2?” No. in all extensions of A.

Does F describe F[sub]2[/sub]? Yes, it does. And the denials of that were another red herring that kept me from seeing why F was still incomplete. Because I just kept trying to show how F[sub]2[/sub] was constructed. But, the question “1+1=0” doesn’t satisfy the following:

[QUOTE=Half Man Half Wit]
Do you, or don’t you accept that if an axiom system A proves a proposition P, this proposition has to be true in all models/extensions of A?
[/QUOTE]

I do now. I realize that you must ask the question in the same domain, and not the domain in the new system. Adding new numbers to the domain doesn’t alter the question that the system A proves. Given the system A, (of natural numbers,) extended with rationals, Ar, There still is no number in the naturals, (the domain of A,) between 1 and 2. Even in the new system, Ar. Why couldn’t anyone tell me that? Why did everyone deny my ability to construct the sets? As soon as I said the domain was important. I convinced myself of your point.

14

[QUOTE=Capt. Ridley’s Shooting Party]
You aren’t teachable. You’ve argued point blank with people who know what they are talking about. You don’t know what you’re talking about, and, even worse, you show no ability to STFU and learn from people who do.

[/QUOTE]

All it takes to teach me is for someone to answer the objections I raise. Unfortunately, I was the first one to do that. Some people show no ability to answer the questions raised and just keep stating the same statement over and over and assuming that “proves” their point many times over.

“x=y”
“but what about z? doesn’t that refute x=y?”
“well, z must not be constructible, because x=y. so, there. I’ve proved you wrong again.”

Not helpful.

15

Here’s a toy axiom system T:

T1: A is a thing.
T2: Every thing is related to just one thing.

According to T, is A related to itself?

16

Well, that’s a two thumbs up for you, then. Seems that even in being wrong, you’re cleverer than all of us!

Do yourself a favour, read up on the Dunning-Kruger effect and take its lesson to heart.

17

I got bored reading the original thread and I can see I am going to get bored reading this one. But I just wanted to make one comment here. The question is not whether x^2 = 2 is decidable from the field axioms (obviously it isn’t, no more than 1 + 1 = 0 is). But the question is there a statement, written in the language of fields that is true in every field, but is not provable from the axioms for fields.

18

Well, that is of course a question, though it’s not, I think, the one which the discussion/argument with ch4rl3s was concerned with.

But, regardless, as for its answer, if, by “provable from”, one means entailment in a semantical sense, so that p is provable from T just in case every model of T satisfies p, then it is of course trivially, tautologically the case that there is no such statement. More substantially, if, by “provable from”, one means syntactic derivability via any standard system of proof rules for first-order logic, then Goedel’s/Henkin’s completeness theorem provides the same answer (i.e., the equivalence of semantic validity and syntactic derivability).

19

(And again, this applies just as well to the axioms of first-order Peano Arithmetic as it does to the field axioms; if something is true in every model of those axioms, then it can be derived from them by standard proof rules. Granted, there are statements which are true of the sole “intended model” of PA which are not true of all the models of PA, whereas with the field axioms there is no unique “intended model” as such, but that’s again just a difference in intent between the axioms of first-order PA and the field axioms, and not an actual mathematical difference between them. In both cases, there are many models, in which the same statement comes out sometimes true and sometimes false, leading to incompleteness.)

20

from a previous post

[QUOTE=Half Man Half Wit]
The field axioms do not answer the question: ‘Is there an x such that x*x=1+1?’, because different fields answer the question differently; if the field axioms did answer the question, all fields would have to agree on that answer.
[/QUOTE]

True. In the x=y sense. You restated the definition that I wasn’t agreeing with, (at the time,) and thought that “proved” your point, again.

[QUOTE=Half Man Half Wit]
You dragging in F2, Presburger arithmetic, ‘logic’ (whatever you may mean by that exactly), etc. is only so much obfuscation brought on by your apparent need to be right about something you frankly don’t seem to understand very well.
[/QUOTE]

And then, deny my counter-example without refuting it. After realizing I was wrong, I went back and read through the thread again. I don’t recall seeing where you showed me that my counter-example was wrong. It was wrong, but you didn’t say so. I see no evidence you even knew it was a valid construction but didn’t prove what I thought it did. It looks to me like you thought it couldn’t be a valid construction because it contradicted your rule. And that looks to me like you didn’t actually understand the rule. You could certainly quote it. Again, and again. And give the same example I was disputing, again and again. If you shout it loud enough, do I have to believe it?

Of course I’m going to continue to believe my counter-example.

Am I supposed to congratulate you for being right? I guess I could… In the same way I would congratulate a lottery winner on his skill at picking the correct numbers, or a sheep for managing to stay with the herd.

H:“x=y”
c:“what about z? doesn’t z say x!=y?”
H:“x=y. so z must be an obfuscation.”

Frylock was very helpful. Indistinguishable was helpful. You weren’t. Are you bitter about that now? Frylock claimed he was probably the least qualified to debate, yet he was the most helpful. And I can go back and see exactly how I was wrong, and how everyone else was right, and I admit it. Are you claiming you gave the information that had to have convinced me?

Do you know how to dispute an argument? If I create a construction, and you show it isn’t valid, I’m just going to make another construction. Unless you show mathematically that no such construction is valid. And that couldn’t be done in this case. You have to actually address the point being made.