logic: justification
system: tableau
name: J₀
description: |
    This is a system for the justification logic J0 (and Jcs, when formulas 
    from the constant specification are added.
    
    It is decidable through the addition of the principle of bivalence, as 
    suggested by Finger (2010) and Ghari (2016). This particular system is 
    based on the one described by Ghari, although the rule CSr was not
    present in the original; it emulates closure of the branch upon 
    encountering [F] φ for some φ ∊ CS.
rules:
    - name: "Te"
      consume: ["[T] T:A"]
      produce:
            - ["[T, e] T:A"]

    - name: "Fe"
      consume: ["[F] T:A"]
      produce:
          - ["[F, e] T:A"]

    - name: "F→"
      consume: ["[F] A → B"]
      produce: 
          - ["[T] A", "[F] B"]

    - name: "T→"
      consume: ["[T] A -> B"]
      produce:
          - ["[F] A"]
          - ["[T] B"]

    - name: "F+"
      consume: ["[F, e] T+S:A"]
      produce:
          - ["[F, e] T:A", "[F, e] S:A"]

    - name: "T·"
      consume: ["[T, e] S:(A → B)", "[T, e] T:A"]
      produce:
          - ["[T, e] (S * T) : B"]
      restrict:
          and:
              - match: "A → B"
                with: [subterms, formulas]
                in:
                    union: [root, assumptions]
              - match: "S · T"
                with: subterms
                in: root
    - name: "CSr"
      consume: []
      produce:
          - ["[T] A"]
      generate:
          match: "A"
          with: all
          in: assumptions
    - name: "PBe"
      consume: []
      produce:
          - ["[T, e] T:A"]
          - ["[F, e] T:A"]
      generate:
          and:
              - match: "A"
                with: [subterms, formulas]
                in: 
                    union: [root, assumptions]
              - match: "T"
                with: [subterms, justifications]
                in: root

    - name: "PBf"
      consume: []
      produce:
          - ["[T] A"]
          - ["[F] A"]
      generate:
          match: "A"
          with: [subterms, formulas]
          in: 
              union: [root, assumptions]