Zulip Chat Archive

Stream: new members

Topic: Classical propositional logic- completeness and soundess


view this post on Zulip jachym simon (Nov 16 2020 at 17:10):

Hello! I was formalising a proof of completeness and soundness of classical propositional logic and i managed succesfuly (did that as a bachelor thesis). I wanted to ask, whether it has some actual value, can be used somewhere or something? I kind of suppose its nothing complicated (maybe it was even done before?), but still. I also would be very thankful- since i am fairly bad with lean and not at all sure with what i created- if someone would be up for scanning through the code to give me some feedback. Its approximately 800 lines long. Cheers, Jachym

view this post on Zulip Johan Commelin (Nov 16 2020 at 17:15):

Congrats on completing your project!
I don't know anything about logic, but I'm sure it doesn't hurt if you paste a link to your code here.

view this post on Zulip jachym simon (Nov 16 2020 at 17:24):

Thank you :)
True, I will upload it and paste the link here.

view this post on Zulip Jasmin Blanchette (Nov 16 2020 at 17:37):

It has been done before in other systems -- see e.g. https://www21.in.tum.de/~nipkow/pubs/types17.pdf . It's always interesting to have these proofs in Lean.

view this post on Zulip jachym simon (Nov 19 2020 at 16:39):

Sooo... i wasnt sure how to share it, so i tried to put it up on github. Here is the link (i hope it works, i dont have much experience with github). Any feedback will be much appreciated!

https://github.com/jachsimon/CPL_completness_soundness-/blob/main/CPL_compl_sound.lean


Last updated: May 12 2021 at 03:23 UTC