A proof that ZFC is inconsistent.

[DV]

Given as theorems of ZFC (proofs and definitions omitted):

1 ZFC is inconsistent —-> PROOFS is an element of C (constant-time)

2 [deleted — ignore this line]

3 [deleted — ignore this line]

4 FP-SAT is not an element of C

5 ZFC is consistent —> FP-SAT reduces to PROOFS in C

6 FP-SAT reduces to PROOFS in C —> (PROOFS is an element of C —> FP-SAT is an element of C)


We want to show:

ZFC is inconsistent.


Proof.

7 ~(PROOFS is an element of C) —> (ZFC is consistent)

contraposition of (1).

8 (|- (PROOFS is not an element of C)) —> (|- (ZFC is consistent))

Assume: (|- (PROOFS is not an element of C)). We have from (7) that: (PROOFS is not an element of C) —> (ZFC is consistent). Further, because (7) is a theorem of ZFC, we have that: |- ( ~(PROOFS is an element of C) —> (ZFC is consistent) ). Thus, by our assumption, the immediately preceding statement, and modus ponens, we have: |- (ZFC is consistent). By the deduction theorem, we obtain (|- (PROOFS is not an element of C)) —> (|- (ZFC is consistent)). QED.

9 (|- (ZFC is consistent)) —> (ZFC is inconsistent)

Godel’s Second Incompleteness Theorem.

10 (|- (PROOFS is not an element of C)) —> ZFC is inconsistent

Assume (|- (PROOFS is not an element of C)). Then by that, (8), and m.p., we obtain (|- (ZFC is consistent)). By that statement, (9), and m.p., we obtain (ZFC is inconsistent). By the deduction theorem, we obtain: (|- (PROOFS is not an element of C)) —> ZFC is inconsistent . QED.

11 ZFC is consistent —> ~(|- (PROOFS is not an element of C))

contraposition of (10).

12 ZFC is consistent —> (PROOFS is an element of C —> FP-SAT is an element of C)

Assume ZFC is consistent. By m.p. and (5), we obtain (FP-SAT reduces to PROOFS in C). By that, (6), and m.p. we obtain (PROOFS is an element of C —> FP-SAT is an element of C). By that and the deduction theorem, we obtain ZFC is consistent —> (PROOFS is an element of C —> FP-SAT is an element of C). QED.

13 (PROOFS is an element of C —> FP-SAT is an element of C) —> (FP-SAT is not an element of C —> PROOFS is not an element of C)

contraposition.

14 ZFC is consistent —> (FP-SAT is not an element of C —> PROOFS is not an element of C)

modus ponens and deduction theorem (like previous arguments), (12) and (13).

15 ZFC is consistent —> ( ((ZFC is consistent) |- (FP-SAT is not an element of C)) —> ( |- ((ZFC is consistent) -> (PROOFS is not an element of C))))

Assume ZFC is consistent. Now assume ((ZFC is consistent) |- (FP-SAT is not an element of C)) . By the deduction theorem, we obtain: |- (ZFC is consistent) —> (FP-SAT is not an element of C) . By modus ponens, and our first assumption, we obtain: |- (FP-SAT is not an element of C) . We have already derived (14), thus we have: |- (ZFC is consistent —> (FP-SAT is not an element of C —> PROOFS is not an element of C)) . Next, we use the two preceding statement and Corollary (b) (Mendelson, Intro to Math Logic, 5th Edition) of the deduction theorem to obtain: |- (ZFC is consistent) -> (PROOFS is not an element of C) . By two applications of the deduction theorem (based on our two assumptions at the beginning), we obtain: ZFC is consistent —> ( ((ZFC is consistent) |- (FP-SAT is not an element of C)) —> (|- ((ZFC is consistent) -> (PROOFS is not an element of C)))) . QED.

16 ZFC is consistent —> |- (PROOFS is not an element of C)

