The Math Forum

Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Math Forum » Discussions » sci.math.* » sci.math

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Racing Proofs as a salvage of Naive Set Theory
Replies: 1   Last Post: Apr 10, 2013 3:28 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]

Posts: 2,665
Registered: 6/29/07
Racing Proofs as a salvage of Naive Set Theory
Posted: Apr 10, 2013 2:19 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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

(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.


Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© The Math Forum at NCTM 1994-2018. All Rights Reserved.