Talk:Many-sorted logic

Definition[edit]

The current definition many-sorted logic can reflect formally our intention not to handle the universe as a homogeneous collection of objects leaves me with more questions than answers:

if it "can reflect", what else can it do? Does this mean also that in some circumstances it does not reflect?
whose intention can it reflect? Man's, the authors', some other group?

I would try to improve the definition myself, but I do not know the answers to these questions. -AndrewDressel (talk) 17:18, 26 July 2013 (UTC)[reply]

I thought about improving the article's lead, too, yet still without success.

I think, it should first define what is a logic in general (which seems to me not an easy task if one tries to be compatible to the very abstract setting of the Caleiro+Gonçalves article cited in section Many-sorted_logic#Algebraization), and then what is a many-sorted logic in particular (the existing introductory sentence could be used for that).

Another approach could be first to explain what is first-order predicate logic in general, then to define what is many-sorted first-order predicate logic in particular (I think, I'd be able to do both), and afterwards to mention that there are more abstract views, as in the Caleiro+Gonçalves article (I'm unable to do the latter).

In fact, the Many-sorted_logic#Example section and the Many-sorted_logic#Order-sorted_logic section both is about many-sorted first-order predicate logic, not about general many-sorted logic. Jochen Burghardt (talk) 13:05, 27 July 2013 (UTC)[reply]

Merge?[edit]

Isn't this matter identified with Type theory? Millbug ^talk 03:21, 8 May 2016 (UTC)[reply]

I think, it is somewhat similar to morning star and evening star in Frege's Puzzle: both matters are closely related, but usually tackled from different viewpoints. The section Type theory#Difference from set theory gives some description of the differences, when read with the understanding that many-sorted logic typically belongs to what is called set theories there. In addition, as far as I know, different communities of computer-science researchers are concerned with both matters; and type theory usually happens to deal with some kind of higher-order logic (i.e. allowing for function and/or predicate variables to appear in formulas), while many-sorted logic usually does not. While it would certainly be worthwhile to have an article (part) comparing both approaches, I'm afraid it would have to contain some original research. - Jochen Burghardt (talk) 09:27, 10 May 2016 (UTC)[reply]

So how we could improve it in order to make it "more understandable"? Millbug ^talk 17:07, 10 May 2016 (UTC)[reply]

I would not merge it with type theory. Type theory usually refers to something much more complex - e.g. there are usually infinitely many types. Multi-sorted logic usually refers to systems with just a few types (e.g. just two). More importantly, multi-sorted logic usually refers to a version of first-order logic, while type theory is often formalized with different inference rules that are not present in first-order logic (e.g. for making judgements about typing). — Carl (CBM · talk) 21:12, 10 May 2016 (UTC)[reply]

Thank you both. Now it's clearer for me. Can we reach a consensus in order to insert in the beginning of the page something like "it's a kind of first order logic" (and to develop it)? Millbug ^talk 00:01, 11 May 2016 (UTC)[reply]

I think there is a lot of room for improving the article. Right now the only mention of first-order logic is in the see also section. We could add a section on first-order logic and a section on type theory. — Carl (CBM · talk) 00:40, 11 May 2016 (UTC)[reply]

If there is no opposition, I can start. Okay? Millbug ^talk 02:28, 11 May 2016 (UTC)[reply]

Okay for me. - Jochen Burghardt (talk) 07:39, 11 May 2016 (UTC)[reply]

External links modified[edit]

Hello fellow Wikipedians,

I have just modified 2 external links on Many-sorted logic. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 02:02, 16 January 2018 (UTC)[reply]