a-logic

We present an extension of first-order predicate logic with a novel predicate ‘at t’ meaning intuitively “this term is a variable symbol”. We give simple sequent proof-rules for it, we demonstrate cut-elimination for the resulting logic, and we give a semantics for which the logic is sound and complete. Because we can now make assertions about what would normally be considered an intensional property of a term (being a variable symbol) we can now express inside the logic, properties of its terms and predicates which would normally be external to the logic. We give axiomatisations in a-logic, including of the lambdacalculus, and discuss what relevance this might have to logic programming.

• Type: Conference
• Year: 2005
• Where: BIRTHDAY
• Authors: Murdoch Gabbay, Michael Gabbay
• Keywords: Applied Computing, BIRTHDAY 2005, Predicate ‘at T, Variable Symbol, first-order Predicate Logic