But it's not true in intuitionistic logics.
I have not studied intuitionist logic yet, but...
I believe that intuitionist logic defines 'not' as not proven rather than negation.
If (p v ~p) means, p is provable or p is not provable, then (p v ~p) is not tautologous.
I also believe that Tarski and McKinley (1948) have shown that intuitionist logic is a special case of modal logic (S2).
Do you think we can reduce intuitionist logic to modal logic?
---------- Post added 06-07-2010 at 04:40 AM ----------
So not-a implies that a implies b? I don't see why.
~p -> (p -> q), is a tautology, ie. it is true for all values of the variables p and q.
(~p -> (p -> q)) iff (p v (~p v q)), because (p -> q) =df (~p v q).
(p v (~p v q) iff (p v ~p) v q, because (p v ( q v r)) <-> ((p v q) v r), is a theorem.
We can 'calculate' the truth value of ~p -> (p ->q) by exhausting the possible truth values of p and q.
T=true, F=false, ~T=F, ~F=T.
~T -> (T -> T), is true because (F -> T) is true. ie. (T v T)=T.
~T -> (T -> F), is true because (F -> F) is true. ie. (T v F)=T.
~F -> (F -> T), is true because (T -> T) is true. ie. (F v T)=T.
~F -> (F -> F), is true because (T -> T) is true. ie. (F v T)=T.
((p & ~p) -> q) iff ((~p v p) v q), but (~p v p)=T, that is, (T v q)=T
That is to say, (p & ~p) implies any proposition q, is a tautology.
Also: (~p -> (p ->q)) <-> ((p & ~p) -> q), is true.
This sense of 'logical arithmetic' is prior to 'numerical arithmetic' and might fit your pursuit of fundamental calculations.
I believe that we can extend these 'simple' calculations of propositional logic to include predicate logic, by the definition:
(some x)(Fx) =df (Fa v Fb v Fc ...).
That is to say, we can reduce predicate logic to propositional logic.
What do you think about this possible simplification of predicate logic?