Weekly Log:
Week 1/2
The first week was delayed for the weather, but I started to go through the book “A Mathematical Introduction to Logic” from Herbert Enderton. It’s interesting to see logic itself picked apart into it’s components. I’m trying to adjust to the new notion, sometimes I can’t tell if I actually understand it or not. I’m also adjusting to the older notation of the book, as from what I’ve seen the new notation makes sense.
Week 3
Over the weekend I ended up giving myself a concussion. Thankfully it was minor, but it made it hard to get much work done. The times I was able to work I used it to catch up from missing school, so I wasn’t able to get much done.
I did get to the seminar by Chris Kapulkin about constructionist proofs. I am doing another project more on the philosophy side about how proof-assistant software means as mathematicians and what we consider to be proofs. I don’t understand them enough yet to give a correct or understandable explanation, but the thing I’m highlighting is that these are how proof-assisting software function. There are a few thing you can talk about with this. One of the points I’m making is that we generally are proving thing that are ether useful or interesting. Classical proofs let you do more than constructionist, but the ability to use software to solve or check proofs make it quite useful.
Week 4