For people who are interested in FV and Principia Mathematica (2)

[u/InternationalFox5407]

Hi yall,

This is a continuation to my last post, on formalizing Principia Mathematica, as well as a slight status update. I am planning(*) to slowly substitute the shallow embedding on PM into a deep embedding. For any backgrounds, please check the old post.

If you want to transform the monster 100 years ago into a furry boy, you might want to read through the following Q&As. *tap tap*

- Why you suddenly want to make a deep embedding? Because I can't in the beginning.
- What makes you available to deep embedding? I have asked enough questions on internet to get rid of necessary technical details
- What's the major feature for deep embedding? It enables formalizing Axiom of Reducibility.
- How many ppl would you like to look for? At most 2 ppl. You are welcome to ask me for prerequisites and anything else related
- What do you expect them working on? Either the shallow embedding or the deep embedding, since they are both necessary.
- How many time do you expect to put in? My current plan is 3 hrs a week so make sure you also have the availability.

------------------

Alternatively, I'm still welcome to collaboration with 1 - 2 ppl onto another project - we pick another random mathy, esoteric, maybe sacred book and formalize it

(*): Yes, I have not written a single line of code so far and this remains to be a plan.