Axiomatic system made just for playing

Question

The formalization of mathematics is based on axioms and theorems logically concluded from them. This way we construct solid structures to model different areas of the human knowledge: different branch of maths, logic, physics, or even biology.

My question is: are you aware of examples of axiomatic systems (including new definitions after some theorems) without any a priori practical application? I mean, something along the lines of the "MU puzzle" of Hofstadter, but not so simple. In other words, an axiomatic system created only for fun, not modelling (at a first glance) anything, but rich enough to be interesting.

With no a priori application I mean that maybe at first it was invented like a logical toy but then somebody realized it modelled something...

Answer 1

Hyperbolic geometry, as an axiomatic system in which the fifth euclidean postulate does not hold, had no applications at first. Gauss did not bother to disseminate his findings. The famous quote of János Bolyai

Out of nothing I have created a strange new universe

tells us that his work did not build on prior sources or relies on external motivations. It was built out of frustration, after more than a thousand years of unsuccessful work to deduce the fifth postulate from the other axioms. For some time, it was not clear if this new geometry was "real" or even non contradictory. It was just a game and many mathematicians saw it as meaningless, and kept arguing that euclidean geometry was the true geometry.

Among the many mathematicians who discussed the nature of hyperbolic geometry was Poincaré. In his investigation of differential equations related to fuchsian functions, he needed to study a group that was precisely the isometry group of the hyperbolic plane. That, he said, is real stuff. Hence his famous quote that a geometry cannot be more true or more real than another one, but only more convenient for a given purpose, in other words, more practical.

Answer 2

I guess you should take a look at the work of John Conway. In particular, his game of life seems to be exactly what you are looking for, a pioneering part of recreational mathematics.

Answer 3

Tarski's high school algebra problem involves an axiomatic that has no application as far as I know. It asks whether there are identities involving addition, multiplication, and exponentiation over the positive integers that cannot be proved using a list of eleven high-school level axioms about these operations.

Substraction is not part of that axiomatic and this is what allowed Alex Wilkie in the eighties to provide an explicit identity that cannot be proven in the axiomatic proposed by Tarski.

Answer 4

I’m not sure if this kind of logic already exists as I don’t have access to the research in this field, but I have an axiomatization of an extension of Intuitionistic Logic. Here is an incomplete axiomatization that I am currently patching up.

Roughly, if the standard Intuitionistic negation holds at a state $s$, then at every state $w$ accessible from $s$, the formula under the scope of the negation does not hold. If the weaker negation holds at $s$, then there is some state $y$ to which $s$ has access, such that the formula under the scope of the weak negation does not hold at $y$. Here I use capital English letters to refer to arbitrary formulas in the extended language; further I use “~” for Intuitionistic negation and “¬” for weak negation. Below I have a possibly incomplete axiomatization for this logic, which contains Modus Ponens as its only inference rule.

(P⟹(Q⟹R))⟹((P⟹Q)⟹(P⟹R))

P⟹(Q⟹P) condition 1

(P⟹∼P)⟹∼P

∼P⟹(P⟹Q)

¬∼P⟹¬¬P condition 1

(¬P⟹P)⟹P

(P⟹Q)⟹(¬Q⟹¬P)

(P⟹R)⟹((P⟹Q)⟹(P⟹(Q∧R)))

The standard axioms for disjunction, quantifiers, and conjunction elimination are also included in this logic, but I left them out for brevity.

Condition 1 is met iff “P” is either

1. an atomic formula that does not have “¬“ as its main operator or

2. an implication or

3. a disjunction or conjunction such that each of the sub-formulas in P meets condition 1.

What makes this logic difficult to axiomatize is that there is no Deduction Theorem for an arbitrary formula. For example, ¬P,R⊢¬P, but ¬P⊬R⟹¬P. This is also the reason our conjunction introduction axiom is not the standard one. Further, any substitution of a formula into a theorem must be proven to be valid. E.g., ⊬~(~(~¬P))⟹~¬P, even though for any condition 1 formula it holds that ⊢~(~(~P))⟹~P. Further, I need to formally prove that condition 1 is sufficient for soundness. (Edit: I added parentheses to the above examples, since the formulas did not post correctly.) Finally, I think the main issue is the semantic definition of disjunction. In this logic ⊨Pv¬P, but the semantic definition for disjunction is that Γ⊨AvB iff Γ⊨A or Γ⊨B for a set of sentences Γ.