Suggestion: Revising the proof of Gödel's Completeness Theorem

I would like to propose some changes to GOEDELCP, which contains a proof of Gödel's completeness theorem for first-order logic. Specifically, I would like to suggest changes to the proof of the last theorem:

0.

still_not-bound_in X is finite & X |= p implies X |- p

The current proof of this theorem contains proofs of a few lemmas that I believe can profitably be taken out of the proof. Namely, I propose adding three lemmas before the completeness theorem is stated:

1.

J,v |= X & Y c= X implies J,v |= Y

2.

still_not-bound_in X is finite implies still_not-bound_in (X \/ {p}) is finite

3. X |= p implies not J,v |= X \/ {'not' p}

Lemma 1 is a generalization of a theorem that currently exists only inside the current proof of theorem 0. The current proof of theorem 0 uses lemma 1 twice: in the first use,

X := X \/ {'not' p}

and

Y := X

; in the second use,

X := X \/ {'not' p}

and

Y := {'not' p}

. The two uses are contained in this block of the proof:

        now assume A3: J,v |= X \/ {'not' p};
          now let q such that A4: q in X;
            X c= X \/ {'not' p} by XBOOLE_1:7;
            hence J,v |= q by A3,A4,CALCUL_1:def 11;
          end; then
          J,v |= X by CALCUL_1:def 11;
          now let q such that A6: q in {'not' p};
            {'not' p} c= X \/ {'not' p} by XBOOLE_1:7;
            hence J,v |= q by A3,A6,CALCUL_1:def 11;
          end; then
          J,v |= {'not' p} by CALCUL_1:def 11;

I would like to suggest that this proof block be replaced by

        now assume J,v |= X \/ {'not' p};
            X c= X \/ {'not' p} by XBOOLE_1:7;
            then J,v |= X by 1;
            {'not' p} c= X \/ {'not' p} by XBOOLE_1:7;
           then J,v |= {'not' p} by 1;

This new block is 5 lines long; the original block is 11.

The interpretation judgments

J,v |= {'not' p}

and

J,v |= X

are established to prove

not J,v |= X \/ {'not' p}

. The only hypothesis used to prove that negation is the tautological implication

X |= p

. This observation is the origin of lemma 3. My proof of lemma 3 (included below) uses lemma 1.

Finally, lemma 2 allows us to replace the block

      still_not-bound_in 'not' p is finite by CQC_SIM1:20; then
      still_not-bound_in {'not' p} is finite by Th26; then
      still_not-bound_in X \/
      still_not-bound_in {'not' p} is finite by A1,FINSET_1:14; then
      still_not-bound_in CX is finite by Th27; 

in the proof of theorem 0 by the single line

      still_not-bound_in CX is finite by A1,2;

Finally, here are the proofs of lemmas 1, 2, and 3. I call them Th35, Th36, and Th38 to facilitate copy and paste into goedelcp.miz for checking.

theorem
  Th35:  J,v |= X & Y c= X implies J,v |= Y
  proof
    assume A2: J,v |= X;
    assume A1: Y c= X;    
    p in Y implies J,v |= p
    proof
      assume p in Y;
      then p in X by A1;
      hence thesis by A2,CALCUL_1:def 11;
    end;
    hence thesis by CALCUL_1:def 11;
  end;
  
theorem
  Th36: still_not-bound_in X is finite implies still_not-bound_in (X \/ {p}) is finite
  proof
    assume A0: still_not-bound_in X is finite;
    still_not-bound_in p is finite by CQC_SIM1:20;
    then still_not-bound_in {p} is finite by Th26;
    then still_not-bound_in X \/ still_not-bound_in {p} is finite by A0,FINSET_1:14;
    hence thesis by Th27;
  end;
  
theorem
Th37:  X |= p implies not J,v |= X \/ {'not' p}
  proof
    assume A1: X |= p;
    assume A2: J,v |= X \/ {'not' p};
    X c= X \/ {'not' p} by XBOOLE_1:7;
    then A3: J,v |= X by A2,Th35;
    {'not' p} c= X \/ {'not' p} by XBOOLE_1:7;
    then A4: J,v |= {'not' p} by A2,Th35;
    'not' p in {'not' p} by TARSKI:def 1;
    then J,v |= 'not' p by A4,CALCUL_1:def 11;
    then not J,v |= p by VALUAT_1:28;
    hence contradiction by A1,A3,CALCUL_1:def 12;
  end;

A new proof of theorem 0 can then be given:

theorem
  still_not-bound_in X is finite & X |= p implies X |- p
  proof
    assume A0: still_not-bound_in X is finite;
    assume A1: X |= p;
    assume A2: not X |- p;
    reconsider Y = X \/ {'not' p} as Subset of CQC-WFF;
    A3: still_not-bound_in Y is finite by A0,Th36;
    A4: for A,J,v holds not J,v |= Y by A1,Th37;
    A5: Y is Consistent by A2,HENMODEL:9;
    consider CZ,JH1 such that A6:JH1,valH |= Y by A3,A5,Th34;
    thus contradiction by A4,A6;
    hence thesis;
  end;

The new proof has the advantage of being shorter and illustrating the idea of the proof more clearly.

-- JesseAlama - 13 Dec 2004

Article name:	GOEDELCP
MML version:	4.20.885

|

Follow up