2
$\begingroup$

As part of my research on building an interactive theorem proving system, I have discovered a new logic that I call Abstraction logic. I have written up the details here: https://doi.org/10.47757/abstraction.logic.1

I am an expert in interactive theorem proving, but I would not consider myself an expert in logic. When researching the foundations of my system I came across the work of Rasiowa, and went from there. But that work is a few decades old. So I don't know if Abstraction Logic is actually new, or maybe exists already under a different name, maybe in more general form. Any comments and pointers would be very welcome!

Here is the abstract of the report:

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound and complete with respect to an intuitive and simple algebraic semantics.

Edit: To clarify my question, I think I am basically asking an expert in algebraic logic if my work is new. It seems to me that algebraic logic focuses on propositional logic. That is what Rasiowas book "An algebraic approach to non-classical logics" does. She also treats quantifiers, but separately. Abstraction logic unifies this, because quantifiers are just ordinary constants now. This is of course standard in type-theoretic approaches, but abstraction logic does not need any types. What I am saying is that first-order logic is not the proper extension of propositional calculus. Abstraction logic is. Furthermore, with abstraction logic, the need for type theory goes away: all it really provided was binders anyway, and abstraction logic provides that in a cheaper and simpler package.

Further Edit: In his 1995 paper, "Algebraic semantics for predicate logics and their completeness", Hiroakira Ono concludes that

So, one of the most important questions in the study of algebraic semantics for predicate logics would be how to give an appropriate interpretation of quantifiers, in other words, how to extend algebraic semantics.

I think Abstraction Logic provides such an interpretation. Has this issue been solved since 1995, or would Abstraction Logic be the first solution to this?

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ At the moment, this question is not at all self-contained — it really asks us to read the paper to get a clear idea of what your “abstraction logic” is, so it amounts mostly to “please read my paper and comment”, which is discouraged here. If you could edit the question to include a concise presentation of the logic (at least its key points), then it would be much more answerable. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Oct 22, 2021 at 12:24
  • 1
    $\begingroup$ I "read" the paper. The OP is asking about abstract syntax with variable binding and syntactic signatures. I think we can keep the OP busy reading papers for at least a week. $\endgroup$
    – Andrej Bauer
    Commented Oct 22, 2021 at 12:33

1 Answer 1

Reset to default
4
$\begingroup$

These should get you started on syntax with binding:

  1. Pfenning, Eliott: Higher-Order Abstract Syntax
  2. Gabbay: Foundations of nominal techniques: logic and semantics of variables in abstract syntax
  3. Fiore, Plotkin, Turi: Abstract Syntax of Variable Binding
  4. Power, Tanaka: Binding signatures for generic contexts

As far as syntactic signatures are concerned, I am not sure what original sources to point you to, but you can read a short organized account in A general definition of dependent type theories, and for a formalized version see Expression.v and Signature.v in the accompanying formalization. I am certain there is prior work that is relevant but I cannot think of it now, perhaps someone else can chip in. A variant with abstraction being an explicit operation is described here, and formalized here.

Improve this answer
$\endgroup$
11
  • 1
    $\begingroup$ I read the Higher-Order Abstract Syntax paper, and I am aware of general work on abstract syntax, of course. I am aware of the work in dependent type theories, but the nice thing about my approach is that no type theories are needed. $\endgroup$
    – Steven Obua
    Commented Oct 22, 2021 at 12:42
  • $\begingroup$ Don't dismiss the papers just because they mention type theory in the title or somewhere in the text. Type theories are often organized in two stages, of which the first stage goes under the terms "raw syntax" or "presyntax". Those are single sorted (or sometimes two-sorted, but that's inessential) and describe just the raw syntactic structure of expressions. These concepts correspond quite precisely to the ones you have developed. $\endgroup$
    – Andrej Bauer
    Commented Oct 22, 2021 at 12:49
  • 1
    $\begingroup$ My work actually tries to get rid of type theory altogether :-) So dismissing type theory is kind of the point of it. Note that I am not just providing a syntax. It is a logic, it includes first-order logic, has binders, is complete under very weak assumptions. I also provide new proofs for the completeness of intuitionistic and classical logic using abstraction logic. $\endgroup$
    – Steven Obua
    Commented Oct 22, 2021 at 12:58
  • 1
    $\begingroup$ I think I just have to state more boldly my claim: Abstraction Logic is the simplest self-contained logic that is sound and complete. By self-contained I mean that you can base an interactive theorem proving system on it. It should replace first-order logic in textbooks. Now, if you think the same claim holds for nominal logic, then yes, you could consider them related. Otherwise, it is just not relevant. $\endgroup$
    – Steven Obua
    Commented Oct 22, 2021 at 22:39
  • 1
    $\begingroup$ So my question really is: Is there something simpler or the same out there that has already been done? I don't think so, but obviously it could be the case. Nominal Logic clearly isn't it, that's why I dismiss it. Otherwise they are obviously related, both are extensions of first-order logic, and both provide a way for dealing with binders. But you can write down the axioms for nominal logic in abstraction logic. So abstraction logic can be used as a foundation for nominal logic. I consider nominal logic as orthogonal to abstraction logic and serving a different purpose. $\endgroup$
    – Steven Obua
    Commented Oct 22, 2021 at 22:57

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .