First, I've got proof no. 3. I can offer a nice 4 argument proof, but you wouldn't let me provide it. Second, I tried proof no. 2, where I'm offered words like given and algebra I have no use for.
To make a system like this right it needs to be deductive and have a large library of concepts. Getting this right is complex enough to be a PhD project. Properly scoped could be done for MSc.