Commits

Paweł Wieczorek committed a55ca93

Comments (0)

Files changed (3)

 Tworząc skrypty kierowałem się ideą, aby dowodzić dużo drobnych lematów i korzystać~w~dużej mierze
 z~automatyzacji przy dowodzeniu następnych oraz większych twierdzeń. W~ten sposób uzyskałem
 łatwiejszy w~modyfikacjach kod, co było bardzo pomocne gdy decydowałem się na~modyfikację
-fundamentalnych definicji, oraz bardzo zwięzłe dowody większości lematów i~twierdzeń.
+fundamentalnych definicji, oraz umożliwiało tworzenie więzłych dowodów większości lematów i~twierdzeń.
 
 Niestety niektóre fragmenty dowodów zostały przyjęte z góry (\T{admit}), również najbardziej
-\emph{doniosła} część projektu - twierdzenie o pełności dla logiki pierwszego rzędu - nie obeszła
+\emph{doniosła} część projektu - twierdzenie o~istnieniu modelu (o~pełności)~dla logiki pierwszego rzędu - nie obeszła
 się bez tej taktyki. W niniejszej dokumentacji ustosunkowałem się do~większości przyjętych z góry
 fragmentów.
 
 z~projektem.
 
 \section{Przyjęty system dowodzenia.}
+\renewcommand{\fCenter}{\;\vdash\;}
 
 Pracę nad formalizacją zacząłem od rachunku zdań. Używany przezemnie system
 jest wzięty z książki \cite{ARUT}, czyli są to poniższe aksjomaty i~reguły
 wnioskowania, a sam język zawiera tylko dwa spójniki: implikację i~negację\footnote{
-Autor nie podał skąd wziął te aksjomaty, ale domniemam że jest to jakaś wersja
-systemu Łukasiewicza, ...
+Autor nie podał źródła aksjomatów z~jakich korzysta, ale w~książce Grzegorczyka
+oraz innych źródłach wspomina się o~systemie Łukasiewicza, który również jest
+nad~ubogim językiem i ma bardzo podobne aksjomaty.
 }
 
-TU WPISAĆ AKSJOMATY
+\begin{eqnarray*}
+ \mbox{A1} & & \varphi \to \phi \to  \varphi\\
+ \mbox{A2} & & (\varphi \to \phi \to \gamma) \to (\varphi \to \phi) \to \varphi \to \gamma\\
+ \mbox{A3} & & \neg\varphi \to \varphi \to \gamma\\
+ \mbox{A4} & & (\varphi \to \neg\varphi) \to \neg\varphi\\
+ \mbox{A5} & & (\neg\varphi \to \varphi) \to \varphi
+\end{eqnarray*}
 
-TU WPISAĆ REGUŁY WNIOSKOWANIA.
+\begin{center}
+\Axiom$T \fCenter \varphi \to \phi$
+\Axiom$T \fCenter \varphi $
+\RightLabel{MP}
+\BinaryInf$T \fCenter \phi$
+\DisplayProof  
+\end{center}
+
 
 Autor książki nie załączył wyżej wymienionych aksjomatów na~sztywno do~systemu wnioskowania. Posługiwał się
 zbiorem $A_0$ zawierającym wszystkie formuły o~takich schematach, a twierdzenia fomułował w następujący sposób:
  
 
 \begin{center}
-\renewcommand{\fCenter}{\;\vdash\;}
 \Axiom$T \fCenter \phi  \to \varphi$
 \RightLabel{R1}
 \UnaryInf$T \fCenter \exists x\; \phi \to  \varphi$
 \RightLabel{R2}
 \UnaryInf$T \fCenter \varphi \to \forall x\; \phi$
 \DisplayProof 
+\qquad
+\Axiom$T \fCenter \varphi $
+\RightLabel{SB}
+\UnaryInf$T \fCenter \varphi [x \rightsquigarrow t ]$
+\DisplayProof 
 \end{center}
 
+Reguła $SB$ wymaga, aby term $t$ był podstawialny w $\varphi$ w~miejsce zmiennej $x$. Reguły R1 i~R2 wymagają,
+aby zmienna $x$ nie występowała w~formule $\varphi$.
 
 We wspomnianej książce można znaleźć również definicję systemu bez reguł wnioskowania dotyczących kwantyfikatorów
 (system L - rozdział \emph{Redukcja reguł kwantyfikatorowych do~aksjomatów}). Pracę początkowo rozpoczęłem 
 z~tym systemem, ale doszedłem do~wniosku że nie rozumiem wszystkich szczegółów technicznych i się z~niego wycofałem.
 
