pq-System Explorer

x

4

y

2

z

5

testing: axiom?

NO

theorem?

NO

apply rule of inference

----p--q-----

theorems in the theorem bucket at step n = 1:

-p-q--

theorem bucket step

1

display form

identity

compact

meaning

horse meaning

alt meaning

≥ meaning

number of axioms

1

2

The pq-system [1] is a formal system in which theorems can be derived or generated from axioms or from other theorems by using a rule of inference. Use only the upper sliders to adjust the "pq-string" and test whether it is an axiom or a theorem or neither. (Axioms must follow the axiom schema or pattern

"xp-qx-"

, where

x

represents a string of hyphens.) This Demonstration is a power tool for exploring this sample formal system, but the exploration process occurs in your own mind: do not use the lower slider or buttons until you have thoroughly explored the system or you short-circuit the process! (Details below.)