Common Logic, Propositional Attitudes and Presupositions

[William Frank]

This is a question primarily for John Sowa, but everyone is more than welcome to provide answers.   I apologize for the length of this mail; I had no idea it was going to be this hard to state the question.   

(Also, of course, if I were a professional in this field, I ought to be doing my own research to answer the questions but I'm not.  My day jobs are more mundane and infinitely demanding. ) I wouldn't be surprised if the answers were readily available in your owe writings. 

In summary, my question is, are there any formal languages, such as common logic,  there that adequately represent statements about propositions - statements from which, in natural reaasoning, one can draw conclusions about the elements of the embedded proposition.  

For example, in English, 

Case 1) if  11  it is necessary that General Smith is in the US. Army, then 1.2 the U.S. Army exists 

Case 2) if 2.1 Sally thinks that John is the U.S. Army, then 2,2 Sally thinks that the U.S. army exists.  

Is there a formal language that enables these kinds of inferences?   

Restricting oneself to the locutionary act, ((i.e.the semantics) it seems to me that 

the re-expression of a natural language sentence SN in a formal language F, as SF 

   is adequate 

if and only if  

   for every CN that is a natural deduction from SN, the       inference rules in F, when applies to SF, lead to a          corresponding formal language consequence, CF, 

   and conversely, 

    if CF is derivable from SF, 

    the corresponding natural language consequence of      CN is naturally deducible from SN. 

So, first question: does this criterion for the adequacy of a translation seem reasonable?  

Presuming that the criterion makes sense, for the purpose of answering the adequacy criterion question, it seems to me that there are two cases: based on whether the terms in the subordinate proposition can be elevated to terms in a statement that contains no subordinate proposition.   

In the examples above, in Case 1, one can deduce that   

1,2, the U.S. army exists, a statement with no subordinate proposition, in which "the U.S. Army" has been elevated.  But in Case 2, there is no way to elevate that element.  

It strikes me that the elevatable cases correspond to modal assertions, such as S is necessary or S is required, though the 'required ' is somewhat of an ellipsis for X requires S.   And the non-elevatable cases correspond to verbs of propositional attitude that need a person as their subject, like thinks, believes, doubts, hopes, ('knows' being a more difficult special case).

Of course, we both seem to agree, along with John Corcoran and Gustaf Bergmann, that 'modal logic' is stone soup, because it represents subordinate propositions as single entities, such as P is necessary' implies that P  is possible, so there is no way to get at the elements of the subordinate proposition, which is where the action is, and because each modal logic deals with only a single mode, when in fact all the modes are part of the same natural language and need a formal language that includes them all.   

And the verbs of propositional attitude may better be served by a logic that includes presuppositions, such as 'Sally thinks that John is in the U.S. Army presupposes that the U.S. army exists.  (Though such conclusions are often thought to be part of the pragmatics, rather than the semantics).  

So, can common logic, or any other formal language you know of, adequately treat either one or both of these modal or propositional attitude cases?  And if so, is there an axample at had? 

I think that this is an entirely different problem from the use of higher-order relations, but maybe not? 

--

Wm

We understand what other people say through empathy—imagining ourselves to be in the situation they were in, including imagining wanting to say what they wanted to say.  

– Zellig Harris    

[dr.matt...@gmail.com]

Dear William,

What you are looking for is IKL.

https://www.ihmc.us/users/phayes/IKL/GUIDE/GUIDE.html

It introduces the “that” operator which exactly allows you to make statements about propositions.

Regards

Matthew West

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CALuUwtD5R%2Boc6ZTMUbYDb4a-tgN%2BtrbiW%2Bbyk7BydpWHYg9XnA%40mail.gmail.com.

[William Frank]

Thanks very much, as always, Mathew.   Beautiful.  It' a fantastic piece of work. I am aware of John Sowa's (or Pierce's) diagrams that will represent 'thats', but I had not seen inferences relating to them.   

I've been looking for something that definitely can't be expressed in any current OWL or RDF practice, (they can deal with higher-order relations)

and now I may have found it.     

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/02e401d7c516%241e2fa3f0%245a8eebd0%24%40gmail.com.

[Igor Toujilov]

William,

I have implemented your use cases in pure OWL in the spirit of my MELO project. The implementation consists of three tiny ontologies: the common inference ontology, General Smith ontology, and Sally ontology. The last two ontologies import the first one. Those ontologies are accessible from my MELO project in RDF/XML format: https://sourceforge.net/p/meloproject/code/ci/master/tree/OWL/examples/existing_things/ . Here I describe those ontologies in Manchester syntax.

The common inference ontology just states that all things in the range of is_in property are existing things:

ObjectProperty: is_in

    Range: existing_thing

Class: existing_thing

Individual: US_Army

General Smith ontology states that General Smith is in the US Army:

Individual: General_Smith

    Facts: is_in US_Army

The Sally ontology describes what Sally thinks:

Individual: John

    Facts: is_in US_Army

To test the use cases:

-- download the three ontologies to a local folder;

-- open the second or the third ontology in Protege;

-- run a reasoner, and you will see the inference: US_Army is an existing_thing.

Note that US_Army is an “elevated” thing in both cases.

Cheers,

Igor

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CALuUwtD2AsA_cdPcJSOkcwYuk1uD1prKM2nHQZhfTQOtFQVX6w%40mail.gmail.com.

[dr.matt...@gmail.com]

Dear William,

Well, I would not go that far. There is a way to say much the same thing using possible worlds.

 

For a statement such as “Peter believes that John loves Mary.”

This gets transposed to:

“There is a possible world X in which John loves Mary.”

“Peter believes possible world X is the actual world.”

 

Of course you have to admit possible worlds to make that move.

--

All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CALuUwtD5R%2Boc6ZTMUbYDb4a-tgN%2BtrbiW%2Bbyk7BydpWHYg9XnA%40mail.gmail.com.

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/02e401d7c516%241e2fa3f0%245a8eebd0%24%40gmail.com.

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CALuUwtD2AsA_cdPcJSOkcwYuk1uD1prKM2nHQZhfTQOtFQVX6w%40mail.gmail.com.

[Jon Awbrey]

Dear William,

Those were hot topics in the 80s — scanning an old bib I see:

Salmon, N.U., and Soames, S. (eds.), Propositions and Attitudes,
Oxford University Press, New York, NY, 1988.

And everyone was reading:

Barwise and Perry, Situations and Attitudes
https://web.stanford.edu/group/cslipublications/cslipublications/site/1575861933.shtml

But the roots of that problem go way back,
and of course it can't be rooted out till
more people read and comprehend and apply
Peirce's theory of triadic sign relations.

At this point in time, however, the gravitational pull
of Russell's Planet and its inconstant satellite Quine
continue to weigh against any real progress being made.

But even Russell almost, barely, just not completely broke orbit
at one of those critical branch points of intellectual history —
it appears it was only Wittgenstein who pulled him back from the
brink of 3-adicity and back to the two-folds of dyadic relations.

I discussed this in some detail in the old SUO group and its kin.
Here's a few pertinent fragments I archived at my current haunts:

Russell's “Theory Of Knowledge”
https://oeis.org/wiki/User:Jon_Awbrey/Philosophical_Notes#RTOK._Russell.27s_Theory_Of_Knowledge

Russell's “Philosophy Of Logical Atomism”
https://oeis.org/wiki/User:Jon_Awbrey/Philosophical_Notes#POLA._Philosophy_Of_Logical_Atomism
https://oeis.org/wiki/User:Jon_Awbrey/Philosophical_Notes#POLA._Note_25

Regards.

Jon

On 10/19/2021 12:51 PM, William Frank wrote:
> This is a question primarily for John Sowa, but everyone is more than
> welcome to provide answers. I apologize for the length of this mail; I
> had no idea it was going to be this hard to state the question.
>
> (Also, of course, if I were a professional in this field, I ought to be
> doing my own research to answer the questions but I'm not. My day jobs are
> more mundane and infinitely demanding. ) I wouldn't be surprised if the
> answers were readily available in your owe writings.
>
> In summary, my question is, are there any formal languages, such as common
> logic, there that adequately represent statements about propositions -
> statements from which, in natural reaasoning, one can draw conclusions
> about the elements of the embedded proposition.
>
> For example, in English,
> Case 1) if 11 it is necessary that General Smith is in the US. Army, then
> 1.2 the U.S. Army exists
> Case 2) if 2.1 Sally thinks that John is the U.S. Army, then 2,2 Sally
> thinks that the U.S. army exists.
>
> Is there a formal language that enables these kinds of inferences?
>
> Restricting oneself to the locutionary act