+Dowody w~używanym systemie dowodzenia są bardzo nieintuicyjne, są po prostu ciągiem syntaktycznych operacji
+które bardziej przedstawiają spryt autora w~stosowaniu dostępnych operacji na formułach niż jakąś intuicję stojąca
+za~dowodzonym twierdzeniem. Z drugiej strony mała liczba reguł wnioskowania powoduje uproszczenie dowodów
+metatwierdzeń.
+
+Ponieważ książka Grzegorczyka opierałą się o~podobny system~to mogłem przepisywać z niej dowody wewnątrz systemu,
+których brakowało mi w~książce Rutkowskiego. Ciekawym zagadnieniem jest to, że posługiwanie się ubogim
+językiem, co miało upraszczać dowody, sprawiło mi dużo problemu przy dowodzie twierdzenia o~deduckji.
+
 
 
 \section{Modele.}
 
+Pomysł na~formalizację pojęcia dowodu wziąłem z~paczki \T{Goedel} dostępnej na~stronie domowej systemu Coq.
+Mianowicie jesst to rekord zawierający typ, którego wartości stanowią uniwersum; funkcje interpretujące
+symbole funkcyjne i~relacyjne; funkcje przypisujące arność symbolom; oraz wyszczególniony element uniwersum
+(dowód, że typ jest zamieszkany).
 
 \section{Najciekawsze fragmenty.}
 \subsection{Dowodzenie twierdzeń wewnątrz systemu.}
+
+Dowód formuły w~dostępnych źródłach był zdefiniowany jako skończony ciąg formuł, gdzie ostatni element ciągu
+to~dowodzona formuła oraz każdy elemenet jest aksjomatem albo wynika z~elementów poprzednich za~pomocą reguły
+wnioskowania. Posługiwanie się taką definicją dowodu 
+
+Do budowania dowodów wewnątrz rozważanego systemu skonstruowałem pomocnicze taktyki.
+
  \subsection{Twierdzenie o dedukcji.}
+
+\begin{center}
+\Axiom$T \fCenter \phi  \to \varphi \to \gamma$
+\RightLabel{import}
+\UnaryInf$T \fCenter \phi \wedge \varphi \to \gamma$
+\DisplayProof
+\qquad
+\Axiom$T \fCenter \varphi \wedge \phi \to \gamma$
+\RightLabel{export}
+\UnaryInf$T \fCenter \varphi \to \phi \to \gamma$
+\DisplayProof
+\end{center}
+
+
  \subsection{Twierdzenie o zwartości.}
  \subsection{Rozszerzanie do teorii zupełnej.}
  \subsection{Twierdzenie o pełności.}

doc/metalogic.kilepr

 
 [item:index.tex]
 archive=true
-column=48
+column=49
 encoding=UTF-8
 highlight=LaTeX
-line=82
+line=136
 mode=LaTeX
 open=true
 order=0
 CursorLine=0
 
 [view-settings,view=0,item:index.tex]
-CursorColumn=48
-CursorLine=82
+CursorColumn=49
+CursorLine=136

metalogic/Fol/TheoremModelExistence.v

  **************************************************************************
  **************************************************************************
  * Rozszerzanie do teorii swiadkowo zupelnej (opisowo konstruktywnej).
- *)
+ *
+
+ * ZALOZONE 
 
 
 (**************************************************************************
 *)
 
 
+
+
 (**------------------------------------------------------------------------
  *
 
 
 (* M |= *)
 
-admit.
+(* MAMY T |- p1 --> p2
+ * Chcemy: M |= p1 --> p2.
+ * Wiec wezmy dowolne wartosviowanie v, zgodnie z definicja
+ * aby wykazac M |= p1 --> p2 [v]
+ * musimy wykazac M |= p2 [v] przy zalozeniu M |= p1 [v]
+ * 
+ * Z zal ind mamy T |- p1, korzystajac z reguly odrywania otrzymujemy
+ * T |- p2, ponownie z zalozenia indukcyjnego M |= p2, w szczegolnosci
+ * M |= p2 [v].
+ *)
+
+intro v.
+simpl.
+intro VMp1.
+
+assert (L @ M |= p1) as Mp1.
+apply FolModel_closed' with v; auto.
+
+assert (L @ T ||-- p1); auto.
+destruct H0 as [d2].
+destruct H as [d1].
+generalize v.
+apply IHp2''.
+fol_pose d3 a3 MP p2 from d1 d2.
+fol_pose QED.
+
 
 (* A *)
 admit.