3
$\begingroup$

Some authors refer to their works as "implementation of the theory in (let's say) Agda", some refer as "formalization of the theory in Agda". What is the difference between them?

$\endgroup$
4
  • 1
    $\begingroup$ Can you provide an example of each? It sounds like they are the same idea, but maybe it would be clear from context they are not. $\endgroup$
    – Jason Rute
    Jun 10, 2022 at 18:43
  • 2
    $\begingroup$ If I was to guess maybe I would “implement” an algorithm (and then also prove stuff about it), and “formalize” a definition or theorem. I might also say that a logical core of a theorem prover is an “implementation” of some logic. $\endgroup$
    – Jason Rute
    Jun 10, 2022 at 18:48
  • $\begingroup$ I was searching for "formalization of 2LTT" and found this (github.com/annenkov/two-level ). Look at also this sentence "The results presented here should be formalizable in a computer proof assistant implementing 2LTT." from the paper (arxiv.org/abs/2102.06275 ). That's why I confused about terminology. $\endgroup$
    – phdstudent
    Jun 10, 2022 at 18:52
  • 1
    $\begingroup$ Yes, in that case the mathematical statements and definitions are formalized in a proof assistant which is implementing a specific base logic in its kernel, in this case 2LTT. $\endgroup$
    – Jason Rute
    Jun 10, 2022 at 18:58

1 Answer 1

1
$\begingroup$

To turn my comments into an answer: Typically one would talk about formalizing something which starts out as informal. So proof assistants are good at formalizing informal mathematical definitions and proofs. For example, a lot of recent work has gone into formalizing probability theory.

While it is possible to formalize something in a formal system using just pen and paper (as done in, for example, Principia Mathematica), it is more common now-a-days to formalize something on a computer. The computer can check that your formalization is correct, following the rules of the formal system. But to do that, one needs to implement the formal system. Various proof assistants implement formal systems/logics like (specific versions) of type theory or set theory.

Now as to the paper you mentioned in the comments, it seems to be a paper about a generalization of the univalence principle which can be stated in two-level type theory (2LTT)---itself a generalization of Martin-Löf type theory (MLTT). The paper is "informal" in that it doesn't give formal proofs or supply any computer code. The last sentence in the paper is:

The results presented here should be formalizable in a computer proof assistant implementing 2LTT.

I think the authors are just stating that one can formally write all the definitions and proofs in the paper in a proof assistant based on two-level type theory, if such a proof assistant exists. But since it likely doesn't exist yet, one has to implement 2LTT in some computer proof assistant first. (This is similar to how Vodvosky formalized the univalence axiom and it's consequences in Coq, which implements a variant of MLTT.) (Note: This likely only makes sense since all the theorems in the paper are positive, namely theorems of the form: "In 2LTT the following holds: ...". If on the other hand, there was a meta-theorem of the form "The following can't be proved in 2LTT: ...", then that wouldn't be formalizable in 2LTT because of Gödel's theorem.)

Now, as for the github repo, I see your confusion since they call it a "Lean Formalisation of Two-Level Type Theory", but also describe the file fibrant.lean as an "implementation of the two-level type theory ". Here is what I think is going on. Lean 2 (unlike Lean 3 and 4) has support for homotopy type theory (HoTT) built in. You could say (the HoTT version of) Lean 2 is an implementation of HoTT. I don't know much about 2LTT, but it looks like to implement it o ntop of Lean 2, the repo authors didn't need to change the underlying kernel of Lean 2 which implements type theory. Instead they just have to add in some additional axioms and definitions. (You can see the axioms by looking for keyword constant in the file fibrant.lean.) So they are doing the same kind of tasks as typical formalization work, namely adding a bunch of definitions, axioms, and proofs to Lean 2.

$\endgroup$
1
  • 2
    $\begingroup$ Such a proof assistant didn't exist when the paper was written, but Agda now has an experimental --two-level flag. $\endgroup$ Jun 14, 2022 at 6:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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