> <https://www.amazon.com/How-Do-Things-Words-Lectures/dp/0674411528>, ((i.e.the

> Bergmann <https://www.jstor.org/stable/2251960>, that 'modal logic' is

> stone soup, because it represents subordinate propositions as single
> entities, such as P is necessary' implies that P is possible, so there is
> no way to get at the elements of the subordinate proposition, which is
> where the action is, and because each modal logic deals with only a single
> mode, when in fact all the modes are part of the same natural language and
> need a formal language that includes them all.
>
> And the verbs of propositional attitude may better be served by a logic
> that includes presuppositions

> <https://plato.stanford.edu/entries/presupposition/>, such as 'Sally thinks

[doug foxvog]

On Tue, October 19, 2021 12:51, William Frank wrote:
> ...

>
> In summary, my question is, are there any formal languages, such as common
> logic, there that adequately represent statements about propositions -
> statements from which, in natural reaasoning, one can draw conclusions
> about the elements of the embedded proposition.
>
> For example, in English,

> Case 1) if 1.1 it is necessary that General Smith is in the US. Army,

> then
> 1.2 the U.S. Army exists

I don't know what type of necessity is being referred to here. It could
be a legal or moral necessity, for example. But, i'll take it as merely
that the statement is true. This can be expressed in Cyc:

