Una referencia estándar para el tema es Simpson (2009), mientras que una introducción para no especialistas es Stillwell (2018).
Una introducción a las matemáticas inversas de orden superior, y también el artículo fundador, es Kohlenbach (2005).
En las matemáticas inversas, se comienza con un lenguaje marco y una teoría base -un sistema de axiomas central- que es demasiado débil para demostrar la mayoría de los teoremas en los que uno podría estar interesado, pero lo suficientemente potente como para desarrollar las definiciones necesarias para enunciar estos teoremas.
Por ejemplo, la aritmética de segundo orden puede expresar el principio "Todo espacio vectorial contable tiene una base", pero no puede expresar el principio "Todo espacio vectorial tiene una base".
En términos prácticos, esto significa que los teoremas de álgebra y combinatoria están restringidos a estructuras numerables, mientras que los teoremas de análisis y topología están restringidos a espacios separables.
Por ejemplo, "cada cuerpo tiene una clausura algebraica" no es demostrable en la teoría de conjuntos ZF, pero la forma restringida "cada cuerpo contable tiene una clausura algebraica" es demostrable en RCA0, el sistema más débil típicamente empleado en matemáticas inversas.
Por ejemplo, una función continua en el espacio de Cantor es solo una función que mapea secuencias binarias a secuencias binarias, y que también satisface la definición habitual de continuidad 'épsilon-delta'.
Muchos objetos matemáticos, como numerable anillos, grupos, y cuerpos, así como puntos en espacios polacos efectivos, pueden representarse como conjuntos de números naturales, y módulo a esta representación puede estudiarse en aritmética de segundo orden.
En orden creciente de fortaleza, estos sistemas se denominan por las iniciales RCA0, WKL0, ACA0, ATR0 y Π11-CA0.
La siguiente table resume los "cinco grandes" sistemas y lista las contrapartidas en la aritmética de orden superior.