Classical propositional logic- completeness and soundess

Stream: new members

[jachym simon]

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

[Johan Commelin]

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.

[jachym simon]

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

[Jasmin Blanchette]

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.

[jachym simon]

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