Page 25 of 800
| Page 25 of 800 | Search internet |
Map theory is an axiomatic theory. Map theory resembles ZFC set theory in that all theorems of classical mathematics can be stated and proved in map theory. The consistency of map theory is provable in ZFC if one assumes that there exists an inaccessible ordinal. The consistency of ZFC is provable in map theory.
Map theory is based on lambda calculus as defined by Church and fulfills Church' original aim of introducing lambda calculus which was to make a foundation of mathematics based on functions and abstraction.
The syntax of map theory includes the syntax of lambda calculus which comprises variables, lambda abstraction 
, and functional application 
which we shall write 
in the following. In addition, map theory has a constant 
which represents truth, a selection construct 
, pure existence 
, a fixed point operator, and parallel 'or'. If one does not include bottom or a fixed point operator, one may define them from lambda abstraction and application. Parallel 'or' has no real uses except that it makes the standard model of the computable part of map theory fully abstract.
The Logiweb programming language comprises a computable subset of map theory. More specifically, it comprises lambda abstraction , functional application , truth , and selection . In addition, for the sake of efficiency, the Logiweb programming language supports quotes 
.
The original purpose of Logiweb was to provide a proof system for map theory because map theory is too different from traditional theories to be well supported by existing proof systems. A large map theory proof (300 pages of math) has been formalized in the Isabelle proof system by Sebastian Skalberg, but during that work it became evident that map theory needs its own proof system. Instead of making a proof system tailored for map theory, however, Logiweb was made general purpose. To prove Logiweb to be general purpose, Peano arithmetic has been implemented in it. Ironically, map theory which obviously fits very well to Logiweb has not been implemented at the time of writing.
An implementation of map theory in Logiweb would contain more axioms than map theory itself. As an example, map theory in Logiweb would contain an extra axiom stating that if a term 
reduces to then 
. As another example, map theory in Logiweb would contain an axiom stating that all value definitions can be used as axioms.
Map theory and Logiweb fit very well to each other because map theory allows to reason about Logiweb programs and Logiweb is well suited for implementing a proof system for map theory.
| Page 25 of 800 | Search logiweb.eu |