Groups | Search | Server Info | Login | Register

Groups > comp.theory > #21420

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 11:56, olcott wrote:
> 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.

Non Sequitur means 'does not follow'. But that's its *English/Latin* 
meaning.

You haven't given your NonSequitur() any sort of definition. All you've 
done is claimed that ∀Γ ⊆ T ∀φ WFF(T) ((Γ ⊬ φ) ↔ NonSequitur(Γ, φ)) from 
which we can infer that you are treating 'NonSequitur' as a synonym for 
'unprovable'.

I can claim that ∀Γ ⊆ T ∀φ WFF(T) ((Γ ⊬ φ) ↔ Blue(Γ, φ)), but that 
doesn't make unprovable sentences magically become Blue. It simply 
implies that I am using Blue() as a synonym for 'unprovable'.

If you want NonSequitur() to actually mean something other than simply 
not provable, then you need to actually define it.

But note that if you define it to have some meaning that isn't simply 
'unprovable', then you can't simply assert that ∀Γ ⊆ T ∀φ WFF(T) ((Γ ⊬ 
φ) ↔ NonSequitur(Γ, φ)) unless you can actually prove that this 
statement actually holds given whatever definition of 'NonSequitur' you 
are proposing.

And none of this will alter the fact that if a sentence φ is unprovable 
in T and ¬φ is also not provable in T, then T is incomplete. Any other 
properties which φ might have are not relevant to the definition of 
incompleteness.


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

I cannot make any sense of that sentence whatsoever.

André


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

Back to comp.theory | Previous | Next — Previous 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