Grace/Kernel/Foundation.g17

Open in Workbench Download source

Imports

None

Declarations

Source

1-- Trusted foundation interface2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67-- This navigable document describes the symbols installed by the selected8-- set-theory foundation before any Grace17 module is elaborated. Its entries9-- are documentation anchors; they add no axioms or definitions.1011module Grace.Kernel.Foundation12namespace Grace.Kernel.Foundation1314-- Primitive set operations1516-- @symbol empty17-- empty : Set18-- The empty-set constant, written ∅ and characterized by set.empty.1920-- @symbol pair21-- pair (x y : Set) : Set22-- The unordered-pair operation, written {x, y} and characterized by set.pairing.2324-- @symbol union25-- union (A : Set) : Set26-- The union operation, characterized by set.union.2728-- @symbol powerset29-- powerset (A : Set) : Set30-- The powerset operation, characterized by set.powerset.3132-- @symbol omega33-- omega : Set34-- The distinguished inductive set supplied by set.infinity; nat.omega35-- identifies its members with the proof-registered set-encoded naturals.3637-- @symbol apply38-- apply (f x : Set) : Set39-- Application for set-theoretic function graphs, characterized by function.apply.4041-- @symbol choose42-- choose (A : Set) : Set43-- The ZFG global-choice operation, characterized by set.globalChoice.4445-- @symbol epsilon046-- epsilon0 : Set47-- The distinguished set of ordinal notations below epsilon-zero.4849-- @symbol epsilon0.less50-- epsilon0.less : Set51-- A checked Separation definition of the membership ordering on epsilon0.5253-- @symbol in54-- in (x A : Set) : Prop55-- Primitive set membership, normally written x ∈ A.5657-- Trusted natural-number datatype5859-- @symbol Nat60-- predicate Nat (n : Set)61-- The trusted inductive predicate for von Neumann natural numbers.6263-- @symbol zero64-- zero : Nat65-- The zero constructor; nat.zero proves that zero is definitionally the empty set.6667-- @symbol succ68-- succ (n : Nat) : Nat69-- The successor constructor; nat.succ relates it to n ∪ {n}.7071-- Foundation-installed transparent definitions7273-- @symbol subset74-- predicate subset (A B : Set)75-- Every member of A is a member of B.7677-- @symbol singleton78-- singleton (x : Set) : Set79-- Defined as pair(x, x) and written {x}.8081-- @symbol union282-- union2 (A B : Set) : Set83-- Binary union, defined as union(pair(A, B)).8485-- @symbol orderedPair86-- orderedPair (x y : Set) : Set87-- The Kuratowski ordered pair {{x}, {x, y}}.8889-- @symbol cons90-- cons (x y : Set) : Set91-- The foundational pair constructor, defined using orderedPair.9293-- @symbol relates94-- predicate relates (r x y : Set)95-- Graph membership: orderedPair(x, y) ∈ r.9697-- @symbol functionOn98-- predicate functionOn (f A B : Set)99-- f is a total, single-valued graph from A to B.100101-- @symbol wellFoundedOn102-- predicate wellFoundedOn (r A : Set)103-- Every nonempty subset of A has an r-minimal member.104105-- @symbol E0Ordinal106-- predicate E0Ordinal (x : Set)107-- Membership in the distinguished epsilon0 notation set.108109-- Foundation axioms and checked bootstrap bridges110111-- @symbol set.empty112-- axiom set.empty113-- No set is a member of empty.114115-- @symbol empty.membership116-- checked bootstrap theorem empty.membership117-- Compatibility name for set.empty.118119-- @symbol set.pairing120-- axiom set.pairing121-- Membership in pair(x, y) is equality to x or equality to y.122123-- @symbol pair.membership124-- checked bootstrap theorem pair.membership125-- Compatibility name for set.pairing.126127-- @symbol set.extensionality128-- axiom set.extensionality129-- Sets with exactly the same members are equal.130131-- @symbol extensionality132-- checked bootstrap theorem extensionality133-- Compatibility name for set.extensionality.134135-- @symbol set.union136-- axiom set.union137-- Characterizes membership in union(A).138139-- @symbol set.powerset140-- axiom set.powerset141-- Characterizes membership in powerset(A).142143-- @symbol powerset.membership144-- checked bootstrap theorem powerset.membership145-- Compatibility name for set.powerset.146147-- @symbol function.apply148-- axiom function.apply149-- Application returns the unique value selected by a function graph.150151-- @symbol set.infinity152-- axiom set.infinity153-- omega contains empty and is closed under von Neumann successor.154155-- @symbol set.foundation156-- axiom set.foundation157-- Every nonempty set has a member disjoint from it.158159-- @symbol foundation160-- checked bootstrap theorem foundation161-- Compatibility name for set.foundation.162163-- @symbol epsilon0.less.membership164-- checked bootstrap theorem epsilon0.less.membership165-- Relates epsilon0.less to membership between epsilon0 notations; derived from166-- its Separation definition and Kuratowski-pair injectivity.167168-- @symbol set.choice169-- axiom set.choice170-- The ZFC/ZFG axiom of choice for sets.171172-- @symbol set.globalChoice173-- axiom set.globalChoice174-- The ZFG global-choice law for choose.175176-- @symbol nat.zero177-- checked bootstrap theorem nat.zero178-- Derives zero = empty from the transparent zero definition.179180-- @symbol nat.succ181-- checked bootstrap theorem nat.succ182-- Derives succ(n) = n ∪ {n} from the transparent successor definition.183184-- @symbol nat.omega185-- checked bootstrap theorem nat.omega186-- Derives Nat(n) iff n ∈ omega from the transparent Nat definition.187188end Grace.Kernel.Foundation189