Inny system dowodzenia w logice pierwszego rzędu
: 18 lis 2025, o 13:34
Rozważmy pewien język pierwszego rzędu \(\displaystyle{ \mathcal L}\).
Wprowadzę najpierw kilka definicji mojego autorstwa:
Mówimy, że formuła \(\displaystyle{ \phi}\) wynika tautologicznie ze zbioru formuł \(\displaystyle{ \Delta}\), gdy istnieją formuły rachunku zdań \(\displaystyle{ A_1,\ldots, A_n}\), \(\displaystyle{ A}\) oraz przyporządowanie \(\displaystyle{ \Phi}\) każdej zmiennej zdaniowej \(\displaystyle{ p}\) formuły \(\displaystyle{ \Phi_p}\) takie, że \(\displaystyle{ A_1,\ldots,A_n\vdash A}\), \(\displaystyle{ \phi=A[\Phi]}\) oraz \(\displaystyle{ A_i[\Phi]\in\Delta}\) dla każdego \(\displaystyle{ i}\), gdzie \(\displaystyle{ A[\Phi]}\) oznacza formułę będącą efektem wstawienia w \(\displaystyle{ A}\) w miejsce każdej zmiennej zdaniowej \(\displaystyle{ p}\) formuły \(\displaystyle{ \Phi_p}\).
Mówimy, że formuła \(\displaystyle{ \phi}\) jest efektem podstawienia termu \(\displaystyle{ t}\) w formule \(\displaystyle{ \Phi}\), gdy \(\displaystyle{ \Phi=\forall x\Phi^*}\) dla pewnej zmiennej \(\displaystyle{ x}\) i formuły \(\displaystyle{ \Phi^*}\), zaś \(\displaystyle{ \phi}\) powstaje przez zastąpienie każdego wolnego wystąpienia \(\displaystyle{ x}\) w \(\displaystyle{ \Phi^*}\) termem \(\displaystyle{ t}\), przy czym każde wolne wystąpienie \(\displaystyle{ x}\) w \(\displaystyle{ \Phi^*}\) nie znajduje się w zasięgu kwantyfikatora \(\displaystyle{ \forall y}\) dla zmiennych \(\displaystyle{ y}\) termu \(\displaystyle{ t}\).
Ciąg formuł \(\displaystyle{ (\phi_i)_{i=0}^n}\) nazywamy dedukcją od \(\displaystyle{ \phi}\) do \(\displaystyle{ \psi}\) ze zbioru \(\displaystyle{ \Delta}\) przy ustalonych zmiennych w zbiorze \(\displaystyle{ \mathcal V}\), gdy wszystkie zmienne wolne formuł \(\displaystyle{ \phi_i}\) są w zbiorze \(\displaystyle{ \mathcal V}\), \(\displaystyle{ \phi_0=\phi}\), \(\displaystyle{ \phi_n=\psi}\) oraz dla każdego \(\displaystyle{ i\in\{1,\ldots, n\}}\) formuła \(\displaystyle{ \phi_i}\) wynika tautologicznie ze zbioru \(\displaystyle{ \Delta\cup\{\phi_0,\ldots,\phi_{i-1}\}}\) lub \(\displaystyle{ \phi_i}\) jest efektem podstawienia pewnego termu \(\displaystyle{ t}\) o wszystkich zmiennych w \(\displaystyle{ \mathcal V}\) w pewnej formule \(\displaystyle{ \Phi\in\Delta\cup\{\phi_0,\ldots,\phi_{i-1}\}}\) lub \(\displaystyle{ \phi_i=(\alpha\Rightarrow \beta)}\) dla pewnych formuł \(\displaystyle{ \alpha}\) oraz \(\displaystyle{ \beta}\) i istnieje dedukcja od \(\displaystyle{ \alpha}\) do \(\displaystyle{ \beta}\) ze zbioru \(\displaystyle{ \Delta\cup\{\phi_0,\ldots,\phi_{i-1}\}}\) przy ustalonych zmiennych \(\displaystyle{ \mathcal V}\), lub istnieje generalizacja formuły \(\displaystyle{ \phi_i}\) po pewnej zmiennej \(\displaystyle{ x\notin\mathcal V}\) przy ustalonych zmiennych w \(\displaystyle{ \mathcal V}\) i ze zbioru \(\displaystyle{ \Delta\cup\{\phi_0,\ldots,\phi_{i-1}\}}\).
Ciąg formuł \(\displaystyle{ (\phi_i)_{i=1}^n}\) nazywamy generalizacją formuły \(\displaystyle{ \psi}\) po zmiennej \(\displaystyle{ x}\) przy ustalonych zmiennych w zbiorze \(\displaystyle{ \mathcal V}\) ze zbioru \(\displaystyle{ \Delta}\), gdy \(\displaystyle{ x\notin \mathcal V}\), wszystkie zmienne wolne formuł \(\displaystyle{ \phi_i}\) są w zbiorze \(\displaystyle{ \mathcal V\cup\{x\}}\), \(\displaystyle{ \psi=\forall x \phi_n}\) oraz dla każdego \(\displaystyle{ i\in\{1,\ldots, n\}}\) formuła \(\displaystyle{ \phi_i}\) wynika tautologicznie ze zbioru \(\displaystyle{ \Delta\cup\{\phi_1,\ldots,\phi_{i-1}\}}\) lub \(\displaystyle{ \phi_i}\) jest efektem podstawienia pewnego termu \(\displaystyle{ t}\) o wszystkich zmiennych w \(\displaystyle{ \mathcal V\cup\{x\}}\) w pewnej formule \(\displaystyle{ \Phi\in\Delta\cup\{\phi_1,\ldots,\phi_{i-1}\}}\) lub \(\displaystyle{ \phi_i=(\alpha\Rightarrow \beta)}\) dla pewnych formuł \(\displaystyle{ \alpha}\) oraz \(\displaystyle{ \beta}\) i istnieje dedukcja od \(\displaystyle{ \alpha}\) do \(\displaystyle{ \beta}\) ze zbioru \(\displaystyle{ \Delta\cup\{\phi_1,\ldots,\phi_{i-1}\}}\) przy ustalonych zmiennych \(\displaystyle{ \mathcal V\cup\{x\}}\), lub istnieje generalizacja formuły \(\displaystyle{ \phi_i}\) po pewnej zmiennej \(\displaystyle{ x'\notin\mathcal V\cup\{x\}}\) przy ustalonych zmiennych w \(\displaystyle{ \mathcal V\cup\{x\}}\) i ze zbioru \(\displaystyle{ \Delta\cup\{\phi_1,\ldots,\phi_{i-1}\}}\).
Pytanie 1. Zdaje sobie sprawę, że powyższe definicje dedukcji i generalizacji są rekurencyjne i nie potrafię uzasadnić
ich poprawności. Formalnie mam na myśli dowód istnienia (i ewentualnie jednoznaczności) odpowiednich relacji na zbiorze skończonych ciągów formuł. Dokładnie, każdym \(\displaystyle{ \phi, \psi, \Delta,\mathcal V}\) chciałbym przyporządkować pewien podzbiór rodziny skończonych ciągów formuł (który będzie pełnił rolę ogółu dedukcji od \(\displaystyle{ \phi}\) do \(\displaystyle{ \psi}\) ze zbioru \(\displaystyle{ \Delta}\) przy ustalonych zmiennych w zbiorze \(\displaystyle{ \mathcal V}\)), i podobnie każdym \(\displaystyle{ \phi, x,\Delta,\mathcal V}\) chciałbym przyporządkować pewien podzbiór rodziny skończonych ciągów formuł (czyli ogół generalizacji formuły \(\displaystyle{ \phi}\) po zmiennej \(\displaystyle{ x}\) ze zbioru \(\displaystyle{ \Delta}\) przy ustalonych zmiennych w zbiorze \(\displaystyle{ \mathcal V}\)) - w ten sposób, żeby spełnione były warunki określone w definicjach, gdzie zastępuję bycie dedukcją lub generalizacją przez należenie do wspomnianych podzbiorów.
Mówimy, że formuła \(\displaystyle{ \phi}\) jest twierdzeniem uzasadnionym przez dedukcję, jeśli \(\displaystyle{ \phi=(\alpha\Rightarrow\beta)}\) dla pewnych \(\displaystyle{ \alpha}\) oraz \(\displaystyle{ \beta}\) i istnieje dedukcja od \(\displaystyle{ \alpha}\) do \(\displaystyle{ \beta}\) ze zbioru \(\displaystyle{ \Delta=\emptyset}\) przy braku ustalonych zmiennych tzn. \(\displaystyle{ \mathcal V=\emptyset}\).
Mówimy, że formuła \(\displaystyle{ \phi}\) jest twierdzeniem uzasadnionym przez generalizację, jeśli istnieje generalizacja \(\displaystyle{ \phi}\) po pewnej zmiennej \(\displaystyle{ x}\) i ze zbioru \(\displaystyle{ \Delta=\emptyset}\) przy braku ustalonych zmiennych tzn. \(\displaystyle{ \mathcal V=\emptyset}\).
Mówimy, że formuła \(\displaystyle{ \phi}\) jest twierdzeniem, gdy istnieje ciąg formuł \(\displaystyle{ (\phi_i)_{i=1}^n}\) bez zmiennych wolnych taki, że \(\displaystyle{ \phi_n=\phi}\) oraz dla każdego \(\displaystyle{ i}\) formuła \(\displaystyle{ \phi_i}\) jest twierdzeniem uzasadnionym przez dedukcję lub twierdzeniem uzasadnionym przez generalizację lub \(\displaystyle{ \phi_i}\) wynika tautologicznie ze zbioru \(\displaystyle{ \{\phi_1,\ldots,\phi_{i-1}\}}\) lub \(\displaystyle{ \phi}\) jest efektem podstawienia termu \(\displaystyle{ t}\) (bez zmiennych wolnych) w formule \(\displaystyle{ \Phi\in\{\phi_1,\ldots,\phi_{i-1}\}}\).
Pytanie 2. Jak uzsadadnić, że każde twierdzenie ma w istocie skończony dowód? Mam na myśli fakt, że uzasadnienie twierdzenia może być przez dedukcję/generalizację, która ma w sobie kolejną dedukcję/generalizację itd. ale zawsze skończy się to w skończonej ilości kroków na uzasadnieniu przez wynikanie tautologiczne bądź efekt podstawienia. Potrafię opisać to bardziej formalnie, ale mam nadzieję, że jest zrozumiale.
Pytanie 3. Wydaje mi się, że wszystkie twierdzenia, które jestem w stanie uzyskać w tym systemie, to dokładnie wszyskie twierdzenia klasycznego rachunku predykatów (w języku \(\displaystyle{ \mathcal L}\)), które nie mają zmiennych wolnych. Co sądzicie?
Podam jeszcze przykład dowodu prawa rachunku predykatów \(\displaystyle{ \forall x(A(x)\Rightarrow B(x))\Rightarrow \left(\forall x A(x)\Rightarrow \forall x B(x)\right)}\).
1.0 \(\displaystyle{ \forall x(A(x)\Rightarrow B(x))}\) - założenie
1.1.0\(\displaystyle{ \forall xA(x)}\) - założenie
1.1.1.0 ustalenie \(\displaystyle{ x}\)
1.1.1.1 \(\displaystyle{ A(x)\Rightarrow B(x)}\) - podstawienie \(\displaystyle{ x}\) do 1.0.
1.1.1.2 \(\displaystyle{ A(x)}\) - podstawienie \(\displaystyle{ x}\) do 1.1.0
1.1.1.3 \(\displaystyle{ B(x)}\) - wynikanie tautologiczne z 1.1.1.1 oraz 1.1.1.2
1.1.1 \(\displaystyle{ \forall x B(x)}\) - generalizacja 1.1.1.0-1.1.1.3
1.1. \(\displaystyle{ \forall x A(x)\Rightarrow \forall x B(x)}\) - dedukcja 1.1.0-1.1.1
1. \(\displaystyle{ \forall x(A(x)\Rightarrow B(x))\Rightarrow \left(\forall x A(x)\Rightarrow \forall x B(x)\right)}\) - dedukcja 1.0-1.1
Wprowadzę najpierw kilka definicji mojego autorstwa:
Mówimy, że formuła \(\displaystyle{ \phi}\) wynika tautologicznie ze zbioru formuł \(\displaystyle{ \Delta}\), gdy istnieją formuły rachunku zdań \(\displaystyle{ A_1,\ldots, A_n}\), \(\displaystyle{ A}\) oraz przyporządowanie \(\displaystyle{ \Phi}\) każdej zmiennej zdaniowej \(\displaystyle{ p}\) formuły \(\displaystyle{ \Phi_p}\) takie, że \(\displaystyle{ A_1,\ldots,A_n\vdash A}\), \(\displaystyle{ \phi=A[\Phi]}\) oraz \(\displaystyle{ A_i[\Phi]\in\Delta}\) dla każdego \(\displaystyle{ i}\), gdzie \(\displaystyle{ A[\Phi]}\) oznacza formułę będącą efektem wstawienia w \(\displaystyle{ A}\) w miejsce każdej zmiennej zdaniowej \(\displaystyle{ p}\) formuły \(\displaystyle{ \Phi_p}\).
Mówimy, że formuła \(\displaystyle{ \phi}\) jest efektem podstawienia termu \(\displaystyle{ t}\) w formule \(\displaystyle{ \Phi}\), gdy \(\displaystyle{ \Phi=\forall x\Phi^*}\) dla pewnej zmiennej \(\displaystyle{ x}\) i formuły \(\displaystyle{ \Phi^*}\), zaś \(\displaystyle{ \phi}\) powstaje przez zastąpienie każdego wolnego wystąpienia \(\displaystyle{ x}\) w \(\displaystyle{ \Phi^*}\) termem \(\displaystyle{ t}\), przy czym każde wolne wystąpienie \(\displaystyle{ x}\) w \(\displaystyle{ \Phi^*}\) nie znajduje się w zasięgu kwantyfikatora \(\displaystyle{ \forall y}\) dla zmiennych \(\displaystyle{ y}\) termu \(\displaystyle{ t}\).
Ciąg formuł \(\displaystyle{ (\phi_i)_{i=0}^n}\) nazywamy dedukcją od \(\displaystyle{ \phi}\) do \(\displaystyle{ \psi}\) ze zbioru \(\displaystyle{ \Delta}\) przy ustalonych zmiennych w zbiorze \(\displaystyle{ \mathcal V}\), gdy wszystkie zmienne wolne formuł \(\displaystyle{ \phi_i}\) są w zbiorze \(\displaystyle{ \mathcal V}\), \(\displaystyle{ \phi_0=\phi}\), \(\displaystyle{ \phi_n=\psi}\) oraz dla każdego \(\displaystyle{ i\in\{1,\ldots, n\}}\) formuła \(\displaystyle{ \phi_i}\) wynika tautologicznie ze zbioru \(\displaystyle{ \Delta\cup\{\phi_0,\ldots,\phi_{i-1}\}}\) lub \(\displaystyle{ \phi_i}\) jest efektem podstawienia pewnego termu \(\displaystyle{ t}\) o wszystkich zmiennych w \(\displaystyle{ \mathcal V}\) w pewnej formule \(\displaystyle{ \Phi\in\Delta\cup\{\phi_0,\ldots,\phi_{i-1}\}}\) lub \(\displaystyle{ \phi_i=(\alpha\Rightarrow \beta)}\) dla pewnych formuł \(\displaystyle{ \alpha}\) oraz \(\displaystyle{ \beta}\) i istnieje dedukcja od \(\displaystyle{ \alpha}\) do \(\displaystyle{ \beta}\) ze zbioru \(\displaystyle{ \Delta\cup\{\phi_0,\ldots,\phi_{i-1}\}}\) przy ustalonych zmiennych \(\displaystyle{ \mathcal V}\), lub istnieje generalizacja formuły \(\displaystyle{ \phi_i}\) po pewnej zmiennej \(\displaystyle{ x\notin\mathcal V}\) przy ustalonych zmiennych w \(\displaystyle{ \mathcal V}\) i ze zbioru \(\displaystyle{ \Delta\cup\{\phi_0,\ldots,\phi_{i-1}\}}\).
Ciąg formuł \(\displaystyle{ (\phi_i)_{i=1}^n}\) nazywamy generalizacją formuły \(\displaystyle{ \psi}\) po zmiennej \(\displaystyle{ x}\) przy ustalonych zmiennych w zbiorze \(\displaystyle{ \mathcal V}\) ze zbioru \(\displaystyle{ \Delta}\), gdy \(\displaystyle{ x\notin \mathcal V}\), wszystkie zmienne wolne formuł \(\displaystyle{ \phi_i}\) są w zbiorze \(\displaystyle{ \mathcal V\cup\{x\}}\), \(\displaystyle{ \psi=\forall x \phi_n}\) oraz dla każdego \(\displaystyle{ i\in\{1,\ldots, n\}}\) formuła \(\displaystyle{ \phi_i}\) wynika tautologicznie ze zbioru \(\displaystyle{ \Delta\cup\{\phi_1,\ldots,\phi_{i-1}\}}\) lub \(\displaystyle{ \phi_i}\) jest efektem podstawienia pewnego termu \(\displaystyle{ t}\) o wszystkich zmiennych w \(\displaystyle{ \mathcal V\cup\{x\}}\) w pewnej formule \(\displaystyle{ \Phi\in\Delta\cup\{\phi_1,\ldots,\phi_{i-1}\}}\) lub \(\displaystyle{ \phi_i=(\alpha\Rightarrow \beta)}\) dla pewnych formuł \(\displaystyle{ \alpha}\) oraz \(\displaystyle{ \beta}\) i istnieje dedukcja od \(\displaystyle{ \alpha}\) do \(\displaystyle{ \beta}\) ze zbioru \(\displaystyle{ \Delta\cup\{\phi_1,\ldots,\phi_{i-1}\}}\) przy ustalonych zmiennych \(\displaystyle{ \mathcal V\cup\{x\}}\), lub istnieje generalizacja formuły \(\displaystyle{ \phi_i}\) po pewnej zmiennej \(\displaystyle{ x'\notin\mathcal V\cup\{x\}}\) przy ustalonych zmiennych w \(\displaystyle{ \mathcal V\cup\{x\}}\) i ze zbioru \(\displaystyle{ \Delta\cup\{\phi_1,\ldots,\phi_{i-1}\}}\).
Pytanie 1. Zdaje sobie sprawę, że powyższe definicje dedukcji i generalizacji są rekurencyjne i nie potrafię uzasadnić
ich poprawności. Formalnie mam na myśli dowód istnienia (i ewentualnie jednoznaczności) odpowiednich relacji na zbiorze skończonych ciągów formuł. Dokładnie, każdym \(\displaystyle{ \phi, \psi, \Delta,\mathcal V}\) chciałbym przyporządkować pewien podzbiór rodziny skończonych ciągów formuł (który będzie pełnił rolę ogółu dedukcji od \(\displaystyle{ \phi}\) do \(\displaystyle{ \psi}\) ze zbioru \(\displaystyle{ \Delta}\) przy ustalonych zmiennych w zbiorze \(\displaystyle{ \mathcal V}\)), i podobnie każdym \(\displaystyle{ \phi, x,\Delta,\mathcal V}\) chciałbym przyporządkować pewien podzbiór rodziny skończonych ciągów formuł (czyli ogół generalizacji formuły \(\displaystyle{ \phi}\) po zmiennej \(\displaystyle{ x}\) ze zbioru \(\displaystyle{ \Delta}\) przy ustalonych zmiennych w zbiorze \(\displaystyle{ \mathcal V}\)) - w ten sposób, żeby spełnione były warunki określone w definicjach, gdzie zastępuję bycie dedukcją lub generalizacją przez należenie do wspomnianych podzbiorów.
Mówimy, że formuła \(\displaystyle{ \phi}\) jest twierdzeniem uzasadnionym przez dedukcję, jeśli \(\displaystyle{ \phi=(\alpha\Rightarrow\beta)}\) dla pewnych \(\displaystyle{ \alpha}\) oraz \(\displaystyle{ \beta}\) i istnieje dedukcja od \(\displaystyle{ \alpha}\) do \(\displaystyle{ \beta}\) ze zbioru \(\displaystyle{ \Delta=\emptyset}\) przy braku ustalonych zmiennych tzn. \(\displaystyle{ \mathcal V=\emptyset}\).
Mówimy, że formuła \(\displaystyle{ \phi}\) jest twierdzeniem uzasadnionym przez generalizację, jeśli istnieje generalizacja \(\displaystyle{ \phi}\) po pewnej zmiennej \(\displaystyle{ x}\) i ze zbioru \(\displaystyle{ \Delta=\emptyset}\) przy braku ustalonych zmiennych tzn. \(\displaystyle{ \mathcal V=\emptyset}\).
Mówimy, że formuła \(\displaystyle{ \phi}\) jest twierdzeniem, gdy istnieje ciąg formuł \(\displaystyle{ (\phi_i)_{i=1}^n}\) bez zmiennych wolnych taki, że \(\displaystyle{ \phi_n=\phi}\) oraz dla każdego \(\displaystyle{ i}\) formuła \(\displaystyle{ \phi_i}\) jest twierdzeniem uzasadnionym przez dedukcję lub twierdzeniem uzasadnionym przez generalizację lub \(\displaystyle{ \phi_i}\) wynika tautologicznie ze zbioru \(\displaystyle{ \{\phi_1,\ldots,\phi_{i-1}\}}\) lub \(\displaystyle{ \phi}\) jest efektem podstawienia termu \(\displaystyle{ t}\) (bez zmiennych wolnych) w formule \(\displaystyle{ \Phi\in\{\phi_1,\ldots,\phi_{i-1}\}}\).
Pytanie 2. Jak uzsadadnić, że każde twierdzenie ma w istocie skończony dowód? Mam na myśli fakt, że uzasadnienie twierdzenia może być przez dedukcję/generalizację, która ma w sobie kolejną dedukcję/generalizację itd. ale zawsze skończy się to w skończonej ilości kroków na uzasadnieniu przez wynikanie tautologiczne bądź efekt podstawienia. Potrafię opisać to bardziej formalnie, ale mam nadzieję, że jest zrozumiale.
Pytanie 3. Wydaje mi się, że wszystkie twierdzenia, które jestem w stanie uzyskać w tym systemie, to dokładnie wszyskie twierdzenia klasycznego rachunku predykatów (w języku \(\displaystyle{ \mathcal L}\)), które nie mają zmiennych wolnych. Co sądzicie?
Podam jeszcze przykład dowodu prawa rachunku predykatów \(\displaystyle{ \forall x(A(x)\Rightarrow B(x))\Rightarrow \left(\forall x A(x)\Rightarrow \forall x B(x)\right)}\).
1.0 \(\displaystyle{ \forall x(A(x)\Rightarrow B(x))}\) - założenie
1.1.0\(\displaystyle{ \forall xA(x)}\) - założenie
1.1.1.0 ustalenie \(\displaystyle{ x}\)
1.1.1.1 \(\displaystyle{ A(x)\Rightarrow B(x)}\) - podstawienie \(\displaystyle{ x}\) do 1.0.
1.1.1.2 \(\displaystyle{ A(x)}\) - podstawienie \(\displaystyle{ x}\) do 1.1.0
1.1.1.3 \(\displaystyle{ B(x)}\) - wynikanie tautologiczne z 1.1.1.1 oraz 1.1.1.2
1.1.1 \(\displaystyle{ \forall x B(x)}\) - generalizacja 1.1.1.0-1.1.1.3
1.1. \(\displaystyle{ \forall x A(x)\Rightarrow \forall x B(x)}\) - dedukcja 1.1.0-1.1.1
1. \(\displaystyle{ \forall x(A(x)\Rightarrow B(x))\Rightarrow \left(\forall x A(x)\Rightarrow \forall x B(x)\right)}\) - dedukcja 1.0-1.1