Modal logical operators. Provable Necessary



Kripke Semantics


Free Logic Free logic supports a notion of partiality. Terms aren’t assumed to exists. automating categor theorey is isabelle hol inclusive logic

  • Partial horn logic
  • GATs Generalized algerbaic theories - Catlab.jl
  • Essentially algerbaic theories

Membership equality logic & order sorted logic are two things in maude. See term rewriting notes


Also see:

  • type theory
  • proof theory

Intuitionistic vs constructive. Giving a recipe how to construct a thing (possibly algorithmic) vs saying that it is inconsistent for the thing to not exist. These are not the same notion.

There’s also a feeling of “observation” a bit. The big hang up is certain sectors of our technical culture are saturated by boolean reasoning. Facts are true or false. Proven vs unproven is not the same thing as true or false. An unproven thing may become true if you run your inference a little longer, or perhaps if you add new reasonable axioms. If I only tell you the law of addition that 0 + x = x, can you tell me that x + y = y + x? No, you need more stuff. In this context the fact being “true” is a very relative thing to your axioms, inference rules, and processing time. Now we all kind of agree natural numbers exist. Are these sentences true in the naturals? Yes. In many reasonable systems to model what the naturals might mean, these laws are derivable. But if you get a little more crazy with your questions you start asking hard stuff where it isn’t clear that all reasonable systems can derive these facts. Then truth becomes way more relative feeling, in analogy to the simple intentionally limited case.

Substructural Logics The context Gamma is not set-like. Explicit swapping necessary - list like Explicit duplication - multi-set like. Useful for modelling resource usage. Linear logic


finvect model

Cyclone Regions Tofte

Linear logic is resource sensitive. It is vaguely similar to

  • Rust lifetimes
  • Quantum information nad the no-cloning theorem

Can these be made precise?

It is realted to seperation logic in that both are substructural logics and in

It gives interesting insight into the proof search process of prolog and ilk.

Frank Pfenning had a funky example involving making change.

Chris Martens thesis Interactive worlds with linear logic strange loop talk ceptre Celf Ceptre stateful computation “frame property” all the stuff that strays the same purely functional - pass entire state datalog - database update celf - state update

Idris2 Linear haskell ATS Rust QTT - Quantitative type theory

Mercury has linear types of some kind

What if I modelled destructive rewrite rules in egglog as linear logical? Is a linear logic programmign langguae a good candidate for a prolog metainterpreter?

Separation Logic

Bunched Logic

Non-monotonic logic

In the theory and history of ASP this stuff shows up

  • Default logic
  • Autoepistemic logic