Module prop::hooo

Exponential Propositions

Paper: HOOO Exponential Propositions

By using function pointers, one can force construction of propositions without capturing any variables, such that the proposition is tautological true, instead of just assuming it is true.

When a is tautological provable from b, one expresses it as a^b.

It turns out that this has the same semantics as Higher Order Operator Overloading (HOOO).

One motivation for developing HOOO for Exponential Propositions is to allow substitution in quality ~~ and qubit ~ operator for Path Semantical Quantum Propositional Logic (PSQ).

Vocabulary

• Tautology tauto(a) := a^true
• Paradox para(a) := false^a
• Uniform uniform(a) := a^true ⋁ false^a
• Theory theory(a) := ¬uniform(a)
• Exists ∃ a { b } := ¬((¬b)^a)
• Decidable (a ⋁ ¬a)^true

Overlap with Modal Logic

Modal Logic overlaps with HOOO EP:

• Necessity □p := p^true
• Possibility ◇p := p^true ⋁ theory(p)

For a derived Modal Logic from HOOO EP, see the modal module.

A paradoxical proposition false^p can be translated as □¬p.

Comment conventions

When a function comment says a => b, it is actually (a => b)^true.

The exponent is left out to make the comments more consistent for the whole library. Otherwise, it would be proper to use notation for Exponential Propositions everywhere, but this is unpractical since Exponential Propositions is viewed as an extension of normal Propositional Logic. One would like other modules to not use this notation unless they rely on this extension explicitly.

When a^true is used explicitly, the function returns a function pointer instead of using a _: True argument, since it is natural in programming to not add unused arguments.

Re-exports

• pub use tauto_eq_transitivity as tauto_eq_in_right_arg;

Modules

• pow
  Power extensions.
• tauto
  Tautology extensions.

Functions

• consistency
  ¬(false^true).
• cut
  (a ⋁ b)^c ⋀ d^(e ⋀ a) => (b ⋁ d)^(c ⋀ e).
• cut_elim
  a^b ⋀ c^(d ⋀ a) => c^(b ⋀ d).
• decide
  a^b ⋁ ¬(a^b).
• eq_not_para_to_eq_para
  (¬(false^a) == ¬(false^b)) => (false^a == false^b).
• eq_refl
  (x == x)^true.
• eq_tauto_para_to_para_uniform
  (a^true == false^a) => false^uniform(a).
• eq_tauto_to_eq_para
  (a^true == b^true) => (false^a == false^b).
• eq_tauto_to_eq_para_excm
  (a^true == b^true) => (false^a == false^b).
• exists_construct
  a => ∃ a { a }.
• exists_excm_to_pow
  ∃ a { b } ⋀ (b ⋁ ¬b)^a => b^a.
• exists_fst
  ∃ a ⋀ b { x } => ∃ a { x }.
• exists_join
  ∃ a { x } ⋀ ∃ b { x } => ∃ a ⋀ b { x }.
• exists_left
  ∃ a { x } => ∃ a ⋁ b { x }.
• exists_left_refl
  ∃ a { b } => ∃ a { a }.
• exists_not_to_not_pow
  ∃ a { ¬b } => ¬(b^a).
• exists_not_to_not_tauto_right
  ∃ a { ¬b } => ¬(b^true).
• exists_pow
  ∃ a { x } ⋀ b^a => ∃ b { x }.
• exists_rev_true
  ∃ true { a } => a.
• exists_right
  ∃ b { x } => ∃ a ⋁ b { x }.
• exists_snd
  ∃ a ⋀ b { x } => ∃ b { x }.
• exists_tauto
  a^true => ∃ a { true }.
• exists_to_exists_true
  ∃ a { b } => ∃ true { b }.
• exists_to_not_para
  ∃ true { a } => ¬(false^a).
• exists_true
  a => ∃ true { a }.
• exists_true_true
  ∃ true { true }.
• fa
  a^false.
• hooo_and
  (a ⋀ b)^c => (a^c ⋀ b^c).
• hooo_dual_and
  c^(a ⋀ b) => (c^a ⋁ c^b).
• hooo_dual_neq
  c^(¬(a == b)) => (c^a == c^b).
• hooo_dual_nrimply
  c^(¬(b => a)) => (c^a => c^b).
• hooo_dual_or
  c^(a ⋁ b) => (c^a ⋀ c^b).
• hooo_dual_rev_and
  (c^a ⋁ c^b) => c^(a ⋀ b).
