Logika dla informatyków/Język logiki pierwszego rzędu

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Język logiki pierwszego rzędu.

Język logiki pierwszego rzędu <ref name="dwa">Logika pierwszego rzędu nazywana jest też rachunkiem predykatów lub rachunkiem kwantyfikatorów.</ref> można traktować jak rozszerzenie rachunku zdań, pozwalające formułować stwierdzenia o zależnościach pomiędzy obiektami indywiduowymi (np. relacjach i funkcjach). Dzięki zastosowaniu kwantyfikatorów, odwołujących się do całej zbiorowości rozważanych obiektów, można w logice pierwszego rzędu wyrażać własności struktur relacyjnych oraz modelować rozumowania dotyczące takich struktur. Do zestawu symboli rachunku zdań dodajemy następujące nowe składniki syntaktyczne:

  • Symbole operacji i relacji (w tym symbol równości );
  • Zmienne indywiduowe, których wartości mają przebiegać rozważane dziedziny;
  • Kwantyfikatory, wiążące zmienne indywiduowe w formułach.


Składnia

Symbole operacji i relacji są podstawowymi składnikami do budowy najprostszych formuł, tzw. formuł atomowych. Z tego względu w języku pierwszego rzędu rezygnuje się ze zmiennych zdaniowych.

Definicja 2.1

Przez sygnaturę rozumieć będziemy rodzinę zbiorów , dla oraz rodzinę zbiorów , dla . Elementy będziemy nazywać symbolami operacji -argumentowych, a elementy będziemy nazywać symbolami relacji -argumentowych. Przyjmujemy, że wszystkie te zbiory są parami rozłączne. Umawiamy się też, że znak równości nie należy do . Symbol ten nie jest zwykłym symbolem relacyjnym, ale jest traktowany na specjalnych prawach. W praktyce, sygnatura zwykle jest skończona i zapisuje się ją jako ciąg symboli. Np. ciąg złożony ze znaków (o znanej każdemu liczbie argumentów) tworzy sygnaturę języka teorii ciał.

Definicja 2.2

Ustalamy pewien nieskończony przeliczalny zbiór symboli, które będziemy nazywać zmiennymi indywiduowymi i zwykle oznaczać symbolami . Zbiór termów nad sygnaturą i zbiorem zmiennych definiujemy indukcyjnie:

  • Zmienne indywiduowe są termami.
  • Dla każdego i każdego symbolu operacji , jeśli są termami, to jest też termem.

Zauważmy, że z powyższej definicji wynika, iż stałe sygnatury (czyli symbole operacji zeroargumentowych) są termami.

Definicja 2.3

Dla każdego termu definiujemy zbiór Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle \fv t} zmiennych występujących w . Definicja jest indukcyjna:

  • .
  • Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle FV(f(t_1,\ldots, t_n))=\bigcup_{i=1}^n \fv{t_i}} .


Definicja 2.4

Następnie zdefiniujemy formuły atomowe języka pierwszego rzędu.

  • Symbol fałszu jest formułą atomową.
  • Dla każdego , każdego symbolu relacji -argumentowej oraz dla dowolnych termów , napis jest formułą atomową.
  • Dla dowolnych termów , napis jest formułą atomową.

Konwencja: Niektóre dwuargumentowe symbole relacyjne (np. ) i funkcyjne (np.  ) są zwyczajowo pisane pomiędzy argumentami. Na przykład formułę atomową zwykle piszemy jako "".

Definicja 2.5

Formuły nad sygnaturą i zbiorem zmiennych indywiduowych definiujemy indukcyjnie.

  • Każda formuła atomowa jest formułą.
  • Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi,\psi} są formułami, to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\to\psi)} jest też formułą.
  • Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest formułą, a jest zmienną indywiduową, to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\var\varphi} jest też formułą.

