namespace http://cds.omdoc.org/naproche-sad❚
// NaprocheSad is based on the Sad system, which uses the ForTheL language.
See http://nevidal.org/sad.en.html, in particular for the full grammar.
This is a preliminary formalization made live while listening to a talk by Peter Koepke, the main developer.
❚
theory NaprocheSad : ur:?LF =
set : type❙
// sets may be undefined❙
prop : type❙
// binary connectives assume the (negation of the) first argument to show definedness of the second one❙
equality : set ⟶ set ⟶ prop❙
elementof : set ⟶ set ⟶ prop❙
notion : type❙
is_a : set ⟶ notion ⟶ type❘# 1 is a 2❙
Elem : notion ⟶ type❘# Elem 1❙
// unclear ❙
function: set ⟶ set ⟶ notion❘ # 1 → 2 prec 10❙
Dom : {a,b} Elem a → b ⟶ set❙
apply: {a,b} Elem a → b ⟶ set❙
// unclear:❙
// special expressions: no N, every N for notions N❙
// syntax of linguistic predicates:
is, e.g., x is less than y
is a: x is an element of y
does: x converges to y
has: x has unit y❙
// declarations:
* signature extension: function, predicate, notion
* definition: function, predicate, notion
* axiom
* theorem
Every declaration has an internal structure of low-level declarations: assumptions, affirmations, selection (exists-elimination), case distinction (or-elimination), local definition.
Every theorem has exactly one affirmation, which occurs at the end.❙
// declarations are elaborated into untyped first-order logic (signature declarations are implicit)❙
// ontological correctness: all terms are defined (part of verification)❙
// after elaboration, verification generates proof oblibations for ontological correctness and proof steps (one task per low-level declaration)❙
// A proof step may change the proof goal:
* if a proof of A∧B is expected and a proof of A is provided, the proof goal changes to B
* also for proofs of negation-inverted implication
* also for case distinction (old thesis is relativized by disjunction of cases)
* also for user-defined symbols like subset (unclear how the system knows about that)
❙
// combination of internal and external reasoning and the generated proof obligations (back and forth)
* external provers do not see all ZFC axioms, e.g., only relevant instantiations of extensionality
❙
❚