(implies
(holdsIn ?TIMEINTERVAL (organizationMember ?PERSON ?ORG))
(holdsIn ?TIMEINTERVAL
(and (exists ?PERSON) (exists ?ORG))))

Or more generically:

(implies
(and
(isa ?PREDICATE BiTemporalPredicate)
(holdsIn ?TIMEINTERVAL (?PREDICATE ?PERSON ?ORG))
(holdsIn ?TIMEINTERVAL
(and (exists ?PERSON) (exists ?ORG))))

> Case 2) if 2.1 Sally thinks that John is the U.S. Army, then 2,2 Sally
> thinks that the U.S. army exists.

(implies
(holdsIn ?TIMEPERIOD1
(thinks ?PERSON
(holdsIn ?TIMEPERIOD2 (organizationMember ?PERSON2 ?ORG))))
(holdsIn ?TIMEPERIOD1
(and
(exists ?PERSON)
(thinks ?PERSON (holdsIn ?TIMEPERIOD2 (exists ?PERSON2))))
(thinks ?PERSON (holdsIn ?TIMEPERIOD2 (exists ?ORG))))

Or more generically:

(implies
(holdsIn ?TIMEPERIOD1
(and
(thinks ?PERSON (isa ?PREDICATE BiTemporalPredicate))
(thinks ?PERSON
(holdsIn ?TIMEPERIOD2 (?PREDICATE ?PERSON2 ?ORG))))
(holdsIn ?TIMEPERIOD1
(and
(exists ?PERSON)
(thinks ?PERSON (holdsIn ?TIMEPERIOD2 (exists ?PERSON2))))
(thinks ?PERSON (holdsIn ?TIMEPERIOD2 (exists ?ORG))))

This is a little more accurate, since in the first version it went
unstated that PERSON1 thought that membership was only true if both the
organization and the organization member existed at the time of
membership.

> Is there a formal language that enables these kinds of inferences?
>
> Restricting oneself to the locutionary act

> <https://www.amazon.com/How-Do-Things-Words-Lectures/dp/0674411528>,

> ((i.e.the semantics) it seems to me that
> the re-expression of a natural language sentence SN in a formal language
> F,
> as SF
> is adequate
> if and only if
>
> for every CN that is a natural deduction from SN, the inference
> rules in F, when applies to SF, lead to a corresponding formal
> language consequence, CF,
>
> and conversely,
> if CF is derivable from SF,
> the corresponding natural language consequence of CN is
> naturally deducible from SN.
>
> So, first question: does this criterion for the adequacy of a translation
> seem reasonable?

That requires that every rule valid for everything in SN already exists in
the ontology in order for a translation to be adequate. That seems a bit
too strong. Natural deductions from "General Smith is in the US. Army"
may be that General Smith has a salary within a certain range, that s/he
has been in the US military for a certain range of years, that s/he is in
a certain age range, and that s/he has spent time in the Pentagon, and
that s/he is aware of certain laws and regulations. I'm not sure that the
ontology needs to have all that information for its translations to be
adequate.

> Presuming that the criterion makes sense, for the purpose of answering the
> adequacy criterion question, it seems to me that there are two cases:
> based
> on whether the terms in the subordinate proposition can be elevated to
> terms in a statement that contains no subordinate proposition.

> In the examples above, in Case 1, one can deduce that
> 1,2, the U.S. army exists, a statement with no subordinate proposition, in
> which "the U.S. Army" has been elevated. But in Case 2, there is no way
> to elevate that element.

Correct. But note that there is a temporal constraint on Case 1 which
wasn't stated in English. This temporal constraint also applies to Case
1.2.

> It strikes me that the elevatable cases correspond to modal assertions,
> such as S is necessary or S is required, though the 'required ' is
> somewhat
> of an ellipsis for X requires S. And the non-elevatable cases correspond
> to verbs of propositional attitude that need a person as their subject,
> like thinks, believes, doubts, hopes, ('knows' being a more difficult
> special case).
>
> Of course, we both seem to agree, along with John Corcoran and Gustaf

> Bergmann <https://www.jstor.org/stable/2251960>, that 'modal logic' is

> stone soup, because it represents subordinate propositions as single
> entities, such as P is necessary' implies that P is possible, so there is
> no way to get at the elements of the subordinate proposition, which is
> where the action is, and because each modal logic deals with only a single
> mode, when in fact all the modes are part of the same natural language and
> need a formal language that includes them all.
>
> And the verbs of propositional attitude may better be served by a logic
> that includes presuppositions

> <https://plato.stanford.edu/entries/presupposition/>, such as 'Sally

> thinks
> that John is in the U.S. Army presupposes that the U.S. army exists.

No, it just means that Sally things that both John and the U.S. Army
exist. It only requires Sally to exist.

> (Though such conclusions are often thought to be part of the pragmatics,
> rather than the semantics).

> So, can common logic, or any other formal language you know of, adequately
> treat either one or both of these modal or propositional attitude cases?
> And if so, is there an axample at had?
>
> I think that this is an entirely different problem from the use of
> higher-order relations, but maybe not?
>
> --
> Wm
>
> We understand what other people say through empathy—imagining ourselves
> to
> be in the situation they were in, including imagining wanting to say what
> they wanted to say.
>
> – Zellig Harris
>

[Alex Shkotin]

William,

About your zero question "Is there a formal language that enables these kinds of inferences?"

First of all, we need to write sentences themselves and then look for derivation possibilities. 

"necessary" and, "thinks" may be a special kind of concept (class) and relation of(to) a sentence and to get statement itself as an entity we have in RDF a reification. 

But I am not sure about derivation rules there. Using reification in OWL2 may give some derivations if we can axiomatize "necessary" and, "thinks" in DL fully.

And a little bit about your "first question: does this criterion for the adequacy of a translation seem reasonable? "

From my point of view, unfortunately, in general adequacy of translation from human language to formal language may be checked only by human. For example if we have some CNL (like ACE) and we have hand-written compiler like APE to translate to OWL2 or TPTP, your criteria would be for the author a conclusion: I have done compiler well hence WF-criteria of course satisfied. As we have no possibility to check it:-)

By the way, modal logics itself is a mathematician's game, but sometimes the do something usefull;-)

Alex

вт, 19 окт. 2021 г. в 19:52, William Frank <william...@gmail.com>:

--

[William Frank]

On Sat, Oct 23, 2021 at 4:49 AM Alex Shkotin <alex.s...@gmail.com> wrote:

William,

About your zero question "Is there a formal language that enables these kinds of inferences?"

First of all, we need to write sentences themselves and then look for derivation possibilities. 

"necessary" and, "thinks" may be a special kind of concept (class) and relation of(to) a sentence

For sure.  Modals are predicates that apply to propositions, and propositional attitudes are relations that relate people or their surrogates to a proposition.  

 

and to get statement itself as an entity we have in RDF a reification. 

Ah, this is the key to the matter.  I have read the reification standard in OWL 2, but I couldn't work out somehow, how to use it.  

I need a worked-out example.  Can you then, as you suggest, write out these two propositions 

1.  It is possible that General Smith is in the U.S. Army

2. Sally thinks that John is in the U.S. Army.  

As they would appear in OWL using reification?    This would be immensely helpful to me. 

 

But I am not sure about derivation rules there. Using reification in OWL2 may give some derivations if we can axiomatize "necessary" and, "thinks" in DL fully.

Yah, we could create some axioms, if, after reifying a proposition, is there a way to still get at its constituents.   I mean, take the embedded proposition apart to draw conclusions about its subject or object?   That is the hup of the second question. 

And a little bit about your "first question: does this criterion for the adequacy of a translation seem reasonable? "

From my point of view, unfortunately, in general adequacy of translation from human language to formal language may be checked only by human.

This is absolutely true, and is not unfortunate in my opinion, indeed, given the nature of natural languages, it could be no other way.  That some people think otherwise creeps me out. 

For example if we have some CNL (like ACE) and we have hand-written compiler like APE to translate to OWL2 or TPTP, your criteria would be for the author a conclusion: I have done compiler well hence WF-criteria of course satisfied. As we have no possibility to check it:-)

My criteria involve having a person decide whether the natural deduction inferences match those that would be derived in the formal language. 

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROTeSqVUg72-ZZctvuqR5Z1cfZA5FF67Uaovh7WFDqHTxg%40mail.gmail.com.

[sowa @bestweb.net]

William, Alex, List,

 

Short answer for all the issues in this thread:  Common Logic (CL)s, by itself, is sufficient for almost all these issues.  For the rest, the IKL extension to CL supports metalanguage, which can support the rest.  For the IKL extension to CL, see http://jfsowa.com/ikl/ivve 

 

Short answer about reification: Whenever you convert a verb or an adjective to a noun, you have an example of reification.  For example, the verb 'to swim' can be reified to the noun 'a swim'.  But 'to talk'  and 'a talk' have different senses"  The verb 'give' may be reified to the noun 'donation'.  These syntactic variations result from the fact that English has borrowed words from many different languages.

 

Classical Greek has a simple way to  nominalize any part of speech:  just put a definite article in front of it.  For example,

Cicero translated some of Aristotle's words to Latn, which does not have a definition article.  So he coined the words 'quantitas' and 'qualitas' to translate 'the how much' and 'the what kind'.

 

But nominalization is a mater of ontology, not logic.  As soon as you define thes worrds, you can use them in any version of logic.

 

In a few more minutes, I'll send a longer note about metalanguage and modality in response to questions by Avril.

 

John

[sowa @bestweb.net]

Doug F,

 

I agree with your solution.  As I said, Common Logic with the IKL extension could represent these issues.  In fact, a representative of Cyc participated in the development of the IKL logic.  Doug Lenat & Co. agreed that the IKL extension to Common Logic could represent the Cyc Language.  For more about IKL, see http://jfsowa.com/ikl\

 

These issues are the kinds of reasons why I call OWL and the other products of the 2005 version of the Semantic Web obsolete.  In factk it is a major step backward from Tim B-L's winning proposal of 2000.  These are among the issues I discussed in a keynote speech ffor the Extended/European Semantic Web Conference in May 2020:  http://jfsowa.com/talks/eswc.pdf

 

At ESWC20, many other speakers also presented proposals that went far beyond the 2005 version of the SW.  Tim B-L himself wanted to get more funding to go beyond what was accomplished in 2005, but he didn;t get the funds..

 

John

 

From: "doug foxvog" <do...@foxvog.org>
Sent: Saturday, October 23, 2021 12:38 AM
To: ontolo...@googlegroups.com
Subject: Re: [ontolog-forum] Common Logic, Propositional Attitudes and Presupositions

 

[Alex Shkotin]

William,

about [2]. I am not a fan of RDF.  Please have a look at [1]. Where the RDF* mentioned. 

But it may be something like this using OWL2 functional style [3]

rdf:Statement(:st1)

rdf:subject(:st1 :General_Smith)

rdf:predicate(:st1  :is_in)

rdf:object(:st1  :US_Army)

:possible(:st1)

...

:thinks(:Sally  :st2)

Following [1] and RDF* it may be like

:Sally :thinks <<:John :is_in :US_Army>> 

What do you think? 

Alex

[1] https://stackoverflow.com/questions/1312741/simple-example-of-reification-in-rdf 

[3] https://www.w3.org/2007/OWL/draft/ED-owl2-syntax-20081128/

[2]

[Alex Shkotin]

Just to add,

In Higher-Order Logic we may just define 0-arity predicate (aka proposition), i.e. assign the proposition (closed formula) the identifier like this

declaration st1 :TV ≝ (_General_Smith is_in _US_Army).

where,

-funny " :TV" is a signature, type of function: zero arguments, and Truth Values set (TV) as a range.

-binary predicate "is_in" is used infixly.

-"_General_Smith" and "_US_Army" are entity representatives.

And then add to our theory axiom "Possible(st1)".

So in general we need just the ability to name a proposition to talk about it.

Alex

сб, 23 окт. 2021 г. в 19:27, William Frank <william...@gmail.com>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CALuUwtAjDWKEbQ2xCY1n6Ky7n%3DX00sYoGTyRf9gyvg%2BBjQmUTw%40mail.gmail.com.

[Till Mossakowski]

In standard higher-order logic, which is extensional and compositional, this does not make much sense.

st1 denotes a truth value, and Possible(st1) can only depend on the truth value of st1, not on its contents. That is, the meaning of "Possible" is a map from {T,F} to {T,F}, and in total, there are four such maps, none of which captures what you want to express here.

You would need a kind of intensional higher-order logic, where Possible(st1) and Possible(st2) can differ even if st1 and st2 have the same truth value.

Best, Till

Am 24.10.21 um 10:49 schrieb Alex Shkotin:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROTt9ASdi9JWm-7Xxx4wXEJmaEu33HDJOaRK67fVCMrwxQ%40mail.gmail.com.

[Alex Shkotin]

Till

I am following mostly Maltsev A.I. "Algebraic systems" where we have predicates and functions as variables and the value of proposition st1 depends on the value assigned to predicate is_in on _General_Smith,  _US_Army - it may be True, False or no value at all.

To be more accurate I definitely should refer to a particular kind of HOL, but first of all, it's just beyond the FOL.

Or let me say Tarski's way - the value of st1 depends on the interpretation of is_in on <_General_Smith  _US_Army>.

Alex

вс, 24 окт. 2021 г. в 13:39, Till Mossakowski <ti...@iks.cs.ovgu.de>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/4b725c84-d7a1-4bd3-fd6c-2336a8f91607%40iks.cs.ovgu.de.

[Till Mossakowski]

Alex,

OK, Maltsev uses standard HOL (with Tarskian semantics). This means that Possible(st1) does not formalise what you intend. There are only four options to interpret the predicate Possible:

1) all sentences are possible

2) all sentences are impossible

