Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthortomr
• CommentTimeOct 23rd 2019

I am searching for all the possible features of reasoning (all of them can be expressed in logic), so far I have found the following features:

• non-monotonicity, defeasible reasoning (expressed by special features of consequence relation)
• probabilistic reasoning (expressed by assignment of probabilities to the predicates and by the operations on the probabilities to the connectives and modal operators)
• higher order logic (expressed by allowing the predicated to take other predicates and formulas as arguments)
• modal operators (expressed by the unary operators acting on the predicates and formules)
• special connectives (expressed by special connectives that can arise in linear/substructural setting)

My question is this - are there any other features beside those 5, features that can improve the expresiveness of the logic.

I am trying to combine all those features in one logic and initially I would be happy to know that the set of those 5 features is exhaustive and so - when I come up with the language that can express all those 5 features then there is no more general language than that. Of course, I am thinking about templates, i.e., I will leave open the final set of modal operators and connectives (and the interactions among them), because different concrete logics can arise in each concrete choice of those. My aim is to create reasoner (forward chaining engine) that could be used for such templates and that works modulo concrete set of modal operators and connectives.

Of course, I will have to find common proofs for each of the logic but I plan to automate this task by formalizing each concrete logic in Coq or Isabelle/HOL as it has already be done by linear logics. Then (semi)automatic proof search can lead to the proofs of rejections of soundness and completeness theorems and other theorems for each logic. I am even thinking about combination of genetic search (for the operators/connectives/their sequence rules) with automatic theorem proving (for the theorems about concrete logic) (possibly - with deep learning inspired) for (semi)automatic discovery and development of logics. But to guide all this process, to predict the most general grammar for the possible logics, I should be sure that there is nothing beyond those 5 features. (Neural methods have stuck in deadlock, as can be seen from delayed introduction of autonomous vehicles, that is why strong boost of symbolic methods is necessary and automation of the discovery and research of the logics is the key process for the adoption of symbolic methods in industrial setting).

After that I will have to find semantics, but I am sure that set semantics (with probability distributions and set operations and relations (for modalities and substructural connectives)) is sufficient for all those 5 features, because everything in math can be expressed by (ZFC) set theory and that is why any other possible (sophisticated) semantics can be expressed via sets anyway.

Of course, I am aware of the efforts by Logica Universalis community, but the Florian Rabe, but the community of categorical logics and institution theory. But I am having hard time to find the logic that already encompass those 5 features and also I can not find definite answer that those 5 features are exhaustive or am I missing something?

I would like to add that it is very important that everyone at this time come up with some advice or suggestion, idea. Now the economic crisis is starting again and it is very important to finalize the achievement of artificial intelligence and streamline them into industry exactly now. Only the increase of the supply side productivity (by the artificial intelligence) can save the us from the coming crisis.

• CommentRowNumber2.
• CommentAuthoratmacen
• CommentTimeOct 23rd 2019

My question is this - are there any other features beside those 5, features that can improve the expresiveness of the logic.

Depends on how you define “feature” “expre[ss]iveness”, and “logic”, I suppose.

But to be less fussy: would dependent types make the list?

Also, if you’re confident that ZFC can model everything you’ve considered, why don’t you just use that? Normally the point of formal logic is to restrict expressiveness. (Or from another perspective: increase generality.)

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeOct 24th 2019

There are plenty of points to formal logic other than restricting expressiveness. (But finalizing the achievement of artificial intelligence to save us from the coming economic crisis is not one of them.)

• CommentRowNumber4.
• CommentAuthorTodd_Trimble
• CommentTimeOct 24th 2019

I don’t know which coming crises may be meant, but please let there be no political discussions at this Forum.

• CommentRowNumber5.
• CommentAuthoratmacen
• CommentTimeOct 24th 2019

I see that “point” was the wrong word to use. I meant that logics are normally designed to serve their purpose(s) by restricting expressiveness. But now I’m guessing that’s not how a structuralist sees it.

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeOct 24th 2019

I doubt most logicians would say that ordinary first-order logic, for instance, serves its purpose by restricting expressiveness.

• CommentRowNumber7.
• CommentAuthoratmacen
• CommentTimeOct 24th 2019

Why not? Isn’t it considered less expressive than second-order logic, for example? And isn’t the purpose of the restriction to first order for model theory in order to get completeness?

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeOct 25th 2019

I suppose you could say that the reason a car doesn’t have a rocket engine is so that you’ll be able to control it on the highway, but most people wouldn’t consider “not having a rocket engine” as a defining feature of the design of a car. It’s not as if there is some unique maximally expressive system out there and everything else is obtained from it by reducing expressivity. We design a formal system to serve a particular purpose; it generally ends up being more expressive than some systems and less expressive than others. Maybe sometimes we design it by starting from an existing system and reducing the expressivity, but other times we do it by starting from some existing system and increasing the expressivity, or maybe we build it out of whole cloth without reference to anything on the shelf. Expressivity is certainly related to the purpose of a logic, but I see no evidence for the claim that normally the goal is to decrease expressivity.

• CommentRowNumber9.
• CommentAuthoratmacen
• CommentTimeOct 25th 2019

We design a formal system to serve a particular purpose; it generally ends up being more expressive than some systems and less expressive than others. … Expressivity is certainly related to the purpose of a logic, but I see no evidence for the claim that normally the goal is to decrease expressivity.

If a system is less expressive than some other, and the restriction is important, then I consider it an example. I’m not saying every new logic strives to be more restrictive than all the earlier ones.

To put this back in the context of tomr’s project, he seems to be trying to maximize expressiveness in some sense he hasn’t really explained, but he’s doing it in a way that seemed weird to me: piling a bunch of features into a language, rather than finding a model in which all features he could conceivably be interested in are constructable. He did mention wanting to get a model, but my point was that maybe the model is enough, and a complicated logic doesn’t help.

But considering his message again, it sounds like he might be aiming for a logic programming language, so the suggestion to just use the model was probably silly. (There still ought to be a better way than piling up features, though.)