[FOM] METAMATHEMATICAL THEORIES, OBJEKTS AND MORPHISMS

[Stanislav Barov]

Dear FOMB subscribers!
I decided to collect general concepts of metamathematics
and simple relation between them in folowing text - little
tezarus. I hope what future clarification of that concepts
in discutions on FOM will folow (that is continue)
according to this text.
___________

0) Languages
0.1) Terms, individual constant, variable
0.2) Predicates, equality, logic operations (including
modalities), quantifers
[the Theories of Types of a predicate Calculus (Ramified,
Simple,...?) of different orders]

1) Set and element, identity, equivalence, choice of a
element from a set and other kinds of ordering (linear,
partial, function), infinite sets

2) Function and application
2.1) (lambda - abstraction, application, reduction)
[lambda - calculus]
2.2) Substitution (definition) and string (line)
2.2.1) Production, application, derivation (non-determined
sequence applications of productions - tree) [ Post\'s
machine]
2.2.2) Production, application, program (determined
sequence applications of productions - graph) [Markov\'s
machine, Turing\'s machine]
2.2.3) Superposition, application, follower (choice of
following string in well founded set of strings),
recursion, reversion of the function (minimization); a
limit

3) Category, object, morphism

4)MM Theory, model, interpretation, truth, validity,
generality (tautologicity)

...?

I know following semantics:

1+0) Classic Set Theoretic Semantics (Classic and
Intuitionistic Theory of Sets, New Fundation of Quine),
Theory of Categories of Godel, Bernays, Fon Neumann, ...?

2.2.3+0) Theory of Recursive Functions, Arithmetics,
Ordinal Arithmetics, Theory of Degree of insolvabilities
2.2.1+0) Constructive Theories of Types (Typed lambdas -
calculuses, Intuitionistic Theory of Types of Martin-
Lof, ...?)

3+0) Theory of Categories, Graph theory

4+0) Theory of Models, (Kripke\'s theory of truth,
Semantics of Kripke, ...?)

0+2.2) Theory of deduction and axiomatizability, provers

The theory of Cathegory is interpreted in predicate
Calculus of the First order.
The theory of Models has interpretation in theory of
Categories, Any consistent part of the Theory of
Categories has Model, Propositional calculuses (it is
possible with modalities or supperintuitionistic) has
interpretation in models of Kripke, the Models Kripke are
interpreted in theory of Sets. The theory of Recursive
functions is equivalent to lambda - calculus, Model of
Post\'s , Markov\'s and Turing\'s Machines. The theory of
Recursive Functions is equivalent to Arithmetics.
Arithmetics has set theoretic interpretation. The part of
the Theory of Categories has interpretation in theory of
Sets (objects -> sets, morphismes -> homomorphisms) which
one is named as a Category of Sets, the Theory of Sets is
axiomatic interpretation of a predicate Calculus of any
order with its Theory of Types in a predicate Calculus of
the First Order with constants. The graph theory is
interpreted in theory of Categories. Enlarge by marks of
oriented edges and vertex the graph theory contains
interpretation of Turing\'s machines. The theory of Types
of a predicate Calculus is interpreted in theory of Graphs
(or Topology). The graph theory is interpreted in theory
of Sets. The theory of deduction and axiomatizability is
interpreted in theory of Recursive Functions in this case
the predicate Calculus of the First order is  is
interpreted axiomaticaly as Post\'s machine, Constructive
Type Theories has Proposition As Types (and Proof As
Terms) interpretation in Predicate Calculus, ...?

_____________
I didn\'t include concepts of Topology and Analisis
in \"interpretation\" section. May be Sombody have an idea
of it.