3) all true sentences are possible, all false sentences are impossible

4) all true sentences are impossible, all false sentences are possible

None of these options really makes sense. Option 3) comes closest to making at least a little sense, but it means that Possible(s) is equivalent to s, so you just can omit the Possible predicate.

Best, Till

Am 24.10.21 um 13:59 schrieb Alex Shkotin:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROQhCmNgB_LUTNp7wg%2BctU1ZfPh5pAKv%3DqcZVLiSnLSt%3DA%40mail.gmail.com.

[Alex Shkotin]

Till

My intend is just a formalization: Possible is a unary predicate on sentences. And I wrote to William that as far as we get formalization we need axioms for this unary predicate Possible or maybe a definition. JFS wrote something about possible worlds - why not.

My way is to ask William: what can we say about Possible? 

Now the meaning William has for Possible is unknown, but I hope it is possible to get it and formalize.

Alex

вс, 24 окт. 2021 г. в 18:16, Till Mossakowski <ti...@iks.cs.ovgu.de>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/d3dbf3b4-bc6e-563f-f901-4082db60a61a%40iks.cs.ovgu.de.

[Till Mossakowski]

Alex,

my point is: the semantic space for the predicate Possible in HOL is too narrow already (namely, just the functions from Bool to Bool). With axioms, you only can make it even narrower. So axioms do not help here.

