The country music theorem

In which we prove that in a universe 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.

We proceed here by boldly asserting these two facts about our universe and proving the consequence.

About the steps

[1] In this proof we prove that exists {x. Country x} without any conditions, based on two facts about our mathematical world.

[2] The second assertion about our imagined universe.

[3] Result of rewriting all of step 1.

[4] Add a universal quantifier.

[5] This is a consequence of step 4, where step 4 matches the pattern forall {x. p x => q x}.

[6] This uses step 2 to conclude that the assumption exists {x. not (Rock x)} is true. It internally simplifies, removing the T =>. The statement exists Country means that the predicate Country is true for someone.

[7] This is the customary way of writing an existential statement, equivalent to step 6.

Try it yourself

You can use this space to practice building your own proof. You might like to start by recreating the proof shown above.