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.

  • $\begingroup$ Journal of Formalized Mathematics might be what you want. $\endgroup$ – Dave L. Renfro Aug 17 '16 at 19:14
  • $\begingroup$ You can find examples of proofs everywhere, I would recommend opening some introductory book on mathematics (or perhaps on logic). :) See e.g. math.stackexchange.com/q/728223/321909 $\endgroup$ – Gur Ismael Aug 17 '16 at 19:55
  • $\begingroup$ @GurIsmael, I'm not asking about just any proof. I'm asking about these. $\endgroup$ – Karolis Juodelė Aug 17 '16 at 20:06
  • $\begingroup$ @DaveL.Renfro, it's pretty close, but I'm not actually seeing any proofs. On the few random pages I opened, it's just definitions and "The following propositions are true". $\endgroup$ – Karolis Juodelė Aug 18 '16 at 7:22
  • $\begingroup$ One time, I tried proving "for fun" without any abbreviations in a Hilbert style system that in Peano arithmetic, for each $n,m$ with $m \neq 0$ there are $q,r$ such that $n = qm + r$ and $r < m$. I gave up even trying to prove this for $n = 0$. (Admittedly, this was partially because the LaTeX package I was using to typeset it required rather illegible code.) I think you may be asking for too much. $\endgroup$ – Mees de Vries Aug 18 '16 at 9:35

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.

  • $\begingroup$ I get that such proofs would be long, repetitive, hard to read, and unpractical. I still want to see some. I'll definitely take a better look at proof assistants. But what I really want is to see a small set of formal rewrite rules producing the language of true (provable) statements, and I worry that computer verifiable proofs are not much closer to that, than the usual human proofs. Although, maybe I could write a program which takes a proof in HOL and prints a tree in natural deduction? $\endgroup$ – Karolis Juodelė Aug 18 '16 at 6:27

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))$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.