Skip to content

[WIP] A pedagogical toy for learning natural deduction

Notifications You must be signed in to change notification settings

shonfeder/nd_project

Repository files navigation

ND Project

A pedagogical web toy for learning and playing with Gentzen’s natural deduction.

deduction (n.)

early 15c., deduccioun, “a bringing, a leading;” mid-15c., “action of deducting; a taking away, a number or amount subtracted,” from Old French deduction (Modern French déduction) and directly from Latin deductionem (nominative deductio) “a leading away, an escorting; a diminution,” noun of action from past-participle stem of deducere “lead or bring away or down; derive” (in Medieval Latin, “infer logically”), from de “down” (see de-) + ducere “to lead,” from PIE root *deuk- “to lead.”

Meaning “that which is deducted” is from 1540s. As a term in logic, “derivation as a result from a known principle, an inference, conclusion,” 1520s, from Late Latin use of deductio as a loan-translation of Greek apagoge. Related: Deductional.

Aim

To help people (including myself) understand and internalize basic, constructivistic logic, we attempt to make building proofs as easy as stacking blocks or snapping Legos together.

Approach

The calculus is derived from a naive implementation of natural deduction derive by closely following Gentzen’s original paper.

The interface for constructing proofs is based on ideas that occurred to me while reading Gentzen, playing with proof trees on paper, programming in typed functional languages, and surely from hearing of cool work in the world of PLT (hearing about Hazel must have been an inspiration on the idea of partial proofs with holes). The basic idea is to present derivation trees as a complete interface for constructing proofs.

The tutorial structure is inspired by an iOS game that worked through Euclids elements, which I recall playing back in 2012, but I cannot find. To a lesser extent, by the Dragon Box Algebra games.

Screen Shots

Related work

I didn’t find his work until after I had completed all the designs and the core implementation for this project, but Atkey’s project is very similar.

From a user’s perspective, the only difference is the UI: I use a different syntax for representing the formulas, and I have tried to make the proof tree serve as the sole interface to exploring the proofs (as much as possible). This follows from my hope of creating a game which could serve as a persons very first exposure to formal logic. However, these are really superficial differences.

The more important differences will lie with the implementation. I am an untrained enthusiast, using this project to expand my understanding of natural deduction and hopefully to create a tool that other learners may use to expand their own understanding. Atkey is an academic programming language theory researcher, with theoretical sophistication well beyond my ken: tho I haven’t had time to study his implementation yet, I’d expect it is more principled and illuminating than my own.

Natural Deduction: Google Play app by Laurent Théry

https://play.google.com/store/apps/details?id=org.inria.peanoware&hl=en_US

  • Platform specific (Android)
  • Does not appear to include instructional material or design elements

NaturalDeduction Windows app by Jukka Häkkinen

https://www.microsoft.com/en-us/p/naturaldeduction/9ndb7hz5pfm0?activetab=pivot:overviewtab#

  • Platform specific (Windows)
  • Linear presentation rather than tree based
  • Does not appear to include instructional material or design elements

PANDA

https://sciences.ucf.edu/math/wp-content/uploads/sites/43/2014/10/Tools-for-Teaching-Logic.pdf#page=95

and http://www.phil.cmu.edu/projects/apros/index.php?page=generator

About

[WIP] A pedagogical toy for learning natural deduction

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published