-- Trusted foundation interface
-- Part of the Grace17 proof assistant for mathematics based on set theory.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

-- This navigable document describes the symbols installed by the selected
-- set-theory foundation before any Grace17 module is elaborated. Its entries
-- are documentation anchors; they add no axioms or definitions.

module Grace.Kernel.Foundation
namespace Grace.Kernel.Foundation

-- Primitive set operations

-- @symbol empty
-- empty : Set
-- The empty-set constant, written ∅ and characterized by set.empty.

-- @symbol pair
-- pair (x y : Set) : Set
-- The unordered-pair operation, written {x, y} and characterized by set.pairing.

-- @symbol union
-- union (A : Set) : Set
-- The union operation, characterized by set.union.

-- @symbol powerset
-- powerset (A : Set) : Set
-- The powerset operation, characterized by set.powerset.

-- @symbol omega
-- omega : Set
-- The distinguished inductive set supplied by set.infinity; nat.omega
-- identifies its members with the proof-registered set-encoded naturals.

-- @symbol apply
-- apply (f x : Set) : Set
-- Application for set-theoretic function graphs, characterized by function.apply.

-- @symbol choose
-- choose (A : Set) : Set
-- The ZFG global-choice operation, characterized by set.globalChoice.

-- @symbol epsilon0
-- epsilon0 : Set
-- The distinguished set of ordinal notations below epsilon-zero.

-- @symbol epsilon0.less
-- epsilon0.less : Set
-- A checked Separation definition of the membership ordering on epsilon0.

-- @symbol in
-- in (x A : Set) : Prop
-- Primitive set membership, normally written x ∈ A.

-- Trusted natural-number datatype

-- @symbol Nat
-- predicate Nat (n : Set)
-- The trusted inductive predicate for von Neumann natural numbers.

-- @symbol zero
-- zero : Nat
-- The zero constructor; nat.zero proves that zero is definitionally the empty set.

-- @symbol succ
-- succ (n : Nat) : Nat
-- The successor constructor; nat.succ relates it to n ∪ {n}.

-- Foundation-installed transparent definitions

-- @symbol subset
-- predicate subset (A B : Set)
-- Every member of A is a member of B.

-- @symbol singleton
-- singleton (x : Set) : Set
-- Defined as pair(x, x) and written {x}.

-- @symbol union2
-- union2 (A B : Set) : Set
-- Binary union, defined as union(pair(A, B)).

-- @symbol orderedPair
-- orderedPair (x y : Set) : Set
-- The Kuratowski ordered pair {{x}, {x, y}}.

-- @symbol cons
-- cons (x y : Set) : Set
-- The foundational pair constructor, defined using orderedPair.

-- @symbol relates
-- predicate relates (r x y : Set)
-- Graph membership: orderedPair(x, y) ∈ r.

-- @symbol functionOn
-- predicate functionOn (f A B : Set)
-- f is a total, single-valued graph from A to B.

-- @symbol wellFoundedOn
-- predicate wellFoundedOn (r A : Set)
-- Every nonempty subset of A has an r-minimal member.

-- @symbol E0Ordinal
-- predicate E0Ordinal (x : Set)
-- Membership in the distinguished epsilon0 notation set.

-- Foundation axioms and checked bootstrap bridges

-- @symbol set.empty
-- axiom set.empty
-- No set is a member of empty.

-- @symbol empty.membership
-- checked bootstrap theorem empty.membership
-- Compatibility name for set.empty.

-- @symbol set.pairing
-- axiom set.pairing
-- Membership in pair(x, y) is equality to x or equality to y.

-- @symbol pair.membership
-- checked bootstrap theorem pair.membership
-- Compatibility name for set.pairing.

-- @symbol set.extensionality
-- axiom set.extensionality
-- Sets with exactly the same members are equal.

-- @symbol extensionality
-- checked bootstrap theorem extensionality
-- Compatibility name for set.extensionality.

-- @symbol set.union
-- axiom set.union
-- Characterizes membership in union(A).

-- @symbol set.powerset
-- axiom set.powerset
-- Characterizes membership in powerset(A).

-- @symbol powerset.membership
-- checked bootstrap theorem powerset.membership
-- Compatibility name for set.powerset.

-- @symbol function.apply
-- axiom function.apply
-- Application returns the unique value selected by a function graph.

-- @symbol set.infinity
-- axiom set.infinity
-- omega contains empty and is closed under von Neumann successor.

-- @symbol set.foundation
-- axiom set.foundation
-- Every nonempty set has a member disjoint from it.

-- @symbol foundation
-- checked bootstrap theorem foundation
-- Compatibility name for set.foundation.

-- @symbol epsilon0.less.membership
-- checked bootstrap theorem epsilon0.less.membership
-- Relates epsilon0.less to membership between epsilon0 notations; derived from
-- its Separation definition and Kuratowski-pair injectivity.

-- @symbol set.choice
-- axiom set.choice
-- The ZFC/ZFG axiom of choice for sets.

-- @symbol set.globalChoice
-- axiom set.globalChoice
-- The ZFG global-choice law for choose.

-- @symbol nat.zero
-- checked bootstrap theorem nat.zero
-- Derives zero = empty from the transparent zero definition.

-- @symbol nat.succ
-- checked bootstrap theorem nat.succ
-- Derives succ(n) = n ∪ {n} from the transparent successor definition.

-- @symbol nat.omega
-- checked bootstrap theorem nat.omega
-- Derives Nat(n) iff n ∈ omega from the transparent Nat definition.

end Grace.Kernel.Foundation