Gamifying propositional logic: QED, an interactive textbook

https://terrytao.wordpress.com/2018/07/28/gamifying-propositional-logic-qed-an-interactive-textbook/

by robinhouston • 8 years ago

186 21 8 years ago

terrytao.wordpress.com

chewxy• 8 years ago

There's earlier, non computer game precedence in To Mock a Mockingbird, which I feel is similar in spirit.

Nice find OP

Twisol2• 8 years ago

9.3(d) was a real pain until I thought about how I'd write a function with type `(Either a b, Either a c) -> Either a (b, c)`. Before that, I kept wanting a negation operator.

(EDIT: Looks like some of the exercises are getting shuffled between versions -- 9.3(d) is the one I meant as of v1.2, but that might change over time. At least the type signature is a clue about which one I mean.)

GolDDranks3• 8 years ago

I'm totally stuck. I would write an exhaustive pattern match to implement that function, but I have no clue how to do that in logic, without using negation.

mbrock• 8 years ago

You know A|B and A|C. Prove A|(B&C) by assuming A and separately by assuming B, then use case analysis (by dragging the first conclusion onto the second).

To prove A|(B&C) assuming B, you have to use A|C and yet another (nested) case analysis.

Twisol2• 8 years ago

Right, here's my implementation in Haskell:

    f x y =
      case x of
        Left a -> Left a
        Right b ->
          case y of
            Left a -> Left a
            Right c -> Right (b, c)

Each `case` represents a couple of hypothetical contexts, applying case analysis to the Either (the OR). You're going to have to duplicate some work, since the `Left a` branch appears twice and you're getting the `a` from different places.

kvakil• 8 years ago

Reminds me quite a bit of this, which also includes FOL: http://proofs.openlogicproject.org/

carapace2• 8 years ago

See also "The Markable Mark": http://www.markability.net/

It's an introduction to logic using George Spencer-Brown's Laws of Form notation.

imglorp• 8 years ago

I'm glad you mentioned LoF because I was thinking about it too, from an old article many years ago. I always get tangled up in the philosphy aspects, but what ever happened to it? Is it simply a different and consistent notation, or is there more to it?

carapace2• 8 years ago

Is it simply a different and consistent notation, or is there more to it?

I've found that you can use that question to partition people (who have an opinion on the question) into two major groups: Those who dismiss LoF as just another notation, and those who do find something deeper in it or at least claim to.

Pragmatically it's strictly superior to conventional notation: it's more parsimonious and it admits the rule (due to W. Bricken, I believe):

    A(AB) = A(B)

Which is unknown in other notations, and permits proofs in LoF notation to be extraordinarily concise and elegant (compared to proofs worked in conventional notation.) It also permits a concise implementation of a SAT solver that has the nice property that you don't have to put your problem into normal form.

Recently, George Burnett-Stuart (not Spencer-Brown), the author of the "Markable Mark" site, has worked out how to encode Predicate Calculus http://www.markability.net/prospectus.htm

fizixer• 8 years ago

Last time I spent some time trying to learn mathematical logic I realized that logic texts could benefit from syntax coloring of various languages involved (e.g., metalanguage, object language, logic symbols vs non-logic math symbols, etc, etc).

I'm not sure if this is considered as pedagogically beneficial, and/or feasible without interactivity (on a cursory glance, it doesn't look like Terence Tao has given any importance to coloring in this project).

GolDDranks3• 8 years ago

This is a very nice game/textbook!

I'd love to see some additional features:

- I'm currently at the excercise 9.1, and this far PUSH is always the only operation you can do when dragging from an outer scope to an inner one. Seems pretty fundamental. (To the extent that explicit mentions of "pushing" is not even normally mentioned in textual proofs?) Could this be streamlined somehow, for example applying PUSH automatically just with the drag & drop operation from outer to inner scope?

- Instead of a linear "achievement history", keep records of all produced proofs for each lemma. Highlight the one with the smallest amount of "rules".

- It seems to allow circular proofs by default. Surely this can be detected using a dependency graph?

- Speaking of dependency graphs, I'd love to explore reverse mathematics using this kind of an interactive tool. Maybe add some challenge by counting not only the amount of rules, but amount of axioms/basic rules of inference used, and counting also the size of the whole dependency graph of each proof. Maybe there could be separate record-keeping for different sets of axioms.

taralx• 8 years ago

PUSH is known as "weakening", one of the structural rules of logic.

vanderZwan• 8 years ago

Related: Nicky Case (whose website you really should check out) is currently organizing an Explorables Jam until the nineteenth of August[0][1].

[0] https://explorabl.es/jam/

[1] https://ncase.me/

dukoid• 8 years ago

Shameless plug: I have created an Android game for learning propositional logic that's probably more suitable for younger audiences.

Source code: https://github.com/stefanhaustein/emojic (the page has a playstore link which has screenshots).

Have fun competing with your kids O:)

Bromskloss2• 8 years ago

Cool! Someone should make a sleeker interface for it.

theaeolist• 8 years ago

The interface is good enough. But someone should make a natural deduction version of it!

jackylee0424• 8 years ago

Great works! We are making a VR logic game combining Alice in Wonderland and The Game of Logic. Both were written by Lewis Carroll. Our preview poster: https://sciencevr.com/img/carrollsriddles_s.png

Bromskloss2• 8 years ago

What is the difference between "B [assuming A]" and "A implies B"? Is the distinction something that was introduced for the purposes of this game, or is it made otherwise as well?

pulisse• 8 years ago

Conditional assertion (that is, deducibility of B under the hypothesis A) is distinct from assertion of a conditional (deducibility of the statement that A implies B). This is a fundamental distinction in formal logic. See [1].

[1] https://en.wikipedia.org/wiki/Deduction_theorem

anonlastname• 8 years ago

Should we tell him about Coq? Lol.

Gamifying propositional logic: QED, an interactive textbook

Related Stories