Module prop::mid

Middle Exponential Logic

By building on Existential Logic and Exponential Propositions (HOOO), it is possible to talk about nuances of middle propositions.

All middle exponential propositions implies a theory (in HOOO EP).

Up, Down and Middle

The basic middle exponential propositions are:

up(a) = (¬¬a ⋀ ¬(a^true))
down(a) = (¬a ⋀ ¬(false^a))
mid(a) = up(a) ⋁ down(a)

• The up(a) proposition is close to a^true
• The down(a) proposition is close to false^a
• The mid(a) proposition is close to theory(a)

Collapsing Theory to Up

theory(a) == up(a)
false == down(a)

These theorems are provable when ¬¬a ⋁ ¬a (Excluded Middle of Non-Existence).

Functions

• absurd_down
  down(a) => false.
• absurd_down_with_tauto_e
  down(a) ⋀ (¬¬a ⋁ ¬a)^true => false.
• absurd_theory
  theory(a) => false.
• absurd_theory_tauto_excm
  theory(a) ⋀ (a ⋁ ¬a)^true => false.
• and_e_theory_to_mid
  ((¬¬a ⋁ ¬a) ⋀ theory(a)) => mid(a).
• down
  down(a) => ¬a.
• down_to_e
  down(a) => (¬¬a ⋁ ¬a).
• down_to_excm
  down(a) => (a ⋁ ¬a).
• down_to_not_up
  down(a) => ¬up(a).
• down_to_theory
  down(a) => theory(a).
• down_to_up
  down(a) => up(a).
• down_to_up_with_tauto_e
  down(a) ⋀ (¬¬a ⋁ ¬a)^true => up(a).
• down_to_virtual_not
  down(a) => virtual(¬a).
• mica_to_e
  mica(a) => (¬¬a ⋁ ¬a).
• mid_to_and_e_theory
  mid(a) => ((¬¬a ⋁ ¬a) ⋀ theory(a)).
• mid_to_e
  mid(a) => (¬¬a ⋁ ¬a).
• mid_to_theory
  mid(a) => theory(a).
• paradox
  (up(a) ⋀ down(a)) => false.
• subordinate
  (¬(x^true) => x) => ¬¬x.
• theory_to_mid
  theory(a) => mid(a).
• theory_to_up
  theory(a) => up(a).
• theory_to_up_with_tauto_e
  theory(a) ⋀ (¬¬a ⋁ ¬a)^true => up(a).
• up
  up(a) => a.
• up_excm
  up(a) ⋀ (a ⋁ ¬a) => a.
• up_to_e
  up(a) => (¬¬a ⋁ ¬a).
• up_to_not_down
  up(a) => ¬down(a).
• up_to_theory
  up(a) => theory(a).
• up_to_virtual
  up(a) => virtual(a).
• up_to_virtual_excm
  up(a) ⋀ (a ⋁ ¬a) => virtual(a).
• virtual_to_theory
  virtual(a) => theory(a).

Type Definitions

• Down
  A down proposition ¬a ⋀ ¬(false^a).
• Mid
  A middle proposition (¬¬a ⋀ ¬(a^true)) ⋁ (¬a ⋀ ¬(false^a)).
• MidCatuskoti
  A middle Catuṣkoṭi proposition (a^true ⋁ false^a) ⋁ (up(a) ⋁ down(a)).
• Subordinate
  A subordinate middle proposition ¬(x^true) => x.
• Up
  An up proposition ¬¬a ⋀ ¬(a^true).
• Virtual
  A virtual middle proposition a ⋀ ¬(a^true).