Re: The error of the Tarski Undefinability Theorem (architectural overview)

[olcott]

On 3/9/2020 3:26 PM, David Kleinecke wrote:
> On Monday, March 9, 2020 at 10:08:16 AM UTC-7, olcott wrote:
>> On 3/9/2020 11:58 AM, David Kleinecke wrote:
>>> On Monday, March 9, 2020 at 7:27:32 AM UTC-7, olcott wrote:
>>>> On 3/9/2020 1:16 AM, André G. Isaak wrote:
>>>>> On 2020-03-08 23:44, olcott wrote:
>>>>>> On 3/9/2020 12:00 AM, André G. Isaak wrote:
>>>>>
>>>>>>> You claim that you are using the semantics of HOL (though you don't
>>>>>>> specify which HOL). But the rules of inference defined by HOL make no
>>>>>>> mention of hierarchies or inheritance, so if you actually want to use
>>>>>>> HOL, you need to define 'hierarchy', 'inheritance', and all the other
>>>>>>> concepts which you keep mentioning in terms of HOL. Until you do
>>>>>>> this, no one can possibly point out counterexamples. Since apparently
>>>>>>> you don't seem to understand what is being asked, let me start you
>>>>>>> off by providing a few possible definitions of the sort I mean. Since
>>>>>>> I have a much better understanding of what a 'hierarchy' is than of
>>>>>>> your particular usage of 'inheritance', let's start there.
>>>>>>>
>>>>>>> One of the central relations used in describing hierarchies is that
>>>>>>> of dominance. Nodes can dominate other nodes, and, assuming a
>>>>>>> single-rooted tree, there is a single root node which dominates
>>>>>>> everything else. We can defined dominance in terms of first-order
>>>>>>> logic as follows:
>>>>>>>
>>>>>>> 1. ∀x∀y(Dominates(x,y) → ¬Dominates(y, x)) # Dominance is antisymmetric
>>>>>>>
>>>>>>> 2. ∀x ¬Dominates(x,x) # Dominance is irreflexive.
>>>>>>>
>>>>>>> 3. ∀x∀y∀z ((Dominates(x,y) ∧ Dominates(y,z)) → Dominates(x, y) #
>>>>>>> Dominance is transitive.
>>>>>>>
>>>>>>> 4. ∃x∀y (¬Dominates(x,y) → x = y) # There is a root node.
>>>>>>>
>>>>>>> You don't need to indicate that the root node is unique since that
>>>>>>> follows from 1. and 4.
>>>>>>>
>>>>>>> Other crucial concepts include parent node, child node, and sibling
>>>>>>> node, which can be defined in terms of logic as follows:
>>>>>>>
>>>>>>> Parent(x,y) ↔ (Dominates(x,y) ∧ ¬∃z(Dominates(x,z) ∧ Dominates(z,y))
>>>>>>> Child(x,y) ↔ Parent(y,x)
>>>>>>> Sibling(x,y) ↔ ∃z(Parent(z,x) ∧ Parent(z,y))
>>>>>>>
>>>>>>> Other relations may be be necessary depending on exactly how you view
>>>>>>> the notion of 'hierarchy'.
>>>>>>>
>>>>>>> ONLY once you have defined the relations which define a hierarchy in
>>>>>>> terms of logic such as I have done above can you talk about using HOL
>>>>>>> to make inferences about hierarchies.
>>>>>>>
>>>>>>> So how exactly do you define 'inheritance' in terms of FOL (or HOL)?
>>>>>>>
>>>>>>> How exactly do you define 'connected semantic meanings' in terms of
>>>>>>> FOL (or HOL)?
>>>>>>>
>>>>>>> What exactly is this 'tracing' operation defined in terms of FOL (or
>>>>>>> HOL)?
>>>>>>>
>>>>>>> You *need* to provide such definitions for *every* type of
>>>>>>> relation/entity which you posit or all of your claims are entirely
>>>>>>> vacuous.
>>>>>>>
>>>>>>> André
>>>>>>>
>>>>>>
>>>>>> You are trying to delve into the weeds of implementation details
>>>>>> without first understadning the architecture.
>>>>>
>>>>> Those 'weeds' *are* what defines the architecture.
>>>>>
>>>>
>>>> No not at all not in the least. The sound deductive inference model
>>>> expressed as formal proofs to theorem consequences defines the
>>>> architecture.
>>>>
>>>>> I took me all of three minutes to come up with a first-approximation of
>>>>> the definitions needed to describe a hierarchy (though from your other
>>>>> post it seems like that isn't what you meant by hierarchy, which is why
>>>>> actually providing definitions is important).
>>>>>
>>>>> Surely you can spend three minutes coming up with a formal definition of
>>>>> 'inheritance' and 'connected meaning'. If you can't do that it means
>>>>> that you don't really know what you are talking about.
>>>>>
>>>>> André
>>>>>
>>>>
>>>> 'connected meaning'.
>>>> Some relations between expressions of language are stipulated to be
>>>> truth preserving.
>>>> (a) The truth of the premises guarantees the truth of the deductive
>>>> conlusion.
>>>>
>>>> (b) In formal proofs a theorem is guaranteed to logically follow from
>>>> axioms.
>>>>
>>>> 'inheritance'
>>>> Example: “a cat is an animal”.
>>>> Formalized as: (cat ◁ animal)
>>>> where ◁ is the [is_a_type_of] operator adapted from UML Inheritance
>>>> relation.
>>>>
>>>> https://mathworld.wolfram.com/Theorem.html
>>>> A theorem is a statement that can be [demonstrated to be true] by
>>>> accepted mathematical operations and arguments.
>>>> ∀P (Theorem(F,P) ↔ True(F,P))
>>>
>>> I'm a bit confused. You say "cats are animals" is an axiom. But I was
>>> under the impression you were trying to remove derivable facts from
>>> the list of axioms and, further, "cats are mammals" and "mammals are
>>> animals" are surely already in the axiom list.
>>>
>>
>> I was just trying to present a concrete example of the concept of a
>> syllogism to someone that seemed to be having difficulty with this concept.
>>
>>> It looks to me like you have put all the existing knowledge into the
>>> axioms so there is no need for logical inferences of any kind.
>>>
>>
>> If it looks like this then you have been hardly paying any attention at
>> all.
>>
>> Some expressions of language are stipulated to be true. ≅ AXIOMS
>> Basic Facts: are stipulated relations between finite strings that are
>> defined to have the semantic property of Boolean true. (see also Curry
>> 1977:45).
>>
>> Some relations between expressions of language are stipulated to be
>> truth preserving. ≅ rules-of-inference. Valid deduction is expressed as
>> relations between finite strings.
>
> I'm paying close attention. That's why I am confused.
>
> Can you show an example or two of true statements that aren't
> axioms?
>

All logic symbols are not themselves true yet enable truth to be
propagated from premises to conclusions.