Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.theory > #21417

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

Cross-posted to 4 groups.

Show all headers | View raw

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.

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

-- 
To email remove 'invalid' & replace 'gm' with well known Google mail 
service.

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