• hooo_dual_rev_eq
  ¬(c^a == c^b) => c^(a == b).
• hooo_dual_rev_imply
  ¬(c^b => c^a) => c^(a => b).
• hooo_dual_rev_neq
  (c^a == c^b) => c^(¬(a == b)).
• hooo_dual_rev_nrimply
  (c^a => c^b) => c^(¬(b => a)).
• hooo_dual_rev_or
  (c^a ⋀ c^b) => c^(a ⋁ b).
• hooo_e_rev_not
  ¬((¬¬a)^b) => (¬a)^b.
• hooo_eq
  (a == b)^c => (a^c == b^c).
• hooo_imply
  (a => b)^c => (a^c => b^c).
• hooo_or
  (a ⋁ b)^c => (a^c ⋁ b^c).
• hooo_pord
  (a < b)^c => (a^c < b^c)
• hooo_rev_and
  (a^c ⋀ b^c) => (a ⋀ b)^c.
• hooo_rev_eq
  (a^c == b^c) => (a == b)^c.
• hooo_rev_neq
  ¬(a^c == b^c) => (¬(a == b))^c.
• hooo_rev_not
  ¬(a^b) => (¬a)^b.
• hooo_rev_not_excm
  ¬(a^b) ⋀ (a ⋁ ¬a)^true => (¬a)^b.
• hooo_rev_nrimply
  ¬(b^c => a^c) => (¬(b => a))^c.
• hooo_rev_or
  (a^c ⋁ b^c) => (a ⋁ b)^c.
• hooo_rev_ty
  (b^a : y^x) => ((a : x) => (b : y)).
• hooo_ty
  (b : y)^(a : x) => (b^a : y^x).
• imply_tauto_to_imply_para
  (a^true => b^true) => (false^b => false^a).
• imply_tauto_to_imply_para_excm
  (a^true => b^true) => (false^b => false^a).
• lift_q
  (a == b) ⋀ theory(a == b) => (a ~~ b).
• modus_ponens_to_exists
  b^a ⋀ a => ∃ a { b }.
• not_not_both_to_exists
  ¬¬a ⋀ ¬¬b => ∃ a { b }.
• not_not_para_rev_double
  ¬¬(false^a) => false^a.
• not_not_to_exists
  ¬¬a => ∃ a { a }.
• not_not_to_exists_true
  ¬¬a => ∃ true { a }.
• not_not_to_not_para
  ¬¬a => ¬(false^a).
• not_not_to_para_para
  ¬¬a => false^(false^a).
• not_not_to_para_para_e
  ¬¬a => false^(false^a).
• not_not_to_para_para_with_tauto_excm
  ¬¬a ⋀ (a ⋁ ¬a)^true => false^(false^a).
• not_para_to_exists
  ¬(false^a) => ∃ true { a }.
• not_para_to_not_not
  ¬(false^a) => ¬¬a.
• not_para_to_not_not_e
  ¬(false^a) => ¬¬a.
• not_para_to_para_para
  ¬(false^a) => false^(false^a).
• not_para_to_para_para_e
  ¬(false^a) => false^(false^a).
• not_para_to_para_para_with_tauto_excm
  ¬(false^a) ⋀ (a ⋁ ¬a)^true => false^(false^a).
• not_tauto_not_para_to_theory
  ¬(a^true) ⋀ ¬(false^a) => theory(a).
• not_theory
  ¬theory(a).
• para_and_to_or
  false^(a ∧ b) => false^a ⋁ false^b.
• para_and_to_or_excm
  false^(a ∧ b) => false^a ⋁ false^b.
• para_decide
  false^a ⋁ ¬(false^a).
• para_decide_e
  ¬¬(false^a) ⋁ ¬(false^a).
• para_eq_symmetry
  false^(x == y) => false^(y == x).
• para_eq_transitivity_left
  (false^(a == b) ∧ (b == c)^true) => false^(a == c).
• para_eq_transitivity_right
  ((a == b)^true ∧ false^(b == c)) => false^(a == c).
• para_exists_false
  ∃ a { false } => false.
• para_exists_false_false
  ∃ false { false } => false.
• para_from_or
  false^(a ⋁ b) => false^a ∧ false^b.
• para_in_arg
  (false^a ∧ (a == b)^true) => false^b.
• para_left_and
  false^a => false^(a ∧ b).
• para_liar
  (false^a)^(a^true) ⋀ (a^true)^(false^a) => false.
• para_not
  ¬(false^a) => false^(¬a).
