In mathematics, for any true-or-false propositions *A* and *B*, we can infer that *A* implies *B* knowing *only* that *A* is false. It’s only logical. Honest! See material implication.

Last updated: 2019-04-14

Here we consider simple variations of the famous Barber Paradox (3 versions) and demonstrate the need for set theory in a very simple and direct way. We will prove using set theory that the fabled village barber can actually shave those and only those men in that village who do not shave themselves *if and only if* that barber is *not* a man in the village. This would seem to be impossible to prove using only first-order predicate logic.

Last updated Feb. 10, 2017

Click for full text

Last updated: Nov. 18, 2015

Here we turn Hilbert’s Hotel on its head. Instead of frantically

shuffling infinitely many guests for one room to the next in

Hilbert’s mythical infinite hotel, we start with a leisurely walk

through an ordinary and quite finite village.

Click for full text

Last updated: Oct. 12, 2015

*The Drinker’s Theorem: Consider the set of all drinkers in the world, and the set of all people in a given pub. Then there exists a person who, if he or she is drinking, then everyone in that pub is drinking. *

It doesn’t matter how many people are there. Or how many are drinking. Or how few. No one needs to be taking their cues from some “lead drinker,” but in every pub, in every town and village, it just happens! How is this possible?

There are several possible approaches to this problem. Here, we will turn to British philosopher and mathematician, Bertrand Russell (1872 – 1970). His famous Paradox is the key.

Click for full text

Last updated: Nov. 1, 2016

The Definition of the set of natural numbers

is given by nothing more or less than

Peano’s Axioms.

Click for full text

The Cantor-Bernstein-Schroeder Theorem (CBST), is one of the most important and widely applied results in set theory:

If set

Xcan be mapped one-to-one into setY(an injection), and setYcan be mapped one-to-one into set X (an injection), then X can be mapped one-to-oneonto Y(a bijection).

Though seemingly self-evident, some proofs of CBST can make your head spin! Every line of my machine-verified, formal proof (updated 2014-09-11) is justified by one of a very limited list of simple axioms and rules of inference (indicated in a grey font at the end of each line).

Such complete rigour does come at a price, however. While it is completely free of any of the sort of the hand-waving that plagues many informal versions of this proof, like most formal proofs of any complexity, it is *very* long. My commentary (indicated by a blue font) is inserted throughout using *DC Proof.* I believe this makes my proof considerably more readable than machine-generated formal proofs in other systems.

This proof was written to demonstrate the capabilities of the *DC Proof* system. Though designed for ease of use by the complete beginner, *DC Proof* is quite capable of some mathematical heavy lifting.