[FOM] Clean tautologies

[Lucas Kruijswijk]

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?