One would need a wider semantic space, in a non-Tarskian, non-compositional HOL, to formalise possibility. Has such a HOL been studied? (Maybe one can construe IKL as a higher-order logic...) I myself have only studied intensional (but still compositional) HOL.

Till

Am 24.10.21 um 18:04 schrieb Alex Shkotin:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxRORM5qFwuNWqfcuJrKP2Zi9M%2Bx3MMqgs-jracfg4wMMDDw%40mail.gmail.com.

[Alex Shkotin]

Till,

This is just a misunderstanding. Class rdf:Statement is for named and blank nodes, not for Bool. And it is possible using rdf:subject, rdf:predicate, rdf:object to keep statement structure.

My idea was just to use reification to get statement id in RDF. And when statement itself states particular relationship of GenSmith and USArmy we get id for this relationship:-)

And now we may assign to this id all attributes we know about this relationship. For example probability(st1)=0.1, but WF would like to assign it to class Possible what ever this mean for him.

The logic of possibility and it's formalization is a special issue, sure.

"One would need a wider semantic space, in a non-Tarskian, non-compositional HOL, to formalise possibility. Has such a HOL been studied?"

I don't know. 

Alex

пн, 25 окт. 2021 г. в 00:20, Till Mossakowski <ti...@iks.cs.ovgu.de>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/f53b7411-4d08-ccf0-d72c-46dd70490efb%40iks.cs.ovgu.de.

