I had a course that included proving some theorems using Coq and I really felt stupid. This series is a life saver, thank you very much and hope you're doing great!
Glad I could help! And don't feel stupid, theorem proving is hard enough even when you're not battling with a proof assistant. I had my share of late nights using Isabelle/HOL at uni
27:21 Correction: Proof theory is a major branch of mathematical logic, which in contrast to model theory is not semantic but syntactic in nature. You shouldn't call a deductive system that. But the syntactic aspects of those systems are researched in the field of proof theory.
Metamath builds formal proofs in Hilbert systems, and there is a tool called pmGenerator that can find and parse propositional Hilbert-style proofs from condensed detachment (i.e. implication elimination with instantiation to most common unifiers) notation.
3 years later people still benefit from your efforts, thank a lot dude.
I had a course that included proving some theorems using Coq and I really felt stupid. This series is a life saver, thank you very much and hope you're doing great!
Glad I could help! And don't feel stupid, theorem proving is hard enough even when you're not battling with a proof assistant. I had my share of late nights using Isabelle/HOL at uni
@@vacuoustruth2030 Agda survivor here, great work fellas
Astonishing, thanks so much for the summary.
No worries, glad it was helpful!
Absolute lifesaver !
Truly, you slayed this topic, i was struggling with natural deduction! underrated king! yaas
Just brilliant, thank you.
That's very kind, thanks!
only video i could find that i properly understood.
You're a life saver, thank you so much for this!
No problem, I'm very glad it was so useful!
Thanks for the kind words!
27:21 Correction: Proof theory is a major branch of mathematical logic, which in contrast to model theory is not semantic but syntactic in nature. You shouldn't call a deductive system that. But the syntactic aspects of those systems are researched in the field of proof theory.
Crazy shit man. You gave me the why. All other teachers think i dont want to know the why.
I am stuck for Hilbret-style proof and looking where I lost. I can say your approach is a good one.
Metamath builds formal proofs in Hilbert systems, and there is a tool called pmGenerator that can find and parse propositional Hilbert-style proofs from condensed detachment (i.e. implication elimination with instantiation to most common unifiers) notation.
Is this an alternative to fitch style?