bucephalus.org

Theoretificationisms

Abstract

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

• the usual boolean junctions ¬, ∧, ∨, →, ↔ [Note, that symbols are short in HTML and we use → for the subjunction as in φ → ψ, but also for the function type, as in f:A→ B.] together with the constant values 0 and 1, or false and true, respectively, and the boolean subvalence ⇒ and equivalence relation ⇔. All well-known standard notions. When we use the disjunction ∨ for an arbitrary number of arguments, we also write disj for this "big" disjunctor; and similarly conj for the conjunction ∧.
• The atom (or attribute) set operator @ returns the atom set @φ that occurs in a theory φ, the subatomic ⊆ and equiatomic relation ≈ [Again due to the shortage in HTML, ⊆ and ≈ may be different in other texts.], and a couple of atomic modificators, we use supRed(φ, S) and infRed(φ, S) for the supremum and infimum reduction of a formula φ onto a new atom set S.

Theories, theory functions and theory relations

For each given atom set Atom we introduce

• Theo(Atom) the theory class of Atom; think of it as the set of propositions or truth tables
• ThFun(Atom) is the theory function class on Atom, comprising all functions of type f:Φ→Ψ, with Φ and Ψ subsets of Atom. Usually in mathematics, function are total function. But here, we also allow theory functions to be partial.
• ThRel(Atom) is the theory relation class on Atom, comprising all binary relations R between two subsets Φ and Ψ of Atom.

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

• stdRel:TheoFun(Atom)→TheoRel(Atom) is the standard way of turning a theory function f:Φ→Ψ into a theory relation R:=stdRel(f), where a pair <φ,ψ> is a member of the relation R if and only if f is defined for φ with f(φ)=ψ.
• stdFun:TheoRel(Atom)→TheoFun(Atom) is the standard way of turning a theory relation R between Φ and Ψ into a theory relation f:=stdFun(R), where f:Φ→Ψ. For each element φ of Φ, f(φ) is the element ψ in Ψ for which <φ,ψ> holds in R. f(φ) remains undefined, if such a ψ doesn't exist or isn't unique.

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

card(Theo(Atom)) < card(TheoFun(Atom)) < card(ThRel(Atom))

Theoretificationisms

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

• fn:Theo(Atom)→ThFun(Atom) is the (theory) functionalizator and
• th:ThRel(Atom)→Theo(Atom) is the (relation) theoretificator

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

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

• stdRel ο fn : Theo(Atom) → ThRel(Atom) the theory relationalizator
• th ο stdRel : TheoFun(Atom) → Theo(Atom) the function theoretificator
• stdRel ο fn ο th : ThRel(Atom) → ThRel(Atom) the relation normalizer

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

• The theism must be theory stable in the sense that th(stdRel(fn(θ)))=θ for every theory θ. This theory stability is possible due to the previous cardinality lemma. It says that we can take a theory, first convert it into a function, then into a relation, and finally back into the original theory, without losing any information.
• The theism might also be atomically stable in the sense that for each theory θ, function f and relation R that can be mutually generated from each other, holds: @θ = @f = @R, where @ denotes the atom set of the given argument (for @f that is the union of all the atoms occurring in arguments and results, for @R that is the union of the atoms in each pair of R).
  But we can also design the theism such that every function f and each relation R has the full atom set @f = @R = Atom, the atom set @θ is just a subset of Atom, and still the theism is theory stable.
• The theism may only be constructed in the context of the given theory algebra. fn and th may only be defined in terms of theory algebraic operations.

An example theoretificationism

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

• mean:Theo(Atom)→Theo(Atom)→Theo(Atom) is the meaning function [2], defined by
  mean(θ)(φ) := infRed(θ → φ, @θ ∇ @φ) for all theories θ and φ.
  (∇ is the opposition or symmetric difference operator on sets, so @θ ∇ @φ is the set of all the atoms that occur either in θ or in φ, but not in both theories.)
• deduct:ThRel(Atom)→Theo(Atom) is the deductive theoretificator, defined by
  deduct(R) := conj { φ → μ | <φ,μ> ∈ R } for every theory relation R.

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

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

• app : Theo(Atom) → Theo(Atom) → Theo(Atom) the applicator, defined by
  app(θ)(φ) := supRed(θb∧ φ, @θ ∇ @φ) for the application of a theory θ on another theory φ
• induct : ThRel(Atom) → Theo(Atom) the inductive theoretificator, defined by
  induct(R) := disj { φ ∧ μ | <φ,μ> ∈ R } for every theory relation R.

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.

Oppomorphisms

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

• f is oppositional on an atom set A in the sense that f(φ)=μ implies the φ and μ have disjunct atom sets and the union of these two sets are A.
• f is a ∨-homomorphism (or ∧-homomorphism).

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.

• First of all, each special oppomorphism class Opp(Atom) defines a set of fixpoints in the theism triangle. The set has the same cardinality than Theo(Atom) and the theory functionator is a bijection from Theo(Atom) onto Opp(Atom).
• The oppositionality overcomes the enforced single direction of a conventional function. For example, if θ has the atoms {p,q} and let f := mean(θ) : Theo(Atom) → Theo(Atom) be the meaning function. f is an oppomorphism and it can be partitioned into several functions that act on equi-atomic domains. We obtain functions of the following types: Theo({p})→Theo({q}), Theo({q})→Theo({p}), Theo(∅)→Theo({p,q}), Theo({p,q})→Theo(∅), etc. Information about an atom can be part of the argument or the result and the choice is free.

Links and footnotes

• [1] http://www.bucephalus.org/text/TheoryAlgebras/TheoryAlgebras.html is an introduction to theory algebras with links to further information
• [2] So-called meaning functions were developed and investigated in The introduction of a logical concept of meaning. The function mean we use here was called the true meaning function there, next to another one called the absolute satisfiable meaning function. The latter does produce results which might be more plausible in general, but its definition is more complicated and it might not be suitable for a theoretificationism at all. Actually, the examples for mean(θ)(φ) in the given table are chosen for their plausibility. A probably less intuitive example on first sight is hot ∧ snow as the meaning of rain ∧ wet.
• [3] A more complicated variation of the deductive theoretificator is given by deduct(R) := conj { infRed(φ → μ, @φ ∇ @μ) | <φ,μ> ∈ R }, but we don't discuss the differences here.

[home] [blog]