[Alex Shkotin]

It seems to me that Ken during one of our OntoSumm meetings, when he talked about his KG enhancement, mentioned this trick with reification?

Alex

пн, 25 окт. 2021 г. в 11:50, Alex Shkotin <alex.s...@gmail.com>:

[Till Mossakowski]

Alex,

OK, with rdf:Statement, things are different, of course. I just had refered to your utterance

"In Higher-Order Logic we may just define 0-arity predicate (aka proposition), i.e. assign the proposition (closed formula) the identifier like this

declaration st1 :TV ≝ (_General_Smith is_in _US_Army)."

And 0-arity predicates in HOL semantically are just truth values.

Best, Till

Am 25.10.21 um 10:50 schrieb Alex Shkotin:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROTA8CFtCzT%2B-3Od61ChmNcT9cMfo3mQ9OFE5%2B8dYCmHkA%40mail.gmail.com.

[Alex Shkotin]

Till,

to clarify idea of 0-arity predicates we need not HOL. We may use just FOL. But we need to introduce definitions for 0-arity predicates. 0-arity predicate is a trick to treat closed formula as a predicate.

For example if in some formal theory I have theorem 

∀x∃y y>x.

I may say let th1 is an identifier for ∀x∃y y>x. And say that th1 is 0-arity predicate (from the FOL point of view). [to HOL a little bit: th1 returns True or False depending on the value of binary predicate ">".]

It's just another terminology. One way to formalize this is

declare th1 ≝ (∀x∃y y>x). 

We introduce to the theory new identifire (aka symbol) with possible value True, False i.e. predicate.

consider

declare < (x y)  ≝ not(x>y and x=y). 

where we defined binary predicate. 

0-arity predicate does not have formal parameters.

Anyway this is just terminology for named closed formulas of FOL.

Alex

пн, 25 окт. 2021 г. в 12:57, Till Mossakowski <ti...@iks.cs.ovgu.de>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/fefb669e-dbeb-3199-65a4-b94502cf433f%40iks.cs.ovgu.de.

[Till Mossakowski]

Alex,

exactly. And this shows that with the HOL definition

declaration st1 :TV ≝ (_General_Smith is_in _US_Army)

the HOL sentence

Possible(st1)

does not express what you want. In particular, it is *never* about possibility.

However, if st1 is an RDF statement, the situation is different.

Best, Till

Am 25.10.21 um 12:41 schrieb Alex Shkotin:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROS1JMMis-XBsRbcHPbG%3Dg2Ay4DXU_N%3DaYXO9a0OUQLhQA%40mail.gmail.com.

