Proposed new syntax
Marko Rauhamaa
marko at pacujo.net
Mon Aug 14 05:46:56 EDT 2017
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
More information about the Python-list
mailing list