feat: soundness and completeness of linear logic phase semantics#424
feat: soundness and completeness of linear logic phase semantics#424tannerduve wants to merge 1 commit intoleanprover:mainfrom
Conversation
tannerduve
force-pushed
the
LL-sound-complete
branch
3 times, most recently
from
cf5fa04 to
aa382c6
Compare
|
Could you please do a pass fixing indentation issues? I started to mark them all individually but I think it is just easier to point out that this in general doesn't adhere to indentation at four spaces for theorem statements using multiple lines. |
definitely. I was unaware of this convention for some reason. |
|
just fixed, lmk if there are other issues wrt indentation or style conventions I've missed |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
This isn't comprehensive, but a few style things I noticed. The formatting in general is a bit rough at the moment, I assume because of the AI usage.
I'd prefer to have @fmontesi review the actual content.
fmontesi
left a comment
fmontesi
left a comment
There was a problem hiding this comment.
This looks pretty good to me, thanks!!
I've left a few comments where I had doubts.
|
addressed these, thanks! @fmontesi |
|
@chenson2018 can you accept? |
I'd like to do a more complete review of style here first, working on it now. |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
I've left just a few additional comments below, but I feel like in general there's a lot of remaining AI footprint that does not feel appropriate to merge. It seems like there's a lot of change and unfolding that should be extracted as lemmas.
Head branch was pushed to by a user without write access
|
@chenson2018 did one more style pass, let me know if any issues remain |
tannerduve
force-pushed
the
LL-sound-complete
branch
from
28f75b3 to
0224998
Compare
tannerduve
force-pushed
the
LL-sound-complete
branch
2 times, most recently
from
d0154f1 to
34154a7
Compare
Co-authored-by: aleph-prover-dev[bot] <247854405+aleph-prover-dev[bot]@users.noreply.github.com>
tannerduve
force-pushed
the
LL-sound-complete
branch
from
34154a7 to
986e92c
Compare
|
@kim-em you can ignore review request, accidentally pulled in some unrelated changes and GitHub automatically requested you |
3 participants
This PR proves that the sequent calculus for full classical linear logic (CLL) is sound with respect to phase semantics, and proves completeness for MALL, the multiplicative-additive fragment of classical linear logic. Specifically it shows that every provable sequent is valid in every phase space, and constructs a syntactic phase model to prove that semantic validity implies provability for MALL.
Note on AI usage: Aleph prover proved several lemmas used in proving completeness, and these proofs were heavily iterated on and golfed by me, ensuring they meet style standards.
A couple of proofs could possibly be further golfed, open to receiving help with this