Commits

Paweł Wieczorek  committed e5db417

  • Participants
  • Parent commits c739825

Comments (0)

Files changed (5)

File doc/index.tex

 \newcommand{\T}[1]{\texttt{#1}}
 \newcommand{\q}[1]{,,#1''}
 \begin{document}
+
  \maketitle
 
- \tableofcontents
+\hrule
 \section{Wstęp.}
 
 Niniejszy dokument opisuje prace nad~studenckim projetkem mającym na~celu
 próbę formalizacji twierdzeń logiki matematycznej dotyczących samej logiki.
-Dokument ma formę sprawozdania, ponieważ najlepiej ona pasowała do~opisu
-tych prac oraz pozwoliła opisać pewne napotkane problemy.
 
-Prace nad~formalizacją rachunku zdań opierały się o książkę Rutkiewicza \cite{ARUT}.
-Ponieważ wspomniana książka jest, jak twierdzi sam jej autor, próbą popularnego
-przedstawienia danej tematyki to nie zawiera wszystkich dowodów wspomnianych twierdzeń. Stąd
+Prace nad~formalizacją rachunku zdań opierały się głównie o~książkę Rutkiewicza \cite{ARUT},
 prace nad~formalizacją logiki pierwszego były dodatkowo wspierane przez książkę
-Grzegorczyka \cite{AGRZ}.
-
-Projekt został wykonany z~użyciem systemu Coq w~wersji 8.2pl1. Wynikowy kod został podzielony na~trzy paczki:
-paczka \texttt{Util} zawierająca pewne pomocnicze definicje i~twierdzenia których mi zabrakło w~bibliotece
-standardowej (głównie dotyczących zbiorów) i~które nie są w~żaden sposób tematycznie związane
-z~projektem. Paczka \texttt{Pc} zawiera
-formalizację rachunku zdań, a~paczka \texttt{Fol} zawiera formalizację logiki pierwszego rzędu.
-Wszystkie trzy są osadzone w~paczce o nazwie \texttt{metalogic}. 
+Grzegorczyka \cite{AGRZ}. 
 
 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.
+fundamentalnych definicji, oraz bardzo zwięzłe dowody większości lematów i~twierdzeń.
 
-W niniejszym dokumencie zostały omówione tylko wybrane definicje, twierdzenia oraz pomocnicze lematy,
-natomiast w~kodzie zostały skomentowane wszystkie.
+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
+się bez tej taktyki. W niniejszej dokumentacji ustosunkowałem się do~większości przyjętych z góry
+fragmentów.
+
+Całość jest zawarta w~paczce \T{metalogic}, która wewnętrznie jest podzielona
+na~trzy mniejsze paczki \T{Pc}, \T{Fol}, \T{Util} oznaczające odpowiednio
+część dotyczacą rachunku zdań, logiki pierwszego rzędu oraz małą biblioteczkę
+z~pomocniczymi lematami, dotyczącymi głównie zbiorów, niezwiązanymi tematycznie
+z~projektem.
+
+\section{Przyjęty system dowodzenia.}
+
+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, ...
+}
+
+TU WPISAĆ AKSJOMATY
+
+TU WPISAĆ REGUŁY WNIOSKOWANIA.
+
+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:
+\emph{,,Jeżeli $A_0 \subseteq T$ to w~$T$ zachodzi twierdzenie o...''}. Pozwoliłem sobie na~nieistotną modyfikację
+i~dołączyłem zbiór $A_0$ na~sztywno do systemu, bo ułatwiło mi to pracę.
+
+Do pracy nad logiką pierwszego rzędu ostatecznie użyłem tego samego systemu oraz dołączyłem do~niego aksjomaty
+i~reguły wnioskowania dotyczące kwantyfikatorów z~książki Grzegorczyka (system $L^+$).
+Było to dobrym kompromisem pomiędzy łatwym przeniesieniem wykonanych już prac (opierających się o stare aksjomaty
+i ubogi język)
+oraz korzystaniem z~innej książki (z innymi aksjomatach). Ta synteza była wykonalna bo jedyna istotna różnica
+między systemami z~tych dwóch książek jest taka, że Pan Grzegorczyk posługuje się bogatszym językiem
+i~większym zbiorem aksjomatów. Nowe aksjomaty i reguły wyglądają następująco:
+
+\begin{eqnarray*}
+ \mbox{L1} & & \varphi \to \exists x\; \varphi\\
+ \mbox{L2} & & \forall x\; \varphi \to \varphi
+\end{eqnarray*}
+ 
+
+\begin{center}
+\renewcommand{\fCenter}{\;\vdash\;}
+\Axiom$T \fCenter \phi  \to \varphi$
+\RightLabel{R1}
+\UnaryInf$T \fCenter \exists x\; \phi \to  \varphi$
+\DisplayProof
+\qquad
+\Axiom$T \fCenter \varphi \to \phi$
+\RightLabel{R2}
+\UnaryInf$T \fCenter \varphi \to \forall x\; \phi$
+\DisplayProof 
+\end{center}
+
+
+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.
+
+
+
+\section{Modele.}
+
+
+\section{Najciekawsze fragmenty.}
+\subsection{Dowodzenie twierdzeń wewnątrz systemu.}
+ \subsection{Twierdzenie o dedukcji.}
+ \subsection{Twierdzenie o zwartości.}
+ \subsection{Rozszerzanie do teorii zupełnej.}
+ \subsection{Twierdzenie o pełności.}
+
+\section{}
 
 \section{Spis wszystkich twierdzeń.}
 

File doc/metalogic.kilepr

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

File metalogic/Fol/Lang.v

 Qed.
 
 
+
 End LangExt.
 
 Hypothesis folPropNum: forall L, nat -> folProp L .

File metalogic/Fol/TheoremModelExistence.v

+Require Import Arith.Div2.
+Require Import Arith.
+Require Import String.
+
+
 Require Import metalogic.Fol.Lang.
 Require Import metalogic.Fol.Lang_facts.
 Require Import metalogic.Fol.Proof.
 Require Import metalogic.Fol.Model_facts.
 Require Import metalogic.Fol.TheoremExtensionality.
 Require Import metalogic.Fol.TheoremDeduction.
+Require Import metalogic.Util.List.
 Require Import metalogic.Util.Ensemble.
 Require Import metalogic.Util.Tactics.
 Require Import metalogic.Util.Defs.
 Require Import metalogic.Util.Laws.
 Require Import Program.Equality.
-Require Import Arith.Div2.
-Require Import Arith.
-Require Import List.
-Require Import String.
+
 Require Import FunctionalExtensionality.
 
 (**************************************************************************
 
 Definition LextFuncs L := sum (folFuncs L) (nat).
 
+Hypothesis EnumSig : forall L, nat -> { f : folProp L | True }.
+
 End WitnessExtensionDef.
 
 (**************************************************************************
 
 Let mapP L := folPropMap (LEXT L).
 
-Let Enum n:= projT1 (EnumSig n).
-Let Enum' n := mapP (Enum n).
-Definition U := folProp L'.
+Let newConstS L (n:nat) : LextFuncs L := inr n.
 
-Definition WitnessAX p c : folProp L' := [[E "x"]] p --> p <[ "x" ~> c ]>.
+Let newConstT L (n:nat) : folTerm (LW L).
+Proof.
+intros.
+set (ts := folTnil (LW L)).
+set (c := newConstS L n).
+assert (folFuncAr (LW L) c = 0).
+auto.
+rewrite <- H in ts.
+set ( t := folApp (LW L) c ts).
+auto.
+Defined.
 
-Inductive constr T0 : FolPropSet L' -> nat -> Prop :=
-| base : constr T0 T0 0
-| next : forall Tn n c,
-        constr T0 Tn n
-     -> constr T0 (Tn,,WitnessAX (Enum' n) c) (S n)
+Let newConst_map L : forall c n, fexFuncMap L (LW L) (LEXT L) c <> newConstS L n.
+Proof.
+intros.
+intro H.
+unfold newConstS in H.
+
+(*
+assert (folFuncAr L c = folFuncAr (LW L) (inr n)) as AR.
+rewrite <- H.
+apply (fexFar L (LW L) (LEXT L) ).
+*)
+
+unfold LEXT in H.
+unfold fexFuncMap in H.
+unfold funcMap in H.
+absurd (inl c = inr n); auto; discriminate.
+Qed.
+
+
+Let newConst_notT0 L : forall (T0:FolPropSet L) n,
+     FolPropSet_noC (LW L) (FolPropSetMap (LEXT L) T0) (newConstT L n).
+Proof.
+admit.
+Qed.
+
+Let newConst_genconst L : forall T n p, exists m,
+         FolPropSet_noC (LW L) T (newConstT L n)
+      -> FolPropSet_noC (LW L) (T,,p) (newConstT L m)
+      /\ (forall k, FolPropSet_noC (LW L) (T,,p) (newConstT L k)
+          -> m <= k).
+admit.
+Qed.
+
+ 
+(**------------------------------------------------------------------------
+ * Konstrukcja.
+ *)
+
+Let Enum L n:= projT1 (EnumSig (LW L) n).
+Definition LP := FolLang.
+Definition U := folProp.
+
+
+Definition WitnessAX' L p c : folProp (LW L) := [[E "x"]] p --> p <[ "x" ~> c ]>.
+Definition WitnessAX L p n : folProp (LW L) := [[E "x"]] p --> p <[ "x" ~> (newConstT L n) ]>.
+
+Inductive constr L (T0:FolPropSet (LW L)) : FolPropSet (LW L) -> nat -> nat -> Prop :=
+| base : constr L T0 T0 0 0
+| same : forall Tn n cn,
+        constr L T0 Tn n cn
+     -> (LW L) @ Tn ||-- WitnessAX L (Enum L n) cn
+     -> constr L T0 Tn (S n)
+.
+
+     constr T0 (Tn,,WitnessAX (Enum' n) c) (S n)
+|
 .
 
 Lemma asc_to T0 : forall n, exists Tn, constr T0 Tn n.
 (* E *)
 intros x p IHp closed.
 split; intro H.
-(* CEL: M |= Ex.p -> T |- Ex.p
- * Ustalmy v jako wartosciowanie zwracany wybrany element uniwersum.
- * Mamy M |= Ex.p [v0]
- * Zatem istnieje pewne wartosciowanie v, t.ze: M |= p [v]
- * Zgodnie z lematem o podstawieniu: M |= p [ x ~> v(x) ] [v]
- * v(x) to term stały, zatem zróbmy p <[ x ~> v(x) ]> jest termem stałym.
- * Wiec otrzymujemy M |= p [ x ~> v(x) ]
- * Z zalozenia indukcyjnego T |= p [ x ~> v(x) ]
- *)
 
 (*
- * Niech v0 bedzie wartosciowanie wracajacym wybrany element uniwersum.
+ * Niech v0 bedzie wartosciowaniem zwracajacym wybrany element uniwersum.
  * Poniewaz M |= Ex.p to M |= Ex.p [v0]. A zatem istnieje takie
  * wartosciowanie v, ze M |= p [v].
  *

File metalogic/Util/Ensemble/UpFam.v

 
 End AscendingSetsChainDefP.
 
-
 (*************************************************************************
  * WSTĘPUJĄCA RODZINA ZBIORÓW.
  *