• para_not_and_to_or_e
  false^(¬a ∧ ¬b) => false^(¬a) ⋁ false^(¬b).
• para_not_and_to_or_tauto_e
  false^(¬a ∧ ¬b) ⋀ (¬¬a ⋁ ¬a)^true ⋀ (¬¬b ⋁ ¬b)^true => false^(¬a) ⋁ false^(¬b).
• para_not_double
  false^a => false^(¬¬a).
• para_not_rev_double
  false^(¬¬a) => false^a.
• para_not_rev_triple
  false^(¬¬¬x) => false^(¬x).
• para_not_to_not_not_tauto
  false^(¬a) => ¬¬(a^true).
• para_not_to_para_para
  false^(¬x) => false^(false^x).
• para_not_triple
  false^(¬x) => false^(¬¬¬x).
• para_or_e
  false^a ⋁ false^(¬a).
• para_para
  a => false^(false^a).
• para_para_to_not_not
  false^(false^a) => ¬¬a.
• para_para_to_not_para
  false^(false^a) => ¬(false^a).
• para_pow_contra
  (¬a)^a => false^a.
• para_pow_contra_nn
  (¬a)^(¬¬a) => false^(¬¬a).
• para_rev_not
  false^(¬x) => ¬false^x.
• para_right_and
  false^b => false^(a ∧ b).
• para_to_eq_false
  false^a => (a == false)^true.
• para_to_not
  false^x => ¬x.
• para_to_or
  (false^a ∧ false^b) => false^(a ⋁ b).
• para_to_tauto_excm
  false^a => (a ⋁ ¬a)^true.
• para_to_tauto_excm_transitivity
  false^a ∧ (a == b)^true => (b ⋁ ¬b)^true.
• para_to_tauto_not
  false^a => (¬a)^true.
• para_uniform_and
  false^uniform(a ∧ b) => false^(uniform(a) ∧ uniform(b)).
• para_uniform_to_eq_tauto_para
  false^uniform(a) => (a^true == false^a).
• pow_contra_to_pow_contra_nn
  (¬a)^a => (¬a)^(¬¬a).
• pow_dual_rev_or_lift
  c^a ⋀ c^b => (c^a ⋀ c^b)^d.
• pow_eq_left
  (a == b)^true => (a^c == b^c).
• pow_eq_refl
  x =^= x.
• pow_eq_right
  (b == c)^true => (a^b == a^c).
• pow_eq_symmetry
  (x =^= y) => (y =^= x).
• pow_eq_to_tauto_eq
  (x =^= y) => (a == b)^true.
• pow_eq_transitivity
  (x =^= y) ⋀ (y =^= z) => (x =^= z).
• pow_excm_nn_to_rev_double
  (a ⋁ ¬a)^(¬¬a) => a^(¬¬a).
• pow_imply_to_imply_tauto_pow
  (a => b)^c => (c^true => b^a).
• pow_in_left_arg
  a^b ⋀ (a == c)^true => c^b.
• pow_in_right_arg
  a^b ⋀ (b == c)^true => a^c.
• pow_lift
  a^b => (a^b)^c.
• pow_lower
  (a^b)^c => a^(b ⋀ c).
• pow_modus_tollens
  a^b => (¬b)^(¬a).
• pow_not
  ¬(a^b) => a^(¬b).
• pow_not_double_down
  a^(¬¬b) => (¬¬a)^b.
• pow_not_e
  ¬(a^b) => a^(¬b).
• pow_not_tauto_e
  ¬(a^b) ⋀ (¬¬a ⋁ ¬a)^true => a^(¬b).
• pow_not_tauto_excm
  ¬(a^b) ⋀ (a ⋁ ¬a)^true => a^(¬b).
• pow_refl
  a => a.
• pow_rev_lift_refl
  (a^b)^b => a^b.
• pow_right_and_symmetry
  a^(b ⋀ c) => a^(c ⋀ b)
• pow_tauto_to_imply_tauto
  b^(a^true) => (a^true => b^true).
• pow_tauto_to_pow_tauto_tauto
  b^(a^true) => (b^true)^(a^true).
• pow_to_imply
  b^a => (a => b).
• pow_to_imply_lift
  b^a => (a => b)^c.
• pow_to_pow_exists
  b^a => (∃ a { b })^a.
• pow_to_pow_tauto
  b^a => b^(a^true).
• pow_to_pow_tauto_tauto
  b^a => (b^true)^(a^true).
