Definitions of Reflexive Structures.
|
Polymorphic function are defined using ``patterns''.
|
|
Definable functions are are those definable in set theory from the ``PolyMorphic'' functions.
|
|
The Theory refl-defs
First we introduce for these definitions the new theory "refl-defs", a child of gst.
xl-sml
open_theory "gst";
force_new_theory "refl-defs";
force_new_pc "refl-defs";
set_merge_pcs ["gst","refl-defs"];
|
|
|
Instantiate
The following defines how a pattern is instantiated.
A pattern is instantiated using a function which assigns a value to all possible ``wildcards''.
A wildcard is any set which more or less than one member.
xl-holconst instantiate : (GS → GS) → GS → GS
|
∀f s• instantiate f (Unit s) = Imagep (instantiate f) s
∧ ((¬∃t• s = Unit t) ⇒ instantiate f s = f s)
|
A unit set is a set of patterns, each of which is to be instantiated.
Any other set is a wildcard which must be replaced by the value assigned to it.
|
Membership
Using pattern instantiation we define a new membership relation, ∈ gp, which may be thought of as ``polymorphic'' membership.
xl-sml
declare_infix (230,"∈gp");
|
xl-holconst $∈gp : GS → GS → BOOL
|
∀s t• s ∈gp t ⇔ ∃f• s = instantiate f t
|
|
Function Application
Function application is by juxtaposition (i.e. nothing), which however we have to subscript.
So its an infix subscript p.
xl-sml
declare_infix (240,"p");
|
xl-holconst $p : GS → GS → GS
|
∀f x• f p x = εy• (x ↦g y ∈gp f)
|
|
|
Elaborate
This is the analogue for definable functions of the function ``instantiate''.
The idea is to encode as sets the definable functions roughly as described in Chapter V of Kunen's Set Theory, except that you get to use any set as a starting point
(so instead of a countable number of functions you get a collection the same size as WF).
To understand ``elaborate'' you must think of a set as an encoding of a formula in a set theory with a very large term language
(every set in GS is a term).
The formula has free variables, and elaborate, given an assignment of values to free variables will give a truth value for
the encoded formula.
The first two clauses in the above definition concern atomic formulae (membership and equality), the terms of which are evaluated
using "instantiate".
The final clause addresses non-atomic formulae via a generalised scheffer stroke.
|
Membership
Using elaborate we define another new membership relation, ∈ gp, which may be thought of as ``polymorphic'' membership.
xl-sml
declare_infix (230,"∈gd");
|
xl-holconst $∈gd : GS → GS → BOOL
|
∀s t• s ∈gd t ⇔ elaborate (λv• s) t
|
|
|