Home » forums » LtU Forum

New simple proof system

I took basic logic and made it as familiar and easy to learn as possible. Proofs look just like proofs in elementary school algebra--a series of steps where each step has a formula on the left and a justification on the right. Formulas are manipulated using rewrite rules (commutativity, etc.) rather than the typical deduction rules. This isn't any sort of limitation. It can implement both intuitionistic and classical logic using only rewrite rules (currently it uses intuitionistic).

I wrote up the result as a sort of game. The first real proof is problem 8, which is just a few steps. Some of the later problems are ferociously difficult (but possible)--no one I've shown it to has gotten close to solving them, so if anyone manages to solve problem 25, 35, 36, or 37, please let me know.

https://sftm.schlussweisen.com

It's completely free.

By Edwin Zacharias at 2017-08-13 12:25 | LtU Forum | previous forum topic | next forum topic | other blogs | 3173 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

A deep inference Hilbert proof system

I played a bit with your interface. It resembles deep inference in that there is no explicit context, you act in depth under a tree of conjunctions. It is a Hilbert proof system in the sense that you emphasize a laundry list of tautologies as the mechanism to use to make the proof progress, instead of the more structural presentations of Gentzen-style proof systems (natural deduction or sequent calculus), where logical rules belong each logical connective.

The interface is well-done, but I am not sure whether the approach to the logic is that convenient. It is relatively well-known that Hilbert proof system are tedious to use to write proofs (the fact no one besides you was able to prove associativity of disjunction indicates that it is difficult to write proofs; it is trivial in the sequent calculus).
In logic, they are also less used because the de-emphasis of proof structure (all proofs are list of steps, which does not tell you much) makes meta-theoretical results (cut elimination, consistency etc.) more difficult to establish.

To compare with some other logics-as-serious-games tools, proving associativity of disjunction is tedious but easy (because of the inconvenience of drawing graphs with a mouse) with The Incredible proof machine (this is the sixth exercise in the third session), and very easy in logitext.

(There is a list of other such tools at the end of the Incredible machine blog post; I would distinguish the "serious game" ones that really show the logic and formulas (potentially using extra graphical devices for extra feedback), and the just "game" ones that hide them behind colors, shapes, matching rules, etc.).

By gasche at Sun, 2017-08-13 17:02 | login or register to post comments

Re: A deep inference Hilbert proof system

Thanks for checking it out. I'm not quite sure what you mean by explicit context. There is a lexical context which is introduced in problem 5, and its use removes much of the tedium associated with Hilbert-style systems.

The difficulty level is pedagogical and somewhat artificial. After solving a difficult problem, a rule is usually given which would make solving that problem trivial. With a full set of rules, proofs are pretty much the same as sequent calculus.

In comparison with the other systems you mention, I suppose my system is an exploration of the Heyting algebra view of logic as opposed to something like viewing logic as a wiring diagram. The chief benefit of this is the basic notion of applying algebraic rules such as commutativity or associativity should already be familiar to most people.

By Edwin Zacharias at Sun, 2017-08-13 19:57 | login or register to post comments

Love it!

Neat. Hope I don't get addicted.

By marco at Sun, 2017-08-13 22:29 | login or register to post comments