[FOM] Clean tautologies
L.B.Kruijswijk at inter.nl.net
Tue Apr 20 15:35:40 EDT 2010
I am busy with a kind of reduction algorithm and
I encountered an interesting subset of tautologies.
I like to know whether this is "known science",
because I don't want to re-invent the wheel.
I call the subset "clean tautologies". A clean
tautology is defined as follows:
- It is propositional theorem.
- It is a tautology.
- For any appearing propositional variable,
a proper subset of appearances can not be replaced
by a new propositional variable, while retaining the
property of tautology.
a -> a, is a clean tautology, because if one a is replaced
by b, you get a -> b or b -> a and both are not a tautology.
(a /\ (a -> a)) -> a
is a tautology but not a clean one, because the middle
two appearances can be replaced by a new variable,
while it is still a tautology:
(a /\ (b -> b)) -> a
In a propositional proof system, if the axiom schemes
are only instantiated to clean tautologies, then any
theorem produced by the proof system, is also a clean
Example, if the proof system contains the following
p -> p \/ q
Then it may not be instantiated to the non-clean
p -> p \/ p
If someone has encountered this, then I like to know,
otherwise I investigate it by myself.
Hilbert's program contains hard tests, which are mostly
proven to be impossible. Is there any hard test that can
More information about the FOM