Bueno, no entiendo exactamente en relación a qué va esa pregunta.
Creo que me preguntás esto:
Dados unos símbolos S, y un lenguaje L hecho con ellos,
se dan después unos Axiomas lógicos A1, A2,...
Esa lista de axiomas lógicos son como cualquier otra lista de axiomas.
Es una lista de "expresiones" escritas en el lenguaje formal L, y listo.
En principio, no hay criterio alguno para dar esas reglas.
La gente es capaz de inventar muchas lógicas distintas.
Yo te dí dos ejemplos clásicos sencillos: la lógica clásica, y la intuicionista, que lo único que hace es "quitarle" el axioma del "tercero excluido" a la lista clásica.
Del thread del Teorema de godel, te copio la lista que dio Gustavo de los axiomas de la lógica "clásica", en su momento :
Finalmente, agregamos al lenguaje un símbolo especial, digamos \( \otimes{} \), que servirá para escribir sucesiones de fórmulas. Formalmente definimos:
Axiomas lógicos:
Por definición, un axioma lógico es cualquier fórmula que se obtenga de los esquemas siguientes. (Como ya dije en otro mensaje, estos esquemas definen en realidad un algoritmo que permite reconocer, dada una fórmula, si ésta es, o no, un axioma lógico.)
1. \( F\Rightarrow{}(G\Rightarrow{}F) \), donde \( F \) y \( G \) son fórmuas cualesquiera.
2. \( F\Rightarrow{}(G\Rightarrow{}H)\Rightarrow{}((F\Rightarrow{}G)\Rightarrow{}(F\Rightarrow{}H)) \), donde \( F \), \( G \) y \( H \) son fórmuas cualesquiera.
3. \( (-F\Rightarrow{}-G)\Rightarrow{}(G\Rightarrow{}F) \), donde \( F \) y \( G \) son fórmuas cualesquiera.
4. \( \forall{x}F(x)\Rightarrow{}F(x/t) \).
Una explicación aquí: \( x \) respresenta una variable cualquiera y cuando escribimos \( F(x) \) entendemos que \( x \) es una variable libre en F, \( t \) es un término y \( F(x/t) \) es la fómrula que se obtiene reemplazando toda aparición de la variable \( x \) por el término \( t \). Una restricción: si \( t \) tiene variables, ninguna de éstas puede aparecer afectada por un cuantificador al efectuarse el reemplazo.
5. \( \forall{x}(F\Rightarrow{}G)\Rightarrow{}(F\Rightarrow{}\forall{x}G) \) siempre que \( x \) no aparezca libre en \( F \).
6. \( x = x \), donde \( x \) es una variable cualquiera.
7. \( x = y \Rightarrow{} y = x \), donde \( x \) e \( y \) son variables cualesquiera.
8. \( x = y \Rightarrow{} (y = z\Rightarrow{} x = z) \)
9. \( x = y \Rightarrow{} t(z_1, z_2,\ldots z_{k-1},x,z_{k+1}\ldots z_n) = t(z_1, z_2,\ldots z_{k-1},y,z_{k+1}\ldots z_n) \), donde \( t \) es un término cualquiera.
10. \( x = y \Rightarrow{} F(z_1, z_2,\ldots z_{k-1},x,z_{k+1}\ldots z_n) \Rightarrow{} F(z_1, z_2,\ldots z_{k-1},y,z_{k+1}\ldots z_n) \), donde \( F \) es una fórmula cualquiera.
Los axiomas 9 y 10 dicen esencialmente que si \( x=y \) entonces podemos reemplazar libremente \( x \) por \( y \).
Los esquemas del 1 al 5 son los axiomas de la lógica primer orden, al agregar los otros se obtiene la lógica de primer orden con igualdad.
Ahora bien, para que la lógica "trabaje" hacen falta "reglas de inferencia".
Si hay una lista de proposiciones, todas ellas "axiomas" o "demostradas",
si entre ellas figuran \( p \) y \( p\Rightarrow{q} \), entonces está permitido "escribir" una nueva proposición, a saber, \( q \), y se la considera "demostrada".
Ese es el razonamiento "Modus Ponens".
En la lista anterior están dados unos axiomas escritos todos con \( \Rightarrow{} \).
No figura explícitamente la ley de "no contradicción", así que habrá que "demostrarla" a partir de los axiomas puestos ahí.
Lo mismo con la ley del "tercero excluido", que no me queda claro cómo se demuestra a partir de esa lista de axiomas. Imagino que habrá que hacer varios cálculos hasta lograrlo.
Mas, la cuestión es que uno puede dar entonces otra lista de axiomas en los que figure el "principio de no contradicción":
\( \sim{(F\wedge\sim{F})} \)
Y después uno podría mostrar que estos axiomas lógicos son equivalentes a los de más arriba.
Uno puede poner los axiomas que quiera, y también puede elegir la "regla de inferencia" que se le antoje.
A continuación, uno se pone a analizar si esa lógica tiene "algún sentido".
O sea, una lógica que permitiera demostrar todas las proposiciones del lenguaje, no serviría para nada, ya que nuestro sentido común nos dice que, como vos bien decís, no puede aceptarse que sean demostrables tanto \( P \) como su negación \( \sim{P} \), o sea, no tiene sentido una lógica en que se demuestran "contradicciones".
Luego uno se pone a analizar otras cosas.
Por ejemplo, si con esa lógica es posible construir alguna otra teoría, ya sea de conjuntos , o de números.
Para esto, se agregan más axiomas: axiomas de una teoría específica, o sea, axiomas no lógicos.
Uno podría agregar los Axiomas de Peano, y ver qué pasa.
Al analizar una teoría, uno estudia si los axiomas de esa teoría no se contradicen entre sí, si unos axiomas implican a otros o no (si no lo hacen, se dice que los axiomas son "independientes"), y si la teoría es completa, o sea: dada cualquier proposición p, uno querría poder afirmar si p es demostrable, o bien su negación no-p es demostrable.
Si hay una proposición sobre la que no se puede demostrar ni p ni no-p, se dice que p es "indecidible", claro está, y la teoría que la contiene se dice que es "incompleta", pues hay algo que no se puede demostrar.