[Alex Shkotin]

Till,

I think it is a little bit of a notation problem.

When we wrote "Possible(st1)" we are talking about st1 itself. and the type of argument of Possible is ":TV" i.e. it gets this kind of function as an input.

If we need a result of st1 we should "call" it like this "st1()". 

In FOL any constant is a 0-ary function, but there is an agreement not to use brackets as we do not have functions as an input, and instead of 1()+2() we write 1+2.

So Possible(st1) is about formula - something like metalanguage in the language. 

The idea to formalize possibility this way is not the best, but the syntax is first.

Alex

пн, 25 окт. 2021 г. в 15:54, Till Mossakowski <ti...@iks.cs.ovgu.de>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/4310f57f-5421-d00c-e4db-243d2738011a%40iks.cs.ovgu.de.

[Alex Shkotin]

Let's define a function

declare twc1 Nat:Nat (x) =def 2*x.

and then ask Monotonic(twc1) value. We'll get True.

пн, 25 окт. 2021 г. в 15:54, Till Mossakowski <ti...@iks.cs.ovgu.de>:

Alex,

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/4310f57f-5421-d00c-e4db-243d2738011a%40iks.cs.ovgu.de.

[Till Mossakowski]

Alex,

so you choose (standard) HOL, because there you can use the syntax Possible(st1), where st1 can be an arbitrary complex formula. (This is not possible in FOL.)

However, semantically, Possible is just a predicate on {T,F}, and thus, it does not express possibility of st1.

Generally, in standard HOL, you cannot express the possibility of st1, where st1 is a formula.

To sum up: what you want cannot be done in standard HOL.

Best, Till

Am 25.10.21 um 16:17 schrieb Alex Shkotin:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROQ-NT%3DSae0B0xY8pWswEqM7-kaVy186qtkkgCDD%3DgQYNw%40mail.gmail.com.

[Alex Shkotin]

Till,

"semantically, Possible is just a predicate on {T,F}" for me this proposition is very very doubtable.

so Doubtable(Possible is a predicate on {T,F})

but I am waiting for the answer about Possible from William Frank, as I am not studying Possible myself.

HOL is where a function may be an argument of another function or a result of it.

Alex

пн, 25 окт. 2021 г. в 23:02, Till Mossakowski <ti...@iks.cs.ovgu.de>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/6e8267e2-5629-f783-b8da-f057da5633b0%40iks.cs.ovgu.de.

[Till Mossakowski]

Alex,

Am 26.10.21 um 10:10 schrieb Alex Shkotin:

Till,

"semantically, Possible is just a predicate on {T,F}" for me this proposition is very very doubtable.

of course, your *intended* predicate Possible is not just a predicate on {T,F}.

However, in standard HOL (see [1]), Possible would have type

Possible : o -> o

and in standard HOL, the semantics of o -> o is the function space {T,F} -> {T,F}. This follows from

"By a standard model, we mean a family of domains, one for each type-symbol, as follows: D_\iota is an arbitrary set of elements called inviduals, D_o ist the set consisting of two truth values, T and F, and D_{\beta->\alpha} is the set of all functions defined over D_\beta with values in D_\alpha." [1], p.83, where in the original, instead of D_{\beta->\alpha}, the old-fashioned notation D_{\alpha\beta} is used.

This shows that your intended predicate Possible cannot be expressed in standard HOL as an operator on formulas.

Best, Till

[1] Leon Henkin: Completeness in the Theory of Types. The Journal of Symbolic Logic Vol. 15, No. 2 (Jun., 1950), pp. 81-91
https://www.jstor.org/stable/2266967

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROSuH0oysLz_CJsPwBc3NCg4uY3mWpNYTdemJ6iy4TjaSw%40mail.gmail.com.

[Alex Shkotin]

Till,

thank you for the reference. My problem is that I am not studying Possible - I just don't know what does it mean for William. And the first idea was to formalize Possible as we discussed.

It is possible that I shall study your reference to get that it is impossible to express my intended predicate Possible in standard HOL.

If I am on the way to implementing formalization, I'll ask guys of Coq, HOL4... if my "intended predicate Possible" is implementable, i.e. expressible on their languages - this is the first important thing for me. 

And look I have some axioms for Possible:

declare Poss1_ax :TV =def ∀x,y:(:TV) Possible(x) & Possible(y) → Possible(x & y)

declare Poss2_ax :TV =def ∀x:(:TV) Possible(x) → not Possible(not x)  

Just a little bit more on your "st1 can be an arbitrary complex formula" - "closed" must be added to the formula, i.e. "st1 can be an arbitrary closed formula"

Alex

вт, 26 окт. 2021 г. в 12:25, Till Mossakowski <ti...@iks.cs.ovgu.de>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/a93ecc09-8a6d-a0f6-15c5-ec4c4c684975%40iks.cs.ovgu.de.

[Till Mossakowski]

Alex,