Ponadto, dla każdej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} definiujemy zbiór zmiennych wolnych Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle FV(\var\varphi)} występujących w tej formule:

  • ;
  • ;
  • Parser nie mógł rozpoznać (nieznana funkcja „\cupFV”): {\displaystyle FV{t_1=t_2}=FV{t_1}\cupFV{t_2}} ;
  • Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle FV{\var\varphi\to\psi}=FV\var\varphi\cup FV\psi} ;
  • Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle FV{\forall x\var\varphi}=FV\var\varphi-\{x\}} .

Formułę bez kwantyfikatorów nazywamy formułą otwartą. Natomiast formuła bez zmiennych wolnych nazywa się zdaniem lub formułą zamkniętą.

Negację, koniunkcję, alternatywę, symbol prawdy i równoważność formuł definiujemy podobnie jak w przypadku rachunku zdań. Kwantyfikator egzystencjalny zdefiniujemy jako skrót notacyjny przy pomocy uogólnionego prawa De Morgana:

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \exists x\var\varphi \hspace{1cm} \text{oznacza} \hspace{1cm} \neg\forall x \neg\var\varphi. }


Zmienne wolne a zmienne związane. W Definicji 2.5 nie zakładamy, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle x\in FV\var\varphi} . Zauważmy też, że zmienna może występować w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , podczas gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle x\not\in FV\var\varphi} . Przez wystąpienie zmiennej indywiduowej rozumiemy tu zwykłe pojawienie się  w jakimkolwiek termie w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . I tak na przykład w formule <ref name="trzy">Zakładamy tu, że oraz są symbolami relacji.</ref> zmienna nie występuje, podczas gdy i wystepują po dwa razy, a występuje jeden raz.

Bardzo ważną rzeczą jest rozróżnienie wystąpień zmiennych wolnych i związanych w formułach. Wszystkie wystąpienia zmiennych w formułach atomowych są wolne. Wolne (związane) wystąpienia w formułach Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} pozostają wolne (związane) w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\to\psi} . Wszystkie wolne wystąpienia w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} stają się związanymi wystąpieniami w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \exists x\var\varphi} (związanymi przez dopisanie kwantyfikatora ), a charakter pozostałych wystąpień jest taki sam w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \exists x\var\varphi} .

Przykładowo w formule podkreślone wystąpienie jest wolne, a nie podkreślone jest związane. Obydwa wystąpienia są zwiazane, ale przez różne kwantyfikatory.

Na koniec uwaga o nazwach zmiennych związanych. Rozróżnienie pomiędzy zmiennymi wolnymi a związanymi jest analogiczne do rozróżnenia pomiedzy identyfikatorami lokalnymi a globalnymi w językach programowania. Globalne identyfikatory, widoczne na zewnątrz, odpowiadają zmiennym wolnym, podczas gdy lokalne identyfikatory (związane np. deklaracją w bloku) nie są widoczne na zewnątrz zakresu ich deklaracji. Intuicyjnie naturalne jest oczekiwanie, że zmiana zmiennej związanej na inną zmienną (tak aby nie wprowadzić konfliktu wynikającego ze zmiany struktury wiązań) nie powinna zmieniać znaczenia formuły.<ref name="cztery">Taka zamiana zmiennych bywa nazywana -konwersją.</ref> Tak w istocie będzie, jak się przekonamy poniżej (Fakt 2.12).

Semantyka formuł

Niech będzie sygnaturą. Struktura nad sygnaturą (lub po prostu -struktura) to niepusty zbiór , zwany nośnikiem, wraz z interpretacją każdego symbolu operacji jako funkcji argumentowej Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle f^{\strA}:A^n\to A} oraz każdego symbolu relacji jako relacji -argumentowej . (Na przykład, jeśli składa się z jednego symbolu relacji dwuargumentowej, to każdy graf zorientowany jest -strukturą.) W praktyce, strukturę relacyjną przedstawia się jako krotkę postaci Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathfrak A = \<A, f_1^\mathfrak A,\ldots,f_n^\mathfrak A,r_1^\mathfrak A,\ldots, r_m^\mathfrak A\>} , gdzie są wszystkimi symbolami danej sygnatury. Często, gdy będzie jasne z kontekstu z jaką strukturą mamy do czynienia, będziemy opuszczać nazwę struktury i pisać po prostu zamiast


