If You Build It, They Will Come
Technical Reports by Steven Obua
Updated November 27, 2021 This article is a work in progress Philosophy of Abstraction Logic
Abstraction Logic has been introduced in a previous, rather technical article. In this article we take a step back and look at Abstraction Logic from a conceptual point of view. This will make it easier to appreciate the simplicity, elegance, and pragmatism of Abstraction Logic. We will argue that Abstraction Logic is the best logic for serving as a foundation of mathematics.
October 22, 2021 (revised November 14, 2021) https://doi.org/10.47757/abstraction.logic.2 Abstraction Logic
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 with respect to an intuitive and simple algebraic semantics. Completeness holds for both intuitionistic and classical abstraction logic, and all abstraction logics in between and beyond.
July 29, 2021 https://doi.org/10.47757/practical.types.1 Practical Types
These are preliminary notes about Practal’s logic and its system of practical types. This is ongoing research, and I expect updates to this document over time. Practal Light is a research prototype implementing (part of) what is presented in this document.
July 17, 2021 https://doi.org/10.47757/practal.1 Practal — Practical Logic
This is a first sketch of the design of Practal, an interactive theorem proving system for practical logic.
July 1, 2021 https://doi.org/10.47757/obua.cosmo-id.3 Cosmopolitan Identifiers
I propose a simple Unicode-based lexical syntax for programming language identifiers using characters from international scripts (currently Latin, Greek, Cyrillic and Math). Such cosmopolitan identifiers are designed to achieve much of the simplicity of Fortran identifiers while acknowledging a modern international outlook. This seems particularly advantageous in contexts where such identifiers are not (only) used by professional programmers, but are exposed to normal users, for example through scriptable applications.
May 18, 2021 https://doi.org/10.47757/obua.ll.1 A New Semantics for Local Lexing
A revised semantics for Local Lexing is presented that entirely avoids priority conflicts between non-empty tokens. Pyramid Grammars are introduced, and their semantics is given in terms of Local Lexing. It is demonstrated that they are more expressive than Context-Free Grammars, and at least as expressive as Parsing Expression Grammars.