//   Comments begin with // and end with the delimiter of the current level.
     
     Comments starting with /T count as content themselves and are, e.g., preserved in the HTML  rendering of a file.
     Therefore, all comments in this file start with /T❚


/T   This file contains a definition of first-order logic in MMT as used in the MMT tutorial given at CICM 2016.❚


/T   A namespace declaration defines the root URI of the following content.❚
namespace http://cds.omdoc.org/examples/tutorial❚

/T   A theory defines a language. It may optionally use a meta-theory, which is given by its URI.❚
theory FOL : http://cds.omdoc.org/urtheories?PLF =

  /T The simplest declaration in an MMT theory introduces a named symbol.
     Every declaration can have multiple attributes following the name.
     Each attribute is introduced by a special keywork:
       the type      - introduced by ':'.
       the definiens - introduced by '='
       the notation  - introduced by '#'
     If multiple attributes are present, they must be ended with the object delimiter. 
  ❙

  /T The following declaration introduces the type of FOL propositions.
     Its type is the object 'type', which is defined by LF.❙
  prop  : type ❙
  
  /T All symbols occuring in an MMT object are cross-linked to their declaration.
     Try hovering or control-clicking on 'type' above❙
  
  /T The following declarations introduce the constructors of propositional logic and their notations.❙
  
  /T ⟶ is used for simple functions. It is part of the notations defined by LF.
     It is right-associative. By double-clicking on ⟶, you can see its arguments.❙
  
  true  : prop                                 ❙
  false : prop                                 ❙
  and   : prop ⟶ prop ⟶ prop  ❘ # 1 ∧ 2 prec 15❙
  or    : prop ⟶ prop ⟶ prop  ❘ # 1 ∨ 2 prec 15❙
  impl  : prop ⟶ prop ⟶ prop  ❘ # 1 ⇒ 2 prec 10❙
  not   : prop ⟶ prop         ❘ # ¬ 1   prec 20❙
  /T Note that multiple attributes (here: type and notation) must be separated by ❘.
     Among other things, that allows using :, =, and # as ordinary characters anywhere else.❙

  /T Notations consist of numbers refering to argument positions and arbitrary Unicode strings defining delimiters.
     Optionally, a notation may end in 'prec NUMBER' to define a precedence. Higher precedences bind stronger.
     For example, '1 ∧ 2 prec 15' makes conjunction an infix operator with precedence 15.
  ❙

  /T As an example for a defined symbol, let us consider the equivalence connective.
     We define it in terms of conjunction and implication.
     The definiens uses [x:prop,y:prop], which is the notation defined for lambda-abstraction in LF.
     The types of the bound variables are infered by MMT - try hovering over them to see the types.
  ❙
  equiv : prop ⟶ prop ⟶ prop  ❘ # 1 ⇔ 2 prec 10❘
        = [x,y] (x ⇒ y) ∧ (y ⇒ x)❙
  /T Here three attributes (type, notation, and definition) are present. The order does not matter.❙
  
  /T Now for the first-order aspects.
     We opt for sorted (also called typed) first-order logic, e.g., there may be multiple sorts that we can quantify over separately.❙
  
  /T The following declarations introduce the LF-type of sorts and the LF type of terms of a given sort.❙
 
  sort   : type❙
  term   : sort ⟶ type ❘# tm 1❙
  
  /T The point of the latter is as follows: If, e.g., 's:sort' is a sort, then 'tm s' is the type of all terms of sort s❙

  /T The following declaration introduces a symbol for sorted equality.❙
  equal : {s: sort} tm s ⟶ tm s ⟶ prop❘# 2 = 3 prec 30 ❘ role Eq ❙
  /T Here {s: sort} is the Pi-binder of LF for dependent function spaces.
       Thus, equal takes a sort as its first argument and then 2 terms of that sort.❙
  /T In the notation for equal, the first argument - the sort - is not mentioned.
     That makes the sort an implicit argument that is infered by MMT.
  ❙
  
  /T The types of the quantifiers use LF's higher-order abstract syntax:
     'tm s ⟶ prop' can be used as the type of proposition with a free variables of type 'tm s'.
     The sort is an implicit argument again, and the type of sort is infered by MMT.
  ❙
  forall : {s} (tm s ⟶ prop) ⟶ prop❘# ∀ 2❙
  exists : {s} (tm s ⟶ prop) ⟶ prop❘# ∃ 2❙
  
  /T Finally, we need to be able to talk about the truth of propositions.
     For that, we introduce a Curry-Howard style judgment: The LF-type '⊢ P' is the type of proofs of the proposition 'P'.
  ❙
  proof : prop ⟶ type❘ # ⊢ 1 prec 0
        ❘ role Judgment❙
  /T It's practical to give ⊢ a very low precedence to avoid brackets later on.❙
  
  /T The 'role Judgment' is an attribute introduced by the LF plugin (which tells MMT to be loaded automatically whenever LF is used).
     By annotation the symbol 'proof' in this way, the plugin can add some LF-specific language support, in particular, it can generate appropriate default notations.
  ❙
 
