This repository contains the code for my GSoC'19 project with AOSSIE.
I formalised the arguments for origin essentialism given by Nathan Salmon (summarised here) and by Guy Rohrbaugh & Louis deRosset (in this paper) in modal logic K and S5.
- I used the modal logic formalisations previously created by AOSSIE. K and S5 systems were used as they are.
- Every proof file has the author(s)'s original version mentioned in the beginning.
- A total of six versions have been formalised using the Isabelle theorem prover (v2019).
- I used leibniz identity to denote overlapping. Hence, the arguments do not require necessity of distinction. I have also shown that necessity of distinction can be proved in K, hence the arguments can be proved in K.
- Future work may include some other formalisation for overlapping instead leibniz identity (possibly mereology axioms), or a formalisation of the Four Worlds Paradox.
The working papers for different versions of the proofs presented can be viewed at: