Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
chiron [2014/03/27 21:35] nikolaj |
chiron [2014/09/15 20:10] nikolaj |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ===== Chiron ===== | ===== Chiron ===== | ||
| ==== Meta ==== | ==== Meta ==== | ||
| + | >todo: Make a syntax entry for formal language, and join it with Chiron, Haskell, as well as logical theories. | ||
| + | |||
| {{ chiron-moreau.jpg?X300}} | {{ chiron-moreau.jpg?X300}} | ||
| Line 12: | Line 14: | ||
| == Atomic expressions == | == Atomic expressions == | ||
| We want to work with an unending alphabet and providing it is, apart from a finite part, a task of the meta logic. So reasoning with Chiron always starts out with the specification of //atomic expressions//: | We want to work with an unending alphabet and providing it is, apart from a finite part, a task of the meta logic. So reasoning with Chiron always starts out with the specification of //atomic expressions//: | ||
| - | - A countably infinite collection of //symbols//, denoted by $\mathcal S$, which includes certain default //key words//. (The key words are listed in the Discussion section. Examples are 'type', 'term', 'formula', 'if', 'op', 'op-app' and 'fun-app'.) | + | - A countably infinite collection of //symbols//, denoted by $\mathcal S$, which includes certain default //key words//. (The key words are listed in the last section of this entry. Examples are 'type', 'term', 'formula', 'if', 'op', 'op-app' and 'fun-app'.) |
| - A countable collection of //operator names//, denoted by $\mathcal O$, which includes certain default //built-in operator names//. The operator names must be assigned a //signatur//. That's a sequences of the key words 'type', 'term' and 'formula'. (The operator names are similar to names of typed functions, and the corresponding operators are formalized using the symbols. Examples of the built-in operator names are 'in', 'type-equal' and 'not', but also 'set' and 'class'.) | - A countable collection of //operator names//, denoted by $\mathcal O$, which includes certain default //built-in operator names//. The operator names must be assigned a //signatur//. That's a sequences of the key words 'type', 'term' and 'formula'. (The operator names are similar to names of typed functions, and the corresponding operators are formalized using the symbols. Examples of the built-in operator names are 'in', 'type-equal' and 'not', but also 'set' and 'class'.) | ||
| Line 59: | Line 61: | ||
| Finally, some terminology: We say that assigning a sequence to operator names provides us with a //language// $L$ and a language together with a set of axioms $\Gamma$ is a //theory in Chiron//. Moreover, a bijective mapping from $\mathcal S\cup\mathcal O$ into the sets of some set theory with ordered pair induces a representation of expressions of Chiron. The representation of an expression is called //construction//. | Finally, some terminology: We say that assigning a sequence to operator names provides us with a //language// $L$ and a language together with a set of axioms $\Gamma$ is a //theory in Chiron//. Moreover, a bijective mapping from $\mathcal S\cup\mathcal O$ into the sets of some set theory with ordered pair induces a representation of expressions of Chiron. The representation of an expression is called //construction//. | ||
| - | ==== Discussion ==== | + | Lastly, we list the key words and operator names. |
| === Key words === | === Key words === | ||
| Main key words: | Main key words: | ||
