What is a gross-looking formal axiomatic proof for a relatively simple proposition?

Question

I'm looking for long and hard to follow derivations or symbolic proofs to motivate how tedious it is to actually reason within a formal system. I'm hoping there is an image of the proof, with few if any English sentences carrying the argument.

Answer 1

One place to look is at Nicolas Bourbaki's Theory of Sets. Look at the exposition that proves the existence of the empty set. There is a footnote in the book that shows the formal expression for $\emptyset$. Bourbaki states at this point not to worry - that they won't explicitly describe the formal expressions as they push onward. Like, it would be totally mind numbing to look at pages and pages of (primitive) symbols that describe the real numbers.

It will look ugly even if you read it in French! But beauty is in the eye of the beholder...

Answer 2

Proofs in a natural language are less tedious because steps are omitted in the proofs. Of course, you can take a proof in a formal language and throw away some steps, if you are not concerned with checking the proof. ☺

I am afraid, you cannot find a proof that you are asking for. A full proof in a natural language would be more tedious and longer than its counterpart in a formal language because natural languages are not suited for this task. A formal language provides one symbol (for example, $\forall$, $\lor$) where a natural language requires one or more words. No wonder because most people do not speak mathematical proofs.