Groups | Search | Server Info | Login | Register

Groups > comp.theory > #21380

Simply defining Gödel Incompleteness away V19

Cross-posted to 4 groups.

Show all headers | View raw

Stanford Encyclopedia of Philosophy
considers this as a reasonable approximation of the Gödel sentence:
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
(G) F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉)

If we assume a formal system contains Robinson's arithmetic and has its 
own provability operator then a proof with arithmetization and a proof 
without arithmetization would only vary syntactically and not semantically.

If the two proofs are syntactically different yet semantically identical 
then their provability would be logically equivalent.
(a) F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉)
(b) F ⊢ G_F ↔ (F ⊬ G)

// The formal system of Simple_Arithmetic is defined below
// and has its own provability predicate

You can prove that a true statement is true:
"2 + 3 = 5" ↔ (F ⊬ "2 + 3 = 5")
LHS of ↔ is true.   RHS of ⊬ is true.  RHS of ↔ is false.

You can prove that a false statement is not true:
"2 + 3 = 9" ↔ (F ⊬ "2 + 3 = 9")  LHS of ↔ is false.
RHS of ⊬ is false. RHS of ↔ is true.

Thus there does not exist any WFF G of any formal system F that is 
logically equivalent to it own unprovability because this is 
self-contradictory.

This exact same reasoning applies to (a) because (a) and (b) only vary 
syntactically and not semantically thus must have logically equivalent 
provability.


/****************************************************************************

    This is the formal system of Simple_Arithmetic implemented
    as a membership algorithm on finite strings matching this
    AWK regular expression: /[0-9]+[\+][0-9]+[=][0-9]+/

****************************************************************************/ 



char AddWithCarry(char D1, char D2, char& Carry)
{
   char SUM = ADD_Digit[D1][D2];
   if (Carry == '1' && SUM == '9')
   {
     SUM = '0';
     Carry = '1';
   }
   else if (Carry == '1' && SUM < '9')
   {
     SUM = ADD_Digit[SUM][Carry];
     Carry = ADD_Carry[D1][D2];
   }
   else // Carry == '0'
     Carry = ADD_Carry[D1][D2];
   return SUM;
}


std::string Add(std::string& OP1, std::string& OP2)
{
   std::string SUM;
   char Carry = '0';
   for (int N = OP1.length() - 1; N >= 0; N--)
     SUM += AddWithCarry(OP1[N], OP2[N], Carry);
   if (Carry == '1')
     SUM += '1';
   std::reverse(SUM.begin(), SUM.end());
   return SUM;
}


//
// (Proven && True) || (Unproven && Untrue)
//
bool ProveInput(std::string& OP1,std::string& OP2, std::string& SUM)
{
   std::string RESULT;
   RESULT = Add(OP1, OP2);
   return (RESULT == SUM);
}


-- 
Copyright 2020 Pete Olcott

Back to comp.theory | Previous | Next | Find similar

Thread

Simply defining Gödel Incompleteness away V19 olcott <NoOne@NoWhere.com> - 2020-07-01 21:18 -0500

csiph-web