Definitions of Reflexive Structures.
Overview
This document defines encodings of functions into well-founded sets.
Polymorphic function are defined using ``patterns''.
Definable functions are are those definable in set theory from the ``PolyMorphic'' functions.
Introduction
Goals
1. Goals
3.

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"];

PolyMorphic Functions
Polymorphic function are defined using ``patterns''.
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•
fttabinstantiate f (Unit s) = Imagep (instantiate f) s

fttab((¬∃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)
Definable Functions
Definable functions are are those definable in set theory from the ``PolyMorphic'' functions.
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.


xl-holconst
elaborate : (GS → GS) → GS → BOOL
∀f s t v•
fttabelaborate f (∅gg (s ↦g t)) ⇔ instantiate f s = instantiate f t

fttabelaborate f ((Unit ∅g) ↦g (s ↦g t)) ⇔ instantiate f s ∈g instantiate f t

fttabelaborate f (Pairg (Unit ∅g) ∅gg (v ↦g (s ↦g t)))
fttab⇔ ¬ ∀x•
fttabfttablet f' y = if y = v then x else f y
fttabfttabin (elaborate f' s ∧ elaborate f' t)
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

up quick index © RBJ

privacy policy

Created:

$Id: refl-defns.xml,v 1.2 2012/08/11 21:01:52 rbj Exp $

V