Assume ZFC is consistent. Then by our assumption, (15), and m.p., we obtain: ( ((ZFC is consistent) |- (FP-SAT is not an element of C)) —> ( |- ((ZFC is consistent) -> (PROOFS is not an element of C)))) . By (4), we can easily add an unnecessary assumption to obtain (ZFC is consistent) |- (FP-SAT is not an element of C). By the two preceding statements and m.p., we obtain: ( |- ((ZFC is consistent) -> (PROOFS is not an element of C))) . By the first assumption—that ZFC is consistent—and the immediately preceding statement, we obtain: |- PROOFS is not an element of C. Ultimately, by the deduction theroem, we have: ZFC is consistent —> |- PROOFS is not an element of C.

17 ZFC is inconsistent

Assume ZFC is consistent. By (11) we have: ZFC is consistent —> ~(|- (PROOFS is not an element of C)) . By (16) we have: ZFC is consistent —> (|- (PROOFS is not an element of C)) . By m.p., our assumption, and (11), we obtain: ~(|- (PROOFS is not an element of C)) . By m.p., our assumption, and (16), we obtain: (|- (PROOFS is not an element of C)). This is a contradiction. Thus, by the deduction theorem, contraposition, and modus ponens, we have ZFC is inconsistent.

QED.





--Philip White

[DV]

As I have said elsewhere, I argue that the proof above means that we must re-work ZFC to ensure that GIT1 and GIT2 cannot be proved.

Interestingly, if this theorem is removed from the proof, we can still obtain a very interesting result:

ZFC is consistent —> |- ZFC is consistent

In other words, if we alter the formal theory to what we might term ZFC*, this new theory will be consistent only if its consistency can be proved within this formal theory.

One interesting question about this is: What does that say about the continuum hypothesis?

Also as I said elsewhere, the way to fix logic is probably to ban Godel numberings—perhaps by making formulas that contain functions that map to or from other functions be designated as not well-formed.

For those curious about my activities: I am still studying logic—I’ve finished reading Chapter 1 of Mendelson thoroughly (I’m trying to read 10 pages a day or work 10 exercises a day, alternating days—the first of those two things I have managed, but 10 exercises in a day is too hard for me right now given the difficulty of the later exercises in Ch. 1), and have worked all of the first 30 exercises. My current goal has changed again: I am interested in pursuing graudate mathematics studies at a top-ranked university. I will investigate this more later—ideally after the end of the crazy ordeal involving me being illegally surveilled by the NSA.

-Philip

[DV]

By the way, to clarify:

PROOFS is the language of ZFC wfs with unary proof tape where the wf has a proof that fits on the tape, with special characters alpha and theta enabled. The character alpha is a single-character shorthand symbol that stands for the theorem being proved in the wf. The character represents a proof (list of theorems) that establishes a contradiction in ZFC, if there is one, or the null string if there is no such contradiction.

FP-SAT stands for "formatted and padded SAT." It's basically a language that represents only SAT instances as ZFC wfs; it's pre-formatted and padded with the appropriate number of special blank symbols so that it can be mapped to an instance of PROOFS in a single cycle--the TM just accepts immediately, given a valid instance of FP-SAT. The idea is that FP-SAT is NP-complete and not solvable in constant-time, but also able to be reduced to PROOFS in constant-time, assuming that ZFC is consistent of course.

[DV]

I just realized that there is a minor, fixable problem in the proof above.

The logic in lines 7-17 is correct. The problem is with the assertion of...

(5) ZFC is consistent —> FP-SAT reduces to PROOFS in C

The problem is, the one-cycle reduction requires that the instance of FP-SAT be a genuine instance of SAT, and not (e.g.) some other wf.

The way around this is: We simply include a very specific "rejection oracle" in our model of the UTM. The rejection oracle enables any Turing machine to visit a specific oracle state that will automatically reject any instance of FP-SAT that is not a legitimate SAT instance in 1 cycle. This enables us to build a slightly more complex (time-wise) algorithm that is still constant time that maps all FP-SAT instances to PROOFS in a few cycles.

The idea is (assuming a 2-tape model of the TM) given some legitimate SAT instance, we query the rejection oracle, see that the instance is legitimate, and do not change it, and accept.

If the instance is not a real SAT instance, then we "ruin" it as a provable wf by adding (say) 5 characters to the instance that ensure that it is not a valid wf. Now it certainly has no proof in ZFC. (See the note at the bottom of this post about the other rejection oracle.)

