Expand description
Type Theoretic Existential Philosophy
When reasoning about existence in existential philosophy, one can not assume that one’s own existence is of the form of a universal existence.
The logical nature of existence is unknown.
See this blog post for more information.
However, one can make a weaker assumption ¬¬a ⋁ ¬a,
which is that either one has a negative negative existence,
or one has a negative existence.
This assumption is called “Excluded Middle of Non-Existence”.
Descartes’ “I think, therefore I am.” might be thought of as “I think, therefore I don’t non-exist.” in this logic.
This logic is abbreviated EP (normal) or EPS (path semantical). One property of these logics is that De Morgan’s laws hold, even though the excluded middle is not assumed.
It means that it can be absurd if I do not exist, or I might not exist, but I have no proof that I exist or not exist.
The reason ¬¬a ⋁ ¬a is used, is to investigate
existential philosophy without assuming that the logical nature of existence
has something like the excluded middle,
yet still allow some reasoning that does not hold in ordinary constructive logic.
To assume an existential proposition, use the EProp trait.
The excluded middle implies an existential proposition.
Therefore, a decidable proposition DProp automatically implementes EProp.
Traits
Implemented by Catuṣkoṭi expressions.
Shorthand for existential proposition.
Implemented by existential types.
Functions
Proves that any Catuṣkoṭi with relative excluded middle of non-existence is absurd.
Proves that any Catuṣkoṭi with relative excluded middle is absurd.
(a =x= b) => (¬¬a == ¬¬b).
(a =x= b) ⋀ (b =x= c) => (a =x= c).
(¬¬a == ¬¬b) => (a =x= b).
(a ∨ ¬a) => (¬¬a ∨ ¬a).
¬(¬¬a ∧ ¬¬b) => (¬a ∨ ¬b).
Type Definitions
A Catuṣkoṭi that uses cross equality in excluded middle relation.
a =x= b, defined as (a => ¬¬b) ⋀ (b => ¬¬a).
∀ x { ¬¬x ⋁ ¬x }.
¬¬a == ¬¬b.
Shorthand for ¬¬x.