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.
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
¬
, ∧
, ∨
, →
, ↔
[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 ∧
.
@
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
.
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))
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
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 relationalizatorth ο stdRel : TheoFun(Atom) → Theo(Atom)
the function theoretificatorstdRel ο fn ο th : ThRel(Atom) → ThRel(Atom)
the relation normalizerFor every reasonable version of a theism, a couple of the following axioms should hold.
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.
θ
, 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
).
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.
fn
and th
may only be defined in terms of theory algebraic operations.
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)
,
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 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 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
.
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.
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)
.
θ
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.
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
.
deduct(R) := conj { infRed(φ → μ, @φ ∇ @μ) | <φ,μ> ∈ R }
,
but we don't discuss the differences here.