Fitch Style Modal Logic

[gleachkr]

Apropos a discussion on the mailing list, it'd be nice to have a Fitch-style system of modal logic to go along with the proof system from forall x: Calgary

[rzach]

I got a request for this also from @gfrost-arnold

[ioanmuntean]

Hi Zach and Graham, I tried to work with the hardegree system of modal logic, to no avail. do you have any specific suggestions on how to start an exercise in modal logic on Carnap? Thanks in advance!

[gfrost-arnold]

Hi Ioan --

I had a student whose final project is writing up instructions for how to use the Hardegree system in Carnap. She still hasn't finalized them, but the drafts are up on the "Shared Documents" page:

Propositional Logic: @.***/How%20to%20Make%20a%20Proof%20Documentation%20SL%20Final%20Version-6.md

Predicate Logic (note conventions for tagging worlds): @.***/How%20to%20make%20a%20proof%20predicate%20logic-5.md

Basic Notation: @.***/Hardegree%20Notation%20Final%20Version-2.md

I hope this helps! Greg

On Thu, Apr 18, 2024 at 11:59 PM Ioan Muntean @.***> wrote:

Hi Zach and Graham, I tried to work with the hardegree system of modal logic, to no avail. do you have any specific suggestions on how to start an exercise in modal logic on Carnap? Thanks in advance!

— Reply to this email directly, view it on GitHub https://github.com/Carnap/Carnap/issues/298#issuecomment-2065708957, or unsubscribe https://github.com/notifications/unsubscribe-auth/AQMSDEL5SO4KT3CQ4UTWS73Y6CJDXAVCNFSM5MQQYGF2U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TEMBWGU3TAOBZGU3Q . You are receiving this because you were mentioned.Message ID: @.***>

[ioanmuntean]

Dear Greg I think we met a couple of years ago on the conference circuit. What a great surprise. Thanks for the heads-up. I teach a symbolic logic course at U of Illinois and I used Carnap for first-order logic with some mixed success. Thanks for pointing out these documents by Tayla and yourself. I think I downloaded them and tried to reformulate some proofs, but I had no success. I looked up your document and Tayla's and I have some feeling that they can work. I did not manage to start the sandbox on anything....

When I taught Modal logic (a full course) I used tableaux from Girle's book, but now I follow ForAllX Calgary remix which has some Finch-style natural deduction for Modal Propositional Logic. I think also that the Open Logic project has modal logic Natural deduction in it. Did you try talking to Zach or Graham about implementing something like this. Exchanging some ideas would be very beneficial. I do not have anything yet to share but if I make the Hardegree system work I'll let you know. Thanks, and I really hope to meet you sometime. Cheers! Ioan

[rzach]

This very issue report is about adding forall x: YYC's (ie., Fitch's) modal ND systems.

(OLP doesn't (yet) have ND for modal logic -- there are Fitting tableaux though)

[ioanmuntean]

Zach, Thanks. I want to tell you how much I appreciate your work with both ForAllX and Open Logic Project. You are right, I was thinking about ND in intuitionistic logic in OLP, and I got confused with modal logic. I use Carnap.io and I was trying to give students homework in extension of FOL: modal logic and/or intuitionistic logic. Carnap.io has Hardegree's system, but I could not make it work and I do not know of any intuitionistic logic in Carnap.io. If there is a way to contribute and implement the ND from ForAllX in Carnap and I can help, let me know. Probably Greg and Tayla are interested. The alternative is to implement tableaux as in OLP or in Girle. That would be awesome! I did not know that ForAllX added modal logic in the last year or so. Thanks! Ioan Muntean

[rzach]

For intuitionistic logic it's easy: just tell them they can't use IP. (@gleachkr there is no secret option to prohibit a set of rules in a derivation is there?)

There is a separate system for intuitionistic logic in Gentzen format: https://carnap.github.io/Carnap-Manual/gentzen-ND.html