Re: Formal specification of Minimal Type Theory (updated)

[olcott]

On 10/17/2020 8:33 AM, André G. Isaak wrote:
> On 2020-10-16 17:54, olcott wrote:
>> On 10/16/2020 6:33 PM, Ben Bacarisse wrote:
>>> olcott <No...@NoWhere.com> writes:
>>>
>>>> On 10/16/2020 4:15 PM, Ben Bacarisse wrote:
>>>>> olcott <No...@NoWhere.com> writes:
>>>>>
>>>>>> On 10/16/2020 3:20 PM, olcott wrote:
>>>>>>> On 10/16/2020 3:03 PM, Ben Bacarisse wrote:
>>>>>>>> olcott <No...@NoWhere.com> writes:
>>>>>>>>
>>>>>>>>> ... we all know that this: "⊬" is the might not be provable symbol
>>>>>>>>
>>>>>>>> No it isn't.
>>>>>>>>
>>>>>>>
>>>>>>> So then the following set includes zero "*might* be undecidable"
>>>>>>> propositions, thus proving that Andre's position is baseless:
>>>>>>>
>>>>>>> A theory T is incomplete if and only if there is some sentence φ
>>>>>>> such that (T ⊬ φ) and (T ⊬ ¬φ).
>>>>>>>
>>>>>>> On 10/16/2020 11:50 AM, André G. Isaak wrote:
>>>>>>>    > The point is that we do not *know* whether it is an undecidable
>>>>>>>    > proposition or merely an undecided proposition. It *might* be
>>>>>>>    > undecidable.
>>>>>>
>>>>>> Since Andre would know that this: "⊬" is not the "might not be
>>>>>> provable" symbol his position is a lie and not merely an honest
>>>>>> mistake.
>>>>>
>>>>> Hmm... and this makes me think that Jeff Barnett may be right -- that
>>>>> you do indeed know you are wrong.  There's no mistake and certainly no
>>>>> lies.
>>>>
>>>> Andre has been consistently claiming that in some cases the the φ in
>>>> this expression may not be known to be undecidable in T:
>>>>
>>>> A theory T is incomplete if and only if there is some sentence φ such
>>>> that (T ⊬ φ) and (T ⊬ ¬φ).
>>>
>>> He has been consistently (and correctly) claiming that there is no way
>>> to know, /in general/, if any given sentence φ is such that T ⊬ φ and T
>>> ⊬ ¬φ.  Anything else you think he's been saying is in your head.
>>>
>>
>> Sure that is correct AND a dishonest dodge.
>>
>>> Meanwhile, you have been consistently (and evasively) pretending that
>>> this doesn't matter.
>>
>> If an expression of language: φ is stipulated to be undecidable in
>> theory T: (T ⊬ φ) and (T ⊬ ¬φ),
>>
>> then we can know with complete certainty that φ is indeed undecidable
>> in theory T.
>
> You don't "stipulate" a proposition to be undecidable. It either is or
> it isn't.
>

This: (T ⊬ φ) and (T ⊬ ¬φ) is stipulated to define the concept of
undecidable proposition. Symbols only have meanings when meanings have
been assigned to them.

> The problem is that for theories such as the ones with which Gödel is
> concerned, we've only identified a tiny fraction of the undecidable
> propositions. Because there is no general method for deciding whether a
> proposition is decidable, most will never be identified.
>

When we determine that every single undecidable proposition known or
unknown proven or unproven is only undecidable because it is incorrect
then we have covered ALL of them with NONE left out.

When we do this then every single proof of incompleteness that depends
on undecidable propositions utterly fails.

For the same reason that we cannot decide that a medical doctor is
"incompetent" in the basis of their inability to restore health to the
cremated** we cannot decide that a formal system is "incomplete" on the
basis of it inability to prove or disprove incorrect expressions of
language. ** Even Christ never did that.

> If you exclude all known examples of undecidable propositions, that
> still leaves you with all of the unknown examples of undecidable
> propositions, which means the system remains incomplete.
>
> André


When we rename the whole category of "undecidable proposition" to
"incorrect proposition" then there are zero undecidable propositions
left to prove incompleteness.


--
Copyright 2020 Pete Olcott