• pow_to_tauto_imply
  b^a => (a => b)^true.
• pow_transitivity
  b^a ⋀ c^b => c^a.
• pow_ty
  (a : x) ⋀ (b^a : y^x) => (b : y).
• pow_unfold_fa
  a^(a^false) => a.
• q_in_left_arg
  (a ~~ b) ∧ (a == c)^true => (c ~~ b).
• q_in_right_arg
  (a ~~ b) ∧ (b == c)^true => (a ~~ c).
• qu_in_arg
  ~a ∧ (a == b)^true => ~b.
• tauto_and
  a^true ∧ b^true => (a ∧ b)^true.
• tauto_and_to_eq_pos
  (a^true ∧ b^true) => (a == b)^true.
• tauto_decide
  a^true ⋁ ¬(a^true).
• tauto_e_to_or
  (¬¬a ⋁ ¬a)^true => ((¬¬a)^true ⋁ (¬a)^true).
• tauto_e_to_or_pow
  (¬¬a ⋁ ¬a)^true => ((¬¬a)^b ⋁ (¬a)^b).
• tauto_eq_excm_to_tauto_excm_eq
  ((a ⋁ ¬a) == (b ⋁ ¬b))^true => ((a == b) ⋁ ¬(a == b))^true.
• tauto_eq_in_left_arg
  (a == b) ∧ (a == c) => (c == b).
• tauto_eq_symmetry
  (x == y)^true => (y == x)^true.
• tauto_eq_to_pow_eq
  (a == b)^true => (x =^= y).
• tauto_eq_transitivity
  (a == b)^true ∧ (b == c)^true => (a == c)^true.
• tauto_excm_to_not_theory
  (a ⋁ ¬a)^true => ¬theory(a).
• tauto_excm_to_or
  (a ⋁ ¬a)^true => (a^true ⋁ (¬a)^true).
• tauto_excm_to_or_pow
  (a ⋁ ¬a)^true => (a^b ⋁ (¬a)^b).
• tauto_excm_to_tauto_excm_not
  (a ⋁ ¬a)^true => (¬a ⋁ ¬¬a)^true.
• tauto_excm_to_uniform
  (a ⋁ ¬a)^true => uniform(a).
• tauto_from_eq_true
  (a == true)^true => a^true.
• tauto_from_para_transitivity
  (false^(a == b) ∧ false^(b == c)) => (a == c)^true.
• tauto_hooo_and
  (a ⋀ b)^c => (a^c ⋀ b^c)^true.
• tauto_hooo_dual_and
  c^(a ⋀ b) => (c^a ⋁ c^b)^true.
• tauto_hooo_dual_neq
  c^(¬(a == b)) => (c^a == c^b)^true.
• tauto_hooo_dual_nrimply
  c^(¬(b => a)) => (c^a => c^b)^true.
• tauto_hooo_dual_or
  c^(a ⋁ b) => (c^a ⋀ c^b)^true.
• tauto_hooo_dual_rev_and
  (c^a ⋁ c^b)^true => c^(a ⋀ b).
• tauto_hooo_dual_rev_eq
  (¬(c^a == c^b))^true => c^(a == b).
• tauto_hooo_dual_rev_imply
  (¬(c^b => c^a))^true => c^(a => b).
• tauto_hooo_dual_rev_neq
  (c^a == c^b)^true => c^(¬(a == b)).
• tauto_hooo_dual_rev_nrimply
  (c^a => c^b)^true => c^(¬(b => a)).
• tauto_hooo_dual_rev_or
  (c^a ⋀ c^b)^true => c^(a ⋁ b).
• tauto_hooo_eq
  (a == b)^c => (a^c == b^c)^true.
• tauto_hooo_imply
  (a => b)^c => (a^c => b^c)^true.
• tauto_hooo_or
  (a ⋁ b)^c => (a^c ⋁ b^c)^true.
• tauto_hooo_pord
  (a < b)^c => (a^c < b^c)^true
• tauto_hooo_rev_and
  (a^c ⋀ b^c)^true => (a ⋀ b)^c.
• tauto_hooo_rev_eq
  (a^c == b^c)^true => (a == b)^c.
• tauto_hooo_rev_neq
  (¬(a^c == b^c))^true => (¬(a == b))^c.
• tauto_hooo_rev_not
  (¬(a^b))^true => (¬a)^b.
• tauto_hooo_rev_nrimply
  (¬(b^c => a^c))^true => (¬(b => a))^c.
