Module prop::existence

Existential Logic

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

• Catuskoti
  Implemented by Catuṣkoṭi expressions.
• EProp
  Shorthand for existential proposition.
• Existential
  Implemented by existential types.

Functions

• and
  (¬¬(a ⋀ b) ⋁ ¬(a ⋀ b)).
• and_ea_eb_to_excm_crosseq
  ((¬¬a ∨ ¬a) ⋀ (¬¬b ∨ ¬b)) => ((a =x= b) ⋁ ¬(a =x= b)).
• and_ea_eb_to_or_crosseq
  ((¬¬a ∨ ¬a) ⋀ (¬¬b ∨ ¬b)) => ((a =x= b) ⋁ (¬a =x= b)).
• catuskoti_e_absurd
  Proves that any Catuṣkoṭi with relative excluded middle of non-existence is absurd.
• catuskoti_excm_absurd
  Proves that any Catuṣkoṭi with relative excluded middle is absurd.
• crosseq_adj_to_eqe
  (¬a =x= b) => ((¬¬a ∨ ¬a) == (¬¬b ∨ ¬b)).
• crosseq_adj_to_ncrosseq
  (¬a =x= b) => ¬(a =x= b).
• crosseq_adjoint
  (¬a =x= b) => (a =x= ¬b).
• crosseq_refl
  a =x= a.
• crosseq_symmetry
  (a =x= b) => (b =x= a).
• crosseq_to_eqe
  (a =x= b) => ((¬¬a ∨ ¬a) == (¬¬b ∨ ¬b)).
• crosseq_to_eqn
  (a =x= b) => (¬a == ¬b).
• crosseq_to_eqnn
  (a =x= b) => (¬¬a == ¬¬b).
• crosseq_transitivity
  (a =x= b) ⋀ (b =x= c) => (a =x= c).
• double_neg_e
  ¬¬(¬¬x ⋁ ¬x).
• en
  (¬¬a ∨ ¬a) => (¬¬¬a ∨ ¬¬a).
• eq_to_crosseq
  (a == b) => (a =x= b).
• eqn_to_crosseq
  (¬a == ¬b) => (a =x= b).
• eqnn_to_crosseq
  (¬¬a == ¬¬b) => (a =x= b).
• excm_to_e
  (a ∨ ¬a) => (¬¬a ∨ ¬a).
• imply
  (¬¬(a => b) ⋁ ¬(a => b)).
• imply_e
  (¬¬a ⋁ ¬a) ⋀ (¬¬b ⋁ ¬b) => (¬¬(a => b) ⋁ ¬(a => b)).
• or
  (¬¬(a ⋁ b) ⋁ ¬(a ⋁ b)).
• or_e
  (¬¬a ⋁ ¬a) ⋀ (¬¬b ⋁ ¬b) => (¬¬(a ⋁ b) ⋁ ¬(a ⋁ b)).
• or_from_de_morgan
  ¬(¬¬a ∧ ¬¬b) => (¬a ∨ ¬b).
• rev_crosseq_adjoint
  (a =x= ¬b) => (¬a =x= b).
• rev_en
  (¬¬¬a ∨ ¬¬a) => (¬¬a ∨ ¬a).

Type Definitions

• CrossCatus
  A Catuṣkoṭi that uses cross equality in excluded middle relation.
• CrossEq
  a =x= b, defined as (a => ¬¬b) ⋀ (b => ¬¬a).
• E
  ∀ x { ¬¬x ⋁ ¬x }.
• EqNN
  ¬¬a == ¬¬b.
• NN
  Shorthand for ¬¬x.