abstract type Operation end

An operation is a function which takes zero or more operands to a well-defined output value.

See also BinaryOperation, arity.

struct BinaryOperation{N,M<:SMatrix{N,N,FiniteTruth}} <: AbstractBinaryOperation
    truthtable::M
end

A binary operation on a set S is a mapping of the elements of the Cartesian product S × S → S. The closure property of a binary operation expresses the existence of a result for the operation given any pair of operands. Binary operations are required to be defined on all elements of S × S.

See also Operation, arity.

struct Axiom{Symbol} end

An axiom is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. Axioms aim to capture what is special about a particular structure (or set of structures).

See also checkaxiom.

function checkaxiom(a::Axiom, args...)

Check if axiom a is satisfied.

See also Axiom.

function checkaxiom(
    ::typeof(Commutativity),
    o::O
) where {
    O<:AbstractBinaryOperation
}

A binary operation * on a set S is called commutative if x * y = y * x ∀ x, y ∈ S.

See also Axiom, BinaryOperation.

function checkaxiom(
    ::typeof(Associativity),
    o::O
) where {
    O<:AbstractBinaryOperation
}

A binary operation * on a set S is called associative if it satisfies the associative law: (x * y) * z = x * (y * z) ∀ x, y, z ∈ S.

See also Axiom, BinaryOperation.

function checkaxiom(
    ::typeof(AbsorptionLaw),
    o1::O,
    o2::O
) where {
    O<:AbstractBinaryOperation
}

The absorption law or absorption identity is an identity linking a pair of binary operations. Two binary operations, * and ⋅, are said to be connected by the absotprion law if a * (a ⋅ b) = a ⋅ (a * b) = a.

See also Axiom, BinaryOperation.

function checkaxiom(
    ::typeof(LeftIdentity),
    o::O,
    e::T
) where {
    O<:AbstractBinaryOperation,
    T<:Truth
}

Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a left identity if e * s = s ∀ s ∈ S.

See also Axiom, BinaryOperation.

function checkaxiom(
    ::typeof(RightIdentity),
    o::O,
    e::T
) where {
    O<:AbstractBinaryOperation,
    T<:Truth
}

Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a right identity if s * e = s ∀ s ∈ S.

See also Axiom, BinaryOperation.

function checkaxiom(
    ::typeof(IdentityElement),
    o::O,
    e::T
) where {
    O<:AbstractBinaryOperation,
    T<:Truth
}

An identity element or neutral element of a binary operation is an element that leaves unchanged every element when the operation is applied. I.e., let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a two-sided identity, or simply identity, if e is both a left identity and a right identity.

See also Axiom, BinaryOperation, LeftIdentity, RightIdentity.

function checkaxiom(a::Axiom, m::Monoid{N}) where {N}

Check if axiom a is satisfied by the operation of the monoid m.

See also Axiom, Monoid.

function checkaxiom(
    ::typeof(RightResidual),
    m::Monoid{T}
) where {
    T<:Truth,
}

Check that ∀ x ∈ S there exists for every x ∈ S a greatest y ∈ S such that x ⋅ y ≤ z.

See also Axiom, Monoid.

function checkaxiom(
    ::typeof(LeftResidual),
    m::Monoid{T}
) where {
    T<:Truth,
}

Check that ∀ x ∈ S there exists for every y ∈ S a greatest x ∈ S such that x ⋅ y ≤ z.

See also Axiom, Monoid.

function checkaxiom(
    ::typeof(ResiduationProperty),
    m::Monoid{N}
) where {
    N
}

Check that ∀ x ∈ S there exists for every x ∈ S a greatest y ∈ S and for every y ∈ S a greatest x ∈ S such that x ⋅ y ≤ z.

See also Axiom, Monoid.

function checkaxiom(
    ::typeof(Implication1),
    o::B,
    top::Truth
) where {
    N,
    B<:BinaryOperation{N}
}

Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and a binary operation →, a → a = ⊤ holds.

See also Axiom, BinaryOperation.

function checkaxiom(
    ::typeof(Implication2),
    o1::B,
    o2::B
) where {
    N,
    B<:BinaryOperation{N}
}

Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and two binary operations ∧ (o1) and → (o2), a ∧ (a → b) = a ∧ b holds.

See also Axiom, BinaryOperation.

function checkaxiom(
    ::typeof(Implication3),
    o1::B,
    o2::B
) where {
    N,
    B<:BinaryOperation{N}
}

Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and two binary operations ∧ (o1) and → (o2), b ∧ (a → b) = b holds.

See also Axiom, BinaryOperation.

