[FOM] Clean tautologies

Lucas Kruijswijk L.B.Kruijswijk at inter.nl.net
Tue Apr 20 15:35:40 EDT 2010

Dear all,


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

axiom scheme:

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.




Lucas Kruijswijk


Hilbert's program contains hard tests, which are mostly

proven to be impossible. Is there any hard test that can

falsify Platonism?

More information about the FOM mailing list