Wartościowaniem w -strukturze nazwiemy dowolną funkcję . Dla wartościowania , zmiennej oraz elementu definiujemy nowe wartościowanie , będące modyfikacją wartościowania na argumencie , w następujący sposób,

Parser nie mógł rozpoznać (nieznana funkcja „\begin{cases}”): {\displaystyle \varrho_x^a(y)= \begin{cases} \varrho(y)}, \mbox{jeśli} y\neq x \\ a, \mbox{w przeciwnym wypadku} \end{cases}}


Najpierw zdefiniujemy znaczenie termów. Wartość termu w -strukturze przy wartościowaniu oznaczamy przez , lub , gdy jest znane. Definicja jest indukcyjna:

  • .
  • .

Znaczenie formuł definiujemy poniżej. Napis

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A , \varrho ) \vDash \var\varphi. }

czytamy: formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest spełniona w strukturze przy wartościowaniu . Zakładamy tu, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} oraz są nad tą samą sygnaturą. Spełnianie definiujemy przez indukcję ze względu na budowę formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} .

  • Nie zachodzi .
  • Dla dowolnego , oraz dla dowolnych termów , przyjmujemy, że wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \langle [[t_1]]^{\mathfrak A}_\varrho, \ldots [[t_2]]^{\mathfrak A}_\varrho \rangle \in r^{\mathfrak A } .
  • , wtedy i tylko wtedy, gdy
  • Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A , \varrho ) \vDash \var\varphi \to \psi } , gdy nie zachodzi lub zachodzi
  • Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A , \varrho ) \vDash \forall x\var\varphi } wtedy i tylko wtedy, gdy dla dowolnego zachodzi


Nastepujące twierdzenie pokazuje, że spełnianie formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} w dowolnej strukturze zależy jedynie od wartości zmiennych wolnych Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle FV(\var\varphi)} . Uzasadnia ono następującą konwencję notacyjną: napiszemy na przykład Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle ( \mathfrak A , x:a,y:b ) \vDash \var\varphi } zamiast Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A, \varrho )\vDash \var\varphi } , gdy , a przy tym wiadomo, że w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} występują wolno tylko zmienne . Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest zdaniem, to wartościowanie można całkiem pominąć.

Fakt 2.6

Dla dowolnej -struktury i dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , jeśli wartościowania i przyjmują równe wartości dla wszystkich zmiennych wolnych w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , to

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho) \vDash\var\varphi } wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle ( \mathfrak A, \varrho') \vDash\var\varphi. }

Dowód

Ćwiczenie.

End of proof.gif

Prawdziwość i spełnialność formuł

Powiemy, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi } jest spełnialna w , gdy istnieje wartościowanie w strukturze  takie, że zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho) \vDash\var\varphi} . Formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest spełnialna, gdy istnieje struktura , w której Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest spełnialna.

Formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest prawdziwa w , gdy dla każdego wartościowania w zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho)\vDash\var\varphi} . W tym przypadku mówimy też, że jest modelem dla formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} (oznaczamy to przez Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A\models\var\varphi} ). Dla zbioru formuł i -struktury powiemy, że jest modelem dla (piszemy ), gdy dla każdej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\in\Gamma} , zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A\models\var\varphi} . Formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest tautologią (oznaczamy to przez Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\var\varphi} ), gdy jest ona prawdziwa w każdej -strukturze.

Oczywiście jeśli weźmiemy dowolną tautologię rachunku zdań, to po podstawieniu na miejsce zmiennych zdaniowych dowolnych formuł logiki pierwszego rzędu dostaniemy tautologię logiki pierwszego rzędu. Poniżej podajemy przykłady tautologii logiki pierwszego rzędu, których nie da się w ten sposób otrzymać.

Fakt 2.7

