October 2009


A theoretificationism shows how a theory defines a function and relation on theories, and the other way round, how these functions and relations induce unique theories. [Although a theory may also be more complex, the point we are going to make here becomes more simple and more powerful, if you think of theories as ordinary propositional formulas or their truth tables.] So in the context of a given theoretificationism, a theory θ is also a function, can be applied to a theory φ and we yield a unique theory μ as a result. But different to most usual functions, we are able to change the role of the function, its arguments and results, because we may as well apply φ to θ or even to φ itself. At the same time, θ is also a binary relation and we can ask if φ and μ are θ-related or not. On the other hand, if f and R are a function and binary relation on theories, respectively, then f and R induce unique theories, which, taken as a function and relation again, behave like the original ones, or at least as much as possible. As a consequence of this approach, the distinction between a set and its elements vanishes as well. There is an order like ⊆ and ∈, but no type hierarchy. A theoretificationism thus provides a universal representation of the three fundamental concepts in modern mathematics, namely sets, functions and relations. Everything is a theory.

Repetition of the theory concept

The notion of a theory algebra is well-introduced by now [1], a theory is just a member of such an algebra. Allthough we keep this terms in the sequel, you may as well replace "theory algebra" with "propositional algebra" and "theory" with "propositional formula" here. That covers the most interesting cases anyway, especially since we have effective implementations for propositional theory algebras by now and that implies and immediate implementation for the concepts we are about to develop below.

Let us recall the main operations in a theory algebra. There are

Theories, theory functions and theory relations

For each given atom set Atom we introduce

There is a common translation of functions into relations and vice versa. We formalize this as follows:

Obviously, for the cardinality of this three sets, the cardinality lemma does hold:

card(Theo(Atom)) < card(TheoFun(Atom)) < card(ThRel(Atom))
One embedding of TheoFun(Atom) into ThRel(Atom) is of course given by stdRel.


A theoretificationism or theism defines, for every atom set Atom, a pair of functions <fn, th>, where

Let us depict the whole situation in a triangular figure:
              Theo(Atom)                                fn : Theo(Atom)  → ThFun(Atom)
             /          \                               th : ThRel(Atom) → Theo(Atom)
            /            \                          stdRel : ThFun(Atom) → ThRel(Atom)
        fn /              \ th                      stdFun : ThRel(Atom) → ThFun(Atom)
          /                \
         /                  \
        /        stdRel      \
   ThFun(Atom)  ---------  ThRel(Atom)

By combining these basic functions (with the ο denoting the composition of functions), we can reach any corner set of the triangle from any given corner, i.e. we have


For every reasonable version of a theism, a couple of the following axioms should hold.

An example theoretificationism

For every given atom set Atom, a theism is given by <trueMean, deduct>, where

Suppose, the atom set is Atom = {cold, hot, rain, snow, wet, windy} and an example "weather" theory θw on it is given by

¬(rain ∧ snow) ∧ (wet ↔ (rain ∨ snow)) ∧ (rain → hot) ∧ (snow → ¬hot),
saying that "it cannot rain and snow, that it is wet iff if it rains or snows, that rain implies hot and snow implies not hot". In this given theism, mean is the theory functionalizator, and the following table shows some argument-result examples of the function mean(θw) of our example weather theory.
φ mean(θ)(φ)
rain ∧ ¬snow hot ∧ wet
rain ∧ snow false ∧ hot ∧ wet, which is equivalent to false
¬(rain ∧ snow) true ∨ hot ∨ wet, which is equivalent to true
cold ∧ wet ∧ snow ¬hot ∧ rain ∧ (cold ∨ ¬cold), which is equivalent to ¬hot ∧ rain
θ true
¬θ false

The first row may e.g. be read as: in our given world, the meaning of "rain and not snow" is "hot and wet".

The theoretificator deduct of this theism is chosen so that the whole is theory stable, i.e. deduct ο stdRel ο mean must be the identity on theories. In our particular case, if we put R := stdRel(mean(θw)), then R is made of all pairs <φ, mean(θ)(φ)>, and deduct(R) is the conjunction of all φ → mean(θ)(φ), which turns out to be the original θw again, as required. [3]

Another example theoretificationism

Another theoretificationism is given by <app, induct>, where

The titel "application" is a natural generalization of an application concept in propositional logic. Take the formula φ = p ↔ (q ∨ ¬r) and a valuator ω, i.e. the boolean-valued functions that assigns 0 or 1 to atoms, e.g. ω = [p:=0, q:=1, r:=0]. The application of φ on ω is then the obvious new formula app(φ)(ω) = 0 ↔ (1 ∨ ¬0) ⇔ 0. More general, let ψ = p ↔ q be a second formula. There are four different valuators for the two atoms p and q and two of them are the unit valuator of ψ, namely [p:=0, q:=0] and [p:=1, q:=1]. Written as literal conjunctions, these two unit valuator turn into two formulas ¬p ∧ ¬q and p ∧ q and ψ itself is the disjunction of these two formulas, i.e. ψ ⇔ (¬p ∧ ¬q) ∨ (p ∧ q). We can therefore define the application of φ on ψ as the disjunction of the applications on the two zero valuators: app(φ)(&psi) := app(φ)([p:=0, q:=0]) ∨ app(φ)([p:=1, q:=1]) = (0 ↔ (0 ∨ ¬r)) ∨ (1 ↔ (1 ∨ ¬r)) ⇔ r ∨ 1.


An oppomorphism is a theory function f : Theo(Atom) → Theo(Atom) such that at least the following two properties are satisfied:

The theory functionalizators mean and app of the two example theoretificationisms are oppomorphisms. In fact, all theoretificationisms we have in mind produce oppomorphisms, because these theory functions show some remarkable proporties.

Links and footnotes

[home] [blog]