Cite as https://practal.com/press/aair/1 February 5, 2023In my last post I have described in detail the theory
Foundation.practal, which I planned to become the basis of any theory development in Practal. A version without custom syntax is displayed again below:
The idea was that any other theory had to directly or indirectly
import this foundational theory. As such,
Foundation.practal would be special. Therefore I didn’t
consider it a problem that Practal would need to treat the abstractions
\for-all in a special way which
is not apparent from looking at
out of Abstraction Logic’s four proof rules, two have been specially
designed to help capture the meaning of
\implies A Band
A, the theorem
Bcan be deduced.
A[x], the theorem
\for-all x. A[x]can be deduced. Note that this inference rule cannot be simply represented as the axiom
\implies A[x] (\for-all x. A[x]), as this axiom actually describes the existential quantifier, not the universal one.
In the semantics of Abstraction Logic, these special rules are represented by the move from general abstraction algebras to logic algebras.
The other two proof rules, axiom invocation and substitution, are generic and do not depend in any way on the particular abstractions involved.
This morning I started to think about how to organize theory import and modules. At some point I realized that my current concept of abstraction logic is too narrow. Instead of defining an abstraction logic as a logic signature together with a list of axioms, I should rather define it as follows:
An abstraction logic is a signature together with a list of inference rules.
This definition eliminates any mention of special abstractions like
\for-all, and replaces the list
of axioms by a list of inference rules. Axioms are just inference rules
without any premisses, so this redefinition of our notion of abstraction
logic strictly generalizes the old one.
Of course, the success of this new definition depends on whether we can represent inference rules similarly straightforwardly as we represent axioms. An axiom is just a term. An inference rule consists of a conclusion and a list of premisses. The conclusion is just a term, while a premise is a template \([x_1, \ldots, x_n.\ t]\). The semantic idea is that the \(x_1, \ldots, x_n\) are universally quantified over.
The inference rules for modus ponens and universal quantification could then be written like this:
rule Modus-ponens: premise \implies A B premise A infer B
Introduction of universal quantification
rule Universal-quantification-intro: premise x. A[x] infer \for-all x. A[x]
We can thus replace the previous four proof rules by just two proof rules, one rule for substitution, and the other one for applying inference rules. It is even possible to go one step further, and to replace the proof rule for substitution by an inference rule:
rule Substitution: premise x. A[x] infer A[x]
This leaves us with a single proof rule, the one for applying inference rules!
It should be relatively easy to implement inference rules for Practal. Of course, we still need to carefully check if the theory of Abstraction Logic holds up under these changes. Ideally, we do that by formalizing Abstraction Logic in Practal!
Foundation.practal is of course still a special
theory in that it forms a complete logical system (at least if all the
details turn out to be correct), and internally, Practal might optimize
it, from an external point of view
now a theory just like any other. This is good news for theory import
and for modularization!
Even under this new definition, Abstraction Logic has still a proper model-theoretic semantics. So these inference rules are really axioms after all; it is just that our first take on how the axioms of Abstraction Logic look like was too simple.
If you’ve read so far, and like the direction Practal is going, please consider sponsoring Practal. I am now working full-time on Practal, and would like to continue to do so! I am also happy to give talks about Practal and Abstraction Logic either remotely or on-site. If you’d like to leverage Practal for your business, I am available for consulting services. I speak both English and German, and am happy to communicate in either of these languages.
You can contact me either through Practal’s sponsoring
page, or directly via