Groups | Search | Server Info | Login | Register

Groups > comp.theory > #21457

Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21

Cross-posted to 4 groups.

Show all headers | View raw

On 2020-07-05 14:25, olcott wrote:
> On 7/5/2020 2:16 PM, André G. Isaak wrote:
>> On 2020-07-05 12:56, olcott wrote:
>>> On 7/5/2020 1:44 PM, André G. Isaak wrote:
>>>> On 2020-07-05 12:38, olcott wrote:
>>>>> On 7/5/2020 11:53 AM, André G. Isaak wrote:
>>>>>> On 2020-07-05 10:42, olcott wrote:
>>>>>>> On 7/5/2020 11:28 AM, André G. Isaak wrote:
>>>>>>>> On 2020-07-05 09:31, olcott wrote:
>>>>>>>>> On 7/5/2020 8:17 AM, André G. Isaak wrote:
>>>>>>>>>> On 2020-07-04 15:28, olcott wrote:
>>>>>>>>>>> On 7/4/2020 1:21 PM, André G. Isaak wrote:
>>>>>>>>>>>> On 2020-07-04 10:36, olcott wrote:
>>>>>>>>>>>>> OVERVIEW:
>>>>>
>>>>>>> Since I view all of these things from the formalist approach of 
>>>>>>> operations on finite strings I assume that every variable refers 
>>>>>>> to a
>>>>>>> random finite strings unless somehow specified otherwise.
>>>>>>
>>>>>> The formalist approach doesn't involve 'random strings'. The 
>>>>>> formalist approach approach refers to a specific way of 
>>>>>> interpreting formal systems. Formal systems do not consist of 
>>>>>> 'random strings'.
>>>>>
>>>>> Formal systems can be construed as applying to random finite 
>>>>> strings through a two stage vetting process:
>>>>> (1) The finite string is a WFF
>>>>> (2) The finite is derived from a possibly empty set of premises.
>>>>>
>>>>>     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).
>>>>>
>>>>> If we focus on the most essential aspect of formal systems that is 
>>>>> common across all formal systems:
>>>>>
>>>>> formal systems are comprised of a membership algorithm that decides 
>>>>> whether or not finite string w of alphabet Σ is a theorem of formal 
>>>>> system F.
>>>>>
>>>>>
>>>>> On 7/2/2020 9:22 PM, David Kleinecke wrote:
>>>>>  >    There is a finite set called Alphabet
>>>>>  >    Strings is the set of all finite successions
>>>>>  >      of members of Alphabet
>>>>>  >
>>>>>  >    A FormalSystem is a function on Strings to Boolean.
>>>>>  >
>>>>>
>>>>>> I don't see any step at all. I see a link to a google search page. 
>>>>>> What is the supposed step involved here?
>>>>>>
>>>>>> André
>>>>>
>>>>> Do you understand and agree with the simplified essence of the most 
>>>>> generic basis of the notion of a formal system as specified in 
>>>>> computer science by me and specified in math by David?
>>>>
>>>>
>>>> No. I do not agree with it at all.
>>>>
>>>> André
>>>
>>> So there are formal systems that don't have anything like the notion 
>>> of a theorem?
>>
>> No. I am saying that isn't the definition of 'formal system'.
>>
>> André
>>
> 
> I need to go item-by-item, detail-by-detail and step-by-step to build a 
> mutual understanding. Simply saying that you disagree with one or more 
> things that I said short circuits this process of attaining mutual 
> understanding.

Concepts like 'formal system' and 'completeness' already have 
well-established definitions. Simply sticking with those would be the 
best way to attain mutual understanding.

But, here are two specific objections:

(1) Central to the definition of a formal system are a formal language, 
a set of axioms, and a set of rules of inference which allow one to 
derive theorems from axioms. Your 'minimal essence' fails to mention 
axioms or rules of inference at all. A membership algorithm which tests 
for theoremhood might constitute *part* of a formal system, but it is 
certainly not what defines a formal system.

(2) A formal system must include some mechanical procedure which can 
verify that a particular WFF can be derived from the axioms of the 
system by applying a specific sequence of rules of inference, i.e. it 
must be possible to mechanically determine that a *specified* proof is 
valid. That is not the same as the requirement that there exist some 
algorithm for determining whether there *is* a proof for some putative 
theorem, which is what you are insisting upon.

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 V21 olcott <NoOne@NoWhere.com> - 2020-07-04 11:36 -0500
  Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-04 12:21 -0600
    Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-04 16:28 -0500
      Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 07:17 -0600
        Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 10:31 -0500
          Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 10:28 -0600
            Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 11:42 -0500
              Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 10:53 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 13:38 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 12:44 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 13:56 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 13:16 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 15:25 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 14:46 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 16:08 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 David Kleinecke <dkleinecke@gmail.com> - 2020-07-05 15:28 -0700
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) olcott <NoOne@NoWhere.com> - 2020-07-05 17:50 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) Keith Thompson <Keith.S.Thompson+u@gmail.com> - 2020-07-05 17:13 -0700
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) olcott <NoOne@NoWhere.com> - 2020-07-05 20:37 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) André G. Isaak <agisaak@gm.invalid> - 2020-07-05 20:46 -0600
    Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-04 17:39 -0500
    Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 13:15 -0500

csiph-web