Truth of a sentence in predicate logic I'm working through the exercises in this Logic problem set and I'm struggling to understand ex. 7.5:

Determine whether the following sentence is logically true in predicate logic:

There is someone such that, if he or she is asleep, everyone is asleep.


The solutions section suggests this is True and gives a formal 'Natural Deduction' proof that I don't really understand (it probably doesn't help that I don't have a copy of the book the solutions keep referring to).
Is there another way to approach this?
 A: This is a classic example of the mismatch between the meaning of if in classical logic and its ordinary intuitive meaning. It is called the drinker's paradox.
Let's use the fact that $\varphi \to \psi$ is equivalent to $\lnot \varphi \lor \psi$ in classical logic to paraphrase the sentence in natural language and avoid the troublesome if.
There exists a person w such that w is not asleep or everyone is asleep.

Let $c$ be an arbitrary person in our group of people.
Suppose everyone is asleep, then we pick $w$ to be $c$. Since everyone is asleep, this value of $w$ satisfies the condition.
Suppose at least one person is awake, call them $a$. Then we pick $a$ as $w$.
I think the reason why this is counterintuitive is that the choice of $w$ depends on who happens to be asleep right now or not, but the phrasing of the question in natural language implies that a fixed $w$ has some special property that someone causally determines which configurations of awake and asleep people are possible.
The paradox goes away completely if we give the conjunction or wide scope over exists. We can do this unambiguously in natural language by reordering the dijsuncts. Reordering the dijsuncts, and changing the order of the disjunction and existential quantifier in this specific case are both allowed in classical logic.
Everyone is asleep or there's a person who is not asleep.

A: Case 1: There is someone who is not asleep. In that case, let $p$ be the person who is not asleep.
Then we see the following implication holds: if $p$ is asleep, then everyone is asleep. This is vacuously true, since $p$ is not asleep.
Then there indeed exists some person $p$, such that if $p$ is asleep, everyone is asleep.
Case 2: There is not anyone who is not asleep. In that case, everyone is asleep. Let $p$ be some person.
Then we see that the following implication holds: if $p$ is asleep, then everyone is asleep. This is true because everyone is, in fact, asleep.
Then there indeed exists some person $p$, such that if $p$ is asleep, everyone is asleep.
A: This is a sometimes odd-sounding feature of existentially quantified implications.
If we express the statement formally it's: $$\exists x (A(x) \to \forall y\, A(y)).$$
Consider two cases:

*

*everyone is asleep, or

*not everyone is asleep.

In case 1, $\forall y\, A(y)$ holds, and hence the implication $A(x) \to \forall y\, A(y)$ would hold (without worrying about whether $x$ is asleep or not),
In case 2, we can find someone so that $A(x)$ is false, hence again the implication must be true.
A: 
[...] It seems entirely trivial by comparison to the long chain of formal manipulations given as the solution, so I assumed it had to be faulty. [...]

The problem with your assumption is that formal proofs from scratch need to prove every single bit of the reasoning involved. In particular, how exactly do you justify that either "there is someone who is not asleep" or "there is not anyone who is not asleep"? Depending on your specific chosen formal system, this may be an axiom called LEM (law of excluded middle) or require a few lines of proof. Similarly, to get from the latter to "everyone is asleep" again may be allowed in one inference step or require some more lines of proof.
Here is a completely formal proof using a Fitch-style natural deduction system with LEM. The key to get an intuitive proof is to use LEM, so if the system does not support LEM then you simply prove the instance of LEM that you need! Shorter proofs in a formal system may be less intuitive.
If ∃x∈People:  [✰]
  ∃y∈People ( ¬Asleep(y) ) ∨ ¬∃y∈People ( ¬Asleep(y) ).  [LEM]
  If ∃y∈People ( ¬Asleep(y) ):
    Let c∈People such that ¬Asleep(c).
    If Asleep(c):
      Contradiction.
      ∀x∈People ( Asleep(x) ).
    Asleep(c) ⇒ ∀x∈People ( Asleep(x) ).
    ∃a∈People ( Asleep(a) ⇒ ∀x∈People ( Asleep(x) ) ).
  If ¬∃y∈People ( ¬Asleep(y) ):
    Let d∈People.  [from ✰]
    If Asleep(d):
      Given any x∈People:
        If ¬Asleep(x):
          ∃y∈People ( ¬Asleep(y) ).
          Contradiction.
        Asleep(x).
      ∀x∈People ( Asleep(x) ).
    Asleep(d) ⇒ ∀x∈People ( Asleep(x) ).
    ∃a∈People ( Asleep(a) ⇒ ∀x∈People ( Asleep(x) ) ).
  ∃a∈People ( Asleep(a) ⇒ ∀x∈People ( Asleep(x) ) ).

Important note: The statement in your question is actually not a logical tautology. As you should see from the above proof, it depends crucially on the assumption that there exists some person, otherwise it is trivially false.
~ ~ ~ ~ ~ ~ ~
Also, contrary to popular belief, the apparent paradox here is not really due to any mismatch between the English "if" and logical "if"! Rather, it is due to incorrect translation of the English sentence, due to the use of the generic present tense! Notice that the following sentence is actually true when interpreted according to standard English:

There is someone such that, if he or she is asleep at midnight on 16 Mar 2021, then everyone is asleep at midnight on 16 Mar 2021.

The problem with the original sentence was that because it used the present tense without a context specifying a single time, the time ended up being quantified outside the "if", and so it ended up being interpreted as:

There is a person A such that, at every time t, if A is asleep at time t, then everyone is asleep at time t.

Such implicit quantifiers do not go past explicit quantifiers, which is why it did not go all the way to the outside. Note that the logical tautology corresponds precisely to that:

At every time t, there is a person A such that, if A is asleep at time t, then everyone is asleep at time t.

I hope this partly linguistic explanation satisfies your inquiry into the apparent paradox, and yes as you guessed it is a quantifier swap, though not quite involving sleep-states but involving time. On the other hand, be aware that in general it is difficult to set down any rules to translate English into logical form. After all, there are still many people who insist on saying "All that glitters is not gold." instead of "Not all that glitters is gold."...
A: Assume we have a non-empty universe of people, i.e. there exists at least one person. Using a simple form of natural deduction, we have the following proof by contradiction (lines 2 -13) where

*

*P(x) means x is a person

*S(x) means x is sleeping (or drinking?)

(Screen print from my proof checker)