Następujące formuły są tautologiami logiki pierwszego rzedu:

  1. .
  2. Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle \varphi\to \forall x \varphi$, o ile $x\not\in\fv\varphi} .
  3. .
  4. .
  5. , dla , .
  6. , dla .

Dowód

Aby się przekonać, że formuła (1) jest tautologią, rozpatrzmy dowolną strukturę i jakieś wartościowanie . Załóżmy najpierw, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho) \vDash \forall x(\var\varphi\to\psi)} oraz Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho) \vDash \forall x\,\var\varphi } . Oznacza to, że dla dowolnego zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho^a_x) \vDash \var\varphi } oraz Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho^a_x) \vDash \var\varphi\to\psi} . Musi więc zajść Z dowolności mamy , a stąd Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho) \vDash \forall x(\var\varphi\to\psi) \to (\forall x \varphi \to \forall x \psi)} .

Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle ( \mathfrak A, \varrho) \not\models \forall x(\var\varphi\to\psi)} lub , to nasza formuła jest spełniona przez wprost z definicji. Uzasadnienie części (3-6) pozostawiamy czytelnikowi.

End of proof.gif

Ponadto mamy następujący

Fakt 2.8

Dla dowolnej tautologii Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i dowolnej zmiennej , formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\var\varphi} jest też tautologią.

Dowód

Ćwiczenie.

End of proof.gif

Uzasadnienie, że dana formuła jest tautologią, polega na analizie jej spełniania w dowolnych modelach (por. Fakt 2.7). Natomiast wykazanie, że tak nie jest, polega na podaniu odpowiedniego kontrprzykładu. Takiego jak ten:

Przykład 2.9

Zdanie nie jest tautologią. Rozpatrzmy bowiem model , w którym:

  • , wtedy i tylko wtedy, gdy jest parzyste;
  • , wtedy i tylko wtedy, gdy jest nieparzyste;

Ponieważ , więc . (Mamy tu do czynienia ze zdaniem, więc wartościowanie jest nieistotne i dlatego je pomijamy.) Stąd otrzymujemy . Z drugiej strony , ponieważ . Rzeczywiście, .

Podstawianie termów

Dla formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , termu i zmiennej , napis Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi (t/x)} oznacza wynik podstawienia na wszystkie wolne wystąpienia w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Wykonywanie takiego podstawienia bez dodatkowych zastrzeżeń może prowadzić do kłopotów. Na przykład sens formuł oraz jest taki sam. Tymczasem "naiwne" podstawienie w miejsce w obu tych formułach daje w wyniku odpowiednio i , a te dwie formuły znaczą całkiem co innego. Przyczyną jest to, że w pierwszym przypadku zmienną  wstawiono w zasięg kwantyfikatora .

Źródłem problemu w powyższym przykładzie było to, że po wykonaniu podstawienia pojawiały się nowe wiązania kwantyfikatorem. Sugeruje to następującą definicję. Powiemy, że term  jest dopuszczalny dla zmiennej w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} (lub że podstawienie Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst\var\varphi tx} jest dopuszczalne, jeśli dla każdej zmiennej występującej w , żadne wolne wystąpienie w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} nie jest zawarte w zasięgu kwantyfikatora lub . Mamy więc następującą indukcyjną definicję dopuszczalnego podstawienia,<ref name="piec">Podstawianie termu do termu na miejsce zmiennej oznaczamy podobnie: . Takie podstawienie jest zawsze wykonalne.</ref> w której każda lewa strona jest dopuszczalna pod warunkiem, że prawa strona jest dopuszczalna.

  • , gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle x\not\in FV(\var\varphi)} ;
  • ;
  • ;
  • Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\to\psi)(t/x) = \var\varphi(t/x)\to\psi(t/x)} ;
  • Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\forall x\var\varphi)(t/x) = \forall x\var\varphi} ;
  • Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\forall y\var\varphi)(t/x) = \forall y\var\varphi(t/x)} , gdy , oraz ;
  • W pozostałych przypadkach podstawienie jest niedopuszczalne.


