¿Las constantes de la verdad se consideran fórmulas atómicas?

Question

Esta es una cuestión puramente terminológica (y tediosa).

Dado un lenguaje de lógica de primer orden que incluye la constante de verdad $\bot$ (falsedad), ¿se considera esta constante como un atómica ¿fórmula o no?

Sé que la obra de Prawitz " Deducción natural " (p. 14) define $\bot$ como fórmula atómica.

Por el contrario, el programa de Troelstra y Schwichtenberg " Teoría básica de la prueba " (p. 2) no considera $\bot$ como fórmula atómica.

A menudo, una fórmula atómica en la lógica de primer orden se define simplemente como una $n$ -Símbolo de predicado de carácter secundario aplicado a $n$ términos, pero en una lengua en la que $\bot$ no está incluido. Este es el caso, por ejemplo, de la página de Wikipedia que define fórmulas bien formadas (pero la página de Wikipedia que define fórmulas atómicas adopta la terminología de Troelstra y Schwichtenberg).

¿Existen otros manuales (conocidos) de lógica que consideren $\bot$ como fórmula atómica? ¿Cuál es la solución terminológica más común en la literatura?

Answer 1

En realidad hay tres formas de tratar el $\bot$ (y lo mismo para $\top$ Si eso forma parte de su idioma).

1. Como fórmula atómica (diferente, sin embargo, de la fórmula atómica más "típica" que tiene un término de predicado)

2. Como algo que no es una fórmula atómica pero que sigue "actuando como" una fórmula atómica en sus usos. Por ejemplo, se podría definir el conjunto de "fórmulas base" como el conjunto de "fórmulas atómicas" (las que implican símbolos de predicado) junto con $\bot$ (y $\top$ ), y esas "fórmulas base" pueden combinarse con otras utilizando conectivos de verdad-función.

3. Como abreviatura sintáctica de una disyunción generalizada con $0$ disyuntivas. Es decir, se puede ver el $\bot$ no es una fórmula atómica ni actúa como tal, sino que es una fórmula compleja (es decir, una disyunción generalizada (que disjunta cualquier número de declaraciones) ... con $0$ disyuntivas). Esto puede ser útil cuando se tienen disyunciones generalizadas como parte de la manera formal de construir enunciados (a diferencia de los enfoques más "tradicionales" en los que las disyunciones se entienden típicamente como si tomaran exactamente dos enunciados para sus disyuntos), y cuando se hace eso, también podría ser útil (por ejemplo, para sus pruebas metateóricas) permitir que las disyunciones generalizadas tengan $0$ disyuntivas ... y utilizar $\bot$ como una forma de expresarlos.

Ah, y en realidad hay otro uso que a veces veo para el $\bot$ que es utilizarlo como valor de verdad $False$ o como el valor $0$ en un álgebra booleana. Realmente no me gusta esa práctica, ya que hay una gran diferencia importante entre un valor de verdad y un enunciado (aunque sea uno, como el $\bot$ que siempre adquiere un cierto valor de verdad), por lo que a mis ojos no merece un 4. ... pero como he dicho, puede que se vea esto en otros libros todavía.

Por mi experiencia, diría que la 3 es bastante inusual, pero tanto la 1 como la 2 son bastante comunes.