Definition:LAST

From ProofWiki
Jump to navigation Jump to search





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.
  • Logical connectives:
    • The and symbol: $\land$
    • The or symbol: $\lor$
    • The negation symbol: $\neg$
  • Quantifier symbols:


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 $\paren {\neg \phi}$ is a formula 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.


Sources