W dalszym ciągu będziemy rozważać jedynie podstawienia dopuszczalne.

Lemat 2.10 (o podstawieniu)

Niech będzie dowolną strukturą oraz dowolnym wartościowaniem w . Niech będzie dowolnym termem.

  1. Dla dowolnego termu i zmiennej mamy
    gdzie .
  2. Dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , jeśli term jest dopuszczalny dla w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , to
wtedy i tylko wtedy, gdy
gdzie .

Dowód

Część 1 dowodzimy przez indukcję ze względu na budowę termu . Jeśli jest zmienną , to obie strony są równe . Jeśli jest zmienną (różną od ), to obie strony są równe . Jeśli jest postaci , to mamy następujące równości.





Dowód części 2 przeprowadzamy przez indukcję ze względu na budowę formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi}  jest postaci , to teza jest oczywista. Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest formułą atomową, to tezę natychmiast dostajemy z wyżej udowodnionej części 1. Na przykład, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest postaci to mamy:

wtedy i tylko wtedy, gdy

wtedy i tylko wtedy, gdy
wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\varrhp”): {\displaystyle (\mathfrak A, \varrhp^a_x) \models s_1 = s_2 }

Druga z powyższych równoważności wynika z części 1.

Krok indukcyjny dla przypadku, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest postaci jest oczywisty i pozostawimy go czytelnikowi. Rozważymy przypadek, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest postaci . Jeśli zmienne oraz są równe, to nie występuje wolno w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i wówczas teza wynika natychmiast z Faktu 2.6. Tak więc przyjmijmy, że oraz są różnymi zmiennymi. Wówczas z dopuszczalności dla w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} wynika, że nie występuje w . Ponadto Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst\var\varphi tx} jest identyczne z Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \forall y\subst\psi tx} . Mamy następujące równoważności:

wtedy i tylko wtedy, gdy dla każdego

wtedy i tylko wtedy, gdy dla każdego

gdzie . Ponieważ nie występuje w , więc . Skoro zmienne oraz są różne, to . Tak więc warunek jest równoważny warunkowi , dla każdego . Czyli

End of proof.gif

Natychmiastowym wnioskiem z Lematu 2.10 jest następujący przykład tautologii.

Fakt 2.11

Dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , zmiennej i termu dopuszczalnego dla w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , formuła

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\var\varphi\to\var\varphi(t/x)}

jest tautologią logiki pierwszego rzędu.

Dowód

Ćwiczenie.

End of proof.gif

Fakt 2.12

Jeśli zmienna jest dopuszczalna dla w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} oraz Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle y\not\in\fv\var\varphi} , to

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models(\forall x\var\varphi)\leftrightarrow (\forall y \var\varphi(y/x))}
.

Dowód

Z Faktu 2.11 oraz Faktu 2.8 otrzymujemy

Zatem na mocy Faktu 2.7(1) wnioskujemy, że

.

Na mocy Przykładu 2.7(2) otrzymujemy implikację . Odwrotna implikacja wynika z już udowodnionej implikacji oraz z następujących prostych obserwacji:

  • Jeśli jest dopuszczalna dla w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , to jest dopuszczalna dla w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(y/x)} .
  • Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle y\not\in FV\var\varphi} , to nie występuje wolno w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(y/x)} .
  • Wynik podstawienia Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(y/x)(x/y)} jest identyczny z Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} .
End of proof.gif

Fakt 2.12 pozwala zamieniać zmienne związane dowolnie, tak długo jak są spełnione założenia. W szczególności jeśli chcemy wykonać podstawienie termu do formuły w sytuacji, gdy ten term nie jest dopuszczalny to wystarczy zamienić nazwy pewnych zmiennych związanych, tak aby term stał się dopuszczalny. Łatwo jest uogólnić Fakt 2.12: znaczenie formuły nie ulega zmianie także przy wymianie zmiennych związanych kwantyfikatorami wystepującymi wewnątrz formuły.

Przypisy

<references/>