This fixes the problem with the proof. Note, none of the other proofs are rendered ineffective by our modification to the UTM.

- - -

By the way, to prove...

(4) FP-SAT is not an element of C

...we first assume f.s.o.c. that FP-SAT is an element of C. Then there exists a natural-valued k s.t. a TM M decides FP-SAT in k cycles. Let j = the smallest such value k. Then we devise a satisfiable 3CNF SAT instance X1 with j clauses s.t. X1 is satisfiable. Then we concatenate two more contradictory clauses to X1 (e.g., "(z1 v z1 v z1) ^ (~z1 v ~z1 v ~z1)") to form X2, an unsatisfiable SAT instance. Distinguishing between X1 and X2 requires more than j cycles. This is a contradiction, so FP-SAT is not an element of C.


I'm omitting the other proofs for now. The proof of (1) involves showing that every ZFC wf has the same string (including alpha and theta) as its proof. Note, we'll need one additional rejection oracle to eliminate bad wfs from consideration in the PROOFS language.

[DV]

There may be some (mild) NSA typo interference in my writing above.

In particular, I meant to say, "non-wfs," not "bad wfs."

[DV]

Another quick comment: We must make sure that the UTM is defined in such a way that the oracle tape begins with a copy of the input. That way, we don't have to spend a linear amount of time copying the input tape to the oracle tape to use the oracle. Also, I am not using the idea of a tape head that can move around the tape freely; the tape head must move strictly one square to the left, one square to the right, or stay in place, at any time. It is a two-tape, two-tape-head model of the TM, where as I said the second tape is the oracle tape.

- - -

Update on my studying activities (not that anyone necessarily cares): I have cut back to 2 challenging and relevant exercises per day, with each of the daily two exercises selected from a 10-page section of the book. Many of the exercises are hard. I've been working 3 hours a day, alternating between 10+ pages of reading and as many exercises as I can do. I decided to cut back to 2 exercises / day as of today, because I'm on page 67 with reading, but only page 21 with exercises. So, I will not be working all exercises in the textbook right now.

[DV]

My best idea (so far) for fixing the inconsistency in ZFC is as follows:

Short version: Ban assertions about unprovability when using modus ponens, i.e., given formulas A, A—>B, no sub-formula of A may be logically equivalent to wf H(x2), where H(x2) = (forall x1) ~Pf(x1,x2) .

The challenge is, how do you tell if a particular wf is logically equivalent to another wf? You have to prove it, and that’s not always easy.

I suggest the following: Use the predicate calculus (which is provably consistent and thus may be utilized fully, with modus ponens included without pre-conditions) to try to prove that none of the subformulas and H(x2) are logically equivalent. If such a proof can be found, accept the logical inequivalences, and allow modus ponens to be applied for this one deduction in ZFC* as I am calling it. If no such proof is found, modus ponens cannot be used in ZFC* (until a proof is found).


What do I mean by “sub-formula?” Basically, do this process:

Given A, A—>B: We must prove that “no sub-formula C of A” is such that C <—> H(x2). I.e., we must prove: ((~C) <—> H(x2)), for all sub-formulas C of A. A subformula of a formula is defined as follows:

A is a subformula of A
If A is of the form D —> E, then D and E are both subformulas of A.
If A is of the form ~D, then D is a subformula of A.
If A is of the form (forall x_i) D, then D is a subformula of A.
Any subformulas of a subformula of A are also subformulas of A

(We assume that —> and ~ are the only connectives for now, and of course quantifiers are allowed, too.)

Note, for all free variables of A and all of its subformulas C, we must consider the possibility that x2 could be substituted for each such free variable in C. So for each subformula C, we must consider all versions of C (call them C’, C’’, ...) with x2 substituted for one free variable at a time in the subformula. Also note, the process of generating all versions of all subformulas of A is polynomial time. The hard part is proving all of the equivalences (or inequivalences, depending on how you want to think about it).

Finally, I am still studying logic, and not sure that this idea works perfectly. In particular, there is no way at all to prove that G (the Godel sentence) will remain unprovable in the event that this change is put in place. Right now, I am just sharing some thoughts.

-Philip