# The country music theorem

### What are we proving?

We will prove that in a world where everyone loves either rock music or country music (or both), and there is someone who does not love rock music, there is definitely someone who loves country.

In this proof the variables such as `x`

represent people such as
Garth, or Jimmy, or Dolly.

`Rock x`

means that person x loves rock music.`Country x`

means that person x loves country music.`forall {x. Rock x | Country x}`

means that every person loves rock music or country music (or both!). We read the symbol`forall`

as “for all”.`exists {x. Country x}`

means that some person exists who loves country music. We read the symbol`exists`

as “there exists”.

We start proof in the usual way. You should see a first step that
says `exists {x. Country x} => exists {x. Country x}`

. If not press
the “Clear Work” button. Selecting the `exists {x. Country x}`

on the
**left** side of the formula, several options show up as suggestions.
Choose the one that uses the fact that:

`forall {x. p x => q x} & exists p => exists q`

Wow, what does this mean? It says, “suppose that everything with
property `p`

also has property `q`

, and suppose that something exists
with property `p`

. If that is all true, then there also exists
something with property q.

This step fills in `q`

as `exists {x. Country x}`

.
Soon `p`

will become `{x. not (Rock x)}`

, but not yet.

For the condition `exists p`

, choose specifically
`exists {x. not (Rock x)}`

, one of the two conditions
expected to be in the result of the proof. This choice is
offered in the menu.

Now check the tautology that `not a => b == a | b`

with the plan
to use it in the next step. You will need to enter the formula,
typing `\not a => b == a | b`

.

Finally, select the part of step 3 that says `not (Rock x) => Country x`

. Now the menu should offer “`Rock x | Country x`

using step 4” as
one of the options. Selecting this, you should get the desired
result, and the proof editor should indicate “✓ Proof
complete.”.

#### Alternative

This proof works “backward”, starting with the desired conclusion. It transforms the assumptions into the ones expected, step-by-step removing ones that are not desired. It is also possible to work “forward”, starting with the expected assumptions, e.g.

`((exists {x. (not (Rock x))}) & (forall {x. ((Rock x) | (Country x))})) => ((exists {x. (not (Rock x))}) & (forall {x. ((Rock x) | (Country x))}))`

and transforming the *conclusion* into the desired one. Would
you be able to create a version of this proof that works forward?