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