Pqf.Environments

• Overview: Environments
• Connecting two kinds of multisets
• A well-founded order and tactic on multi-sets
• Multiset utilities
• Conjunction, disjunction, and implication
• A dependent version of `map`
• Tactics

Pqf.Formulas

• Overview: formulas
• Definitions and notations.
• Countability of the set of formulas
• Weight

Pqf.PropQuantifiers

• Overview: Propositional Quantifiers
• Definition of propositional quantifiers.
• Correctness
  • (i) Variables
  • (ii) Entailment
  • Uniformity
• Pitts' Theorem

Pqf.SequentProps

• Overview: admissible rules in G4ip sequent calculus
• Weakening
• Inversion rules
• Contraction
• Admissibility of LJ's implication left rule
• Correctness of optimizations
• Generalized rules
  • Generalized OrL and its invertibility
  • Generalized AndR
  • Generalized invertibility of AndR
  • Generalized AndL
  • Generalized OrR

Pqf.Sequents

• Overview: Sequent calculus G4ip
• Definition of provability in G4ip
• Tactics