❚

  
/T   Now we define the proof theory of LF using natural deduction proof rules.
     It is practical to do this in a separate theory that includes the syntax above.
❚        
theory NatDed : http://cds.omdoc.org/urtheories?LF =

  /T 'include THEORY' includes another theory.
     When refering to a theory, we do not actually have to give the absolute URI.
     Below the relative URI '?FOL' is resolved relative to the current namespace and yields http://cds.omdoc.org/examples/tutorial?FOL.
  ❙
  include ?FOL ❙

  /T Some FOL proof rules talk about contradictioins.
     A FOL theory is contradictory if we can derive any formula. That can be captured by the LF type '{a: prop} ⊢ a'. If this type is non-empty, a theory is inconsistent.
     We introduce an abbreviation for it:❙
  contra : type ❘ = {a} ⊢ a❘ # ↯❙

  trueI : ⊢ true❙

  falseE : ⊢ false ⟶ ↯❙
  
  andI  : {A,B} ⊢ A ⟶ ⊢ B ⟶ ⊢ A ∧ B   ❙
  andEl : {A,B} ⊢ A ∧ B ⟶ ⊢ A         ❙
  andEr : {A,B} ⊢ A ∧ B ⟶ ⊢ B         ❙

  orIl  : {A,B} ⊢ A ⟶ ⊢ A ∨ B         ❙
  orIr  : {A,B} ⊢ B ⟶ ⊢ A ∨ B         ❙
  orE   : {A,B,C} ⊢ A ∨ B ⟶ (⊢ A ⟶ ⊢ C) ⟶ (⊢ B ⟶ ⊢ C) ⟶ ⊢ C
                                      ❙

  impI  : {A,B} (⊢ A ⟶ ⊢ B) ⟶ ⊢ A ⇒ B ❙
  impE  : {A,B} ⊢ A ⇒ B ⟶ ⊢ A ⟶ ⊢ B   ❙

  notI  : {A} (⊢ A ⟶ ↯) ⟶ ⊢ ¬ A❘# notI 2❙
  notE  : {A} ⊢ ¬ A ⟶ ⊢ A ⟶ ↯  ❘# notE 2 3❙

  /T Because equivalence is defined, we can derive its rules.
     As usual for Curry-Howard style representations, a derived rule is simply a rule with a definiens.
  ❙

  equivI : {A,B} (⊢ A ⟶ ⊢ B) ⟶ (⊢ B ⟶ ⊢ A) ⟶ ⊢ A ⇔ B  ❘
         = [A,B,p,q] andI (impI [x] p x) (impI [x] q x)  ❙
         
  equivEl : {A,B} ⊢ A ⇔ B ⟶ ⊢ A ⟶ ⊢ B❘
          = [A,B,p,a] impE (andEl p) a ❙
  equivEr : {A,B} ⊢ A ⇔ B ⟶ ⊢ B ⟶ ⊢ A❘
          = [A,B,p,b] impE (andEr p) b ❙
          
  forallI  : {s, A: tm s ⟶ prop} ({x} ⊢ (A x)) ⟶ ⊢ ∀ A ❘ # allI 3❙
  forallE  : {s, A: tm s ⟶ prop} ⊢ (∀ A) ⟶ {x} ⊢ (A x) ❘ # allE 3 4❙

  existsI  : {s, A: tm s ⟶ prop} {c} ⊢ (A c) ⟶ ⊢ ∃ [x] (A x) ❘# exI 3 4❙
  existsE  : {s, A: tm s ⟶ prop, C} ⊢ (∃ A) ⟶ ({x} ⊢ (A x) ⟶ ⊢ C) ⟶ ⊢ C ❘ # exE 4 5❙

  /T The rules for equality consist of the equivalence rules at every sort ...❙
  refl     : {s,x: tm s} ⊢ x = x ❘ # refl 2 ❙
  sym      : {s,x: tm s,y} ⊢ x = y ⟶ ⊢ y = x❘# sym 4❙
  trans    : {s,x: tm s,y,z} ⊢ x = y ⟶ ⊢ y = z ⟶ ⊢ x = z❘ # trans 5 6❙
  /T ... and congruence rules for substituting a subterm x with y in any term T or formula F.❙
  congTerm : {s,t, T: tm s ⟶ tm t}{x,y} ⊢ x = y ⟶ ⊢ (T x) = (T y)❘# congTerm 3 6❙
  congForm : {s,   F: tm s ⟶ prop}{x,y} ⊢ x = y ⟶ ⊢ (F x) ⟶ ⊢ (F y)❘# congForm 2 5 6❙
❚

/T   The rules declared so far only yield intuitionistic first-order logic. To get to classical logic,
we can use the modular approach and extend NatDed by the law of excluded middle: ❚
theory ClassicalSFOL : ur:?LF =
	include ?NatDed ❙
	
	TND : {A} ⊢ A ∨ ¬ A ❘ # TND 1 ❙
❚