Groups | Search | Server Info | Login | Register

Groups > comp.theory > #21400

Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic)

Cross-posted to 4 groups.

Show all headers | View raw

On 7/2/2020 5:00 PM, André G. Isaak wrote:
> On 2020-07-02 14:31, olcott wrote:
>> On 7/2/2020 3:01 PM, olcott wrote:
>>> On 7/2/2020 2:54 PM, André G. Isaak wrote:
>>>> On 2020-07-02 13:19, olcott wrote:
>>>>> The definition of incompleteness:A theory T is incomplete if and 
>>>>> only if there is some sentence φ such that (T ⊬ φ) and (T ⊬ ¬φ).
>>>>>
>>>>> Violates valid/sound deductive inference model:
>>>>> ∀F ∈ Formal_Systems ∀C ∈ WFF(F) ((F ⊢ C)  ↔ True(F, C))
>>>>> ∀F ∈ Formal_Systems ∀C ∈ WFF(F) ((F ⊢ ¬C) ↔ False(F, C))
>>>>> ∀F ∈ Formal_Systems ∀C ∈ WFF(F) ((F ⊬ C)  ↔ NonSequitur(F, C))
>>>>
>>>> As far as I can tell, that entails that if some φ can be proven to 
>>>> be false but cannot be proven to be true, then it is both false and 
>>>> a non-sequitur.
>>>>
>>>> So what is the difference between the two?
>>>>
>>>> André
>>>>
>>>
>>> Ah you got me. I did not encode it the way that I usually do:
>>> ∀F ∈ Formal_Systems ∀C ∈ WFF(F)
>>> (((F ⊬ C) ∧ (F ⊬ ¬C)) ↔ NonSequitur(F, C))
>>
>> Let's try all that using the formal system of Simple_Arithmetic (SA)
> 
> Unless you actually define what you mean by Simple_Arithmetic, the below 
> is entirely meaningless.
> 
> André
> 
>> A := "2 + 3 = 5" (SA ⊢ A)(true)  (SA ⊢ ¬A)(false)
>> B := "2 + 3 = 9" (SA ⊢ A)(false) (SA ⊢ ¬A)(true)
>> B := "2 # 3 = 9" (SA ⊢ A)(false) (SA ⊢ ¬A)(false)
>>
>> Since Simple_Arithmetic cannot express self-contradictory sentences 
>> the only finite strings that cannot be proved or disproved in the 
>> system are strings that are not WFF.
>>

I have a whole C++ program for people that disingenuously claim that 
they can't begin to understand that "2 + 3 = 5" is true "2 + 3 = 9" is 
false and "2 # 3 = 9" is gibberish.

/**
   Truth-conditional semantics is an approach to semantics of natural
   language that sees meaning (or at least the meaning of assertions)
   as being the same as, or reducible to, their truth conditions.
   https://en.wikipedia.org/wiki/Truth-conditional_semantics

   This program demonstrates [truth conditional semantics] for a very
   tiny subset of analytic knowledge. It can only evaluate finite strings
   matching this AWK regular expression: /[0-4]\+[0-4]=[0-8]/

   The finite string transformation rules specified by this source-code
   provide the means to formally prove whether a finite string of the
   language of the Tiny_Arithmetic formal system has the semantic property
   of Boolean true.

   This AWK regular expression: /[0-9]+[\+*][0-9]+[=][0-9]+/ specifies
   the entire language of the Simple_Arithmetic Sound Deductive Formalist
   formal system.
**/

#include <cstdio>
#include <string>
#include <vector>
#include <fstream>
#include <iostream>
#include <sstream>
#include <iomanip>


char   ADD_Digit[58][58];
char   ADD_Carry[58][58];
char  MULT_Digit[58][58];
char  MULT_Carry[58][58];


void DebugString(std::string& S)
{
   for (int N = 0; N < S.length(); N++)
     printf("[%d]{%c}{%02d}\n", N, S[N], S[N]);
}

int LengthOfNumericString(std::string S)
{
   int N;
   if (S.length() == 0)  // This should never occur
     return 0;
   if (S[0] > '0')
     return(S.length());
   // Skip Leading Zeroes
   for (N = 0; N < S.length() && S[N] == '0'; N++)
     ;
   if (N == S.length())  // All Zeroes
     return 1;
   return (S.length() - N);
}

bool Numeric_Less_Than(std::string& OP1, std::string& OP2)
{
   if (LengthOfNumericString(OP1) < LengthOfNumericString(OP2))
     return true;
   if (LengthOfNumericString(OP1) > LengthOfNumericString(OP2))
     return false;
   return (OP1 < OP2);
}


bool Numeric_Greater_Than(std::string& OP1, std::string& OP2)
{
   if (LengthOfNumericString(OP1) > LengthOfNumericString(OP2))
     return true;
   if (LengthOfNumericString(OP1) < LengthOfNumericString(OP2))
     return false;
   return (OP1 < OP2);
}


void PrependPadding(std::string& S, int Width)
{
   std::string Zeroes;
   for (int N = 0; N < Width; N++)
     Zeroes += '0';
   S = Zeroes + S;
}


void MakeSameLength(std::string& OP1, std::string& OP2)
{
   if (OP1.length() > OP2.length())
     PrependPadding(OP2, OP1.length() - OP2.length());
   else if (OP1.length() < OP2.length())
     PrependPadding(OP1, OP2.length() - OP1.length());
}


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;
}

void SkipSpace(int& N, std::string& Input)
{
   while(N < Input.length() && Input[N] == ' ' || Input[N] == '\t')
     N++;
}