it might help to move to intuitionistic HOL [2,3], because there, the type o can be interpreted more generally than just {T,F}, namely it can be a so-called frame (frames are a certain type of Heyting algebras). Then you could interpret o as, say, the function space W->{T,F}, where W is a set of worlds (worlds as in Kripke semantics for modal logic). Still, it is not clear to me how to smuggle in the accessibility relation of Kripke semantics, if you want to use that for defining your Possible operator. (Of course, you can make everything explicit, as in the standard translation of modal logic to FOL, but I think we are not on that path here.)

Best, Till

[2] Peter Aczel. A note on interpreting intuitionistic higher-order logic, 1980. http://www.cs.man.ac.uk/~petera/note_on_interpreting_higher_order_logic.pdf

[3] J. Lambek P. J. Scott. Introduction to Higher-Order Categorical Logic. Cambridge Studies in Advanced Mathematics, 1988

   

Am 26.10.21 um 12:08 schrieb Alex Shkotin:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROTFJcW08qyOhkrjw8TqZD6HO2iDy_RVMJwFtkHvuDTpWg%40mail.gmail.com.

[Alex Shkotin]

Till, thank you.

We should not dig Possibility without William Frank, as he is the Initiator of this direction. Consider that the sentence would be "It's a good idea that Gen Smith is in USArmy." and we discuss formalization like

Good_idea(st1).

A possibility has been investigated many times in all possible directions:-)

For me, the situation with this kind of modality is that if in my theory would be a modality of some kind I should choose the best formalization from many available.

For example, if I need to formalize the text of the standard of programming language (Pascal...) I remember they use "must", "might", "can"...

But I need not:-)

Alex

вт, 26 окт. 2021 г. в 14:19, Till Mossakowski <ti...@iks.cs.ovgu.de>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/c9ff994f-ad32-5a98-0705-7c1b08d686bb%40iks.cs.ovgu.de.

[Alex Shkotin]

William,

I should mention another way of formalizing back to Łukasiewicz and others from Lwów–Warsaw School.

Let's add Possible to Truth Values i.e. to True and False.

(GSmith is_in USArmy)=Possible → ∃x x=USArmy.

{T,F,P} calculi may be interesting and even impossible:-)

What do you think?

Alex

[sowa @bestweb.net]

Alex and William,

 

I'm writing a response to Avril that clarifies the difference between the syntax of some language (natural or formal) on some topic (such as modality) and a semantic theory that explains what the syntactic features mean.  But this note is a short comment about about some issues in your notes.

 

Alex:  I should mention another way of formalizing back to Lukasiewicz and others from Lwów–Warsaw School.

Let's add Possible to Truth Values i.e. to True and False.

 

L's truth tables are interesting, but they are just another way of representing relationships that are as old as Aristotle.  They say that necessary(p) implies true(p);   true(p) implies possible(p); and necessary(p) is equivalent to not(possible(not(p)).  They don't explain what the words 'necessary' and 'possible' mean.

 

William:  are there any formal languages, such as common logic,  there that adequately represent statements about propositions - statements from which, in natural reaasoning, one can draw conclusions about the elements of the embedded proposition.  

 

Common Logic, with an ontology about propositions can state Aristotle's axioms or anybody else's.  But it cannot relate a name of a proposition (such as the letter 'p') to the statement of the proposition in some expression.   The IKL extension to CL adds a special operator named 'that'. which relates an expression  of a proposition to a name.  For example, the following IKL sentence says that 'p' is the name of a proposition that says "The sky is blue."

 

(exists (p proposition)  (= p (that (blue sky)))).

 

The operator 'that' is the only extension to IKL that is required to state any or every possible theory about propositions and modality.  But it still does not explain what the words 'necessary' and 'possible mean.

 

To do that, we need a version of model theory (e.g. an extension of Tarksi's model theory) .  The most commonly used theory is by Saul Kripke, who related the words 'necessary' and 'podsible' (or the symbols that represent them) to possible worlds and an accessibility relation among them. 

 

Later, Michael Dunn developed a much simpler and more understandable theory that got rid of Kripke's possible worlds and accessibility by explaining modality in terms of laws and facts.

 

See http://jfsowa.com/pubs/5qelogic.pdf

 

All the following examples by William can be translated to CL with the IKL operator 'that'.

 

John

__________________

 

William: For example, in English, 

[Alex Shkotin]

John,

Great! Thank you. As far as I find the logic of possibility in the theory I am formalizing I know the way to go for variants. 

I am formalizing graph theory and have not met the possibility yet. One thing is just when "possible" means "exists". Like [2] from [1].

Alex

[1] https://books.google.ru/books?id=f-lQAAAAMAAJ

[2] 

ср, 27 окт. 2021 г. в 18:39, sowa @bestweb.net <so...@bestweb.net>:

--

All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/6198ef47b030410ca6eb0320b7d83f4c%40bestweb.net.