Groups | Search | Server Info | Keyboard shortcuts | Login | Register
| Subject | Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V20 |
|---|---|
| Newsgroups | comp.theory, comp.ai.philosophy, comp.ai.nat-lang, sci.lang.semantics |
| References | <QYqdne2udKHUrmPDnZ2dnUU7-evNnZ2d@giganews.com> <rdle1p$haf$1@dont-email.me> <MLCdnSmK2a-RoGPDnZ2dnUU7-dfNnZ2d@giganews.com> <rdlg1c$uka$1@dont-email.me> <npSdnccBb44Ey2PDnZ2dnUU7-bXNnZ2d@giganews.com> |
| From | olcott <NoOne@NoWhere.com> |
| Date | 2020-07-02 17:10 -0500 |
| Message-ID | <Xu6dnTKUHtvdxmPDnZ2dnUU7-RvNnZ2d@giganews.com> (permalink) |
Cross-posted to 4 groups.
On 7/2/2020 4:50 PM, olcott wrote:
> On 7/2/2020 3:28 PM, André G. Isaak wrote:
>> On 2020-07-02 14:01, 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))
>>
>> Do you understand that (F ⊬ C) is synonymous with ¬(F ⊢ C)?
>>
>> Removing the extraneous opening parenthesis, that means that
>>
>> (F ⊬ C) ∧ (F ⊬ ¬C) ↔ NonSequitur(F, C)
>>
>> is equivalent to
>>
>> ¬(F ⊢ C) ∧ ¬(F ⊢ ¬C) ↔ NonSequitur(F, C)
>>
>> Which means that (ignoring your extraneous parentheses)
>>
>> (F ⊬ C) ∧ (F ⊬ ¬C) ↔ NonSequitur(F, C)
>>
>> Contradicts both
>>
>> (F ⊢ C) ↔ True(F, C)
>>
>> and
>>
>> (F ⊢ ¬C) ↔ False(F, C)
>>
>> If your intention is to introduce some sort of three-valued logic,
>> then you need to make this explicit.
>>
>> If your intention is to use standard, two-valued logic, then your
>> claims are simply a mess.
>>
>> André
>>
>
> Every C always evaluates to exactly one of True, False, NonSequitur.
> See my other reply for a concrete example in the formal system of
> Simple_Arithmetic (SA).
>
>
X := "2 + 3 = 5"
Γ := {"3 > 2", "4 > 3"}
(Γ ⊬ X) ∧ (Γ ⊬ ¬X) // Thus non sequitur
Even though X is true in PA it does not logically follow from its
premises therefore is non sequitur.
--
Copyright 2020 Pete Olcott
Back to comp.theory | Previous | Next — Previous in thread | Next in thread | Find similar
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