# `ShotDs.Hol.Definitions`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.0.0/lib/shot_ds/hol/definitions.ex#L1)

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}$$

# `type_i`

```elixir
@spec type_i() :: ShotDs.Data.Type.t()
```

Base type for individuals (type $\iota$).

# `type_ii`

```elixir
@spec type_ii() :: ShotDs.Data.Type.t()
```

Type for symbols of type $\iota\to\iota$, i.e., endomorphisms/operators on
type $\iota$.

# `type_ii_ii`

```elixir
@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.

# `type_iii`

```elixir
@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.

# `type_iio`

```elixir
@spec type_iio() :: ShotDs.Data.Type.t()
```

Type for symbols of type $\iota\to\iota\to o$, e.g. relations on individuals.

# `type_io`

```elixir
@spec type_io() :: ShotDs.Data.Type.t()
```

Type for symbols of type $\iota\to o$, e.g. sets of individuals or predicates
over individuals.

# `type_io_i`

```elixir
@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$).

# `type_io_io`

```elixir
@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$.

# `type_io_io_io`

```elixir
@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.

# `type_io_io_o`

```elixir
@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.

# `type_io_o`

```elixir
@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.

# `type_o`

```elixir
@spec type_o() :: ShotDs.Data.Type.t()
```

Base type for booleans (type $o$). Represents true or false.

# `type_oo`

```elixir
@spec type_oo() :: ShotDs.Data.Type.t()
```

Type for symbols of type $o\to o$, e.g. unary connectives like negation.

# `type_ooo`

```elixir
@spec type_ooo() :: ShotDs.Data.Type.t()
```

Type for symbols of type $o\to o\to o$, e.g. binary connectives like
conjunction.

# `and_const`

```elixir
@spec and_const() :: ShotDs.Data.Declaration.const_t()
```

Constant representing the conjunction operator $\lor_{o\to o\to o}$.

# `equals_const`

```elixir
@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$.

# `equivalent_const`

```elixir
@spec equivalent_const() :: ShotDs.Data.Declaration.const_t()
```

Constant representing the equivalence operator $\equiv_{o\to o\to o}$.

# `false_const`

```elixir
@spec false_const() :: ShotDs.Data.Declaration.const_t()
```

Constant representing falsity $\bot_o$.

# `implies_const`

```elixir
@spec implies_const() :: ShotDs.Data.Declaration.const_t()
```

Constant representing the implication operator $\supset_{o\to o\to o}$.

# `neg_const`

```elixir
@spec neg_const() :: ShotDs.Data.Declaration.const_t()
```

Constant representing the negation operator $\neg_{o\to o}$.

# `or_const`

```elixir
@spec or_const() :: ShotDs.Data.Declaration.const_t()
```

Constant representing the disjunction operator $\land_{o\to o\to o}$.

# `pi_const`

```elixir
@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$.

# `sigma_const`

```elixir
@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$.

# `true_const`

```elixir
@spec true_const() :: ShotDs.Data.Declaration.const_t()
```

Constant representing truth $\top_o$.

# `and_term`

```elixir
@spec and_term() :: ShotDs.Data.Term.term_id()
```

Term representing the conjunction operator $\land_{o\to o\to o}$.

# `equals_term`

```elixir
@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$.

# `equivalent_term`

```elixir
@spec equivalent_term() :: ShotDs.Data.Term.term_id()
```

Term representing the equivalence operator $\equiv_{o\to o\to o}$.

# `false_term`

```elixir
@spec false_term() :: ShotDs.Data.Term.term_id()
```

Term representing falsity $\bot_o$.

# `implied_by_term`

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$.

# `implies_term`

```elixir
@spec implies_term() :: ShotDs.Data.Term.term_id()
```

Term representing the implication operator $\supset_{o\to o\to o}$.

# `nand_term`

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)$.

# `neg_term`

```elixir
@spec neg_term() :: ShotDs.Data.Term.term_id()
```

Term representing the negation operator $\neg_{o\to o}$.

# `nor_term`

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)$.

# `not_equals_term`

```elixir
@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)$.

# `or_term`

```elixir
@spec or_term() :: ShotDs.Data.Term.term_id()
```

Term representing the disjunction operator $\lor_{o\to o\to o}$.

# `pi_term`

```elixir
@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$.

# `sigma_term`

```elixir
@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$.

# `true_term`

```elixir
@spec true_term() :: ShotDs.Data.Term.term_id()
```

Term representing truth $\top_o$.

# `xor_term`

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)$.

# `andrews_equality`

```elixir
@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)$$

# `extensional_equality`

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$.

# `leibniz_equality`

```elixir
@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\}$

---

*Consult [api-reference.md](api-reference.md) for complete listing*