void GetDigitString(int& N, std::string& S, std::string& Input)
{
   SkipSpace(N, Input);
   while(N < Input.length() && Input[N] >= '0' && Input[N] <= '9')
     S += Input[N++];
}


void GetRelationalOperator(int& N, int& Operator, std::string& Input)
{
   SkipSpace(N, Input);
//if (Input[N] == '=' || Input[N] == '<' || Input[N] == '>')
   if (Input[N] == '=')
     Operator = Input[N++];
}


void ProveInput(std::string& OP1,
                 std::string& OP2,
                 std::string& SUM)
{
   std::string RESULT;
//  printf("%s + %s %c %s---",
//         OP1.c_str(), OP2.c_str(), Relational_OP, SUM.c_str());
     MakeSameLength(OP1, OP2);
     RESULT = Add(OP1, OP2);
     printf("\"%s + %s = %s\" ",
            OP1.c_str(), OP2.c_str(), SUM.c_str(), RESULT.c_str());

     if (RESULT == SUM)
       printf("is proven and true!\n");

     else if (Numeric_Less_Than(RESULT, SUM))
       printf("is disproven and false!\n");

     else if (Numeric_Greater_Than(RESULT, SUM))
       printf("is disproven and false!\n");

     else
       printf("is unproven and untrue!\n");
}


bool ParseInput(std::string Input)
{
std::string OP1;
std::string OP2;
std::string SUM;
char ErrorCount = 0;
int Relational_OP = 0;

   int N = 0;
   int MaxLength = Input.length();
   GetDigitString(N, OP1, Input);
   if (OP1.length() == 0)
     ErrorCount++;

   SkipSpace(N, Input);
   if (Input[N++] != '+')
     ErrorCount++;

   GetDigitString(N, OP2, Input);
   if (OP2.length() == 0)
     ErrorCount++;

   GetRelationalOperator(N, Relational_OP, Input);
   if (Relational_OP == 0)
     ErrorCount++;

   GetDigitString(N, SUM, Input);
   if (SUM.length() == 0)
     ErrorCount++;

   if (ErrorCount)
     printf("[%s] ParseError(%d)\n", Input.c_str(), ErrorCount);
   else
     ProveInput(OP1, OP2, SUM);

   return (ErrorCount == 0);
}


void InitSumDigits()
{
   for (char D1 = '0'; D1 <= '9'; D1++)
     for (char D2 = '0'; D2 <= '9'; D2++)
     {
       char Sum  = (D1-'0')+(D2-'0');
       char Mult = (D1-'0')*(D2-'0');
         ADD_Digit[D1][D2]  = (Sum % 10)  + '0';
         ADD_Carry[D1][D2]  = (Sum / 10)  + '0';
        MULT_Digit[D1][D2]  = (Mult / 10) + '0';
        MULT_Carry[D1][D2]  = (Mult % 10) + '0';

//    printf("%c + %c = %c%c ---- ", D1, D2, ADD_Carry[D1][D2], 
ADD_Digit[D1][D2]);
//    printf("%c * %c = %c%c\n", D1, D2, MULT_Digit[D1][D2], 
MULT_Carry[D1][D2]);
     }
}


// main() returns void to reduce clutter
void main(int argc, char *argv[])
{
   InitSumDigits();

   if (argc == 2)
//  GetLines(argv[1]);
     ParseInput(argv[1]);
   else
     printf("Enter Quoted Equality Expression line this: \"2 + 3 = 5\"\n");
}





-- 
Copyright 2020 Pete Olcott

Back to comp.theory | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Simply defining Gödel Incompleteness and Tarski Undefinability away V20 olcott <NoOne@NoWhere.com> - 2020-07-02 14:19 -0500
  Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 André G. Isaak <agisaak@gm.invalid> - 2020-07-02 13:54 -0600
    Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 olcott <NoOne@NoWhere.com> - 2020-07-02 15:01 -0500
      Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 André G. Isaak <agisaak@gm.invalid> - 2020-07-02 14:28 -0600
        Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) olcott <NoOne@NoWhere.com> - 2020-07-02 16:01 -0500
        Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 olcott <NoOne@NoWhere.com> - 2020-07-02 16:50 -0500
          Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 olcott <NoOne@NoWhere.com> - 2020-07-02 17:10 -0500
      Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) olcott <NoOne@NoWhere.com> - 2020-07-02 15:31 -0500
        Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) olcott <NoOne@NoWhere.com> - 2020-07-02 15:56 -0500
        Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) André G. Isaak <agisaak@gm.invalid> - 2020-07-02 16:00 -0600
          Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) olcott <NoOne@NoWhere.com> - 2020-07-02 17:14 -0500
            Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) Keith Thompson <Keith.S.Thompson+u@gmail.com> - 2020-07-02 18:41 -0700
              Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) olcott <NoOne@NoWhere.com> - 2020-07-02 21:03 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) Keith Thompson <Keith.S.Thompson+u@gmail.com> - 2020-07-02 21:17 -0700
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) olcott <NoOne@NoWhere.com> - 2020-07-03 00:33 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) André G. Isaak <agisaak@gm.invalid> - 2020-07-02 23:10 -0600
            Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) André G. Isaak <agisaak@gm.invalid> - 2020-07-02 23:24 -0600
              Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) olcott <NoOne@NoWhere.com> - 2020-07-03 01:00 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) André G. Isaak <agisaak@gm.invalid> - 2020-07-03 01:02 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) olcott <NoOne@NoWhere.com> - 2020-07-03 12:56 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 (Simple_Arithmetic) André G. Isaak <agisaak@gm.invalid> - 2020-07-03 12:17 -0600

csiph-web