Have any of the metalogical theorems of first order logic, such as the deduction theorem, been formalized and proven in a system such as Coq or HOL? If not, what are the main obstacles to doing so?

  • 1
    $\begingroup$ cs.nott.ac.uk/~psztxa/g52ifr/src/Meta.v mentions the deduction theorem $\endgroup$ Commented Apr 19, 2018 at 5:08
  • 1
    $\begingroup$ Far more complicated systems, e.g. NuPRL, have been formalized in Coq and had meta-theorems of various sorts proven. Something like Twelf is particularly geared to such meta-theorems. Proving something like the deduction theorem for FOL is more like something that would be given as a (sizeable) exercise as opposed to the limits of research. $\endgroup$ Commented Apr 19, 2018 at 5:17
  • $\begingroup$ @DerekElkins If I wanted to formalize and prove the metatheorems that I encounter as I learn first order logic, would you suggest Twelf as a good tool for a beginner to learn? $\endgroup$
    – user695931
    Commented Apr 19, 2018 at 5:28
  • 1
    $\begingroup$ @user695931 Probably not. Mostly because being familiar with Coq or Isabelle/HOL would be much more valuable than being familiar with Twelf. If you are going to invest a large amount in time and effort into learning one of these systems, those would be better choices. Coq and Isabelle/HOL also have more resources and better support. No serious proof assistant that I'm aware of has a gentle learning curve. $\endgroup$ Commented Apr 19, 2018 at 5:39


You must log in to answer this question.

Browse other questions tagged .