The hijack about proof theory

Great Debates
41

The principle of Parsimony (I’ll just call it “Parsimony” from now on) says that nothing can exist according to an axiom set unless its existence is required for that axiom set to be consistent.

The principle of Permission ("Permission) says that anything can exist according to an axiom set as long as its existence is consistent with the axioms in that set.

The principle of Transferability says that identically worded axioms in different axiom sets are consistent with all of the same things.

Ch4rl3s adheres to Parsimony, and does not believe Transferability to be true. (I interpret his latest post as essentially denying the premise from my post “S1 and S2 are identical to SX1 and SX2”. He seems to be saying there is a distinction between them, even though they are identically worded–and that distinction rests on their being parts of different axiom sets.)

I think it’s true that if Parsimony is true, then Transferability must be false. My argument against Parsimony above implicitly relied on Transferability, and Ch4rl3s’s response basically defended Parsimony on the basis of a denial of Transferability.

Now it seems to me that there are two different relevant questions to ask. First, do actual mathematicians and logicians follow Parsimony, or rather Permission and Transferability? Second, can some kind of proof theory actually work (i.e. regardless of what actual mathematicians and logicians actually do) if Transferability is false?

As to the first question, I hope someone with this kind of thing ready to hand can provide an example or two of an uncontroversial and relatively simple demonstration in the literature that makes use of Transferability and Permission.

As to the second question, I’m still thinking about what such a system would amount to. It would mean that you can’t assume that two consistent axiom sets which share certain identically worded axioms are thereby consistent with any other identically worded statements. I haven’t had enough spare time since reading Ch4rl3s’s post to figure out if there could be a sensible system of logic that works this way.

As to the system actually used by practicing mathematicians and logicians, it is surely one that adheres both to Permission and Transferability, but as I indicated above, I don’t have ready to hand a simple and uncontroversial demonstration from the literature that clearly uses both of these principles. I’m hoping someone else in the thread can supply something.

ETA: The Fano Axioms were an unfortunate example, it turns out, because they require the existence of further objects than those specified in the axioms. What is needed is an example of an axiom set which allows the existence of further objects without requiring them–and which mathematicians and logicians typically do model in a way that involves the existence of these further objects. And now that I’ve edited to add this paragraph, I’m thinking just a little bit of easy thought should let me come up with a simple example, but it’s too early in the morning and I haven’t had my coffee so I’m leaving it for later.

This largely contentless post has been brought to you by Frylock

42

To add a bit:

The thing is, Permission follows trivially simply from the definition of satisfaction. A model satisfies a set of axioms if, in the model, by the relevant interpretation, each axiom in the set is true. That’s what satisfaction consists in. And by that definition, the set consisting of two objects A and B, where A is related to B and B is related to A, trivially satisfies the axiom set SX. This means that a second object can exist according to SX. Yet the existence of a second object is not required by SX. Hence, Permission is true.

It’s a textbook example, and it shows that Permission is true. It’s just that it’d be nice if we could actually cite a textbook instead of my just asserting that “it’s a textbook example.”

Throughout this discussion I’ve googled in vein for the online equivalent of a “textbook” on this material. I’m surprised if there’s nothing like that online, but so far, I haven’t been able to find one! I just did an (albeit brief) search simply for a definition of “satisfy” in this context and couldn’t find anything! Do we have to actually cite physical books here? It’s been a while since I had to deal with one of those! :smiley:

43

There may be something here but I have to leave now.

44

I’m beginning to think you must mean by S2 that “Every thing is related to just one OTHER thing.” The way it’s phrased could mean “There is just one thing in S to which any and all other things can be related” and that’s how I took it. So is this what you mean:

T1: A is a thing
T2: Every thing is [a successor of] just one other thing
T3: No thing is [a successor of] itself

But if so, then you have another problem instead. [Note: I get what you are saying about excluding identity from the list of relationships, but I don’t see where that was specified. Since identity is a relationship, S is not universally applicable to all relationships. So it isn’t consistent for all relationships. So you are sometimes right about S. So let’s see if T is one of those times.]

Now, if we use your model T above, which is an example you give of a type of relationship you did have in mind, then your model says “A is a successor of B” and “B is a successor of A”, correct? Succession is inductive so it is a step-wise, or iterative, process. In order for B to succeed from A, A must be preexistent, and indeed it is by axiom. But how can it then be a successor of B as your proof-by-model states? The only alternative is that A has zero relationships, which is inconsistent with S2/T2. That’s why I didn’t believe you meant “one other thing” rather than “just one thing” in the absolute sense that I took it.

Or did you mean by S2 “Every thing is related to A MAXIMUM of just one thing”?

45

I suppose the “toggle” could be the one (and only?) type of “counting” that the model you give can do. 1–>0–>1–>0–>1…, as an example. Or more broadly with similar models, I guess any repeating sequence, but A will eventually have to be a successor of one of its progeny to fulfill S2 so it can’t be a method of counting nor any other form mathematical induction that doesn’t have a restricted, finite domain. I think you accidentally hit onto this when you said “But if S were inconsistent, linear orderings (such as that used in the simple counting process) would be impossible.” But linear orderings can’t in fact result from S or T using the model (or the class of models) you use to “prove” consistency. Or am I wrong?

Btw, I hope you don’t think I’m just being a pest. I’m very interested in this thread, and I agree that parsimony is not regarded as the default rule for these systems. I realize that when you say “consistent” you mean only in the semantic sense of “satisfiable” and you are not arguing completeness. I just don’t think the S example really works, that’s all.

46

Also, in response to your request

I don’t think you have to come up with a specific example. Is there not a Gödel sentence in EVERY such system (sufficiently complex to pertain to simple arithmetic)? I think that this observation alone proves that nobody is assuming parsimony.

47

Nitpick: Your interpretation should be going the other way, given how you’ve phrased S. “A is related to B” should be interpreted as “B is a successor of A”. On this interpretation, S2 is validated, and simply states that “successor of _” is a function. On the “reverse” interpretation, S2 fails, for 0 is not any counting number’s successor.

It should also be emphasized, since I think Defero is mistakenly assuming otherwise, that this relation need not (and, indeed, in the above interpretation, will not) be symmetric; i.e., “A is related to B” does not imply “B is related to A”.

48

No, it means “just one thing.” Another axiom–S3–makes makes it impossible (in S) for anything to be related to itself, so it indeed must be some other thing. But S2 doesn’t say or mean that. The "other"ness of the thing related comes from S3, not S2.

S is not supposed to be talking about all possible relationships. It’s talking about any relationship you care to interpret it as talking about–as long as that interpretation satisfies all the axioms in S. (Is this addressing what you’re saying, or am I missing your point?)

49

Oh dammit, and I sat there and thought about it too. :smiley:

50

You might be right. (Look, I shouldn’t be talking about this at all, really, because my grasp of the Goedel stuff is very, very, very shaky. I only grasp it when I’m reading about it and can think through it step by step. Outside that context I can not say anything intelligent about it.) I was hoping for more elementary, textbook examples though.

51

Thanks, Indistinguishable, but I didn’t think they were assumed to be bidirectional from the definition of S. It was only his model example (with f(A)=B and f(B)=A both explicitly stated) that I was driving at:

…changing “related” to “a successor of”.

52

Ah, ok.

53

Just quickly, since I’ve only skimmed your conversation with Defero…

I agree with Frylock on these points. That’s how I was reading it… “related to” is a phrase to define a specific “operation” performed on “things” in these axiom sets.

54

Crackrat: Although, in what? two posts? you have some of the best arguments I’ve seen on this topic, I have a couple issues.

My question had been, basically, using the parsimony principle, as Frylock calls it, why can’t we have a theorem in one axiom set that isn’t a theorem in an extension. That’s what I said when I described T having an axiom that S doesn’t. But the answer to that isn’t this:

That, while it might be true, isn’t the proof of itself. I asked, “why is this true?” and get back the question as the definition “proving” itself. (edit: so can someone tell me why that is true?)

also, this:

doesn’t answer the question:

It does answer a very important question, even a more important question, but it doesn’t answer the one asked. Just want to clairify that, since there has been a lot of bad “proofs” in this discussion. (edit: and it was presented as answering that question. I don’t want anyone to think it actually did.)

Sorry, gotta go, more later.