¿Es posible esta prueba en Fitch?

¡Buenas noches! Tengo una pregunta sobre la siguiente prueba práctica que me ha dado mi profesor:

Premisa:

  1. ∃x ((P(a) ∧ ∀y (P(y) → y = x)) ∧ R(x))
  2. P(b) ∧ ∀y (P(y) → y = b)

Demostrar: R(b)

Entiendo que esta prueba es cierta , sin embargo, parece que no puedo demostrarlo usando las reglas de Fitch.

Esto es lo que tengo hasta ahora. ¿Cómo debo hacer para probar esto aún más? Estaba pensando así: si de alguna manera puedo llegar a P(a) ∧ ∀y (P(y) → y = b)) ∧ R(b)), puedo obtener R(b) a través de la eliminación de conjunciones. Sin embargo, no estoy seguro de cómo la segunda premisa puede ayudar con eso.

Editar: parece que esta prueba se puede hacer solo con reglas de eliminación. Todavía tengo que averiguarlo.

ingrese la descripción de la imagen aquí

Primero, danos una demostración informal. Luego, podemos ayudarlo a traducirlo en una prueba formal.
@MarkGuardando la forma en que estaba pensando era esta: si puedo llegar a P(a) ∧ ∀y (P(y) → y = b)) ∧ R(b)), puedo obtener R(b) a través de la eliminación de conjunciones . Sin embargo, no estoy seguro de cómo la segunda premisa puede ayudar con eso.
Es mejor que agregue los pensamientos anteriores a su publicación original, también su interfaz de usuario de Fitch adjunta es ilegible ...
@mohottnad agregó mis pensamientos a la publicación original, la interfaz de usuario parece estar bien de mi lado, ¿qué tiene de ilegible?
Parece demasiado pequeño para leer en mi escritorio.
@mohottnad He publicado una imagen más grande, debería ser mejor.
Sin la segunda premisa, no puede estar seguro de que debe existir b en el dominio, y su segundo conjunto le asegura que siempre que P(y) se mantenga y debe ser b ...

Respuestas (1)

La clave es que no puedes sustituir b inicialmente, sólo una constante arbitraria C esta permitido. Entonces puedes intentar usar el segundo conjunto de tu segunda premisa para probar C = b dentro de la misma subdemostración. Entonces también tienes que invocar tus reglas de igualdad relacionadas y PAG ( b ) se necesita aquí para permitirle invocar la regla ∀-elim (permitirle sustituir con seguridad b para y ) en la subdemostración subsiguiente para llegar a C = b ...

¿Es posible esta prueba en Fitch?
RespuestasAquíPolítica de privacidad1y, 0v