Provides definitions for common HOL types, terms and constants.
This module implements the following propositional constants:
$$ \top_o \quad \bot_o \quad \neg_{o\to o} \quad \lor_{o\to o\to o} \quad \land_{o\to o\to o} \quad \supset_{o\to o\to o} \quad \equiv_{o\to o\to o} $$
Additionally, the following parameterized higher-order constants:
$$ =_{\tau\to\tau\to o} \quad \Pi_{(\tau\to o)\to o} \quad \Sigma_{(\tau\to o)\to o} $$
Summary
Simple Types
Base type for individuals (type $\iota$).
Type for symbols of type $\iota\to\iota$, i.e., endomorphisms/operators on type $\iota$.
Type for symbols of type $(\iota\to\iota)\to\iota\to\iota$, i.e., iterators like Church numerals.
Type for symbols of type $\iota\to\iota\to\iota$, i.e., binary operators on type $\iota$ or Church's encoding of booleans.
Type for symbols of type $\iota\to\iota\to o$, e.g. relations on individuals.
Type for symbols of type $\iota\to o$, e.g. sets of individuals or predicates over individuals.
Type for symbols of type $(\iota\to o)\to\iota$, e.g. the choice operator (Hilbert's $\epsilon$).
Type for symbols of type $(\iota\to o)\to\iota\to o$, e.g. predicate modifiers over type $\iota$.
Type for symbols of type $(\iota\to o)\to(\iota\to o)\to\iota\to o$, e.g. set or predicate operations like intersection.
Type for symbols of type $(\iota\to o)\to(\iota\to o)\to o$, i.e. relations between sets of individuals, e.g. the subset relation.
Type for symbols of type $(\iota\to o)\to o$, e.g. sets of sets of individuals, or predicates over sets of individuals.
Base type for booleans (type $o$). Represents true or false.
Type for symbols of type $o\to o$, e.g. unary connectives like negation.
Type for symbols of type $o\to o\to o$, e.g. binary connectives like conjunction.
Constants
Constant representing the conjunction operator $\lor_{o\to o\to o}$.
Constant representing equality $=_{\tau\to\tau\to o}$ over instances of the given simple type $\tau$.
Constant representing the equivalence operator $\equiv_{o\to o\to o}$.
Constant representing falsity $\bot_o$.
Constant representing the implication operator $\supset_{o\to o\to o}$.
Constant representing the negation operator $\neg_{o\to o}$.
Constant representing the disjunction operator $\land_{o\to o\to o}$.
Constant representing the $\Pi_{(\tau\to o)\to o}$ operator (universal quantification) over the given element type $\tau$.
Constant representing the $\Sigma_{(\tau\to o)\to o}$ operator (existential quantification) over the given element type $\tau$.
Constant representing truth $\top_o$.
Terms
Term representing the conjunction operator $\land_{o\to o\to o}$.
Term representing the equality operator $=^\tau$ over instances of the given type $\tau$.
Term representing the equivalence operator $\equiv_{o\to o\to o}$.
Term representing falsity $\bot_o$.
Term representing the converse of the implication operator $\subset_{o\to o\to o}$. As it is not part of the signature, it is represented as implication with flipped arguments $\lambda P Q. Q \supset P$.
Term representing the implication operator $\supset_{o\to o\to o}$.
Term representing the negated conjunction operator. As it is not part of the signature, it is represented as negated conjunction $\lambda P Q. \neg (P \land Q)$.
Term representing the negation operator $\neg_{o\to o}$.
Term representing the negated disjunction operator. As it is not part of the signature, it is defined as negated disjunction $\lambda P Q. \neg (P \lor Q)$.
Term representing unequality over instances of the given type $\tau$. As it is not part of the signature, it is represented as negated equality $\lambda X_\tau Y_\tau. \neg (X =^\tau Y)$.
Term representing the disjunction operator $\lor_{o\to o\to o}$.
Term representing the $\Pi_{(\tau\to o)\to o}$ operator (universal quantification) over the given element type $\tau$.
Term representing the $\Sigma_{(\tau\to o)\to o}$ operator (existential quantification) over the given element type $\tau$.
Term representing truth $\top_o$.
Term representing the exclusive disjunction operator. As it is no part of the signature, it is represented as negated equivalence $\lambda P Q.\neg(P \equiv Q)$.
Equality
Constructor for Andrews equality on the given type, which defines equality by stating that both arguments share all reflexive relations. Generates an abstraction which can be applied to two arguments.
Constructor for extensional equality on the given function type, which defines equality by equality of the extensions. Generates an abstraction which can be applied to two arguments.
Constructor for Leibniz equality on the given type, which defines equality by stating that both arguments share the same properties. Generates an abstraction which can be applied to two arguments.
Simple Types
@spec type_i() :: ShotDs.Data.Type.t()
Base type for individuals (type $\iota$).
@spec type_ii() :: ShotDs.Data.Type.t()
Type for symbols of type $\iota\to\iota$, i.e., endomorphisms/operators on type $\iota$.
@spec type_ii_ii() :: ShotDs.Data.Type.t()
Type for symbols of type $(\iota\to\iota)\to\iota\to\iota$, i.e., iterators like Church numerals.
@spec type_iii() :: ShotDs.Data.Type.t()
Type for symbols of type $\iota\to\iota\to\iota$, i.e., binary operators on type $\iota$ or Church's encoding of booleans.
@spec type_iio() :: ShotDs.Data.Type.t()
Type for symbols of type $\iota\to\iota\to o$, e.g. relations on individuals.
@spec type_io() :: ShotDs.Data.Type.t()
Type for symbols of type $\iota\to o$, e.g. sets of individuals or predicates over individuals.
@spec type_io_i() :: ShotDs.Data.Type.t()
Type for symbols of type $(\iota\to o)\to\iota$, e.g. the choice operator (Hilbert's $\epsilon$).
@spec type_io_io() :: ShotDs.Data.Type.t()
Type for symbols of type $(\iota\to o)\to\iota\to o$, e.g. predicate modifiers over type $\iota$.
@spec type_io_io_io() :: ShotDs.Data.Type.t()
Type for symbols of type $(\iota\to o)\to(\iota\to o)\to\iota\to o$, e.g. set or predicate operations like intersection.
@spec type_io_io_o() :: ShotDs.Data.Type.t()
Type for symbols of type $(\iota\to o)\to(\iota\to o)\to o$, i.e. relations between sets of individuals, e.g. the subset relation.
@spec type_io_o() :: ShotDs.Data.Type.t()
Type for symbols of type $(\iota\to o)\to o$, e.g. sets of sets of individuals, or predicates over sets of individuals.
@spec type_o() :: ShotDs.Data.Type.t()
Base type for booleans (type $o$). Represents true or false.
@spec type_oo() :: ShotDs.Data.Type.t()
Type for symbols of type $o\to o$, e.g. unary connectives like negation.
@spec type_ooo() :: ShotDs.Data.Type.t()
Type for symbols of type $o\to o\to o$, e.g. binary connectives like conjunction.
Constants
@spec and_const() :: ShotDs.Data.Declaration.const_t()
Constant representing the conjunction operator $\lor_{o\to o\to o}$.
@spec equals_const(ShotDs.Data.Type.t()) :: ShotDs.Data.Declaration.const_t()
Constant representing equality $=_{\tau\to\tau\to o}$ over instances of the given simple type $\tau$.
@spec equivalent_const() :: ShotDs.Data.Declaration.const_t()
Constant representing the equivalence operator $\equiv_{o\to o\to o}$.
@spec false_const() :: ShotDs.Data.Declaration.const_t()
Constant representing falsity $\bot_o$.
@spec implies_const() :: ShotDs.Data.Declaration.const_t()
Constant representing the implication operator $\supset_{o\to o\to o}$.
@spec neg_const() :: ShotDs.Data.Declaration.const_t()
Constant representing the negation operator $\neg_{o\to o}$.
@spec or_const() :: ShotDs.Data.Declaration.const_t()
Constant representing the disjunction operator $\land_{o\to o\to o}$.
@spec pi_const(ShotDs.Data.Type.t()) :: ShotDs.Data.Declaration.const_t()
Constant representing the $\Pi_{(\tau\to o)\to o}$ operator (universal quantification) over the given element type $\tau$.
@spec sigma_const(ShotDs.Data.Type.t()) :: ShotDs.Data.Declaration.const_t()
Constant representing the $\Sigma_{(\tau\to o)\to o}$ operator (existential quantification) over the given element type $\tau$.
@spec true_const() :: ShotDs.Data.Declaration.const_t()
Constant representing truth $\top_o$.
Terms
@spec and_term() :: ShotDs.Data.Term.term_id()
Term representing the conjunction operator $\land_{o\to o\to o}$.
@spec equals_term(ShotDs.Data.Type.t()) :: ShotDs.Data.Term.term_id()
Term representing the equality operator $=^\tau$ over instances of the given type $\tau$.
@spec equivalent_term() :: ShotDs.Data.Term.term_id()
Term representing the equivalence operator $\equiv_{o\to o\to o}$.
@spec false_term() :: ShotDs.Data.Term.term_id()
Term representing falsity $\bot_o$.
Term representing the converse of the implication operator $\subset_{o\to o\to o}$. As it is not part of the signature, it is represented as implication with flipped arguments $\lambda P Q. Q \supset P$.
@spec implies_term() :: ShotDs.Data.Term.term_id()
Term representing the implication operator $\supset_{o\to o\to o}$.
Term representing the negated conjunction operator. As it is not part of the signature, it is represented as negated conjunction $\lambda P Q. \neg (P \land Q)$.
@spec neg_term() :: ShotDs.Data.Term.term_id()
Term representing the negation operator $\neg_{o\to o}$.
Term representing the negated disjunction operator. As it is not part of the signature, it is defined as negated disjunction $\lambda P Q. \neg (P \lor Q)$.
@spec not_equals_term(ShotDs.Data.Type.t()) :: ShotDs.Data.Term.term_id()
Term representing unequality over instances of the given type $\tau$. As it is not part of the signature, it is represented as negated equality $\lambda X_\tau Y_\tau. \neg (X =^\tau Y)$.
@spec or_term() :: ShotDs.Data.Term.term_id()
Term representing the disjunction operator $\lor_{o\to o\to o}$.
@spec pi_term(ShotDs.Data.Type.t()) :: ShotDs.Data.Term.term_id()
Term representing the $\Pi_{(\tau\to o)\to o}$ operator (universal quantification) over the given element type $\tau$.
@spec sigma_term(ShotDs.Data.Type.t()) :: ShotDs.Data.Term.term_id()
Term representing the $\Sigma_{(\tau\to o)\to o}$ operator (existential quantification) over the given element type $\tau$.
@spec true_term() :: ShotDs.Data.Term.term_id()
Term representing truth $\top_o$.
Term representing the exclusive disjunction operator. As it is no part of the signature, it is represented as negated equivalence $\lambda P Q.\neg(P \equiv Q)$.
Equality
@spec andrews_equality(ShotDs.Data.Type.t()) :: ShotDs.Data.Term.term_id()
Constructor for Andrews equality on the given type, which defines equality by stating that both arguments share all reflexive relations. Generates an abstraction which can be applied to two arguments.
$$ \mathcal{A}^\tau := \lambda X_\tau Y_\tau.\text{ }\Pi(\lambda Q_{\tau\to\tau\to o}.\text{ } (\Pi(\lambda Z_\tau.\text{ }Q\text{ }Z\text{ }Z)) \supset Q\text{ }X\text{ }Y) $$
Constructor for extensional equality on the given function type, which defines equality by equality of the extensions. Generates an abstraction which can be applied to two arguments.
$$ \mathcal{E}^{\alpha\to\beta} := \lambda X_{\alpha\to\beta} Y_{\alpha\to\beta}.\text{ }\Pi(\lambda Z_\alpha. X\text{ }Z \doteq^\beta Y\text{ }Z) $$
for some interpretation of the inner equality relation $\doteq^\beta$.
@spec leibniz_equality(ShotDs.Data.Type.t(), :equiv | :imp | :conv_imp) :: ShotDs.Data.Term.term_id()
Constructor for Leibniz equality on the given type, which defines equality by stating that both arguments share the same properties. Generates an abstraction which can be applied to two arguments.
$$ \mathcal{L}^\tau := \lambda X_\tau Y_\tau.\text{ }\Pi(\lambda P_{\tau\to o}.\text{ }P\text{ }X \odot P\text{ }Y) $$
where $\odot \in \{\supset, \subset, \equiv\}$