• tauto_hooo_rev_or
  (a^c ⋁ b^c)^true => (a ⋁ b)^c.
• tauto_hooo_rev_ty
  (b^a : y^x)^true => (b : y)^(a : x).
• tauto_hooo_ty
  (b : y)^(a : x) => (b^a : y^x)^true.
• tauto_imply_in_left_arg
  (a => b)^true ∧ (a == c)^true => (c => b)^true.
• tauto_imply_in_right_arg
  (a => b)^true ∧ (b == c)^true => (a => c)^true.
• tauto_imply_pow
  (b^a)^true => (a => b)^true.
• tauto_imply_to_imply_tauto_pow
  (c => (a => b))^true => (c^true => b^a).
• tauto_imply_to_pow
  (a => b)^true => b^a.
• tauto_imply_to_pow_tauto
  (a => b)^true => b^(a^true).
• tauto_imply_transitivity
  (a => b)^true ∧ (b => c)^true => (a => c)^true.
• tauto_in_arg
  a^true ∧ (a == b)^true => b^true.
• tauto_modus_ponens
  (a => b)^true ∧ a^true => b^true.
• tauto_not
  ¬(x^true) => (¬x)^true.
• tauto_not_double
  x^true => (¬¬x)^true.
• tauto_not_excm
  ¬(x^true) ⋀ (a ⋁ ¬a)^true => (¬x)^true.
• tauto_not_to_para
  (¬a)^true => false^a.
• tauto_or
  (a^true ⋁ b^true) => (a ⋁ b)^true.
• tauto_or_left
  a^true => (a ⋁ b)^true.
• tauto_or_right
  b^true => (a ⋁ b)^true.
• tauto_para_rev_not
  false^(¬x) => (¬false^x)^true.
• tauto_pow_eq_left
  (a == b)^true => (a^c == b^c)^true.
• tauto_pow_eq_right
  (b == c)^true => (a^b == a^c)^true.
• tauto_pow_imply
  (a => b)^true => (b^a)^true.
• tauto_qu_eq
  (a == b)^true => (~a == ~b)^true.
• tauto_rev_and
  (a ∧ b)^true => a^true ∧ b^true.
• tauto_rev_not
  (¬x)^true => ¬(x^true).
• tauto_rev_or
  (a ⋁ b)^true => (a^true ⋁ b^true).
• tauto_to_eq_true
  a^true => (a == true)^true.
• tauto_to_or
  a^true ⋁ (¬a)^true.
• tauto_to_or_e
  (¬¬a)^true ⋁ (¬a)^true.
• tauto_to_or_pow
  a^b ⋁ (¬a)^b.
• tauto_to_or_pow_e
  ((¬¬a)^b ⋁ (¬a)^b).
• tauto_to_para_not
  a^true => false^(¬a).
• tauto_to_tauto_excm
  a^true => (a ⋁ ¬a)^true.
• theory_in_arg
  theory(a) ⋀ (a == b)^true => theory(b).
• theory_not_to_theory
  theory(¬a) => theory(a).
• theory_to_not_para
  theory(a) => ¬(false^a).
• theory_to_not_tauto
  theory(a) => ¬(a^true).
• to_not_pow
  ¬a ⋀ ¬¬b => ¬(a^b).
• tr
  true^a.
• uniform
  uniform(a).
• uniform_and
  uniform(a) ∧ uniform(b) => uniform(a ∧ b).
• uniform_dual_and
  uniform(a ∧ b) => uniform(a) ⋁ uniform(b).
• uniform_dual_rev_or
  uniform(a) ∧ uniform(b) => uniform(a ⋁ b).
• uniform_in_arg
  uniform(a) ⋀ (a == b)^true => uniform(b).
• uniform_refl
  uniform(a == a).
• uniform_symmetry
  uniform(a == b) => uniform(b == a).
• uniform_to_tauto_excm
  uniform(a) => (a ⋁ ¬a)^true.
• uniform_transitivity
  uniform(a == b) ∧ uniform(b == c) => uniform(a == c).

Type Definitions

• Exists
  There exists statement ∃ a { b } := ¬((¬b)^a).
• Para
  A paradoxical proposition para(a) := false^a.
• Pow
  a^b.
• PowEq
  Power equivalence =^=.
• Tauto
  A tautological proposition tauto(a) := a^true.
• Theory
  A proposition is a theory when non-uniform theory(a) := ¬(a^true ⋁ false^a).
• Uniform
  A uniform proposition uniform(a) := a^true ⋁ false^a.