1

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?

|improve this question
  • It might be worth posting the content of de_morgan_so.ctt in this question in case it changes. Welcome to Philosophy! – Frank Hubeny Feb 7 at 22:16
  • 1
    By "inhabitance", do you mean "existence"? – virmaior Feb 7 at 22:44
  • 1
    and by classical logic, do you mean modern logic (i.e. written out with variables and quantifiers)? (Classical logic usually refers to Aristotle's logic where "All unicorns are white" is false because all statements require at least one member to be true vs. contemporary logic which can have empty sets). – virmaior Feb 7 at 22:45
  • 2
    @virmaior When logicians talk about classical logic they usually mean classical as opposed to intuitionistic. Aristotelian logic is pretty much insignificant. As for the question itself, it seems to me that you are asking for a very basic fact. I would even go so far as to say, if you haven't understood that, you shouldn't study type theory. Start at the beginning, as the saying goes. – Jishin Noben Feb 7 at 23:02
  • @JishinNoben bit lost as to what you're trying to say to me. People still read the Organon where I did my PhD, and those who do call the Aristotelian picture classical logic. Moreover, the distinction I describe in the square of opposition is the basic distinction and seems to be what the OP is asking about by "inhabitance". See for instance, researchgate.net/post/… – virmaior Feb 7 at 23:42
0

When the domain is empty, ∀x P(x) will be vacuously true, and hence ¬∀x P(x) → ∃x ¬P(x) shall be true; because classical logic holds conditionals to be true when their antecedents are false.

NB: ∃x ¬P(x) shall also be vacuously false, but that does not matter.   The conditional false → false is true.

Obviously, the latter statement requires that there would also exist at least one spaghetti monster.

So, no, that is not so.   If there are in fact no spaghetti monsters, then it would be unsound to use modus ponens to establish the consequence, "some spaggetti monsters are not blue", since the premise, "not all spaghetti monsters are blue", is fallacious.

|improve this answer

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.