Proposed new syntax

[Paul Rubin]

Marko Rauhamaa <marko at pacujo.net> writes:
> For the non-logicians in the audience, an "axiom schema" is a generator
> pattern that produces an infinity of actual axioms. 

For non-logicians this is not worth worrying about: schemas are
basically a technical hack to get around the inability of first-order
logic to quantify over formulas.  Naively most of us think of single
axioms with second-order quantifiers, instead of schemas.

For example, arithmetic induction goes something like:

  FORALL P. [ P(0) and P(n) -> P(n+1) ]

where "FORALL P" means quantifying over all formulas P.  Since in FOL we
can only quantify over numbers and not formulas, we write down a
separate axiom for each possible formula.  Since there are infinitely
many formulas, this is an infinite axiom schema.

Historically (in "naive set theory") we didn't bother with any of this.
We could write { S : S \not\in S } for the set of all sets that are not
members of themselves.  Is S a member of itself ("Russell's paradox")?
Either way leads to contradiction.  So the comprehension axiom schemas
for set theory had to be designed to not allow formulas like that.