Trade
stuff.

Meet
people.

Prove
theorems.

I did not write Metal and Money to make a puzzle game. My goal was (get ready for this) to take the experience of proving theorems in intuitionistic propositional logic and disguise it as a video game.

The activity of playing metal and money is isomorphic to the activity of doing formal proofs intuitionistic propositional logic. I mean this in the technical sense; just as there are rules for deduction, there are rules in Metal and Money, and one could spell out the isomorphism between the two.

I wrote M&M for a logic course I taught at Bentley College in the Spring 2007 term. It served the following three pedagogical purposes.

	Expose the enjoyable puzzle-like nature of formal logic
	Give a flavor to each type of action in formal logic
	Prepare for learning about isomorphisms of fomal systems

If you're hoping this website will spell out the game-to-logic isomorphism, I'm afraid I must disappoint you. Here's why: I began my Spring 2007 course teaching propositional logic and simultaneously having the students play M&M in their spare time. After two weeks I asked them what the game had to do with the course. They told me, and they were almost completely correct. I wouldn't want you to miss out on having the joy of discovery! Furthermore, I want other logic classes to be able to think through the isomorphism as well. (Including my own future classes!)

So play the game and figure out the correspondence to logic for yourself!

Some details:

	Although the logic the game embodies is intuitionistic, the experience is similar enough to that of classical logic that the difference can be swept under the rug if describing the game-to-logic isomorphism informally.
	Later in our course we covered intuitionistic logic, and discussed the Curry-Howard isomorphism. The students were better prepared for this because they had already experienced something that was isomorphic to the activity of doing proofs: playing M&M.