I don't know what I mean, but I know I'm right!

Welcome to Circle-Dot! The object of the game is to construct a circle-dot word made of entirely $\bigcirc$'s and $\bullet$'s. You do not have any words to begin with. On each of your turns you can apply one of the five available rules to your current list of constructed circle-dot words to produce a new word. It may require some study and investigation on your part to come up with an efficient strategy for beating this game at the higher levels of difficulty.

Play Circle-Dot!

Game Components

As described in the Introduction, this game illustrates the basic features of a formal proof system.

The Math Behind the Fun

This game is much more similar to actual formal mathematical proofs than the other games in the Toy Proofs collection. The circle-dot words correspond to mathematical statements. The goal word is the statement we are trying to prove. Each rule is called a rule of inference. The output of a rule is called the conclusion of that rule. We say that the word produced by that rule is deduced or follows from the inputs by that rule of inference. The list of words we construct correspond to the statements in our proof, each of which is justified by a reason. The reason consists of the name of the rule that is used to deduce that line followed by the line numbers of the previously proven statements that are used as inputs to that rule.

Like many actual rules of inference in logic, the circle-dot rules have parameters that must be supplied by the person doing the proof in order to apply the rule. As in ordinary rules of inference these parameters are often statements in that formal proof system, but in general they do not have to be.

Since circle-dot strings clearly have no intrinsic meaning to us, they illustrate that we we can prove statements in a formal system without assigning any meaning to those statements whatsoever. Verifying that a particular statement can be proven in a formal system is a purely mechanical, algorithmic one. In this way we can achieve one of the two goals of a mathematical proof mentioned in the introduction: Objectivity. Whether we can produce a particular circle-dot word or not in the game is not dependent at all on any intuitive meanings we might want to assign to them. Thus even if two people have slightly different intuitive impressions about what a particular circle-dot word means ("I think $\bigcirc\bullet\bigcirc$ means 'eyeglasses'") it will not have any affect on whether or not it can be proven in the game.

In mathematics, we usually do have meaning assigned to our statements. Indeed, assigning meaning to the statements often will be your best guide in figuring out how to prove a given statement. Indeed, one of the main long term goals of our proofs should be to provide an intuitive explanation of why the particular statement is true. However, formal proof systems allow us to prove those statements no matter what meaning we might choose to assign to them... or even if we chose to assign no meaning to the statements at all. This gives us the objectivity we desire and has a secondary benefit that we are free to assign whatever meanings we like to our statements as long as they are practical and useful to us. In this way, we can say with confidence that while we may not know what we mean by our statements... we know that we are right!