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.