>Igneous Rocks: An axiomatic theory

Российская Академия Наук

(http://www.RAS.ru)

Государственный геологический музей им. Вернадского

(http://www.SGM.ru)

Igneous Rocks: An axiomatic theory

Исследовательский отчёт

отдел ГИС, руководитель: В.М. Ряховский

петрология: Д.И. Кудрявцев

математика: А.В. Шкотин

Summer 2013

© 2013 Государственный геологический музей им. Вернадского

We report here first version of axiomatic approach to give definitions and find out prime (primitive) terms for petrology, taking as the basic a task of definitions for igneous rocks.

Basically this report is converting maths of https://sites.google.com/site/alex0shkotin/formalnaa-geologia/acmgp-september (1) to axiomatic theory form.

The main difference is an introduction and systematic usage of operators (fuctions of functions) in formulas. From this point of view we investigate this new technique - FOL with operators and numbers. FOL has many sorts for variables, constants and function arguments/results, i.e. is a many-sorted language.

Operator VPC - Volume Percentage Content

We have a sort "sb" (solid body) for "objects" of our theory. So constant of sort "sb", for ex. Sample01, is representing some sample of igneous rock carefully stored in some geo-laboratory.

We consider names of mineral as unary predicate of sort sb. In a sense that predicate is a function with result from a sort of True Values (TV) a signature of predicates for minerals is sb:TV - from value of sb sort to true value.

We declare predicates this way:

Declare melilite sb:TV prime.

To say that melilite is a predicate on sort sb. "prime" means the same as "primitive", i.e. not definable, basic, fundamental...

So we have

<YAFOLL>

Declare melilite sb:TV prime.

Declare kalsilite sb:TV prime.

Declare leucite sb:TV prime.

Declare Ol sb:TV prime. -- for olivine.

Declare Opx sb:TV. -- is not prime and we are looking forward for definition of orthopyroxene class of minerals.

Declare Cpx sb:TV. -- is not prime and we are looking forward for definition of clinopyroxene class of minerals.

Declare hornblende sb:TV prime.

Declare garnet sb:TV prime.

Declare spinel sb:TV prime.

Declare biotite sb:TV prime.

</YAFOLL>

We put text on YAFOLL (Yet Another First Order Logic Language) in XML-tags just for fun.

In this case (of fun) the begining of our theory is

<YAFOLL>

Declare R sort "DIGIT}+({Dot}{DIGIT}+)?". -- an intrinsic sort of real numbers.

Declare TV sort. Declare True:TV constant. Declare False:TV constant.

Declare sb sort.

</YAFOLL>

Sort R is not an "object" sort but sort with values of string being satisfied regular expression. And "intrinsic" just means that we may put this string to sentence without ""-quotes.

Let's declare 5 more mineral groups following [1] part 2.

<YAFOLL>

Declare Q sb:TV. Declare A sb:TV. Declare P sb:TV. Declare F sb:TV. Declare M sb:TV.

</YAFOLL>

All these predicates should have definitions. And for M we'll see it.

Till now we just have another notation for usual FOL things, but let's introduce operator VPC:

Declare VPC (sb:TV):(sb:R).

So this function of functions takes predicate and returns R-value function. Let's

Declare Sample007:sb constant.

to keep information on some rock sample. Then VPC(melilite)(Sample007) means volume percentage content of melilite in this rock sample.

VPC(melilite) is definitely a function - being applyed to any solid it gives VPC of melilite in it (mostly - 0%).

To finish with paragraph 2 of [1] here you are our first axioms:

Axiom A_VPC_biotite_0 (∀x:sb (0% ≤ VPC(biotite)(x))).

Axiom A_VPC_biotite_100 (∀x:sb (VPC(biotite)(x) ≤ 100%)).