Groups | Search | Server Info | Login | Register

Groups > comp.theory > #21419

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/3/2020 2:02 AM, André G. Isaak wrote:
> On 2020-07-03 00:00, olcott wrote:
>> On 7/3/2020 12:24 AM, André G. Isaak wrote:
>>> On 2020-07-02 16:14, olcott wrote:
>>>> 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.
>>>
>>> That C++ program is a computer program, not a formal system. It is 
>>> possible that it instantiates some formal system called SA, but 
>>> unless you actually provide us with such a formal system we'll never 
>>> know.
>>>
>>
>> The C++ IS the formal system implemented as a recursive language with 
>> a membership algorithm.
>>
>>      A language L on Σ is said to be recursive if there exists a
>>      Turing machine M that accepts L and halts on every w in Σ+.
>>      In other words, a language is recursive if and only if there
>>      exists a membership algorithm for it. (Linz 1990:288).
>>
>> /**
>>    This AWK regular expression: /[0-9]+[\+*][0-9]+[=<>][0-9]+/
>>    specifies the entire language of the Simple_Arithmetic.
>>
>>    This source file implements a member function that decides
>>    whether or not an arbitrary finite string is a theorem of
>>    the formal system of Simple_Arithmetic (SA).
>> **/
>>
>>> If I were to attempt to guess what SA is supposed to be based on this 
>>> program, all I can come up with is some system which doesn't satisfy 
>>> the conditions which Gödel sets out in his proof. Gödel's theorem 
>>> only applies to formal systems in which a certain minimal amount of 
>>> arithmetic can be performed and, AFAICT, your SA doesn't come close 
>>> to meeting that minimal threshold. 
>>
>> You are probably right there.
>>
>>> Ergo, it is entirely irrelevant to any discussion of Gödel.
>>
>> You are wrong there. It provides the basis for redefining the notion 
>> of a formal system as implementing the sound deductive inference model 
>> which in turn eliminates both Incompleteness and Undefinability.
>>
>> The conventional definition of incompleteness:
>> A theory T is incomplete if and only if there is some sentence φ such 
>> that (T ⊬ φ) and (T ⊬ ¬φ).
>>
>> When construed within the sound deductive inference model:
>> ∀Γ ⊆ T ∀φ WFF(T) ((Γ ⊬ φ) ↔ NonSequitur(Γ, φ))
> 
> All you're doing here is claiming that you have some two-place function 
> NonSequitur() which is equivalent to Γ ⊬ φ. Is this supposed to actually 
> achieve something?
> 
> If there is some φ such that (T ⊬ φ) and (T ⊬ ¬φ) then T is incomplete. 
> With your addition NonSequitur(T, φ) is also true. This doesn't have any 
> bearing on the fact that T is incomplete.
> 

NonSequitur means logically-invalid. A formal system cannot be construed 
as incomplete on the basis of its inability to prove a logically 
incorrect sentence, unless "incomplete" is a term of the art meaning 
"complete".

>> Back to the concreteness of Simple_Arithmetic to double check the 
>> reasoning with a concrete example:
>>
>> {"2+3=5", "3+2=2+3"} ∴ "3+2=5" is both true and valid
>> {"2+3=5", "3+2=2+3"} ∴ "3+2=7" is both false and invalid
> 
> Neither {"2+3=5", "3+2=2+3"} nor {"2+3=5", "3+2=2+3"} are even inputs 
> that would be accepted by your program. So where exactly is this ∴ 
> coming from? Your program doesn't provide a mechanism for going from 
> premises to conclusions so it can't possibly evaluate these.
> 
> André
> 


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