WOLFRAM|DEMONSTRATIONS PROJECT

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.)