BeHOLd.ClassicalHOL.Definitions (behold v1.1.3)

Contains macros for the connectives of classical higher-order logic. This includes constants and terms facilitating pattern matching and term construction. Note that more types, constants and terms can be introduced via the HOL library.

The module offers a limited amount of common types under the section Types. New types can be introduced via the function HOL.Data.mk_type/2.

It also provides a collection of common HOL connectives which are either from the signature or defined in terms of connectives from the signature.

Summary

Signature

signature_symbols()

Returns a list of the names of the signature symbols in the logic.

Types

type_i()

Base type for individuals (type ι).

type_ii()

Type for symbols of type ι⇾ι, i.e., endomorphisms/operators on type ι.

type_iii()

Type for symbols of type ι⇾ι⇾ι, i.e., binary operators on type ι.

type_iio()

Type for symbols of type ι⇾ι⇾o, e.g. relations on individuals.

type_io()

Type for symbols of type ι⇾o, e.g. sets of individuals or predicates over individuals.

type_io_i()

Type for symbols of type (ι⇾o)⇾ι, e.g. the choice operator (Hilbert's ε).

type_io_io_io()

Type for symbols of type (ι⇾o)⇾(ι⇾o)⇾ι⇾o, e.g. set operations like union (∪) or intersection (∩).

type_io_io_o()

Type for symbols of type (ι⇾o)⇾(ι⇾o)⇾o, i.e. relations between sets of individuals, e.g. the subset relation (⊆).

type_io_o()

Type for symbols of type (ι⇾o)⇾o, e.g. sets of sets of individuals, or predicates over sets of individuals.

type_o()

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

type_oo()

Type for symbols of type o⇾o, e.g. unary connectives like negateion.

type_ooo()

Type for symbols of type o⇾o⇾o, e.g. binary connectives like conjunction.

Constants

and_const()

Constant representing the conjunction operator.

equals_const(type)

Constant representing equality over instances of the given type.

equivalent_const()

Constant representing the equivalence operator.

false_const()

Constant representing falsity.

implies_const()

Constant representing the implication operator.

neg_const()

Constant representing the negation operator.

or_const()

Constant representing the disjunction operator.

pi_const(element_type)

Constant representing the pi operator (universal quantification) over the given element type.

sigma_const(element_type)

Constant representing the sigma operator (existential quantification) over the given element type.

true_const()

Constant representing truth.

Terms

and_term()

A term representation of the conjunction operator.

equals_term(t)

A term representation of the equality operator operating on the given type.

equivalent_term()

A term representation of the equivalence operator.

false_term()

A term representation of falsity.

implied_by_term()

Term representation of the reverse implication operator. Rewrites the term in terms of (normal) implication.

implies_term()

A term representation of the implication operator.

nand_term()

Term representation of the NAND-operator. Rewrites the term in terms of negated conjunction.

neg_term()

A term representation of the negation operator.

nor_term()

Term representation of the NOR-operator. Rewrites the term in terms of negated disjunction.

not_equals_term(t)

Term representation of the negated equality operator operating on the given type.

or_term()

A term representation of the disjunction operator.

pi_term(element_type)

A term representation of the pi operator (universal quantification) for the given element type. Returns a lambda abstraction that takes a predicate.

sigma_term(element_type)

A term representation of the sigma operator (existential quantification) for the given element type. Returns a lambda abstraction that takes a predicate.

true_term()

A term representation of truth.

xor_term()

Term representation of the XOR-operator. Rewrites the term in terms of negated equivalence.

Signature

signature_symbols()

(macro)

Returns a list of the names of the signature symbols in the logic.

Example

iex> signature_symbols()
["⊤", "⊥", "¬", "∨", "∧", "⊃", "≡", "Π", "Σ", "="]

Types

type_i()

(macro)

@spec type_i() :: HOL.Data.type()

Base type for individuals (type ι).

type_ii()

(macro)

@spec type_ii() :: HOL.Data.type()

Type for symbols of type ι⇾ι, i.e., endomorphisms/operators on type ι.

type_iii()

(macro)

@spec type_iii() :: HOL.Data.type()

Type for symbols of type ι⇾ι⇾ι, i.e., binary operators on type ι.

type_iio()

(macro)

@spec type_iio() :: HOL.Data.type()

Type for symbols of type ι⇾ι⇾o, e.g. relations on individuals.

type_io()

(macro)

@spec type_io() :: HOL.Data.type()

Type for symbols of type ι⇾o, e.g. sets of individuals or predicates over individuals.

type_io_i()

(macro)

@spec type_io_i() :: HOL.Data.type()

Type for symbols of type (ι⇾o)⇾ι, e.g. the choice operator (Hilbert's ε).

type_io_io_io()

(macro)

@spec type_io_io_io() :: HOL.Data.type()

Type for symbols of type (ι⇾o)⇾(ι⇾o)⇾ι⇾o, e.g. set operations like union (∪) or intersection (∩).

type_io_io_o()

(macro)

@spec type_io_io_o() :: HOL.Data.type()

Type for symbols of type (ι⇾o)⇾(ι⇾o)⇾o, i.e. relations between sets of individuals, e.g. the subset relation (⊆).

type_io_o()

(macro)

@spec type_io_o() :: HOL.Data.type()

Type for symbols of type (ι⇾o)⇾o, e.g. sets of sets of individuals, or predicates over sets of individuals.

type_o()

(macro)

@spec type_o() :: HOL.Data.type()

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

type_oo()

(macro)

@spec type_oo() :: HOL.Data.type()

Type for symbols of type o⇾o, e.g. unary connectives like negateion.

type_ooo()

(macro)

@spec type_ooo() :: HOL.Data.type()

Type for symbols of type o⇾o⇾o, e.g. binary connectives like conjunction.

Constants

and_const()

(macro)

@spec and_const() :: HOL.Data.declaration()

Constant representing the conjunction operator.

equals_const(type)

(macro)

@spec equals_const(HOL.Data.type()) :: HOL.Data.declaration()

Constant representing equality over instances of the given type.

equivalent_const()

(macro)

@spec equivalent_const() :: HOL.Data.declaration()

Constant representing the equivalence operator.

false_const()

(macro)

@spec false_const() :: HOL.Data.declaration()

Constant representing falsity.

implies_const()

(macro)

@spec implies_const() :: HOL.Data.declaration()

Constant representing the implication operator.

neg_const()

(macro)

@spec neg_const() :: HOL.Data.declaration()

Constant representing the negation operator.

or_const()

(macro)

@spec or_const() :: HOL.Data.declaration()

Constant representing the disjunction operator.

pi_const(element_type)

(macro)

@spec pi_const(HOL.Data.type()) :: HOL.Data.declaration()

Constant representing the pi operator (universal quantification) over the given element type.

sigma_const(element_type)

(macro)

@spec sigma_const(HOL.Data.type()) :: HOL.Data.declaration()

Constant representing the sigma operator (existential quantification) over the given element type.

true_const()

(macro)

@spec true_const() :: HOL.Data.declaration()

Constant representing truth.

Terms

and_term()

(macro)

@spec and_term() :: HOL.Data.hol_term()

A term representation of the conjunction operator.

equals_term(t)

(macro)

@spec equals_term(HOL.Data.type()) :: HOL.Data.hol_term()

A term representation of the equality operator operating on the given type.

equivalent_term()

(macro)

@spec equivalent_term() :: HOL.Data.hol_term()

A term representation of the equivalence operator.

false_term()

(macro)

@spec false_term() :: HOL.Data.hol_term()

A term representation of falsity.

implied_by_term()

(macro)

@spec implied_by_term() :: HOL.Data.hol_term()

Term representation of the reverse implication operator. Rewrites the term in terms of (normal) implication.

implies_term()

(macro)

@spec implies_term() :: HOL.Data.hol_term()

A term representation of the implication operator.

nand_term()

(macro)

@spec nand_term() :: HOL.Data.hol_term()

Term representation of the NAND-operator. Rewrites the term in terms of negated conjunction.

neg_term()

(macro)

@spec neg_term() :: HOL.Data.hol_term()

A term representation of the negation operator.

nor_term()

(macro)

@spec nor_term() :: HOL.Data.hol_term()

Term representation of the NOR-operator. Rewrites the term in terms of negated disjunction.

not_equals_term(t)

(macro)

@spec not_equals_term(HOL.Data.type()) :: HOL.Data.hol_term()

Term representation of the negated equality operator operating on the given type.

or_term()

(macro)

@spec or_term() :: HOL.Data.hol_term()

A term representation of the disjunction operator.

pi_term(element_type)

(macro)

@spec pi_term(HOL.Data.type()) :: HOL.Data.hol_term()

A term representation of the pi operator (universal quantification) for the given element type. Returns a lambda abstraction that takes a predicate.

sigma_term(element_type)

(macro)

@spec sigma_term(HOL.Data.type()) :: HOL.Data.hol_term()

A term representation of the sigma operator (existential quantification) for the given element type. Returns a lambda abstraction that takes a predicate.

true_term()

(macro)

@spec true_term() :: HOL.Data.hol_term()

A term representation of truth.

xor_term()

(macro)

@spec xor_term() :: HOL.Data.hol_term()

Term representation of the XOR-operator. Rewrites the term in terms of negated equivalence.