Nominalistic Logic (Extended Abstract)

TL;DR

Nominalistic Logic (NL) is a novel presentation of Intensional Type Theory using sequent calculus and a nominalization axiom, enabling natural number derivations without extensionality or infinity axioms.

Contribution

It introduces a new sequent calculus formulation of ITT with a succinct nominalization axiom, expanding the logical framework for natural number derivation.

Findings

Derives Peano's postulates using the nominalization axiom

No need for extensionality or infinity axioms in NL

Provides a flexible comprehension axiom

Abstract

Nominalistic Logic (NL) is a new presentation of Paul Gilmore's Intensional Type Theory (ITT) as a sequent calculus together with a succinct nominalization axiom (N) that permits names of predicates as individuals in certain cases. The logic has a flexible comprehension axiom, but no extensionality axiom and no infinity axiom, although axiom N is the key to the derivation of Peano's postulates for the natural numbers.