This is actually easy to answer from a formal logic standpoint. A proof is a sequence of statements where every statement is an axiom or follows from a set of axioms and previous statements through the rules of inference.
There’s no requirement of non-obviousness because it’s very hard to define what’s obvious.
Given Peano’s Postulates P1 - P5, as well as the following definition of addition:
Def: Let a and b be in N. If b = 1, then define a + b = a’
(using P1 and P2). If b isn’t 1, then let c’ = b, with c in N
(using P4), and define a + b = (a + c)’.
Theorem1: 1 + 1 = 1’
Proof: Use the definition of addition with a = 1.
Is the above proof necessary?
In fact, let me make things even simpler
Theorem2: 1 is in N
Proof: P1 postulate
According to your definition (proof is a sequence of statements where every statement is an axiom or follows from a set of axioms and previous statements through the rules of inference), a proof could simply consist of 1 axiom.
Even if you are technically correct in your definition of what constitutes proof, you must agree that a single line consisting of quoting an axiom is pushing the limits of what proof is, and to me, becomes so trivial as to be considered “true by definition”.
Yes.
What limits? Either something is a proof, or it isn’t. Notions like triviality and obviousness are not relevant.
Darn, I hadn’t ever noticed x in base y is the same as y in base x.
Ultra, you’re right, but I think what Thudlow is getting at is the possible controversy over justification, not of logical rules, but of completeness. Is any proof that leaves out the Axiom of Identity (x = x) invalid? Well, yes, but most proofs leave it assumed. That’s why I mentioned R&W’s 362 page proof of 1 + 1 = 2. They didn’t leave out diddly. 
… no it isn’t, how comes the examples I worked with before posting worked.
27 base 8 != 8 base 27
no wonder I hadn’t spotted that one before :smack:
Maybe this will help clear things up: definitions have no truth value; axioms do.
You fell right into an affirmation of the consequent fallacy! A implies B does not imply B implies A. 
Only if it uses that. Otherwise, there’s no problem with leaving it out.
I think your underlying point is clear, that there’s a question of what level of detail is necessary. But I disagree–either every step follows from a previous step or the axioms, or you don’t have a proof. Derived rules of inference are fine as long as they’ve been proved.
And I agree with you. But often, one or more premises are implicit in a single premise. It is necessary that the axiom of identity hold for every mathematical and logical expression. Thus, if you hold axiomatically that a theorem in K, K(A), is true, then it must be the case that A <-> A; otherwise, you could argue something like this: All cats meow; all dogs are cats; therefore, all dogs meow.
As a matter of fact, Ultra, that’s pretty much Polerius’s fallacy. He is holding that an axiom and a definition are identical.
That’s a valid inference. What’s your point again?
Well, yes, it’s valid, but it’s unsound, because the minor premise is false. That’s my point. Circular arguments are also valid, but useless. Mere validity does not a good argument make.
Where have I stated that? I find your ability to put words in my mouth very amusing.
Is this where you are getting it from: "Even if you are technically correct in your definition of what constitutes proof, you must agree that a single line consisting of quoting an axiom is pushing the limits of what proof is, and to me, becomes so trivial as to be considered “true by definition” ?
If so, you are mistaken that I meant that axioms are the same as definitions.
Let’s say I have a system with one axiom
Axiom:
Theorem1: 1 is in the set N
Proof: Axiom 1
The above constitutes a proof, according to ultrafilter’s definition of what a proof is, which I technically agree with.
Notice that there are no definitions above, just axioms. And yet, I could say, very sloppily I admit, that Theorem 1, once you accept Axiom 1, is true by definition.
The very act of accepting Axiom 1 automatically makes Theorem1 true.
Maybe a more accurate term would have been “true by axiom” if such a term exists.
Axioms have truth value; definitions do not.
It’s very good that you understand this.
What are you debating at this point, Polerius?
Not much left really. I accept your definition of what constitutes a proof.
I was just trying to see why Liberal thinks I consider axioms and definitions to be identical, but it’s pointless anyway.
In any case, I’m surprised that such a simple question in the OP went on for more than one page.
Polerius, it is not remarkable that there is one axiom in that proof. Some systems have only one axiom (with an infinite number of formulas), or axiom schema. Like I said when I linked you to it, it is one version of the proof. If you want 362 pages of definitions, axioms, and inferences, consult the aforementioned Russel and Whitehead’s Principia Mathematica.
Ugh, what a day I’m having. Where were we?
Mathematics is not about science, as it is currently formulated. On this I’m in complete agreement with you. Where I disagree is with the statement that it is impossible to scientifically prove “1+1=2”.
That nobody bothers to prove it scientifically in this modern day and age does not change the fact that mathematics, especially arithmetic, has the same origins as the rest of physical science: observations of the real world. Peano didn’t make this stuff up out of whole cloth. All of these rules of inference and axioms and definitions have their origins in observations of the natural world, just like the laws of physics.
That said, you do raise a good point here:
This is true. A scientific proof that, say, “10 * 10^(100) = 10^(101)” is never going to happen. If I insist on a scientific viewpoint of mathematics, then that will put horrible limitations on the mathematics I can do. But nevertheless, basic statements of arithmetic like “1+1=2” have as much of a scientific basis as statements like “F=-GMm/r^2”.
On to Liberal…hang on, I’m playing catch-up here…
Empirically testing something all day long and always getting the same answer is what I mean by “scientifically proving that 1+1=2”. I agree that it’s entirely possible, logically speaking, that one day gravity will reverse and the Earth will spontaneously explode. Scientifically speaking, though, I’m not going to hold my breath, because by the standards of science (not logic) repeated empirical testing is what establishes the correctness of a hypothesis. Yes, a scientific hypothesis can be overturned at any time by new data. But saying “1+1=2” can’t be proved scientifically for that reason means (as you seem to be arguing) that the law of gravity can’t be proven scientically either.
Which requires, I think, a specific and somewhat narrow use of the word “prove”. More specific than I wish to use.
However, as you’ve stated, there’s no point in arguing over definitions. We certainly seem to agree that the law of gravity has no more of a scientific proof than “1+1=2” does. I do have some other issues to raise with you, however:
I would argue that equations don’t prove jack. Because at some point we have to acknowledge that mathematics (in its modern, purely logical formulation) and philosophy are only models of the real world. Because of this, we always have to consider the possibility that at some point the model will fail to reflect reality.
Suppose I live in Flatland. Based on observations, I infer that the laws of geometry in my world are those of the Euclidean plane. Inspired by these observations, I write down the laws of Euclidean geometry, and from those I conclude that the area of a circle is pi times the square of its radius.
Would I say that the equations, i.e. my formal reasoning based on the axioms of Euclidean geometry, have “proved” this law? Yes…but only within the formal system I’ve developed to model the real world. It only proves things in the real world to the extent that the model continues to reflect reality in the face of continuing observations. If I later discover that Flatland is in fact really a very big Sphereland, then my formal model has “proved” something that’s in fact false.
That in a nutshell is my view of the current relationship between science and mathematics. Laws of mathematics are inspired, at their root, by real world observations. As such, theorems of mathematics can be approached either from a logical/mathematical standpoint – do they follow from the axioms? – or a scientific standpoint – do they agree with the observed phenomena?
Neither is perfect. A scientific hypothesis may have to be thrown out because of new data. A mathematical theorem may be shown at some later point to not correctly model reality. But both viewpoints have their uses.
One more comment:
You’re correct: I should have used the word “infer”, instead. Although “deduce” and “infer” are synonyms in common usage, in the context of logic “deduce” has additional meaning which would make my statements incorrect if one insisted on the more formal use of the word.
Hence, please replace “deduce” with “infer” and my intended meaning will hopefully be clearer to you. A more exact word would be “induce”, but that word is not commonly used as I would use it here (i.e. “to conclude by induction”). Induction, of course, is part and parcel of the scientific method, as it is how we go from observations to hypotheses.