function checkaxiom(
    ::typeof(DistributiveLaw),
    o1::B,
    o2::B
) where {
    N,
    B<:BinaryOperation{N}
}

Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) and two binary operations ⋅ and *, ⋅ is distributive over * if ∀ a, b, c ∈ L: a ⋅ (b * c) = (a ⋅ b) * (a ⋅ c).

See also Axiom, BinaryOperation.

const Commutativity

A binary operation * on a set S is called commutative if x * y = y * x ∀ x, y ∈ S.

See also Axiom, BinaryOperation, checkaxiom.

const Associativity

A binary operation * on a set S is called associative if it satisfies the associative law: (x * y) * z = x * (y * z) ∀ x, y, z ∈ S.

See also Axiom, BinaryOperation, checkaxiom.

const AbsorptionLaw

The absorption law or absorption identity is an identity linking a pair of binary operations. Two binary operations, * and ⋅, are said to be connected by the absorption law if a * (a ⋅ b) = a ⋅ (a * b) = a.

See also Axiom, BinaryOperation, checkaxiom.

const LeftIdentity

Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a left identity if e * s = s ∀ s ∈ S.

See also Axiom, BinaryOperation, checkaxiom.

const RightIdentity

Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a right identity if s * e = s ∀ s ∈ S.

See also Axiom, BinaryOperation, checkaxiom.

const IdentityElement

An identity element or neutral element of a binary operation is an element that leaves unchanged every element when the operation is applied. I.e., let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a two-sided identity, or simply identity, if e is both a left identity and a right identity.

See also Axiom, BinaryOperation, LeftIdentity, RightIdentity, checkaxiom.

const RightResidual

The right residual between two elements z, x ∈ S is the greatest y ∈ S such that x ⋅ y ≤ z.

See also Axiom, Monoid, checkaxiom.

const LeftResidual

The left residual between two elements z, y ∈ S is the greatest x ∈ S such that x ⋅ y ≤ z.

See also Axiom, Monoid, checkaxiom.

const ResiduationProperty

A lattice (L, ∨, ∧, ⋅, ⊥, →) is residuated if ∀ x ∈ S there exists for every x ∈ S a greatest y ∈ S and for every y ∈ S a greatest x ∈ S such that x ⋅ y ≤ z.

See also Axiom, Monoid, checkaxiom.

const Implication1

Axiom Implication1 is satisfied if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and a binary operation →, a → a = ⊤ holds.

See also Axiom, checkaxiom.

const Implication2

Axiom Implication2 is satisfied if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) and two binary operations ∧ (o1) and → (o2), a ∧ (a → b) = a ∧ b holds.

See also Axiom, checkaxiom.

const Implication3

Axiom Implication3 is satisfied if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) and two binary operations ∧ (o1) and → (o2), b ∧ (a → b) = b holds.

See also Axiom, checkaxiom.

const DistributiveLaw

Given a bounded lattice (H, ∨, ∧, ⊥, ⊤) and two binary operations ⋅ and *, ⋅ is distributive over * if ∀ a, b, c ∈ L: a ⋅ (b * c) = (a ⋅ b) * (a ⋅ c).

See also Axiom, checkaxiom.

abstract type FiniteAlgebra{N} <: AbstractAlgebra{FiniteTruth} end

A finite algebra is an algebraic structure defined over a finite set.

See also AbstractAlgebra.

struct Monoid{T<:Truth,D<:AbstractVector{T},B<:BinaryOperation{T}}
    operation::B
    identityelement::T
end

A monoid (S, ⋅, e) is a set S equipped with a binary operation S × S → S, denoted as ⋅, satisfying the following axiomatic identities:

• (Associativity) ∀ a, b, c ∈ S, the equation (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c) holds.
• (Identity element) There exists an element e ∈ L such that for every element a ∈ S, the equalities e ⋅ a = a and a ⋅ e = a hold.

The identity element of a monoid is unique.

See also BinaryOperation, Axiom, checkaxiom, checkmonoidaxioms, Associativity, IdentityElement.

struct CommutativeMonoid{N} <: FiniteAlgebra{N}
    operation::BinaryOperation{N}
    identityelement::FiniteTruth
end

A commutative monoid (S, ⋅, e) is a monoid whose operation is commutative.

See also Monoid, Commutativity.

struct FiniteLattice{N} <: FiniteAlgebra{N}
    join::BinaryOperation{N}
    meet::BinaryOperation{N}
end

A finite lattice is a lattice defined over a finite set.

A lattice is an algebraic structure (L, ∨, ∧) consisting of a set L and two binary, commutative and associative operations ∨ and ∧ on L satisfying the following axiomatic identities for all elements a, b ∈ L (sometimes called absorption laws):

• a ∨ (a ∧ b) = a
• a ∧ (a ∨ b) = a

See also FiniteAlgebra, BinaryOperation.

