I have a problem reading existing question's answers. I've successfully encoded the proof of one of De Morgan's Laws, ¬∃x P(x) → ∀x ¬P(x)
, for Quantifiers formally via cubicaltt type-checker via Curry-Howard correspondence, the solution is available on GitHub. As the basis, I took the answers from StackExchange question mentioned above, but as I went through their steps, this was unclear to me:
In my Curry-Howard proof, I had to provide a witness that the type is inhabited, and it makes total sense. Without it, the law in its form ¬∀x P(x) → ∃x ¬P(x)
can be formulated as: If it's not true that all spaghetti monsters are blue, it follows that there exists a spaghetti monster that isn't blue. Obviously, the latter statement requires that there would also exist at least one spaghetti monster. Does classical logic not concern itself with inhabitance?