Can You Use Kind ( Remotely ) Similarly to Metamath?

[zicklag]

Hey there!

This is a relatively uninformed question I believe, so if it's not worth your time to answer, feel free not to! :)

Anyway, I've recently discovered Metamath and I love the concept of being able to define abstract logic through axioms and use them to prove theorems.

I've also seen kind/HVM a little while ago and it looks like it's recently come pretty far. ( Good job! I see so much potential with this technology! )

Anyway, I'm wondering whether or not Kind can be used effectively to prove theorems similar to Metamath. I understand that Metamath is intentionally simpler, acting as just a substitution engine essentially, while Kind is more of a proof assistant of sorts.

But does the same concept hold? That I may define my own axiom schemes and prove theorems using propositional/predicate calculus and set theory, etc.?

[zicklag]

I did find some examples in wikind that seem promising: https://github.com/Kindelia/Wikind/blob/master/Quantifier/.

This is pretty exciting to me. I don't have a functional programming background. Functional languages always looked quite bizarre to me, but after reading the Metamath intro on logic, and abstract mathematics, everything didn't seem as scary or confusing and now I'm kind of fascinated by some of the concepts.

I was looking for something I could experiment with writing proofs and not sure whether I should use metamath, mm0, or something else. It looks like Kind will work. :)

Add that to the HVM and it's revolutionary speed, plus Kindelia and it's tokenless ( perfect! ) blockchain model, this is some amazing work.

[algebraic-dev]

Hey there!

This is a relatively uninformed question I believe, so if it's not worth your time to answer, feel free not to! :)

Anyway, I've recently discovered Metamath and I love the concept of being able to define abstract logic through axioms and use them to prove theorems.

I've also seen kind/HVM a little while ago and it looks like it's recently come pretty far. ( Good job! I see so much potential with this technology! )

Anyway, I'm wondering whether or not Kind can be used effectively to prove theorems similar to Metamath. I understand that Metamath is intentionally simpler, acting as just a substitution engine essentially, while Kind is more of a proof assistant of sorts.

But does the same concept hold? That I may define my own axiom schemes and prove theorems using propositional/predicate calculus and set theory, etc.?

Yes, you can proof propositions, define your own axioms and prove theorems but right now kind is unsound so we can find some proof of falses in Kind... kinda easily.