6
$\begingroup$

You open a code editor, define a syntax with lambdas, a few primitives. Then you invent some nice computation rules, some cool typing rules, and write a corresponding interpreter and "type checker". Congratulations! You just built a proof assistant! Now you can formalize all of mathematics on it! Or can you? After all, what makes the thing you built a valid "proof assistant"? What constitutes a "type checker"? As far as I'm concerned, you could have actually implemented Tetris, claimed that blocks are terms, their shapes are types, and the game loop is the computation rule. Who has authority to argue you're wrong?

When it comes to implementing a "programming language", the definition is much more clear. Just invent a syntax, a set of reduction rules and prove your thing Turing-complete. Then it is as good as a programming language is expected to be. When it comes to implementing a proof assistant, I have no idea. Sure, there are common things I see present in proof assistants, so, intuitively, I know what they are. They have lambdas and the corresponding dependent function space, they have inductive datatypes and their introductions and eliminations, and they must be consistent, which mean at least some type is uninhabited. But what if my "proof assistant" has no lambdas nor datatypes? It could have for example just combinators. I don't have a precise definition of what makes a "type theory" a "type theory".

What, formally, makes a program a valid proof assistant, in the same sense that Agda/Coq are? What is a precise and complete definition of a type theory? And what one must do to "justify" his syntax, reduction and typing rules? I'm making this specifically because, while I feel like I can, given enough time, implement something like A Cosmology of Datatypes, I do not feel the freedom to make any change, even minimal, to whatever the author did, because I do not know what justifies those things he did.

Improve this question
$\endgroup$
7
  • 3
    $\begingroup$ The term "proof assistant" certainly has no formal definition, and I don't think type theory could be given one either. And I don't agree at all with your definition of "programming language": Turing completeness is a fairly arbitrary boundary for that. It seems like you maybe what you are actually asking is how to justify the consistency of a logic/type theory which is a much more sensible question. $\endgroup$
    – Max New
    Sep 16, 2018 at 3:16
  • 2
    $\begingroup$ Not all proof assistants have lambdas or dependent types. I don't see why you'd care whether you could call whatever you built a "proof assistant" if it is solving a problem for you. $\endgroup$
    – Derek Elkins left SE
    Sep 16, 2018 at 5:00
  • $\begingroup$ In practice, almost all practical programming languages are Turing-complete - even XSLT is Turing-complete. However, one reason why you might not want to make a programming language Turing-complete, is that if you also want to make your programming language a proof assistant, you probably don't want infinite loops in your programs to be able to be used to prove 1=2, and Turing-completeness requires the ability to construct infinite loops. $\endgroup$
    – Robin Green
    Sep 16, 2018 at 18:29
  • 1
    $\begingroup$ You can in fact build a proof assistant using a language which has non-termination, as long as you have good canonicity theorems for values (the results of computations), and that you are willing to wait for the proof computation to terminate, and not just to type-check, before you claim that you have a proof. $\endgroup$
    – gasche
    Sep 16, 2018 at 18:45
  • $\begingroup$ @gasche Wouldn't this criterion work only for quantifier-free statements? Given an unconstrained fix combinator, I would expect you would be able to write a term in normal form of type forall (x : Nat). x = suc x. You would start by matching on x before the recursive call to make sure the term is stuck. $\endgroup$
    – gallais
    Sep 16, 2018 at 19:28

2 Answers 2

Reset to default
8
$\begingroup$

I would expect a proof assistant to provide:

  1. a syntax to express some mathematical statements
  2. a syntax to express a proof of one of those statements
  3. a computational process to "check" that a proof of a statement is indeed valid (returns success or failure, or maybe does not return at all)

Finally, for such a proof assistant to be trustworthy, it should come with a justification of the fact that when its checking process says that a proof of a statement is valid, then indeed this statement is valid in the usual mathematical sense -- there exists a mathematical proof that mathematicians will accept.

Improve this answer
$\endgroup$
5
  • $\begingroup$ That makes absolute sense to me, but then, what is the "usual mathematical sense"? I'm honestly confused about that. Mathematics usually is built on top of set theory. Type theory is, in a way, another take on set theory. So, that sounds like circular reasoning. "Type theory is defined as something that does mathematics, and mathematics is defined using type theory". $\endgroup$
    – MaiaVictor
    Sep 16, 2018 at 22:40
  • 3
    $\begingroup$ Your question is not about proof-assistants anymore, but about logic. One way to side-step it is to justify the meaning of your statements and the behavior of your checker using a pre-existing logic that is accepted by the community. If you want to build your own logic, then indeed building a model of it in set theory (to show that the statement it proves are also true in set theory) is a good way to convince mathematicians, whether you personally believe that set-theory should be taken as a foundational framework or not. It's a form of portability. $\endgroup$
    – gasche
    Sep 17, 2018 at 6:46
  • $\begingroup$ So, in the end, we just assume set theory is what makes something true in the mathematical sense. Then we model type theory in set theory as a way to say "I can translate proofs on my system to a set-theoretical proof", which obviously makes it perfectly suitable for mathematics. Is that it? If you / anyone else has examples of this practice; i.e., defining your own toy logic and modeling it in set theory; I'd be so thankful. $\endgroup$
    – MaiaVictor
    Sep 17, 2018 at 15:28
  • $\begingroup$ @MaiaVictor Most type theories have no foundational aspirations. My answer here about foundations and its linked question may be useful. It doesn't answer your questions, but your statements suggest you have some misperceptions about how much mathematicians and type theorists think and care about foundations and what foundations are for. More relevant to your questions are questions about the "circularity" between logic and set theory. $\endgroup$
    – Derek Elkins left SE
    Sep 18, 2018 at 3:44
  • 1
    $\begingroup$ When you add a new backend to your compiler, it doesn't mean that you believe this is the best instruction-set ever, and all software should be seen in terms of it. You add it to let more people run your code, that's all. A typical example of consistency proof in set theory would be Benjamin Werner's Set in types, types in set, 1997, which justifies the Calculus of Inductive Constructions (CIC) in terms of ZF set theory, and also the other way around. $\endgroup$
    – gasche
    Sep 18, 2018 at 21:09
5
$\begingroup$

I would think a proof assistant is something which can represent proofs and validate the reasoning is correct. The underlying logic/type theory just determines which reasoning can be represented and validated.

I like your example of Tetris, perhaps it is a proof assistant for a limited subset of geometry, which checks a proof of "these shapes of blocks with these orientations form a solid row of blocks" or something like that 😋

Improve this answer
$\endgroup$

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.