What is a "trivial implication" in mathematics?

Question

Most often when a certain axiom or proposition implies another proposition, this implication is not trivial, or "immediate". That is, you need a proof consisting of some number of steps to reach the second proposition.

So in that case we can say, proposition A implies but does not trivially imply proposition B.

My (philosophical) question is: what does it mean for a proposition to trivially imply another, or in other words, that it follows "immediately"? Is there a way to objectively determine whether an implication is trivial? Does a trivial implication only rely on an appeal to an intuition about "primitive notions"?

Perhaps we should exclude from this analysis cases where a theorem is implicitly used but simply not explicitly stated for the sake of brevity.

Answer 1

"Trivial" in mathematics is a subjective term. Something is "trivial" if my audience, in my opinion, comes faster to the conclusion that they can definitely provide a proof, then the time it takes me to demonstrate such a proof.

Such a proof can actually be quite lengthy, as long as all the steps involved are simple or purely mechanical. For example, one proof that some 16 digit number is a prime would be trivial (because it is completely mechanical) but would still be very long.

The same proof can be trivial if the audience consists of experienced mathematicians and be not trivial if the audience consists of beginners.

Answer 2

the key word here is "immediate", not "trival". The latter is an informal, psychologistic term; the latter can be expressed formally in terms of complexity. in logic, though the usual term is "cannonical". loosely, a cannonical proof cannot be simplified. for example, if you have A, and you also have B, then you ipso facto have A /\ B, by the intro rule for /\ . So the proof (explicitly written out) is cannonical - immediate. If your proof has steps that can be eliminated then it is non-cannonical. Note that a cannonical proof could have many steps. so we might say that a trivial proof is a cannonical proof of one step. Also note that this is closely related to the notion of normal form.

Dag Prawitz has written extensively about this sort of thing. It's quite subtle. Note also there is a difference between inference (something we do) and proof (a mathematical structure? something we endorse?) A web search will show some publicly available papers.