Expand description
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
- Power extensions.
- Tautology extensions.
Functions
¬(false^true)
.(a ⋁ b)^c ⋀ d^(e ⋀ a) => (b ⋁ d)^(c ⋀ e)
.a^b ⋀ c^(d ⋀ a) => c^(b ⋀ d)
.a^b ⋁ ¬(a^b)
.(¬(false^a) == ¬(false^b)) => (false^a == false^b)
.(x == x)^true
.(a^true == false^a) => false^uniform(a)
.(a^true == b^true) => (false^a == false^b)
.(a^true == b^true) => (false^a == false^b)
.a => ∃ a { a }
.∃ a { b } ⋀ (b ⋁ ¬b)^a => b^a
.∃ a ⋀ b { x } => ∃ a { x }
.∃ a { x } ⋀ ∃ b { x } => ∃ a ⋀ b { x }
.∃ a { x } => ∃ a ⋁ b { x }
.∃ a { b } => ∃ a { a }
.∃ a { ¬b } => ¬(b^a)
.∃ a { ¬b } => ¬(b^true)
.∃ a { x } ⋀ b^a => ∃ b { x }
.∃ true { a } => a
.∃ b { x } => ∃ a ⋁ b { x }
.∃ a ⋀ b { x } => ∃ b { x }
.a^true => ∃ a { true }
.∃ a { b } => ∃ true { b }
.∃ true { a } => ¬(false^a)
.a => ∃ true { a }
.∃ true { true }
.a^false
.(a ⋀ b)^c => (a^c ⋀ b^c)
.c^(a ⋀ b) => (c^a ⋁ c^b)
.c^(¬(a == b)) => (c^a == c^b)
.c^(¬(b => a)) => (c^a => c^b)
.c^(a ⋁ b) => (c^a ⋀ c^b)
.(c^a ⋁ c^b) => c^(a ⋀ b)
.¬(c^a == c^b) => c^(a == b)
.¬(c^b => c^a) => c^(a => b)
.(c^a == c^b) => c^(¬(a == b))
.(c^a => c^b) => c^(¬(b => a))
.(c^a ⋀ c^b) => c^(a ⋁ b)
.¬((¬¬a)^b) => (¬a)^b
.(a == b)^c => (a^c == b^c)
.(a => b)^c => (a^c => b^c)
.(a ⋁ b)^c => (a^c ⋁ b^c)
.(a < b)^c => (a^c < b^c)
(a^c ⋀ b^c) => (a ⋀ b)^c
.(a^c == b^c) => (a == b)^c
.¬(a^c == b^c) => (¬(a == b))^c
.¬(a^b) => (¬a)^b
.¬(a^b) ⋀ (a ⋁ ¬a)^true => (¬a)^b
.¬(b^c => a^c) => (¬(b => a))^c
.(a^c ⋁ b^c) => (a ⋁ b)^c
.(b^a : y^x) => ((a : x) => (b : y))
.(b : y)^(a : x) => (b^a : y^x)
.(a^true => b^true) => (false^b => false^a)
.(a^true => b^true) => (false^b => false^a)
.(a == b) ⋀ theory(a == b) => (a ~~ b)
.b^a ⋀ a => ∃ a { b }
.¬¬a ⋀ ¬¬b => ∃ a { b }
.¬¬(false^a) => false^a
.¬¬a => ∃ a { a }
.¬¬a => ∃ true { a }
.¬¬a => ¬(false^a)
.¬¬a => false^(false^a)
.¬¬a => false^(false^a)
.¬¬a ⋀ (a ⋁ ¬a)^true => false^(false^a)
.¬(false^a) => ∃ true { a }
.¬(false^a) => ¬¬a
.¬(false^a) => ¬¬a
.¬(false^a) => false^(false^a)
.¬(false^a) => false^(false^a)
.¬(false^a) ⋀ (a ⋁ ¬a)^true => false^(false^a)
.¬(a^true) ⋀ ¬(false^a) => theory(a)
.¬theory(a)
.false^(a ∧ b) => false^a ⋁ false^b
.false^(a ∧ b) => false^a ⋁ false^b
.false^a ⋁ ¬(false^a)
.¬¬(false^a) ⋁ ¬(false^a)
.false^(x == y) => false^(y == x)
.(false^(a == b) ∧ (b == c)^true) => false^(a == c)
.((a == b)^true ∧ false^(b == c)) => false^(a == c)
.∃ a { false } => false
.∃ false { false } => false
.false^(a ⋁ b) => false^a ∧ false^b
.(false^a ∧ (a == b)^true) => false^b
.false^a => false^(a ∧ b)
.(false^a)^(a^true) ⋀ (a^true)^(false^a) => false
.¬(false^a) => false^(¬a)
.false^(¬a ∧ ¬b) => false^(¬a) ⋁ false^(¬b)
.false^(¬a ∧ ¬b) ⋀ (¬¬a ⋁ ¬a)^true ⋀ (¬¬b ⋁ ¬b)^true => false^(¬a) ⋁ false^(¬b)
.false^a => false^(¬¬a)
.false^(¬¬a) => false^a
.false^(¬¬¬x) => false^(¬x)
.false^(¬a) => ¬¬(a^true)
.false^(¬x) => false^(false^x)
.false^(¬x) => false^(¬¬¬x)
.false^a ⋁ false^(¬a)
.a => false^(false^a)
.false^(false^a) => ¬¬a
.false^(false^a) => ¬(false^a)
.(¬a)^a => false^a
.(¬a)^(¬¬a) => false^(¬¬a)
.false^(¬x) => ¬false^x
.false^b => false^(a ∧ b)
.false^a => (a == false)^true
.false^x => ¬x
.(false^a ∧ false^b) => false^(a ⋁ b)
.false^a => (a ⋁ ¬a)^true
.false^a ∧ (a == b)^true => (b ⋁ ¬b)^true
.false^a => (¬a)^true
.false^uniform(a ∧ b) => false^(uniform(a) ∧ uniform(b))
.false^uniform(a) => (a^true == false^a)
.(¬a)^a => (¬a)^(¬¬a)
.c^a ⋀ c^b => (c^a ⋀ c^b)^d
.(a == b)^true => (a^c == b^c)
.x =^= x
.(b == c)^true => (a^b == a^c)
.(x =^= y) => (y =^= x)
.(x =^= y) => (a == b)^true
.(x =^= y) ⋀ (y =^= z) => (x =^= z)
.(a ⋁ ¬a)^(¬¬a) => a^(¬¬a)
.(a => b)^c => (c^true => b^a)
.a^b ⋀ (a == c)^true => c^b
.a^b ⋀ (b == c)^true => a^c
.a^b => (a^b)^c
.(a^b)^c => a^(b ⋀ c)
.a^b => (¬b)^(¬a)
.¬(a^b) => a^(¬b)
.a^(¬¬b) => (¬¬a)^b
.¬(a^b) => a^(¬b)
.¬(a^b) ⋀ (¬¬a ⋁ ¬a)^true => a^(¬b)
.¬(a^b) ⋀ (a ⋁ ¬a)^true => a^(¬b)
.a => a
.(a^b)^b => a^b
.a^(b ⋀ c) => a^(c ⋀ b)
b^(a^true) => (a^true => b^true)
.b^(a^true) => (b^true)^(a^true)
.b^a => (a => b)
.b^a => (a => b)^c
.b^a => (∃ a { b })^a
.b^a => b^(a^true)
.b^a => (b^true)^(a^true)
.b^a => (a => b)^true
.b^a ⋀ c^b => c^a
.(a : x) ⋀ (b^a : y^x) => (b : y)
.a^(a^false) => a
.(a ~~ b) ∧ (a == c)^true => (c ~~ b)
.(a ~~ b) ∧ (b == c)^true => (a ~~ c)
.~a ∧ (a == b)^true => ~b
.a^true ∧ b^true => (a ∧ b)^true
.(a^true ∧ b^true) => (a == b)^true
.a^true ⋁ ¬(a^true)
.(¬¬a ⋁ ¬a)^true => ((¬¬a)^true ⋁ (¬a)^true)
.(¬¬a ⋁ ¬a)^true => ((¬¬a)^b ⋁ (¬a)^b)
.((a ⋁ ¬a) == (b ⋁ ¬b))^true => ((a == b) ⋁ ¬(a == b))^true
.(a == b) ∧ (a == c) => (c == b)
.(x == y)^true => (y == x)^true
.(a == b)^true => (x =^= y)
.(a == b)^true ∧ (b == c)^true => (a == c)^true
.(a ⋁ ¬a)^true => ¬theory(a)
.(a ⋁ ¬a)^true => (a^true ⋁ (¬a)^true)
.(a ⋁ ¬a)^true => (a^b ⋁ (¬a)^b)
.(a ⋁ ¬a)^true => (¬a ⋁ ¬¬a)^true
.(a ⋁ ¬a)^true => uniform(a)
.(a == true)^true => a^true
.(false^(a == b) ∧ false^(b == c)) => (a == c)^true
.(a ⋀ b)^c => (a^c ⋀ b^c)^true
.c^(a ⋀ b) => (c^a ⋁ c^b)^true
.c^(¬(a == b)) => (c^a == c^b)^true
.c^(¬(b => a)) => (c^a => c^b)^true
.c^(a ⋁ b) => (c^a ⋀ c^b)^true
.(c^a ⋁ c^b)^true => c^(a ⋀ b)
.(¬(c^a == c^b))^true => c^(a == b)
.(¬(c^b => c^a))^true => c^(a => b)
.(c^a == c^b)^true => c^(¬(a == b))
.(c^a => c^b)^true => c^(¬(b => a))
.(c^a ⋀ c^b)^true => c^(a ⋁ b)
.(a == b)^c => (a^c == b^c)^true
.(a => b)^c => (a^c => b^c)^true
.(a ⋁ b)^c => (a^c ⋁ b^c)^true
.(a < b)^c => (a^c < b^c)^true
(a^c ⋀ b^c)^true => (a ⋀ b)^c
.(a^c == b^c)^true => (a == b)^c
.(¬(a^c == b^c))^true => (¬(a == b))^c
.(¬(a^b))^true => (¬a)^b
.(¬(b^c => a^c))^true => (¬(b => a))^c
.(a^c ⋁ b^c)^true => (a ⋁ b)^c
.(b^a : y^x)^true => (b : y)^(a : x)
.(b : y)^(a : x) => (b^a : y^x)^true
.(a => b)^true ∧ (a == c)^true => (c => b)^true
.(a => b)^true ∧ (b == c)^true => (a => c)^true
.(b^a)^true => (a => b)^true
.(c => (a => b))^true => (c^true => b^a)
.(a => b)^true => b^a
.(a => b)^true => b^(a^true)
.(a => b)^true ∧ (b => c)^true => (a => c)^true
.a^true ∧ (a == b)^true => b^true
.(a => b)^true ∧ a^true => b^true
.¬(x^true) => (¬x)^true
.x^true => (¬¬x)^true
.¬(x^true) ⋀ (a ⋁ ¬a)^true => (¬x)^true
.(¬a)^true => false^a
.(a^true ⋁ b^true) => (a ⋁ b)^true
.a^true => (a ⋁ b)^true
.b^true => (a ⋁ b)^true
.false^(¬x) => (¬false^x)^true
.(a == b)^true => (a^c == b^c)^true
.(b == c)^true => (a^b == a^c)^true
.(a => b)^true => (b^a)^true
.(a == b)^true => (~a == ~b)^true
.(a ∧ b)^true => a^true ∧ b^true
.(¬x)^true => ¬(x^true)
.(a ⋁ b)^true => (a^true ⋁ b^true)
.a^true => (a == true)^true
.a^true ⋁ (¬a)^true
.(¬¬a)^true ⋁ (¬a)^true
.a^b ⋁ (¬a)^b
.((¬¬a)^b ⋁ (¬a)^b)
.a^true => false^(¬a)
.a^true => (a ⋁ ¬a)^true
.theory(a) ⋀ (a == b)^true => theory(b)
.theory(¬a) => theory(a)
.theory(a) => ¬(false^a)
.theory(a) => ¬(a^true)
.¬a ⋀ ¬¬b => ¬(a^b)
.true^a
.uniform(a)
.uniform(a) ∧ uniform(b) => uniform(a ∧ b)
.uniform(a ∧ b) => uniform(a) ⋁ uniform(b)
.uniform(a) ∧ uniform(b) => uniform(a ⋁ b)
.uniform(a) ⋀ (a == b)^true => uniform(b)
.uniform(a == a)
.uniform(a == b) => uniform(b == a)
.uniform(a) => (a ⋁ ¬a)^true
.uniform(a == b) ∧ uniform(b == c) => uniform(a == c)
.
Type Definitions
- There exists statement
∃ a { b } := ¬((¬b)^a)
. - A paradoxical proposition
para(a) := false^a
. a^b
.- Power equivalence
=^=
. - A tautological proposition
tauto(a) := a^true
. - A proposition is a theory when non-uniform
theory(a) := ¬(a^true ⋁ false^a)
. - A uniform proposition
uniform(a) := a^true ⋁ false^a
.