6 ms·

I have a project to write a proof assistant that is as simple as possible while still usable. A kind of turing tar pit but for proofs instead of programs. Some

by cjfd 3y ago

I have a project to write a proof assistant that is as simple as possible while still usable. A kind of turing tar pit but for proofs instead of programs. Some early attempts did not quite work out. I try to get it off the ground using the calculus of constructions (not the calculus of inductive constructions) together with a small set of axioms. As axioms I aim, at the moment, to use a hilbert epsilon operator to contstruct objects from theorems that state their existence, proof irrelevance and an infinity axiom that states that an infinite set exists. Also I do use an infinite hierarchy of Types a bit like the universes of coq. I am still debating with myself whether I also should provide the luxury of not having to specify universe levels and just keep constraints between them like in coq. The article proposes the calculus of inductive constructions but I think that is just too big and complicated to be a good candidate for a foundation of mathematics. I think it makes more sense to use a more concise foundation and maybe attempt to prove that the calculus of inductive constructions is a conservative extension of that.

bvssvni 3y ago
Is your goal to have as few axioms as possible, or as few syntactic constructions as possible?
- cjfd 3y ago
  Both really. Just as few givens as possible whether they are baked in or added on as axioms.
zarzavat 3y ago
The calculus of inductive constructions is not very big? It seems simpler than ZFC to me. The version that Coq uses is quite large, but that's the difference between theory and practice: Coq is designed to be maximally usable not minimally simple.
- cjfd 3y ago
  Well, inductive constructions need positivity conditions to be consistent. These are complicated enough to suggest that they need to be proven instead of accepted as part of the formal system.
lacker 3y ago
Once you have an infinite hierarchy of types, including universe levels, can the proof assistant really be "as simple as possible"? I feel like a simple-as-possible proof assistant would be more like, proving things about programs written in a minimal Lisp dialect, where the proof validator is itself written in that Lisp dialect. That said, I personally would rather have an extremely usable proof assistant, rather than a simple-as-possible one. In many ways those things point in opposite directions; consider the usability and simplicity of Python vs the lambda calculus.
- blueberry87 3y ago
  What are your other options? A type-based proof system implies dependent types, implies universe levels if you want it to be consistent.
  - lacker 3y ago
    You would have to not use a type-based proof system. I think those are not going to be the "as simple as possible" ones. Consider metamath for example.
  - JonChesterfield 3y ago
    Why do dependent types require universe levels to be consistent? I mostly see that in the context of the type of all types and similar, which doesn't seem especially necessary to express. A variable that denotes a type could have type 'any' or 'unspecified', as opposed to a type T^1 or similar.
    - deltasepsilon 3y ago
      I believe the parent was referring to Girard's paradox [1], but it's been a while and I'm not a specialist in this area. [1] https://en.wikipedia.org/wiki/System_U#Girard's_paradox https://en.wikipedia.org/wiki/System_U#Girard's_paradox
    - cjfd 3y ago
      They do not really require it but note my other answer in this subthread.
c-cube 3y ago
If you want something as simple as possible, look at HOL and similar simple logics! CIC is powerful but it's also quite complex in comparison. Proof assistants based on HOL are plenty and they're definitely usable (see Isabelle/HOL, HOL light, etc.)
- cjfd 3y ago
  I did study HOL Light. Although it is very simple, I found parts of it to be a bit ugly. It treats the left of the turnstyle (|-) as a kind of set where you sometimes have to remove all alpha-equivalent terms. I.e., the DEDUCT_ANTISYM_RULE in https://en.wikipedia.org/wiki/HOL_Light https://en.wikipedia.org/wiki/HOL_Light. Another thing that I found ugly in HOL Light is that if one looks at the very basic code that is the kernel of the system all variables carry their type around with them. I think the lambda calculus where (\x: T, body) just has the type of x in the lambda and not in every instance of x inside body is just nicer.
  - c-cube 3y ago
    I agree that the treatment of alpha equivalence might not be the best. Isabelle/HOL has pattern unification which makes it easier. For the type variables: it's a matter of taste! I prefer it this way, and it's quite useful if you expect terms and theorems to have free variables (quite common in automatic provers). Having free variables is a good way to specify things like rewrite rules, backward chaining clauses, etc. so it doesn't come out of the blue.

by cjfd 3y ago

bvssvni 3y ago

Is your goal to have as few axioms as possible, or as few syntactic constructions as possible?

cjfd 3y ago
Both really. Just as few givens as possible whether they are baked in or added on as axioms.

zarzavat 3y ago

The calculus of inductive constructions is not very big? It seems simpler than ZFC to me. The version that Coq uses is quite large, but that's the difference between theory and practice: Coq is designed to be maximally usable not minimally simple.

cjfd 3y ago
Well, inductive constructions need positivity conditions to be consistent. These are complicated enough to suggest that they need to be proven instead of accepted as part of the formal system.

lacker 3y ago

Once you have an infinite hierarchy of types, including universe levels, can the proof assistant really be "as simple as possible"? I feel like a simple-as-possible proof assistant would be more like, proving things about programs written in a minimal Lisp dialect, where the proof validator is itself written in that Lisp dialect. That said, I personally would rather have an extremely usable proof assistant, rather than a simple-as-possible one. In many ways those things point in opposite directions; consider the usability and simplicity of Python vs the lambda calculus.

blueberry87 3y ago
What are your other options? A type-based proof system implies dependent types, implies universe levels if you want it to be consistent.
- lacker 3y ago
  You would have to not use a type-based proof system. I think those are not going to be the "as simple as possible" ones. Consider metamath for example.
- JonChesterfield 3y ago
  Why do dependent types require universe levels to be consistent? I mostly see that in the context of the type of all types and similar, which doesn't seem especially necessary to express. A variable that denotes a type could have type 'any' or 'unspecified', as opposed to a type T^1 or similar.
  - deltasepsilon 3y ago
    I believe the parent was referring to Girard's paradox [1], but it's been a while and I'm not a specialist in this area. [1] https://en.wikipedia.org/wiki/System_U#Girard's_paradox https://en.wikipedia.org/wiki/System_U#Girard's_paradox
  - cjfd 3y ago
    They do not really require it but note my other answer in this subthread.

c-cube 3y ago

If you want something as simple as possible, look at HOL and similar simple logics! CIC is powerful but it's also quite complex in comparison. Proof assistants based on HOL are plenty and they're definitely usable (see Isabelle/HOL, HOL light, etc.)

cjfd 3y ago
I did study HOL Light. Although it is very simple, I found parts of it to be a bit ugly. It treats the left of the turnstyle (|-) as a kind of set where you sometimes have to remove all alpha-equivalent terms. I.e., the DEDUCT_ANTISYM_RULE in https://en.wikipedia.org/wiki/HOL_Light https://en.wikipedia.org/wiki/HOL_Light. Another thing that I found ugly in HOL Light is that if one looks at the very basic code that is the kernel of the system all variables carry their type around with them. I think the lambda calculus where (\x: T, body) just has the type of x in the lambda and not in every instance of x inside body is just nicer.
- c-cube 3y ago
  I agree that the treatment of alpha equivalence might not be the best. Isabelle/HOL has pattern unification which makes it easier. For the type variables: it's a matter of taste! I prefer it this way, and it's quite useful if you expect terms and theorems to have free variables (quite common in automatic provers). Having free variables is a good way to specify things like rewrite rules, backward chaining clauses, etc. so it doesn't come out of the blue.