Theorie von Kepler (KEP)

Grundmengen
P   Menge der Planeten inklusive der Sonne
T   Menge der Zeitpunkte

Hilfsbasismengen
\mathbb{N}   die Menge der natürlichen Zahlen
\mathbb{R}   die Menge der reellen Zahlen

Relation
s   Ortsfunktion

Konstanten
p0  die Sonne
k    Keplerkonstante

Definition
\mathbb{R} 3   die Menge der 3-dimensionalen, reellen Vektoren

Typisierungen
θ1   s ∈ \cal FUN ( P × T : \mathbb{R} 3 )
θ2   k ∈ \mathbb{R} +
θ3   p0 ∈ P

Hypothesen
H1   ∀ t ∈ T ( D 2s ( p0, t ) = 0
H2   ∀ t ∈ T ∀ p ∈ P ( D 2s ( p, t ) = – k ⋅ ( s ( p, t ) – s ( p0, t ) ) / | s ( p, t ) – s ( p0, t ) | 3 )
H3   ∀ t ∈ T ∀ p ∈ P ( 1/2 ⋅ | Ds ( p, t ) – Ds ( p0, t ) | 2 – k ⋅ |  s ( p, t ) – s ( p0, t ) | -1 < 0 )

Modelle
x ist ein Modell des Kepler Systems M(KEP) gdw es Mengen P, T, \mathbb{N}, \mathbb{R} 3, s, p0, k gibt, so dass gilt:

x = 〈 P, T, \mathbb{N}, \mathbb{R} 3, s, p0, k 〉

und die Funktion s und die Konstanten k und p0 haben die Typen θ1, …, θ3 und die Hypothesen H1 ( P, T, \mathbb{N}, \mathbb{R} 3, s, p0, k ) und … und H3 ( P, T, \mathbb{N}, \mathbb{R} 3, s, p0, k ) gelten in x.

I(KEP) ist die Menge der intendierten Systeme.

Beispiele
– «unser» Planetensystem (einschließlich «unserer» Sonne)
– der Planet Jupiter mit seinen Monden