undefined

points

by dwheeler6 hours ago |

comments

by leonidasrup6 minutes ago|

[-]

Metamath is interesting for education in the principles of formal proofs, because:

1. The Metamath Book is self-contained well written, simple introduction.

2. Everything is explicit, nothing is hidden.

3. Because of extremely simple syntax and semantics it's easy write own proof verifier.

The drawbacks are:

1. Non-standard approach to free and bound variables.

2. Very weak logic in comparison to Lean. The logical syntax rules and logical semantics rules used for proving mathematical statements in Metamath, have to be explicitly specified in the Metamath database. In Lean they are part of the Lean kernel. An bug in this Metamath specification is equivalent to a bug in Lean kernel.

3. Almost no proof automation. No tactics. Long, hard to read proofs.

I would characterize Metamath as the assembly language of proof assistants, very low level and detailed way to write proofs.

by ux2664786 hours ago|

prev|

[-]

What semantics do you use for your HOL library? I scanned around but documentation on that page is a bit sparse. The github repo goes to a random user's page, and all I could find there was this unrelated repo: https://github.com/digama0/HOL

by xelxebar6 hours ago|

parent|

[-]

Yeah, that github URL should be fixed. The HOL database is here https://github.com/metamath/set.mm/blob/develop/hol.mm

by SpaceManNabs3 hours ago|

prev|

[-]

There are other forms of logic? is intuitionistic logic as rigorous? fascinating

edit: the link says it is a weakening. if it is weakened, how can you prove the same stuff? i am a bit confused but i can see how it is useful for smarter people than me!

by nimih2 hours ago|

parent|

[-]

> if it is weakened, how can you prove the same stuff?

Sometimes, you can't. In particular, so-called "non-constructive" proofs don't work in intuitionistic logic. Some mathematicians like to work in intuitionistic logic: for philosophical reasons, pragmatic technical considerations, or just because they think it's interesting.

by zozbot2341 hours ago|

parent|

[-]

This is not entirely true: non-constructive proofs can be fully understood within intuitionistic logic as proofs of negative statements, viz. statements about what isn't constructively true or doesn't constructively exist. From this point of view, intuitionistic logic can be seen as stronger and more powerful than classical logic, because it can endow positive statements (particularly statements about logical disjunctions or existentials) with computational content whenever they have a direct proof.

Classical logic doesn't bother with this; positive and negative statements are completely dual to one another, and this duality is elegant in its own way (as people who are committed to classical logic will readily point out), but one needs linear logic in order to combine it with an awareness of constructive statements.

by black_knight2 hours ago|

parent|

prev|

[-]

Having a weaker base system means you can distinguish more fine grained between statements.

For example, in an intuitionistic setting there is a difference between a set being non-empty and a set having an element.

by IsTom2 hours ago|

parent|

prev|

[-]

Intuitionistic logic can prove less than classical logic, but what you gain is that proofs are constructive. Also you can use it to reason about things for which law of excluded middle doesn't hold (typically types).