How do I know what we already know in a proof when the assumptions we can use are even more complex?

I think one reason why I find proofs so difficult is that I don't know what it is we're permitted to know and what we assume we don't know.

For example, "proving $0x = 0$" seems so incredibly obvious and yet I have to prove it with "simpler" assumptions and try to find some clever workaround:

$$\begin{array} {rcll} 0x &=& 0x &\text{ by reflexivity x=x}\\ (0+0)x &=& 0x &\text{ by additive identity x+0=x and... substitution?}\\ 0x + 0x &=& 0x &\text{ by distributive axiom}\\ 0x + 0x &=& 0x + 0 &\text{ by additive identity again}\\ 0x &=& 0 &\text{ by cancellation law}\\ \end{array}$$

But anyways these proofs already feel unsatisfactory to me. How do I know what "rules" I'm allowed to work with? For instance the distributive law being an axiom I never would have guessed in a hundred years was an axiom because it seems far more "complicated" than the idea of proving $0x=0$.

Is there a general way to know what we can and cannot use in order to prove something? Why are these "more complicated" assumptions like distributive law (which seem to encapsulate several rules at once, like addition, multiplication, restructuring of the statement, etc) allowed?

• Yes, indeed, if you don't know or care what the definitions/axioms in that area are, you can't prove a thing. Surprise. – Professor Vector Mar 3 '18 at 18:52
• Are you taking a "discrete math for computer science" course by any chance? The common textbooks in that subject are mostly awful on this point. They purport to teach proof techniques, but never state the axioms the student is allowed to use. If you are not told what the axioms are, there is no way to write a formal proof. Your complaint is fully justified. – saulspatz Mar 3 '18 at 19:01
• @saulspatz I'm not a student, just someone interested in math – user537069 Mar 3 '18 at 19:01
• +1 because I think there is a legitimate question here. I don't have time to try and address it, and I'm not really sure what I'd say anyway, but it seems to me that proving such things either (a) in the context of abstract algebra (not real numbers, as I assume you're working with) or (b) in the context of constructing the various number systems (natural numbers, integers, rational numbers, real numbers) and establishing various results about them, would cause less philosophical concerns of this type. – Dave L. Renfro Mar 3 '18 at 19:04
• In general, you need a "context" i.e. a theory with definitions and axioms to be used and - obviously - any tehorem already proved in that context. – Mauro ALLEGRANZA Mar 3 '18 at 19:04

As others have said in the comments, you know what rules and axioms you can use because you are given or choose a particular collection. One of the most common misunderstandings I see is the thought that there is one set of rules and axioms that all mathematicians agree on. This is especially pernicious in logic but exists in other areas too. Usually what happens is a student sees one definition and assumes that that is the definition. It usually takes a while before they realize that all of these things have a variety of different but equivalent definitions, and in most cases also have genuinely different definitions. In the case of logic, just looking at the sheer number of entries under "logic" in the Stanford Encyclopedia of Philosophy, many of which correspond to different logics, gives an indication. And it is not comprehensive by any means.

For your example, all the reasoning is equational so which logic we're using is not as critical. We do need the laws for equality which could be roughly described as "a congruence with respect to everything". First, equality is an equivalence relation meaning it is reflexive, $x=x$; symmetric, if $x = y$ then $y = x$; and transitive, if $x = y$ and $y = z$ then $x = z$. Then what makes equality equality is the indiscernibility of indenticals which is usually expressed as a rule rather than an axiom and states: if $x = y$ and $P$ is some predicate with free variable $z$, then if $P[x/z]$ is provable so is $P[y/z]$ where $P[x/z]$ means $P$ with all free occurrences of $z$ replaced with $x$, i.e. substituting $x$ for $z$, and similarly for $P[y/z]$. (Again, there are other ways of presenting these rules and axioms. Indeed, this set is redundant...)

The proof of a statement like $0x=0$ is common in the theory of rings. For example, using the definition of a ring given on Wikipedia, this is a theorem but not an axiom. The aspect I mentioned before strikes here too. There are other choices you could take for the axioms of a ring, including ones where $0x=0$ is taken axiomatically. Also, the term "ring" is ambiguous as many authors consider "rings without unit" (i.e. which don't necessarily have an element that behaves like $1$). The definition Wikipedia gives is a ring with unit. These definitions are not equivalent.

Anyway, using the definition on Wikipedia, one way to prove $0x=0$ is the following: \begin{align} &0x-0x=0 \tag{additive inverse} \\ \iff & (0+0)x-0x=0 \tag{additive identity} \\ \iff & (0x+0x)-0x = 0 \tag{left distributivity} \\ \iff & 0x+(0x-0x) = 0 \tag{additive associativity} \\ \iff & 0x + 0 = 0 \tag{additive inverse} \\ \iff & 0x = 0 \tag{additive identity} \end{align}

Each $\iff$ is hiding a use of the indiscernibility of identicals. For example, the first step is: let $P$ be $zx-0x=0$, the additive identity axiom for $0$ states $0+0=0$ or, by symmetry, $0=0+0$, if $P[0/z]$ is provable, then $P[(0+0)/z]$ is provable. This gives the $\Rightarrow$ direction, the $\Leftarrow$ direction just uses the same equality the other way.

So why don't we just take $0x=0$ as an axiom. Well, we could. However, doing so wouldn't let us derive the other axioms and given the other axioms we can derive this one. Using a minimal collection of axioms makes it easier to verify if something is a ring (or a ring homomorphism). We would have to explicitly verify $0x=0$ while having it be a theorem means we can derive it once and for all for all rings. Another factor affecting the choice of axioms is also evident in Wikipedia's presentation. We often want to build our definitions in a modular fashion (which often leads to non-minimal lists of axioms). In this case, Wikipedia's definition starts with the axioms of an commutative group. That is, a ring is an commutative group and simultaneously a monoid whose "multiplication" distributes over the group operation. This way of presenting rings allows us to "import" theorems about commutative groups and monoids and apply them to rings. We could, of course, still do this if we had a different presentation of the axioms of a ring, but we'd have to derive the commutative group/monoid structure first, and this structure may not be obvious from the alternate presentation.

If you really want to get a visceral feel for all of this, I recommend getting familiar with a proof assistant like Agda, Coq, LEAN, or several others. I particularly recommend Agda as it puts all the gory details of the proofs right in your face. Most other proof assistants use a tactics-based approach which means you typically write "proof scripts" which are little programs that search for proofs for you. You don't typically see the proofs in those systems. Nevertheless, any of them will make it very apparent what it means to work with a given definition, what is and is not available at any point in time, and why structuring definitions one way versus another may be desirable. They all have pretty steep learning curves though and LEAN and Coq have better introductory material than Agda.

• Side note: Ohh, \tag is what I was looking for BTW! Thanks – user537069 Mar 4 '18 at 6:11

Using set theory, the rules of logic and Peano's Axioms (for $N, S$ and $0$), it is actually possible to prove the existence of addition and multiplication functions on $N$ and that they are associative, commutative, distributive, etc. Hundreds of lines of formal proof would be required to do this, however, so most textbooks will usually skip all that and simply "define" addition and multiplication and their algebraic properties in only a few lines. And the definitions will vary somewhat from one textbook to another depending the intended audience and preferences of the author. It is unavoidable. If you are confused about which definitions you are allowed to use for a given assignment, ask your instructor to clarify.