The Rules of the Hilbert-Style Proof Builder

Open the applet in this window…

This help is simply a brief summary of the rules. If you need help with the use of the applet go to Help with Applet. If you need help with the formal language go to Help with Language. Note that this text is not an introduction to formal logic. It presupposes some acquaintance with a deductive system.

Modus ponendo ponens (elimination of a conditional) allows you to move from two propositions p, p -> q to a proposition q.
Assertion allows you at any time to assert a proposition of your liking. You may, for example, assert that P & Q is true, and use the calculus to show which consequences your assertion has.
Axiom allows you to add an axiom to your derivation.