Math Forum Discussions

Zaljohar@gmail.com

Posts: 2,665
Registered: 6/29/07

Racing Proofs as a salvage of Naive Set Theory
Posted: Apr 10, 2013 2:19 PM

Plain Text

Racing proofs, is a topic that I was trying to define, whereby proofs
are sorted into two sorts: Trivial proofs, Non trivial proofs.

Now we take the set of all logical validities in first order logic
with identity (identity axioms to be considered among the logical
axioms) and membership "FOL(=,e)" to be among the sentences of our
theory T. Then we add to this set all statements that are provable by
non trivial proofs from Naive comprehension.

The idea is to find a criterion of non triviality of proofs such that
theory T is consistent (in the sense that a model exist for T).

Now lets call the set of all validities in FOL(=,e) as "VLD".
Lets call the additional set of theorems proved by non trivial proofs
from Naive comprehension as "ADD" (short for additional).

A preliminary trial to define non triviality of proofs is the
following:

(1) Must not end up proving a validity or a negation of a validity.
(2) Must not end up proving a statement that has already (by a shorter
proof) been proved or been disproved.
(3) Must not end up proving a statement that has been proved already
(by a shorter proof) to be equivalent to a statement that has already
(by a shorter proof) been proved or been disproved
(4) Must not contain an initial n-2 steps that are the same of a proof
that ends up with the opposing statement.

We can lay down restrictions on the language such that at each n we
only have *finitely* many n-sized proofs. So the above can be imaged
to occur on a stepwise basis.

I think this would generally fail, but IF (and this is a big if) we
can somehow calculate the shortest size proof of equivalence of any
theorem proved by n-sized proof with a theorem (or its negation)
proved by m-sized proof, then we might be able to secure a consistent
theory T, provided we eliminate the possibility of having two opposing
non trivial theorems of the SAME length, but I think we still can take
the shorter one (the one with the less symbols) if such equi-length
proved opposing theorems should exist.

Anyhow the computation of all of these is taxing if not impossible.

Zuhair