Examples of non-trivial proofs in deductive systems

Question

I want to get a better grasp of what a rigorous formal proof is. So I was hoping to find proofs of interesting results using natural deduction or Hilbert system or similar. The "interesting result" could be anything from infinitude of primes to Lagrange's theorem. "Interesting result" is not $x \wedge y \implies y \wedge x$ or similar. In particular I'm interested in how mathematical objects (like primes or groups in the examples) fit into the proofs.

Answer 1

Nobody uses Hilbert systems to actually write down fully formal proofs of anything interesting. The explosion in size that results from repeated use of the Deduction Theorem makes them completely unfeasible for practical work.

Using natural deduction instead avoids this problem, but still one needs to have some sort of facility for using abbreviations for defined notions; otherwise the properties you want to prove will themselves become completely impenetrable spaghetti balls of primitive notions.

This means that systems of the kind usually presented by logic texts are not really well suited to doing actual work, but only for theoretical investigations into the limits of what can be proved. For actual work you need a system with native support for defined notions, something like formalized metatheorems, and so forth.

What you'll want is probably to download an actual proof assistant software with an existing library of basic concepts, and look at how the proofs in that library look -- for example Isabelle/HOL (which was all the rage a decade or two ago when I had a connection with the area, but may be obsoleted by something else these days, for all I know). Be aware that there's something of a learning curve if you start out with just knowledge of abstract textbook-style proof systems, but the basic concepts ought to be recognizable.

Answer 2

I will present proofs of two interesting formulas (both proofs are hopefuly interesting enough). I will not use any specific calculi, but the reasoning I will show is precisely how you would prove it in Hilbert style calculus or in natural deduction.

An interesting proof can be the one of Peirce law $(A\to B)\to A)\to A$:

Assume (1) $ (A\to B)\to A$ and further assume (2) $\neg A$. From (2) you obtain $A\to B$, thus from (1) you get $A$. It means that (1) and $\neg A$ implies A, contradiction. You can conclude $(1)$ implies $A$. Which is the Peirce law.

Another interesting proof, this time in first order classical logic, is for the drinking guru formula $\exists x (D(x)\to \forall y D(y))$. Meaning D is a unary predicate symbol. Lets say that D(x) means $x$ is drinking. Then the formula stands for: There is someone who whenever he is drinking, everyone else is drinking. Proof:

We will use the following instace of the law of excluded middle: $\forall x D(x)\vee\neg\forall x D(x)$. It is now enough to show that the desired formula is consequence of both of these - this is a proof by cases argument - which is formalised by the Hilbert style axiom $(A\to C)\to ((B\to C)\to (A\vee B\to C))$. Assume $\forall x D(x)$, then easily one get the following chain: $\forall y D(y)$, $D(x)\to \forall y D(y)$ (using weakening), $\exists x (D(x)\to \forall y D(y)) $ (exist. quantification). Now assume $\neg \forall x (D(x))$, from this we prove $\exists x (\neg D(x))$ (interderivability of quantifiers). Next from $\neg D(x)$ you can prove $D(x)\to \forall y D(y) $ (this is is true because from a false premis everything follows). Therefore from $\exists x (\neg D(x)) $ you conclude the desired $\exists x (D(x)\to \forall D(y))$.