Miscellaneous work using gst.
Overview
Miscellaneous proof work using the gst axioms.
Proof of a putative strong infinity axiom for HOL and a speculative axiomatisation for the surreal numbers in HOL.
This section demonstrates the truth of a proposed strong infinity principle.
This section supplies an axiomatisation of surreal numbers independent of set theory.
Introduction
Proof of a putative strong infinity axiom for HOL and a speculative axiomatisation for the surreal numbers in HOL.
Motivation
The idea here is that instead of axiomatising set theory in Higher Order Logic you chose a strong axiom of infinity and then develop one or more set theories by conservative extension.
The Theory gst-misc

xl-sml
open_theory "gst-ax";
force_new_theory "gst-misc";
force_new_pc "gst-misc";
merge_pcs ["xl_cs_∃_conv"] "gst-misc";
set_merge_pcs ["basic_hol", "gst-ax", "gst-misc"];

Strong Infinity in HOL
This section demonstrates the truth of a proposed strong infinity principle.
Strong Infinity using Sets
The purpose of this section is to verify the consistency of a proposed axiom of infinity relative to the axioms of GST in HOL by proving that the axiom is true of the type GS. (It is intended to be asserted of IND). The axiom will then be asserted in a theory higher up the tree, and eventually the axiomatization of GST will be replaced by a conservative extension of that theory.
xl-sml
set_goal([], ⌜∃e: GS → GS → BOOL• ∀p• ∃q• (e p q ∧ (∀x• e x q ⇒ (
ftbr (∃y• e y q ∧ ∀Z• ∃z• e z y ∧ ∀v• e v z ≡ e v x ∧ (Z v))
ftbr ∧ (∀f•(∀u• e u x ⇒ e (f u) q) ⇒ ∃y• e y q ∧ ∀u• e u x ⇒ e (f u) y))))
⌝);
a (∃_tac ⌜$∈g⌝ THEN strip_tac);
a (strip_asm_tac (∀_elim ⌜p⌝ galaxies_∃_thm));
a (∃_tac ⌜g⌝ THEN REPEAT strip_tac);
(* *** Goal "1" *** *)
a (∃_tac ⌜℘g x⌝ THEN REPEAT strip_tac);
(* *** Goal "1.1" *** *)
a (all_fc_tac [get_spec ⌜galaxy⌝]);
(* *** Goal "1.2" *** *)
a (∃_tac ⌜Sep x Z⌝
fttabTHEN rewrite_tac[gst_relext_clauses]
fttabTHEN REPEAT strip_tac);
(* *** Goal "2" *** *)
a (∃_tac ⌜Imagep f x⌝
fttabTHEN rewrite_tac[]
fttabTHEN REPEAT strip_tac);
(* *** Goal "2.1" *** *)
a (lemma_tac ⌜Imagep f x ⊆g g⌝
fttabTHEN1 (rewrite_tac [get_spec ⌜$⊆g⌝, get_spec ⌜Imagep⌝]
fttabfttabTHEN REPEAT strip_tac
fttabfttabTHEN asm_rewrite_tac[]
fttabfttabTHEN REPEAT (asm_fc_tac[])));
a (fc_tac[GImagepC]);
a (list_spec_nth_asm_tac 1 [⌜x⌝, ⌜f⌝]);
(* *** Goal "2.2" *** *)
a (∃_tac ⌜u⌝ THEN asm_rewrite_tac[]);
val strong_infinity_thm = save_pop_thm "strong_infinity_thm";

Strong Infinity using Ordinals
A version of the strong infinity axiom phrased as if about ordinal numbers has also been formulated, and may be found documented but not asserted in the theory "strong_infinity".
Axioms for the Surreal Numbers
This section supplies an axiomatisation of surreal numbers independent of set theory.
Introduction
Primitive Types and Constants

xl-sml
new_theory "surreal";
new_parent "wf_relp";
new_type ("No", 0);
new_const ("∅s", qqco.gifNo⌝);
declare_alias ("∅", ⌜∅s⌝);
new_const ("<s", qqco.gifNo → No → BOOL⌝);
declare_alias ("<", ⌜<s⌝);
new_const ("IC", qqco.gif(No → BOOL) → No → No⌝);
declare_infix (240, "<<");

Definitions

xl-holconst
fttabrank: No → No
fttab∀n• rank n = IC (λx•T) n

xl-holconst
fttab$<<: No → No → BOOL
fttab∀n m• n << m = rank n < rank m
The Zero Axiom

xl-sml
new_axiom (["SZeroAx"], ⌜∀x• rank x = ∅ ≡ x = ∅⌝ );

The Cut Axiom
The following axiom states that, for:
  1. any property p of surreals and
  2. surreal n such that p is downward closed on the surreals of lower rank than n
there exists a surreal number (IC p n) such that:
  • (IC p n) is in between the surreals of rank less than n with the property and those of rank less than n without the property, and
  • where p and q define the same cut on the surreals of rank less than n then (IC p n) is the same surreal as (IC q n).

xl-sml
new_axiom (["SCutAx"],
⌜∀p: No → BOOL; n: No•
fttab(∀x y: No• x << n ∧ y << n ∧ x < y ∧ p y ⇒ p x)
fttab⇒ (∀x: No• x << n ⇒ (p x ≡ x < (IC p n)) ∧ (¬ p x ≡ (IC p n) < x))
fttab∧ (∀q: No → BOOL• (∀x• x << n ⇒ (p x ≡ q x)) ≡ (IC p n) = (IC q n))
⌝);

The Induction Axiom

The following axiom states that for any property p of surreals, if p holds for a surreal n whenever it holds for all the surreals of lower rank than n, then it holds for all surreals.

This is the same as Conway's induction axiom since the union of the two sides of the canonical cuts ("games") on which this axiomatization is based is the set of all numbers of lower rank.


xl-sml
new_axiom (["SIndAx"], ⌜well_founded $<<⌝);

Strong Infinity
This is the ordinal version of my strong infinity for HOL axiom, asserted of the surreals rather than the individuals. I have a fairly low level of confidence in this as yet. I don't know whether it's best to assert it of "<<", or of "<<" restricted to ordinals.
xl-sml
declare_infix (240, "e");
new_axiom (["SInfAx"], ⌜∀p:No• ∃q• (p << q ∧ (∀x• x << q ⇒ (
ftbr (∃y $e• y << q ∧ (∀Z• ∃u• u << y ∧ (∀v• v << x ⇒ (v e u ≡ Z v))))
ftbr ∧ (∀G•(∀u• u << x ⇒ (G u) << q) ⇒ ∃y• y << q ∧ ∀u• u << x ⇒ (G u) << y))))
⌝);


up quick index © RBJ

privacy policy

Created:2003

$Id: gst-miscellany.xml,v 1.3 2006/12/11 12:14:52 rbj01 Exp $

V