Definition:LAST
Jump to navigation
Jump to search
![]() | It has been suggested that this page or section be merged into Definition:Language of Set Theory. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Mergeto}} from the code. |
![]() | This page has been identified as a candidate for refactoring of advanced complexity. Until this has been finished, please leave {{Refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code. |
Definition
LAST stands for LAnguage of Set Theory.
It is a formal system designed for the description of sets.
Formal Language
This is the formal language of LAST:
The Alphabet
The alphabet of LAST is as follows:
The Letters
The letters of LAST come in two varieties:
- Names of sets: $w_0, w_1, w_2, \ldots, w_n, \ldots$
These are used to refer to specific sets.
- Variables for sets: $v_0, v_1, v_2, \ldots, v_n, \ldots$
These are used to refer to arbitrary sets.
The Signs
The signs of LAST are as follows:
- The membership symbol: $\in$, to indicate that one set is an element of another.
- The equality symbol: $=$, to indicate that one set is equal to another.
- Quantifier symbols:
- The universal quantifier: For all: $\forall$
- The existential quantifier: There exists: $\exists$
- Punctuation symbols:
- Parentheses: $($ and $)$.
Formal Grammar
The formal grammar of LAST is as follows:
- Any expression of one of these forms:
- $\paren {v_n = v_m}$
- $\paren {v_n = w_m}$
- $\paren {w_m = v_n}$
- $\paren {w_n = w_m}$
- $\paren {v_n \in v_m}$
- $\paren {v_n \in w_m}$
- $\paren {w_m \in v_n}$
- $\paren {w_n \in w_m}$
is a formula of LAST.
- If $\phi, \psi$ are formulas of LAST, then:
- $\paren {\phi \land \psi}$
- $\paren {\phi \lor \psi}$
are formulas of LAST.
- If $\phi$ is a formula of LAST, then expressions of the form:
- $\paren {\forall v_n \phi}$
- $\paren {\exists v_n \phi}$
are formulas of LAST.
- No expressions that can not be constructed from the above rules are formulas of LAST.