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.