Proposed new syntax

[Marko Rauhamaa]

Jussi Piitulainen <jussi.piitulainen at helsinki.fi>:

> However, I did find there a nice name for this axiom schema based on
> yet another of its many names: "erotteluskeema" ("schema of
> separation"). <https://fi.wikipedia.org/wiki/Joukko-oppi> I like that.

For the non-logicians in the audience, an "axiom schema" is a generator
pattern that produces an infinity of actual axioms. For example, the
"axiom [schema] of separation" states:

    ∀x ∈ variables:
        ∀y ∈ variables:
            ∀ϕ ∈ first-order formulas:
                ∀z (z ∈ { x ∈ y | ϕ } ↔ (z ∈ y ∧ ϕ[x/z]))

where ϕ[x/z] refers to a formula obtained from ϕ by replacing every free
occurrence of x with z.


Marko