For anyone interested in formal verification, there's this super slick project Metamath Zero [0] by Mario Carneiro that is working to implement a verifier that can verify itself, compiled binary and all.
As discussed on the project page, Lean is aimed at being ergonomic but at the price of a large (and somewhat buggy) codebase. On the opposite end of the spectrum is Metamath [1] which aims at being the minimum needed for formal verification, but at the cost of extremely pedantic (albeit interesting!) proofs.
Metamath Zero, attempts to find a happier balance by designing a language which is both ergonomic for the proof-writer as well as minimal enough to allow self-verification.
At the moment, the project is still pretty alpha but Mario is both extremely talented and actively developing. That said, if you are someone like me and just want to dive into the math, definitely check out Metamath [1]. It's library of proofs for standard ZFC foundations, set.mm [2], is seriously impressive. I mean, you can find a proof of the fundamental theorem of calculus and trace it all the way back to axioms if you so please (see theorems ftc1 [3] and ftc2 [4])!
For someone with a background in math, the set.mm [2] database is an absolute blast to rogue around in. It takes some getting used to, but I am starting to prefer set.mm over Wikipedia when applicable.
Not the point of the article at all, but in my experience when an author says "canonical map" it can typically be made precise as a unique natural transformation between whatever functors capture the objects of discussion. I think this is part of what MacLane meant by Category Theory being invented to talk about natural transformations.
Avigad, one of the Lean authors has several resources cited elsewhere in Xena Project. These are really useful to learn the necessary background [1,2].
IMHO, logic and type theory are the algebra and calculus of computer science. CS degrees should be designed around some core courses on these, in the same way Math degrees tend to build up on linear algebra and real analysis coursework.
Should a language be able to form predicates total over all possible expressions in the language (including these predicate expressions) in a non trivial way, could these be then identified as 'types' in the sense that each can partition the set of all expressions in the language into 'of the type' and 'not of the type'? Is this still type theory, or something else?
Usually it's not possible to form such a predicate. If we have impredicative base universe, then it's possible to form a predicate over all types in the base universe (which may or may not be all types in the language), including the predicate itself. However, this feature is rarely used in type theory, because it is incompatible with classical logic.
In programming, this is more commonly available, because we don't necessarily care about propositions, let alone classical logical proofs. The polymorphic identity function type `forall a. a -> a` in System F quantifies over all types including itself.
> Should a language be able to form predicates total over all possible expressions in the language (including these predicate expressions) in a non trivial way, could these be then identified as 'types' in the sense that each can partition the set of all expressions in the language into 'of the type' and 'not of the type'?
Normally you'd want to give each term a single type, rather than say that terms do or don't have a bunch of different predicate types.
> Is this still type theory, or something else?
If your predicates apply opaquely to complete expressions then it's not (nontrivial) type theory. The point of type theory is that your typing rules tell you the types of your expressions (or whether they're validly typed at all) in terms of the types of their subexpressions.
Is it just me, or is "proof" used in two ways also – the logic and the result? To use the given example, do I need to understand the logic of the Bolzano-Weierstrass proof in order to use it?
No, those are different things. The proposition and its proof. You can assume a proposition and make use of it without a proof.
A proof furnishes the evidence that a given proposition is attainable (e.g., true).
Truly, you could even see this as being composed of three things
- The proposition
- The "stamp of truth"
- (there's a word from Kant that hits this, but I've forgotten it)
- The proof
A proof always furnishes the "stamp of truth", but you could imagine receiving the stamp of truth without receiving the proof. For instance, an authority you trust implicitly tells you it. Alternatively, take a look at all of the zero-knowledge proof work in crypto.
Additionally, there may be many proofs of a single proposition, and thus the "stamp of truth" seeks to represent them as a the equivalence class of proofs instead of giving each different method its own identity. This, formally, is the notion of "proof irrelevance". It flies in the face of computation where we care a great deal about algorithmic concerns, but from a correctness perspective perhaps all you need is the "stamp of truth".
One last way to give color here is to note what the advantage of proof _relevance_ is. In particular, if the structure of the proof itself is visible then we can do things such as _transform_ proofs (think: lisp macro). In this way, we can get more flexible systems which are allowed to port much of a proof's mechanism over to a new target automatically.
Of course, mathematicians demand proof relevance because mathematicians (a) don't trust things they can't see and (b) want to cannibalize proofs for their mechanism and to reuse those mechanisms on other problems. Proof irrelevance is often important for computational reasons: we don't want to carry around the burden of proof (literally) if we don't have to.
It is both, in the same way as a function is both its implementation and its "extension" (its effect on all inputs). You don't need to know how `sort` is implemented, if you know that it sorts; similarly, you don't need to know how Bolzano-Weierstrass is proved if you want to use it.
> It is both, in the same way as a function is both its implementation and its "extension" (its effect on all inputs).
Note that, according to definition of 'function' most common in math, this is false. A function need not even be implementable.
Aside: As someone trained in math I've always found explanations of type theory "fractally confusing" because of stuff like this: type theorists' words mean something different from my words, and in the explanation of what they do mean, they use words that also mean something different.
A function is rather like a group: it's more important as an idea than as a rigorous definition. Working mathematicians may be vaguely aware that a function "is" a set of ordered pairs (just as they may be vaguely aware that a real number "is" a Dedekind cut), but they're unlikely to think about a function in those terms when they're actually working with it (unless they're working specifically on foundational issues). Indeed the set-theoretic model of a function accommodates impossible functions - but that's one of the main problems that type theory exists to solve. The type-theoretic model of a function does not correspond directly to the ZFC model of a function, but the hope of type theory is that it should correspond more closely to the day-to-day working concept of a function (whether you're a mathematician or a programmer).
> > ... a function is both its implementation and its "extension" (its effect on all inputs).
> Note that, according to definition of 'function' most common in math, this is false.
The standard definition of function in ZFC is a set of tuples pairing every "input" with an "output", so I think the previous commenter was correct with this reading.
> A function need not even be implementable.
However, if you are alluding to computable functions, then certainly, the story is a lot more interesting!
Nope, as long there is _any_ proof (i.e. implementation logic), you can use it. Similar to software -- if you're happy with a library's interface, you don't have to read its source code in order to use it.
It is like mathematics in set theory, as set theory can be used for a foundation of mathematics; however, it is not like real analysis, because real analysis cannot be used as a foundation for mathematics (without torture.)
I'm sorry but you misunderstand the situation. Set theory, type theory and category theory can be used for metamathematics [1] whereas real analysis and number theory cannot. They are foundational theories whereas real analysis and number theory are not. The reason for the difference has to do with the expressiveness of the formal languages and how they themselves can be expressed without a prior language other than formal logic itself.
I know they are foundations of mathematics. They are elements of mathematical logic. No disagreement on this.
But how they are not mathematics? They are part of mathematical logic and mathematical logic or logic in general is branch of mathematics. Do you want to say they are somehow separated from math?
No more nonsense than studying English in English. It is true that type theory is mathematics, but the relevant fact is that it (unlike many fields of mathematics) is suitable for studying mathematics with.
As discussed on the project page, Lean is aimed at being ergonomic but at the price of a large (and somewhat buggy) codebase. On the opposite end of the spectrum is Metamath [1] which aims at being the minimum needed for formal verification, but at the cost of extremely pedantic (albeit interesting!) proofs.
Metamath Zero, attempts to find a happier balance by designing a language which is both ergonomic for the proof-writer as well as minimal enough to allow self-verification.
At the moment, the project is still pretty alpha but Mario is both extremely talented and actively developing. That said, if you are someone like me and just want to dive into the math, definitely check out Metamath [1]. It's library of proofs for standard ZFC foundations, set.mm [2], is seriously impressive. I mean, you can find a proof of the fundamental theorem of calculus and trace it all the way back to axioms if you so please (see theorems ftc1 [3] and ftc2 [4])!
For someone with a background in math, the set.mm [2] database is an absolute blast to rogue around in. It takes some getting used to, but I am starting to prefer set.mm over Wikipedia when applicable.
Anyway, I love this stuff!
[0]:https://3g2upl4pq6kufc4m.onion/html?q=metamath%20zero
[1]:http://us.metamath.org/mm.html
[2]:https://github.com/metamath/set.mm
[3]:http://us.metamath.org/mpeuni/ftc1.html
[4]:http://us.metamath.org/mpeuni/ftc2.html