# [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.

Example:

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.

However,

(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

Hypothesis:

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

tautology.

Example, if the proof system contains the following

axiom scheme:

p -> p \/ q

Then it may not be instantiated to the non-clean

tautology:

p -> p \/ p

If someone has encountered this, then I like to know,

otherwise I investigate it by myself.

Regards,

Lucas Kruijswijk

Hilbert's program contains hard tests, which are mostly

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

falsify Platonism?

```