Origin Essentialism // Computational Metaphysics

This repository contains the code for my GSoC'19 project with AOSSIE.

1. Summary of Work

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.

2. Details

• 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.

3. Working Paper

The working papers for different versions of the proofs presented can be viewed at:

• K
• S5
• S5 abriged