struct FiniteBoundedLattice{N} <: FiniteAlgebra{N}
    join::BinaryOperation{N}
    meet::BinaryOperation{N}
    bot::FiniteTruth
    top::FiniteTruth
end

A finite bounded lattice is a bounded lattice defined over a finite set.

A bounded lattice is an algebraic structure (L, ∨, ∧, ⊥, ⊤) such that (L, ∨, ∧) is a lattice, the bottom element ⊥ is the identity element for the join operation ∨, and the top element ⊤ is the identity element for the meet operation ∧:

• a ∨ ⊥ = a
• a ∧ ⊤ = a

See also FiniteLattice.

struct FiniteResiduatedLattice{N} <: FiniteAlgebra{N}
    join::BinaryOperation{N}
    meet::BinaryOperation{N}
    monoid::CommutativeMonoid{N}
    rightresidual::BinaryOperation{N}
    leftresidual::BinaryOperation{N}
    bot::FiniteTruth
    top::FiniteTruth
end

A residuated lattice is an algebraic structure L = (L, ∨, ∧, ⋅, e) such that:

• (L, ∨, ∧) is a lattice
• (L, ⋅, e) is a monoid
• ∀ x ∈ L there exists for every x ∈ L a greatest y ∈ L and for every y ∈ L a greatest x ∈ L such that x ⋅ y ≤ z

See also FiniteBoundedLattice,

struct FiniteFLewAlgebra{N} <: FiniteAlgebra{N}
    join::BinaryOperation{N}
    meet::BinaryOperation{N}
    monoid::CommutativeMonoid{N}
    implication::BinaryOperation{N}
    bot::FiniteTruth
    top::FiniteTruth
end

An FLew-algebra is an algebra (L, ∨, ∧, ⋅, →, ⊥, ⊤), where

• (L, ∨, ∧, ⊥, ⊤) is a bounded lattice with top element ⊤ and bottom element ⊥
• (L, ⋅, ⊤) is a commutative monoid
• The residuation property holds: x ⋅ y ≤ z iff x ≤ y → z

See also FiniteBoundedLattice, CommutativeMonoid.

struct FiniteHeytingAlgebra{N} <: FiniteAlgebra{N}
    join::BinaryOperation{N}
    meet::BinaryOperation{N}
    implication::BinaryOperation{N}
    bot::FiniteTruth
    top::FiniteTruth
end

A Heyting algebra (H, ∨, ∧, →, ⊥, ⊤) is a bounded lattice (H, ∨, ∧, ⊥, ⊤) equipped with a binary operation a → b of implication such that (c ∧ a) ≤ b is equivalent to c ≤ (a → b).

Given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and a binary operation →, these together form a Heyting algebra if and only if the following hold:

• (Implication1) a → a = ⊤
• (Implication2) a ∧ (a → b) = a ∧ b
• (Implication3) b ∧ (a → b) = b
• (Distributive law for →) a → (b ∧ c) = (a → b) ∧ (a → c)

See also FiniteBoundedLattice, BinaryOperation.

function precedeq(
    l::L,
    t1::T1,
    t2::T2
) where {
    N,
    L<:FiniteAlgebra{N},
    T1<:Truth,
    T2<:Truth
}

Return true if t1 ≤ t2 in l. Given an algebraically defined lattice (L, ∨, ∧), one can define a partial order ≤ on L by setting a ≤ b if a = a ∧ b.

See also precedes, succeedes, succeedeq.

function precedes(
    l::L,
    t1::T1,
    t2::T2
) where {
    N,
    L<:FiniteAlgebra{N},
    T1<:Truth,
    T2<:Truth
}

Return true if t1 < t2 in l. Given an algebraically defined lattice (L, ∨, ∧), one can define a partial order ≤ on L by setting a ≤ b if a = a ∧ b.

See also precedeq, succeedes, succeedeq.

function succeedeq(
    l::L,
    t1::T1,
    t2::T2
) where {
    N,
    L<:FiniteAlgebra{N},
    T1<:Truth,
    T2<:Truth
}

Return true if t1 ≥ t2 in l. Given an algebraically defined lattice (L, ∨, ∧), one can define a partial order ≤ on L by setting a ≤ b if a = a ∧ b.

See also precedes, precedeq, succeedes.

function succeedes(
    l::L,
    t1::T1,
    t2::T2
) where {
    N,
    L<:FiniteAlgebra{N},
    T1<:Truth,
    T2<:Truth
}

Return true if t1 > t2 in l. Given an algebraically defined lattice (L, ∨, ∧), one can define a partial order ≤ on L by setting a ≤ b if a = a ∧ b.

See also precedes, precedeq, succeedeq.