InqLog.Prelude

InqLog.SetoidLib

• Extensional Equality
• Morphisms
• Subset Types
• Regarding Autosubst

InqLog.ListLib

• InS
  • nil
  • cons
  • app
  • filter
  • map
  • Reflection via inbS
  • Decidability
  • Miscellaneous
• InS_sublist
  • nil
  • cons
  • filter
  • map
  • Decidablity
• InS_eq
  • nil
  • cons
  • app
  • map
  • Decidability
  • Miscellaneous
• Well-Founded Relations on Lists
  • length_order
  • InS_sublist_order
• mult
  • nil
  • cons
  • app
• some
  • nil
  • cons
  • app
• Finiteness and Decidablity

InqLog.FO.Signatures

InqLog.FO.Syntax

• Terms
  • Decidable Equality
  • Variables and Substitutions
  • Rigidity
• Formulas
  • Decidable Equality
  • Notation
  • Substitutions
  • Defined connectives
  • Classic formulas
  • Free Variables

InqLog.FO.Models

• Inquisitive First-Order Models
• States
  • Substates
  • Equivalence/Equality of States
  • Consistent States
  • Example States
• Restricting a Model to a state
• Variable Assignments

InqLog.FO.Support

• Referent of a term
• Support satisfaction
  • Basic properties
  • Ruling out a formula
  • Support conditions for defined connectives
  • Support for lifted formulas
  • Support for multiple formulas
  • Support for some formulas
• Support validity

InqLog.FO.Truth

• Truth satisfaction
  • Truth satisfaction for basic connectives
  • Basic Properties
  • Truth satisfaction for defined connectives
  • Other Truth satisfaction rules
  • Truth of multiple formulas
  • Truth of some formulas
• Truth-conditional formulas

InqLog.FO.Seq

• Labelled Formulae
• A Sequent Calculus for Bounded Inquisitive First-Order Logic
• Corresponding semantic
  • Semantics of Labelled Formulae
  • satisfaction_mult
  • satisfaction_some
  • satisfaction_conseq
  • Soundness
• More derivable rules

InqLog.FO.SingleUnaryPredicate

• Signature
• Syntax

InqLog.FO.SingleBinaryPredicate

• Signature
• Syntax

InqLog.FO.GenericModels

InqLog.FO.DNE

• Double Negation Elimination
• Schematic Truth Validity of DNE
• Atomic Validity of DNE
• Schematic Validiy of DNE

InqLog.FO.Kuroda

• Validity of Kuroda

InqLog.FO.CD

InqLog.FO.Casari

• The Casari Scheme
• Atomic Support Validity
• Schematic Bounded Support Validity
• Failure of Schematic Support Validity of the Casari Schemes
  • Signature and Syntax
  • The Model
  • Intermezzo: Some classical logic properties
  • Some state properties
  • Support for IES
  • Support for CasariSuc IES
  • Support for CasariImpl IES
  • Support for CasariAnt IES
  • Support for Casari IES