XPost: comp.theory, sci.lang.semantics, comp.ai.nat-lang

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.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)