4.11. Developing theories
Given a theory
T (with types, structures and axioms), a development
of T is a extension of T into a theory T' = T∪(pack of
extra components) which remains «equivalent» to T.
This concept has 3 aspects:
- In which sense is T' «equivalent» to T :
- For any extension T' of T, any model of T'
defines by restriction a unique model of T ;
- Such a T' is qualified a development of T if
conversely, any model of T has a «unique extension» as a model
of T', in a sense we need to specify.
- A list of developments schemes, where each is the data of a pair
(X,Y) of theoretical components (a sub-theory X of a theory
Y) so that any morphism from X to a theory T allows to add to
T a copy of the rest of Y beyond its sub-theory X
identified as its image in T. A list of developments schemes
is sufficient when any legitimate development is producible by a succession
of steps each described by one of these schemes.
- On the formal side: how, for each such scheme, the use of extra components in
works (expressions, proofs...) with T' can be translated
into (usually longer) works with T, and thus be seen as
abbreviations of them.
There are 3 levels of development with their respective schemes:
- A proof only adds one ground formula to the axioms, as this
formula is shown to be a theorem (deduced from some of the previous axioms).
- A definition adds both a new structure symbol and a
new axiom.
- A construction adds altogether a new type, new
structure symbol(s) and new axiom(s).
When inserting theories in the set theoretical framework,
constructions become set theoretical definitions, which is why the
distinction between definitions and constructions is not usually
clarified in the literature.
The Galois connection (Mod,Tru)
For any language L, let Thm be the transformation of ℘(X)
where X is the set of all ground formulas with language L,
giving the set of theorems provable from any set of
formulas taken as axioms. It is a closure.
The use of a theorem as an available axiom for the proofs of the
next theorems, abbreviates a repetition of its proof as a part of
the next proofs (with possible substitutions of variables by terms
to which the theorem is applied).
This closure actually coincides with the one Tru⚬Mod of the Galois connection
(Mod,Tru), where Mod gives the class of models of any set of ground formulas
taken as axioms, while Tru gives the set of true formulas which all given
systems have in common.
While it is not a priori well defined as Mod gives a class,
we can still see it a posteriori definite as follows (for countable L).
The truth relation R ⊂ X×Y between X and
the set Y of all L-structures on ℕ and or any subset of it, defines the Galois
connection (Modℕ,Tru) where Modℕ gives
a set of representatives of all finite or countable models of given axioms.
Then Tru⚬Mod = Tru⚬Modℕ = Thm because
Modℕ ≤ Mod ∴ Thm ≤ Tru⚬Mod ≤ Tru⚬Modℕ ≤ Thm
the last inequality given by the completeness
theorem. So, theorems of A ⊂ X are the ground formulas leaving unchanged Mod A
when added to A.
Schemes of definitions
We have 3 schemes of definitions:
- A formula φ defines a new relation symbol R with
arguments the free variables of φ, with the new axiom
∀(variables), R(variables)⇔φ(variables).
The use of R can be replaced by the use of φ as a
sub-formula of other formulas (replacing the free variables of φ by
the terms used as arguments of R).
- A term t defines an operation symbol S,
with the axiom ∀(variables), S(variables)=t(variables).
This S abbreviates, and can be replaced by, its defining term t.
- Given a formula φ(variables, x), if we have
(∀(variables),∃!x, φ(variables, x)) then it defines
a new operation symbol S, with the new axiom
∀(variables), φ(variables, S(variables)). This
scheme may be split in 2 steps : the definition of a
relation symbol R by φ (by the first scheme); then a reduced
version of the last scheme directly using R instead of a
formula φ. This case was discussed with the uniqueness
quantifiers (2.4).
Extending models by undefined structures
Again by the completeness theorem, if every model of T can be extended as a
model of a T' = (T∪{R,A}) where R is a new
symbol and A is a new (set of) axiom(s), then every ground formula of T
provable in T', is also provable in T.
The converse may be wrong: a theory T may be extensible to a theory T'
unable to prove more of its formulas, but to which not all its models are extensible.
Here are some examples from non-standard
models of arithmetic :
- T is any arithmetic and T' expresses non-standardness by letting
R be a constant (number), and A the axiom schema making it non-standard.
- The other expression of non-standardness by a unary predicate symbol R which may mean the standardness predicate in a non-standard model, as A says the
the induction axiom fails on R: R(0) ∧ (∀x, R(x)
⇒ R(S(x))) ∧ (∃x, ¬R(x))
- T = bare arithmetic; T' = Presburger arithmetic
- T = Presburger arithmetic; T' = full arithmetic (with addition and multiplication)
Definitions extend models
For any theory T with a model E, extensions T' of T
by an additional axiom and/or structure symbol may have different effects:
- If T' only has a new axiom A then E may stay or
not as a model of T', depending whether A is true or false in E;
it always does if A is provable from previous axioms;
- If T' only has a new symbol then E may have several extensions as
models of T' by giving this symbol arbitrary interpretations, except for special cases
- Definitions precisely combine a new symbol R and a new axiom A,
so that any model of T has a unique extension to an interpretation of R
that satisfies A, forming a model of the extended theory
(T∪{R,A}).
The uniqueness of the extension for every E, means that in the doubly extended theory
(T∪{R,A,R1,A1})
where (R1,A1) is a copy of (R,A),
one can prove
∀(variables), R⇔R1
Definitions preserve sets of isomorphisms
For any isomorphism f between models E
and F of T, with respective extensions as models E'
and F' of a theory T' extending T by further structures and axioms,
f may stay or not as an isomorphism between E'
and F', i.e. preserve the interpretation of the new structure(s). It will stay an
isomorphism whenever the additional axiom(s) form a definition, determining the new
structure(s), thus qualified as invariant by isomorphisms. Thus, adding a defined
structure to a theory preserves the sets of isomorphisms between its models.
In particular, any relation defined by an expression with language L⊂R without parameters
is invariant by automorphisms, so is in its closure
Inv(AutL E).
This means that adding it to L preserves AutL E.
As we saw how the switch from models to isomorphisms provides similarities between development levels
from proofs to definitions, we shall now see it also providing similarities from definitions to constructions,
giving sense to how constructions also "essentially preserve" theories.
Rebuilding structures in a concrete category
In a small concrete category, the preserved families of relations are precisely all choices of
unions of trajectories of tuples : each predicate symbol s interpreted as relations preserved through
the category, coincides with the union of those so defined with t ranging over
s through all objects K.
However, the class of relational systems obtained by even giving in this way
"all possible structures" to the objects of an otherwise given concrete category, such as
topology, may still admit more morphisms than
those we started with (this construction behaves like a closure).
A monoid M acting on also acts on En by ∀a∈M,
∀x∈En, a⋅x = ⋅⃗(a) ⚬ x.
So, the set Inv(n) M of n-ary relations
invariant by M,
can be described as made of unions of
trajectories
of tuples x∈En.
For any set of transformations L ⊂ EE, the properties of
Galois connections give
Inv(n) L = Inv(n)
〈L〉{Id,⚬} ⊂ RelE(n)
so that closures of transformation sets by the (End, Inv) connection can be written
EndInv(n)L E =
{g∈EE| ∀x∈En,
∃f∈〈L〉{Id,⚬}, f ⚬ x = g ⚬ x}.
EndInv L E =
{g∈EE| ∀n∈ℕ,∀x∈En,
∃f∈〈L〉{Id,⚬}, f ⚬ x = g ⚬ x}.
Constructions
Diverse construction schemes let new types play the roles of sets defined in set
theory by operations between sets named by previous types:
Each of the following schemes suffices to produce both others through the use of previous ones:
- From a type E, a binary relation R on E and the theorem
making R an equivalence relation (∀E x,y, xRy
⇔ (∀E z,xRz⇔yRz)), we can construct a
type Q in the role of the quotient E/R
with a function symbol q:E→Q, and axioms
- ∀E x,y, q(x)=q(y)
⇔ xRy
- ∀Q x, ∃E y, q(y)=x
Any structure S(u,v,...,k) with an argument k of type Q,
abbreviates a structure S'(u,v,...,x),
where x is of type E, with the axiom
∀u,v,...∀E x,y, xRy ⇒
S'(u,v,...,x)=S'(u,v,...,y)
(thanks to properties of equivalence
relations and quotient)
- A type of unary relations: from 2 types E,F
and a relation R between them, we construct the image Q
of E in ℘(F) by the curried R, by 2 new
structures
- a function q:E→Q
- a relation R' between Q and F,
and axioms
- ∀Q x,∃E y, q(y)=x
- ∀E x,∀F y, q(x)R'
y ⇔xRy
- ∀Q x,y, (∀F z, xR' z ⇔
yR' z) ⇒ x=y.
Or equivalently,∀E x,y,(∀z∈F,
xRz ⇔ yRz)⇒ q(x)=q(y)
The last 2 axioms are together equivalent to
- ∀E x,∀Q y,
(∀F z,
yR' z ⇔xRz) ⇔ q(x) =y.
- A type of structures K of any kind defined by a
fixed expression with parameters, meaning all structures
defined by this expression with all values of parameters. Its structures are:
- A quotient operation, from parameters to K
- An evaluator, interpreting K as a set of structures.
The last one can be obtained by composing constructions of products
(to collapse bound variables as one, and the same for parameters),
a definition and a type of unary relations or functions
(either as particular relations, or by adapting the form of axioms, replacing ⇔ by = ).
A development scheme at each level looks like a component at the
next level
Despite their differences of nature, the 3 levels of development
have remarkable similarities:
- A construction of a type of structures is given by a variable structure,
that is a structure symbol with a selection of variables to play
the role of parameters. Structures in the language are invariant, i.e.
without parameter.
This construction is worthless if the chosen symbol is without parameter
(or behaving as such: independent of parameters) which would give singleton; or
without other variable, as it would give the Boolean type.
- Definitions look like axioms: a definition of a predicate is given by a formula
with free variables; axioms are chosen from ground formulas. Any formula
merely defining a Boolean constant, i.e. with value depending only
on the model and not on variables, such as ground formulas or provable formulas
(in the sense that any free variables are implicitly
bound by ∀), do not play any effective role of structures of the
described system (giving roles to objects). Predicates defined without using the language,
are not structuring either.
- As systems using axioms, proofs are similar to contradictions. A
contradiction
is a kind of proof with no theorem but 0 (False),
which would be a very bad axiom. We might regard contradictions
as a 4th kind of component of theories after types, symbols and axioms; not
only the list of given contradictions should be empty for a theory to be of interest,
but the set of possible contradictions should be empty as well.
How constructions preserve isomorphisms
From any theory T, consider any extension T' =
T∪X∪R∪A
where X is a type, R is a pack of structures and A
is a pack of axioms. The existence of an extension of
a given model of T as a model of T', is
a matter of A being small enough for these X and R.
Its uniquess would not make direct sense as any identical copy would also fit.
But extensions may still be qualified as
«essentially unique»
(being all copies of each other) giving sense to how
constructions preserve models, depending on the set of isomorphisms
between them. For any models E'
and F' of T' respective extensions of models E
and F of T, and any isomorphism f : E
→ F,
- An extension of f as an isomorphism from E' to F' will have
to exist if A suffices to "determine" (make essentially unique) the
extension of the model (interpretation of X and R) in the following
sense: any two extensions are isomorphic (making unique the isomorphism class
of extended models E'), by some isomorphism whose restriction to old types is
the identity.
Therefore in this case, any formulas in T' without free variable in the new type
are provably equivalent to formulas expressed in T, may they be ground formulas
(as they describe the extended model) or with some free variables in old types
(as they may define structures on previous types, which the isomorphisms must preserve).
- The uniqueness of the extension of f is a matter of T' having enough
structures to prevent E' from having any more symmetry (nontrivial
automorphism) than E.
For example if R is empty, if the interpretations X and X' in E' and
F' are equinumerous then any bijection between them extends f
as an isomorphism between E'
and F'; this is non-unique when X has at least 2 elements.
- The extension T' of T is a
construction of X in T, when it ensures both the existence
and uniqueness of an extension of f to X as an isomorphism
from E' to F'. This can be formally verified in the doubly extended
theory T''=
(T∪X∪R∪A∪X'∪R'∪A'),
by defining without parameter, a function from X to X',
and proving that it is a bijection extending IdE as
an isomorphism j
between both models E' , E'' of T'
obtained by restricting a model of T'' to copies
(T∪X∪R∪A)
and (T∪X'∪R'∪A') of T'.
Indeed in this case, any 2 isomorphisms g,h from E' to F'
with the same restriction to E, will be equal because
The automorphism h−1⚬g of E'
extended by IdX' forms an automorphism of the model
(E'∪E'') of T''. As j is invariant, it stays equal
to its image j⚬(h−1⚬g)−1
by this automorphism. Therefore h−1⚬g
= IdE'
, i.e. g=h.
What we can see here strictly preserved by constructions, is the class of isomorphisms as an
abstract category. In particular,
constructions leave unchanged the automorphism groups seen as abstract
groups, providing more types on which they act.
Set theory and foundations
of mathematics
1. First foundations of
mathematics
2. Set theory
3. Algebra 1
4. Arithmetic and first-order foundations
5. Second-order foundations
6. Foundations of Geometry