Cool! Someone should make a sleeker interface for it.
Gamifying propositional logic: QED, an interactive textbook
11–20 of 22 posts
Re: Gamifying propositional logic: QED, an interactive textbook
#12See also "The Markable Mark": http://www.markability.net/ It's an introduction to logic using George Spencer-Brown's Laws of Form notation.
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?
Re: Gamifying propositional logic: QED, an interactive textbook
#139.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.)
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.
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.
Re: Gamifying propositional logic: QED, an interactive textbook
#14Great 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
Re: Gamifying propositional logic: QED, an interactive textbook
#159.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.)
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.
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)
Re: Gamifying propositional logic: QED, an interactive textbook
#16What 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?
Re: Gamifying propositional logic: QED, an interactive textbook
#17What 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?
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].
Re: Gamifying propositional logic: QED, an interactive textbook
#18See also "The Markable Mark": http://www.markability.net/ It's an introduction to logic using George Spencer-Brown's Laws of Form notation.
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?
> 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)
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
Re: Gamifying propositional logic: QED, an interactive textbook
#19Earlier quoted context omitted.
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.
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.
Forgot to comment yesterday: thank you! Because of this I got unstuck.
Re: Gamifying propositional logic: QED, an interactive textbook
#20This 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 automat…
PUSH is known as "weakening", one of the structural rules of logic.