3
$\begingroup$

I'm working on a tool for first order logical theories. I want to show the tool can work with real world logical theories. What are some good theories for demos?

I think I want demos that are:

  • finitely axiomizable
  • constructive
  • familiar to ordinary mathematics

I have some ideas for theories but they are a bit ambiguous.

From easy to hard:

  • theory of groups
  • Peano arithmetic
  • lambda calculus
  • set theory
  • simply typed lambda calculus
  • calculus of constructions
  • theory of complete ordered fields (Real numbers)

Some Problems Are:

I have heard there are multiple variants on the induction principle for Peano arithmetic.

I think the call by value lambda calculus with De Bruijn levels would be easiest to formalize. I only know this sort of detail because I know about computer stuff. I'm sure stuff like set theory has similar wrinkles.

There are many variants of set theory. Some are more constructive some are less. I'm not sure I want to get into proper classes but these make finitely axiomised presentations easier. I have heard of NBG (von Neumann–Bernays–Gödel) set theory but I don't know anything about it.

Type theory can be hacked into a first order logical theory with judgments as relation symbols but it's a little ugly.

Improve this question
$\endgroup$
7
  • 1
    $\begingroup$ Set theory and higher-order theories require infinite "axiom schemas" (with syntactical rules being the same as second-order axioms, if you want to formalize them), like this one for taking subsets... $\endgroup$
    – Zhanrong Qiao
    May 12 at 18:17
  • 1
    $\begingroup$ @ZhanrongQiao IIRC NBG can be finitely axiomised and is a conservative extension. I would like to learn more about these sort of hairy details. I'm still not sure if I want to restrict to finitely axiomizable theories. $\endgroup$
    – Molossus Spondee
    May 12 at 18:22
  • 1
    $\begingroup$ Ah, that looks interesting! I'm also trying to write a toy prover for first-order logic, but was unaware of NBG and thought that I have to support second-order things for doing set theory... $\endgroup$
    – Zhanrong Qiao
    May 12 at 18:40
  • 1
    $\begingroup$ @ZhanrongQiao I think maybe you can really support any system in a first order finitely axiomised style but you have to do some ugly coding. Something like assume a sort P of formulas, assume function symbols for connectives and axiomize an entailment relation. Just it's pretty ugly. Sort of like writing a Lisp interpreter to write your programs in. $\endgroup$
    – Molossus Spondee
    May 12 at 19:50
  • 1
    $\begingroup$ I think in any way there must be a method for quantifying over functions/predicates if we want schemas. Even in Metamath, variables are really second-order (since they can be substituted for expressions that contain free variables), which may look ugly because MM allowed some "controlled naming clashes" among those introduced free variables. Metamath Zero is similar, but it gives a better control over the naming thing. (I personally feel that the "free-variable" approach is still less intuitive/natural than using lambda binders...) $\endgroup$
    – Zhanrong Qiao
    May 12 at 21:22

0

Reset to default

Your Answer

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

Browse other questions tagged or ask your own question.