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
  • 1
    By "inhabitance", do you mean "existence"? – virmaior Feb 7 '19 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 '19 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 '19 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 '19 at 23:42
  • Rereading the question with your comment however, the OP is probably using the term classical from the opposition classical vs. intuitionist, but it does seem to be repeating the basic distinction between how Aristotle handled "all" statements vs. the contemporary treatment. Which makes it kind of an odd question. – virmaior Feb 7 '19 at 23:45
1

According to Wikipedia the domain of discourse for a classical first-order logic is usually considered to be non-empty:

An interpretation (or model) of a first-order formula specifies what each predicate means and the entities that can instantiate the variables. These entities form the domain of discourse or universe, which is usually required to be a nonempty set. [my emphasis]

When the domain is permitted to be empty, it is called a free logic in contrast to a classical logic:

A free logic is a logic with fewer existential presuppositions than classical logic. Free logics may allow for terms that do not denote any object. Free logics may also allow models that have an empty domain.

Just insist as is usually required that the variables in a classical first-order logic are instantiated from entities in a non-empty domain of discourse. This should avoid the concern about non-existent entities from empty domains.

Wikipedia contributors. (2019, June 27). First-order logic. In Wikipedia, The Free Encyclopedia. Retrieved 18:58, July 8, 2019, from https://en.wikipedia.org/w/index.php?title=First-order_logic&oldid=903705274

Wikipedia contributors. (2019, April 15). Free logic. In Wikipedia, The Free Encyclopedia. Retrieved 19:01, July 8, 2019, from https://en.wikipedia.org/w/index.php?title=Free_logic&oldid=892578918

|improve this answer
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.