Commits

Paweł Wieczorek committed 53a24ed

  • Participants
  • Parent commits 7265e25

Comments (0)

Files changed (12)

 \usepackage{amsthm}
 \usepackage{amsfonts}
 \usepackage{amssymb}
+\usepackage{url}
 \usepackage{a4wide}
 \usepackage{bussproofs}
 
 łatwiejszy w~modyfikacjach kod, co było bardzo pomocne gdy decydowałem się na~modyfikację
 fundamentalnych definicji.
 
-Postanowiłem nie~przepisywać do~dokumentu żadnych skryptów Coqa, poza momentami omawiania taktyk,
-ponieważ bez wykorzystania
-asystenta zwykle nie są zrozumiałe dla~człowieka. Definicje postawnowiłem przedstawiać w~bardziej
-przyjaznej formie do~omówienia jak na~przykład reguły wnioskowania zamiast surowych
-indukcyjnych definicji Coq'a.
-
 W niniejszym dokumencie zostały omówione tylko wybrane definicje, twierdzenia oraz pomocnicze lematy,
 natomiast w~kodzie zostały skomentowane wszystkie.
 
-\section{Rachunek zdań.}
+\section{Spis wszystkich twierdzeń.}
 
-Pracę nad~rachunkiem zdań nie okazały się tak proste dla mnie jak z~początku przewidywałem,
-w~szczególności że początkowo dobierane przezemnie definicje dowodu były na~tyle beznadziejne,
-że dowód prostego twierdzenia o~dedukcji był technicznym wyzwaniem. Dodatkowo dowód o~możliwości
-uzupełnienia niesprzecznego zbioru formuł do~niesprzecznego i~zupełnego zbioru formuł okazał się dość
-trudny do~sformalizowania ze względu na~swój \q{teorio mnogościowy charakter}.
 
-\subsection{Podstawowe definicje.}
+\newcommand{\ditem}[3]{
+ \item[] \textsc{Lokalizacja:} #1
+ \item[] \textsc{Dotyczy twierdzenia:} #2
+ \item[] #3
+}
 
-Język rachunku zdań został, tak jak w~wzorcowej książce, ograniczony jedynie do dwóch spójników
-$\Set{\Rightarrow, \neg}$, a~system dowodzenia do jednej reguły wnioskowania - reguły odrywania.
-Tak uproszczony system jest prostszy w~analizie i~formalizacji.
-
-\begin{Def}[\p{pcProp}] Zbiór formuł rachunku zdań $F$ jest najmniejszym w~sensie zawierania zbiorem spełniającym
-następujące warunki:
-\begin{enumerate}
- \item Jeżeli $x \in \mathcal{X}$ jest zmienną, to $x$ jest także formułą, $x \in F$.
- \item Jeżeli $\varphi \in F$ to $\neg \varphi \in F$.
- \item Jeżeli $\varphi, \phi \in F$ to $(\varphi \Rightarrow \phi) \in F$
-\end{enumerate}
-\end{Def}
-
-Formuły zostały zakodowane przez indukcyjnie zdefiniowany typ \T{pcProp : Set}, 
-a~zmienne zdaniowe są prezentowane przez napisy (\T{string}).
-
-Definicja dowodu technicznie różni się od~formalnej definicji z książki Rutkowskiego, zamieszczonej poniżej:
-
-\begin{Def}(Rutkowski \cite{ARUT}: Def II.5)
-Niech $A$ będzie dowolnym zbiorem formuł rachunku zdań. Skończony ciąg formuł
-$\alpha_1, \cdots, \alpha_n$ nazywamy dowodem formalnym ze zbioru $A$ (lub krótko:
-dowodem z $A$) formuły $\alpha$ wtedy i~tylko wtedy, gdy spełnione są następujące warunki
-\begin{itemize}
- \item $\alpha_n = \alpha$.
- \item Dla dowolnego $k \le n$, albo $\alpha_k \in A$ albo istnieją liczby $i,j$ mniejsze od~$k$
-i takie, że $\alpha_k$ wynika z~$\alpha_i, \alpha_j$ za pomocą reguły odrywania.
-\end{itemize}
-\end{Def}
-
-Taka definicja dowodu sprawiała wrażenie znaczniej prostszej w~analizie niż drzewiasta definicja
-w~bogatszym systemie naturalnej dedukcji, a w~ostateczności okazało się jednak konieczne przedstawienie
-jej~formie drzewiastej.
-
-Pierwsza próba formalizacji dowodu w~Coqu była przepisaniem definicji książkowej na~pewien predykat stwierdzający
-że dana lista formuł jest poprawnym dowodem, tzn ostatni element listy to~wyprowadzana formuła, a~każda
-formuła w~tym ciągu jest aksjomatem albo wnioskiem. Wadą tego podejścia był brak jakiegoś typu, którego wartości
-by prezentowały jedynie poprawne dowody, a~nie dowolne ciągi formuł; brak jakiejś strukturalnej definicji, po której
-dałoby się robić indukcję (indukcja po liście była bardzo niewygodna, bo nie każda lista była poprawnym dowodem);
-oraz odwoływanie się do~elementów ciągu po indeksach, tzn z~użyciem funkcji \T{nth}. Nie wiele udało mi się osiągnąć
-przy tej definicji.
-
-Kolejna próba była dalej niedostateczna, ale udało mi się znią poczytnić pewne postępy. Definicję z~książki
-rozbiłem na~pojęcie wywodu i~dowodu. Wywód był starą definicją ze skreślonym wymogiem
-dotyczącym ostatniego elementu
-ciągu, a~dowód formuły $\varphi$ to wywód którego ostatnim elementem jest $\varphi$. 
-Sam wywód był dalej kodowany przez listę, lecz teraz nie była to~jedynie lista formuł,
-ale lista formuł wraz z~informacją ($\p{pcCrl}$) czy dana formuła
-zostałą uzyskaną regułą odrywania czy~znajduje się w~założeniach; tymrazem pierwszy element listy
-oznaczał ostatni element ciągu.
-Dodatkowo był indukcyjnie zdefiniowany predykat $\p{PcInfr}$ stwierdzający,
-że lista jest poprawnym wywodem z~danego zbioru formuł. 
-
-
-\begin{Def}[\p{PcCrl}]
-Wywód to~lista wartości typu $\p{pcCrl}$, która zawiera następujące konstruktory:
- $\p{pcCrlAx}(\varphi)$ oznacza że formuła $\varphi$ znajduje się w~założeniach;
- $\p{pcCrlAx}(\phi, \varphi)$ oznacza, że $\varphi$ zostało wywnioskowane za~pomocą
-reguły odrywania zastosowanej do~formuł ($\phi \Rightarrow \varphi$), $\phi$.
-Funkcja $\p{pcCrlsProps}$ zwraca zbiór wszystkich wniosków z~danego wywodu, tzn wg powyższych
-oznaczeń formuły $\varphi$.
-\end{Def}
-
-\begin{Def}[\p{PcInfr}]
-Predykat $\p{PcInfr}(T,xs)$ oznacza, że wywód $xs$ jest poprawny dla zbioru formuł $T$.
-Konstruktory weryfikują odpowiednio informację w~wywodzie, czy dana formuła rzeczywiście
-jest w~zbiorze aksjomatów lub czy została wywnioskowania z~formuł otrzymanych wcześniej.
-Pusta lista nie jest prawidłowym wywodem.
-
-\begin{center}
-\AxiomC{$p \in T$}
-\RightLabel{\pp{pcInfrOne}}
-\UnaryInfC{$\p{PcInfr}(T, \p{pcCrlAx}(p)::\p{nil})$}
-\DisplayProof
-%\end{center}
-\qquad
-%\begin{center}
-\AxiomC{$p \in T$}
-\AxiomC{$\p{PcInfr}(T,xs)$}
-\RightLabel{\pp{pcInfrAx}}
-\BinaryInfC{$\p{PcInfr}(T,\p{pcCrlAx}(p)::xs)$}
-\DisplayProof
-\end{center}
-\vspace{0.3cm}
-\begin{center}
-\AxiomC{$\p{let}\;U\; :=\; \p{pcCrlsProps}(xs)$}
-\noLine
-\UnaryInfC{$\p{in}\; (p\Rightarrow q)\in U \wedge p \in U$}
-\AxiomC{$\p{PcInfr}(T,xs)$}
-\RightLabel{\pp{pcInfrModus}}
-\BinaryInfC{$\p{PcInfr}(\p{pcCrlModus}(p,q)::xs)$}
-\DisplayProof
-\end{center}
-\end{Def}
-
-Mimo że udało mi się sformalizować więcej pomocniczych lematów to~nadal nie potrafiłem udowodnić twierdzenia
-o~dedukcji - nowa definicja właściwie nie naprawiała żadnych problemów prócz dostarczenia jakiejś 
-definicji do~robienia indukcji po wywodzie i~pozbycia się \T{nth}. Problem stanowiła indukcja strukturalna,
-która w~przypadku $\p{pcInfrModus}$ nie dostarczała założenia indukcyjnego dla wywodow $(p \Rightarrow q)$
-oraz $p$ będących sufiksami $xs$. 
-
-Ostateczne podejście wiązało się ze zmianą reprezentacji wywodu na~drzewo, wbrew moim obawom dowody
-z~książki dało się przepisywać bez ich zmian oraz dało się zdefiniować pomocnicze taktyki za pomocą których
-przedstawiało się dowód jako ciąg wnioskowań, tak jak w~książce. Drzewo zostało zdefiniowane jako~typ
-zależny (\p{pcDeriv}) od~zbioru formuł oraz~formuły znajdującej się w~korzeniu.
- 
-\begin{Def}[$\p{pcDeriv}$]
-Definicja drzew jest intuicyjna, warto jedynie podkreślić że $\p{pcDeriv}$ nie jest predykatem, ze względu
-na~potrzebę wykonywania obliczeń na~nim.
-
-\begin{center}
-\AxiomC{$\varphi \in T$}
-\RightLabel{\pp{pcDerivAX}}
-\UnaryInfC{$\p{PcDeriv}(T,\varphi)$}
-\DisplayProof
-%\end{center}
-\qquad
-%\begin{center}
-\AxiomC{$d_1 : \p{pcDeriv}(T,\phi \Rightarrow \varphi)$}
-\AxiomC{$d_2 : \p{pcDeriv}(T,\phi)$}
-\RightLabel{\pp{pcDerivMP}}
-\BinaryInfC{$\p{pcDeriv}(T,\varphi)$}
-\DisplayProof
-\end{center}
-\end{Def}
-
-\begin{Def}[$\p{pcPrf}$]
-Pomocniczy predykat $\p{pcPrf}(T,\varphi)$ oznacza, że ze~zbioru formuł $T$ da się~wyprowadzić formułę $\varphi$.
-Będzie on zapisywany jako $T \Vdash \varphi$.
-
-\begin{center}
-\AxiomC{$d : \p{pcDeriv}(T,\varphi)$}
-\RightLabel{$\pp{pcPrf\_intro}$}
-\UnaryInfC{$T \Vdash \varphi$}
-\DisplayProof
-\end{center}
-
-\end{Def}
-
-Rutkowski w~swojej książce podaje poniższe aksjomaty, ale nie dołącza ich do~systemu wnioskowania \q{na~sztywno}.
-Co owocowało tym, że twierdzenia były formułowane w~następujący sposób:
-\q{Jeżeli $A$ zawiera w~sobie zbiór aksjomatów $A_0$ to zachodzi twierdzenie...}. Ponieważ takie
-formułowania są dośc niewygodne to~dodałem $A_0$ na~sztywno do~systemu (dodano odpowiednie konstruktory
-do~$\p{pcDeriv}$: $\p{pcDerivAX1}$, ...).
-
-\begin{Def}[Rutkowski \cite{ARUT}: Rozdział II.9]
-~
-\begin{eqnarray*}
-A_1 &=& \Set{ \alpha \Rightarrow \beta \Rightarrow \alpha  \mid \alpha, \beta \in F }\\ 
-A_2 &=& \Set{ (\alpha \Rightarrow \beta \Rightarrow \gamma)
-\Rightarrow (\alpha \Rightarrow \beta)
-\Rightarrow \alpha \Rightarrow \gamma \mid \alpha,\beta,\gamma \in F}\\ 
-A_3 &=& \Set{\alpha \Rightarrow \neg \alpha \Rightarrow \beta \mid \alpha,\beta \in F }\\ 
-A_4 &=& \Set{(\alpha \Rightarrow \neg\alpha) \Rightarrow \neg\alpha \mid \alpha \in F}\\ 
-A_5 &=& \Set{(\neg\alpha \Rightarrow \alpha) \Rightarrow \alpha \mid \alpha \in F }\\
-A_0 &=& A_1 \cup A_2 \cup A_3 \cup A_4 \cup A_5\\ 
-\end{eqnarray*}
-\end{Def}
-
-Do~budowania dowodów wewnątrz rozważanego systemu udało się zdefiniować pomocnicze taktyki, dzięki
-którym można sobie wyobrażać dowody jako ciąg, tak jak w~książce. Taktyki są zdefiniowane za~pomocą
-notacji, tak aby wyglądały jak jedna taktyka występująca w~kilku wariantach,
-w~zalezności od argumentów, i~tak zostaną one omówione.
-
-\begin{Def}[\T{pc\_pose}]
-Taktyka jako pierwszy swój argument pobiera nazwę polecenia: \T{REN} oznacza zmianę nazwy istniejącej już
-przesłanki; \T{AX} oznacza podanie aksjomatu ze zbioru $A_0$; \T{MP} oznacza użycie reguły odrywania;
-a \T{QED} oznacza próbę zakończenia dowodu w~systemie Coq (użyteczne gdy skonstruowani dowodu w~badanym
-systemie kończy jakiś meta-dowód).
-
-Argument \T{as d a} oznacza nazwanie skonstruowanego drzewa jako \T{d}, a formuły w~jego korzeniu przez \T{a}.
-Parametr \T{p} jest formuła która ma znajdować się w~korzeniu nowo utworzonego drzewa (będzie wrzucone w~środowisko
-pod nazwą \T{a} za~pomocą taktyki \T{pose}). Parametr \T{from d1 d2} dla~polecenia \T{MP} oznacza, że
-drzewo \T{d1} wyprowadza implikację, a~\T{d2} przesłankę - aby kolejność była intuicyjna jest taka, jak przy
-aplikacji funkcji do~argumentu. Opcjonalny parametr \T{env T} pozwala wskazać zbiór formuł z~którego wyprowadzamy,
-jeżeli nie jest podany to~taktyka bierze go~z~celu.
-
-\begin{verbatim}
- pc_pose REN from D as d a
- pc_pose AX p [env T] as d a
- pc_pose MP p [env T] from d1 d2 as d a
- pc_pose QED
-\end{verbatim}
-
-\end{Def}
-
-Przykładowy skrypt dowodzący trywialnego twierdzenia $\varphi \Rightarrow \varphi$ w~przyjętym systemie:
-\begin{verbatim}
-Remark PcT_pp: forall T p, T ||-- p --> p.
-Proof.
-intros.
-pc_pose AX (p --> (p --> p) --> p)              as d1 a1.
-pc_pose AX (p --> p --> p)                      as d2 a2.
-pc_pose AX (a1 --> a2 --> p --> p)              as d3 a3.
-pc_pose MP (a2 --> p --> p)          from d3 d1 as d4 a4.
-pc_pose MP (p --> p)                 from d4 d2 as d5 a5.
-pc_pose QED.
-Qed.
-\end{verbatim}
-
-
-
-\subsection{Przeliczalność zbioru formuł.}
-
-\subsection{Wybrane pomocnicze twierdzenia.}
-
-\subsection{Twierdzenie o zwartości.}
-
-Z~początku zdawało mi się, że twierdzenie o~zwartości będzie bardzo trudne lub niemożliwe
-do~udowodnienia w~systemie Coq, bo posługuje się pojęciem skończonego podzbioru. Ku mojemu
-zdziwieniu było to pierwsze meta-twierdzenie które udalo mi się udowodnić, a~sam
-skrypt budujący dowód okazał się prosty.
-
-\begin{Tw}[\p{PcCompactness}]
- Zbiór formuł $T$ jest niesprzeczny wtedy i tylko wtedy, gdy każdy jego skończony podzbiór jest niesprzeczny.
-\end{Tw}
-\begin{proof} ($\Rightarrow$) Jeżeli zbiór formuł jest niesprzeczny, to oczywiście każdy jego podzbiór także.
- ($\Leftarrow$) Załóżmy nie wprost, że jednak zbiór formuł $T$ jest sprzeczny. Wtedy istnieją dowody formuł
-$\varphi$ oraz $\neg\varphi$, które wymagają skończonej liczby aksjomatów. Nazwijmy te zbiory odpowiednio
-$A$ oraz $B$, sumując te zbiory otrzymamy skończony zbiór który jest sprzeczny, wbrew założeniu.
-\end{proof}
-
-\subsection{Twierdzenie o dedukcji.}
-
-\begin{Tw}[\p{PcDeduction}]
- W~dowolnym zbiorze formuł $T$ można udowodnić implikację $\varphi \Rightarrow \phi$ wtedy i tylko wtedy, gdy
- w ~ zbiorze
-\end{Tw}
-
-
-\subsection{Rozszerzanie do~teorii zupełnej.}
-
-Możliwość rozszerzania dowolnego niesprzecznego zbioru formuł rachunku zdań do~zbioru formuł, który
-jest zupełny i~niesprzeczny, nie jest, z~punktu widzenia logiki, trudnym do~dowiedzenia faktem. 
-Jednak z~technicznego punktu widzenia zostają tutaj użyte dość skomplikowane mechanizmy, których
-przeniesienie do~Coq'a sprawiło mi trudność.
-
-\begin{Tw}[\p{PcExtensionality}]
- Dla każdego niesprzecznego zbioru formuł $T$ istnieje zbiór formuł $S$ spełniający następujące warunku:
- \begin{itemize}
-  \item $T \subseteq S$.
-  \item Zbiór $S$ jest niesprzeczny i~zupełny.
- \end{itemize}
-\end{Tw}
-\begin{proof}
-Zbiór formuł języka rachunku zdań jest przeliczalny, zatem możemy wszystkie formuły ustawić w~pewien ciąg:
-\[ \varphi_0, \varphi_1, \varphi_2, \cdots \]
-
-Następnie, stwórzmy indukcyjnie następujące zbiory formuł.
-\begin{eqnarray*}
- T_0 & = & T \\
- T_{n+1} & = &
-\begin{cases}
- T_{n} \cup \Set{\neg\varphi_n}  & \mbox{gdy nie można dowieść $\varphi_n$ w $T_n$}  \\ 
- T_{n}   & \mbox{w przec. wyp}
-\end{cases}
-\end{eqnarray*}
-
-\begin{TwLem}[\p{PcExtConstrConsistent}]
- Każdy zbiór formuł $T_n$ jest niesprzeczny.
-\end{TwLem}
-\begin{proof}
-Lematu dowiedziemy za~pomocą indukcji po $n$. Z założenia dowodu $T_0$ jest niesprzeczne. Załóżmy,
-że zbiór $T_n$ jest niesprzeczny. Załóżmy nie wprost, że dodanie nowego aksjomatu $\neg\varphi_n$ powoduje
-sprzeczność.
-
-\end{proof}
-
-Zbiór formuł, o~którego istnieniu mówi twierdzenie konstruujemy tworząc nieskończoną sumę stworzonych
-przez nas zbiorów.
-
-\begin{eqnarray*}
- S &=& \bigcup_{n\in\mathbb{N}} T_n
-\end{eqnarray*}
-
-\begin{TwLem}[\p{PcExtConstrSumConsistent}]
-Zbiór formuł $S$ jest niesprzeczny.
-\end{TwLem}
-\begin{proof}
- Załóżmy nie wprost, że zbiór $S$ jest sprzeczny. Wtedy dowody formuł $\varphi$ i~$\neg\varphi$ wymagają
-łącznie skończonej liczby aksjomatów. Zatem istnieje pewien $n$, taki że te dowody przechodzą również
-w~$T_n$, ale wiadomo już, że te indukcyjnie stworzone zbiory formuł $T_n$ są niesprzeczne.
-\end{proof}
-
-\begin{TwLem}[\p{PcExtConstrSumComplete}]
-Zbiór formuł $S$ jest zupełny.
-\end{TwLem}
-\begin{proof}
-Weźmy dowolną formułę $\varphi$, wiemy, że ma ona pewien swój numer $n$ w~wzietym ciągu.
-Zauważmy, że z~konstrukcji zbioru $T_{n+1}$ wynika, że albo $\varphi$ jest dowodliwa
-w~$T_{n+1}$ albo jej negacja. Ponieważ $T_{n+1} \subseteq S$ to nasza formuła, albo jej negacja,
-jest dowodliwa w~$S$.
-\end{proof}
-
-Z powyższych lematów wynika, że $S$ jest poszukiwanym zbiorem formuł.
-\end{proof}
-
-\subsubsection{Formalizacja dowodu.}
-
-W~formalizacji tego dowodu problemtyczne jest użycie nieskończonej sumy, pojęcia przeliczalności oraz sama
-konstrukcja zbiorów $T_n$.
-Mimo,  że jest ona indukcyjna to podczas konstrukcji wykorzystywany jest fakt, że albo zachodzi $T_n \vdash \varphi_n$,
-albo nie zachodzi. Co samo w sobie jest nierozstrzygalne.
-
-Próbę formalizacji tej konstrukcji zacząłem od próby wyrażenia nieskończonej sumy rodziny zbiorów, indeksowanych
-liczbami naturalnymi. Postanowiłem napisać w~systemie Coq definicję na podobieństwo poniższej:
-\[
- x \in \bigcup_{n \in \mathbb{N}} A_n\Leftrightarrow \exists n \; \in \mathbb{N}.\; x \in A_n
-\]
-
-Co okazało się proste w~realizacji za pomocą poniższej definicji. Idea jest jest taka, że \emph{BigUnion} dostaje
-funkcję, reprezentującą ciąg zbiorów. Następnie aby udowodnić, że $x$ należy, do \emph{BigUnion f} należy wskazać
-wskazać taki $n$, że $x$ należy do $f(n)$. 
-\begin{eqnarray*}
- \p{BigUnion} & & (A : \p{Type}) (f: \p{nat} \to \p{Ensemble}\; A) : \p{Ensemble} A  \\
-  &= & \lambda x:A.\; \exists n:\p{nat}.\; \p{In}\;(f\;n)\; x 
-\end{eqnarray*}
-
-Niestety nie umiałem skonstruować zbiorów $T_n$ tak, abym mógł użyć powyższej definicji. Jest to związane
-z~tym że w~konstrukcji zbiorów potrzebuję korzystać z~prawa wyłącznego środka, a~podczas definiowania funkcji
-system Coq nie pozwala mi na~eliminację termów reprezentujących dowody, związku z czym nie umiałem napisać takiej funkcji i~podejrzewam,
-że nie jest to możliwe.
-
-Użyteczną definicję nieskończonej sumy udało mi się uzyskać, pisząc ją po prostu na podobieństwo ogólnej
-definicji ze~skryptu logiki dla pierwszego roku, czyli aby udowodnić że $x$ należy do~sumy rodziny zbiorów,
-musimy wskazać taki zbiór~z~tej rodziny, do którego należy dany $x$.
-
-\begin{Def}
-\begin{eqnarray*}
- x \in \bigcup \mathcal{R} &\Leftrightarrow& \exists r \in \mathcal{R}.\; x \in r\\
- \p{BigUnionR} & & \p{(A : Type) ($R$: Ensemble (Ensemble A)) : Ensemble A}  \\
-  &= & \lambda x:A.\; \exists r:\p{Ensemble A}.\; \p{In } R\; r \wedge \p{In } r\; x 
-\end{eqnarray*}
-\end{Def}
-
-Następnym krokiem jest skontruowanie zbioru zawierającego wszystkie $T_n$. Ponieważ nie mogę (nie umiem)
-stworzyć funkcji, która dla ustalonego $n$ by tworzyła odpowiedni zbiór $T_n$ to spróbowałem opisać konstrukcję
-z~dowodu za pomocą predykatów.
-
-\begin{Def} Indukcyjnie zdefiniowany predykat $PcPropSet(T,S,n)$ oznacza, że zbiór $S$ jest $n$-tym zbiorem
-z~konstrukcji, dla której początkowym elementem jest $T$.
-
-\begin{center}
-\[ \p{PcExtConstr}: \p{PcPropSet} \to \p{PcPropSet} \to \p{nat} \to \p{Prop} \]
-\end{center}
-
-
-\begin{center}
-\AxiomC{}
-\RightLabel{\pp{pcConstr0}}
-\UnaryInfC{$\p{PcExtConstr}(T,T,0)$}
-\DisplayProof
-\end{center}
-
-\begin{center}
-\AxiomC{$Tn \not\Vdash \varphi_n$}
-\AxiomC{$\p{PcExtConstr}(T,T_n,n)$}
-\RightLabel{\pp{pcConstrSnNP}}
-\BinaryInfC{$\p{PcExtConstr}(T,T_n\cup\Set{\neg\varphi_n},n+1)$}
-\DisplayProof
-\end{center}
-
-\begin{center}
-\AxiomC{$Tn \Vdash \varphi_n$}
-\AxiomC{$\p{PcExtConstr}(T,T_n,n)$}
-\RightLabel{\pp{pcConstrSnP}}
-\BinaryInfC{$\p{PcExtConstr}(T,T_n,n+1)$}
-\DisplayProof
-\end{center}
-
-Konstruktory oznaczają kolejno: konstrukcję początkowego elementu, konstrukcję kolejnego zbioru gdy dodajemy
-nowy aksjomat, konstrukcję kolejnego elementu, gdy nie potrzeba dodawać kolejnego aksjomatu.
-\end{Def}
-
-\begin{Def}
-Przy użyciu poprzedniego predykatu, można skontruować zbiór wszystkich konstrukcji dla~początkowego $T$,
-oraz sumę tej rodziny zbiorów. Pierwsza definicja, mówi że aby udowodnić że zbiór $S$ należy do~opisywanego
-zbioru to~należy udowodnić że jest on $n$-tym elementem z~danej konstrukcji. Druga po prostu wykorzystuje
-rozważaną wcześniej definicję nieskończonej sumy.
-\begin{eqnarray*}
- \p{PcExtConstrSet} & & (T:\p{PcPropSet}) : \p{Ensemble}\; \p{PcPropSet} \\
- &=& \lambda Tn:\p{PcPropSet}.\; \exists n:\p{nat}.\; \p{PcExtConstr}\; T\; Tn\;n\\
- \p{PcExtConstrSum} & & (T:\p{PcPropSet}) : \p{PcPropSet} \\
- &=& \p{BigUnionR}\; (\p{PcExtConstrSet}\;T)
-\end{eqnarray*}
-\end{Def}
-
-Twierdzenie i~zawarte w~nim lematy zostały sformalizowane w~następujący sposób:
-
-\begin{Lem}[\p{PcExtConstrConsistent}]\small
-\begin{eqnarray*}
- & &\forall T:\p{PcPropSet}\; \forall n:\p{nat}\; \forall T_n:\p{PcPropSet}\,.\;\\
- & &\p{PcConsistent}(T) \to \p{PcExtConstr}(T,T_n,n) \to \p{PcConsistent}(T_n)
-\end{eqnarray*}
-
-
-\end{Lem}
-
-
-\subsection{Tautologie rachunku zdań.}
-
-\subsection{Twierdzenie o pełności.}
-
-\section{Logika pierwszego rzędu.}
 
 \begin{thebibliography}{9}
 \bibitem{ARUT}
  Biblioteka Matematyczna, tom 20,
  PWN,
  Warszawa 1973
+
+\bibitem{CODUN}
+ C. Ó D\'{u}nlaing,
+ \emph{Completeness of some axioms of Lukasiewicz's: an exercise in problem-solving},
+ Trinity College, Dublin 2, Ireland,
+ June 30, 1997\\
+ \url{http://www.maths.tcd.ie/report_series/tcdmath/tcdm9705.ps}
 \end{thebibliography}
 
 

doc/metalogic.kilepr

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

metalogic/Fol/Lang.v

 Require Import String.
-Require Import List.
+Require Import metalogic.Util.List.
 Require Import metalogic.Util.Ensemble.
 Require Import metalogic.Util.Defs.
 Require Import metalogic.Util.Tactics.
 
 
 Definition folTerm_closed t := folTermFV t = nil.
+Definition folTermList_closed n ts := folTermListFV n ts = nil.
 Definition folTerm_noFV t x := ~ List.In x (folTermFV t).
 Definition folTermList_noFV n t x := ~ List.In x (folTermListFV n t).
 
 Definition folPropSet_closed (T:FolPropSet) := forall p, folProp_closed p.
 
 Inductive FolSubstCorr x s : folProp -> Prop := 
+| folSubstCorr_const: forall p, folTerm_closed s -> FolSubstCorr x s p
 | folSubstCorr_dummy : forall p, folProp_noFV p x -> FolSubstCorr x s p
 | folSubstCorr_atom : forall (r:folRels L) ts, FolSubstCorr x s (folAtom r ts)
 | folSubstCorr_neg : forall p, FolSubstCorr x s p -> FolSubstCorr x s (folNeg p)
 | folSubstCorr_impl: forall p q, FolSubstCorr x s p -> FolSubstCorr x s q -> FolSubstCorr x s (folImpl p q)
-| folSubstCorr_forall: forall y p, ~ List.In y (folTermFV s) -> FolSubstCorr x s p -> FolSubstCorr x s (folForall y p)
-| folSubstCorr_exists: forall y p, ~ List.In y (folTermFV s) -> FolSubstCorr x s p -> FolSubstCorr x s (folExists y p)
+| folSubstCorr_forall: forall y p, folTerm_noFV s y -> FolSubstCorr x s p -> FolSubstCorr x s (folForall y p)
+| folSubstCorr_exists: forall y p, folTerm_noFV s y -> FolSubstCorr x s p -> FolSubstCorr x s (folExists y p)
 .
 
 Fixpoint folSubst (p:folProp) x s :=
 end.
 
 
+Section wf_ind.
+
+Definition folPropLt L p q := (folPropDepth L p) < (folPropDepth L q).
+
+Theorem folProp_ind_wf L (P: folProp L -> Type) :
+        P (folTrue L)
+     -> (forall r ts, P (folAtom L r ts))
+     -> (forall p, (forall p', folPropLt L p' (!p) -> P p') -> P (!p) )
+     -> (forall p q, (forall p', folPropLt L p' (p-->q) -> P p') -> P (p --> q) )
+     -> (forall x p, (forall p', folPropLt L p' ([[A x]]p) -> P p') -> P ([[A x]] p))
+     -> (forall x p, (forall p', folPropLt L p' ([[E x]]p) -> P p') -> P ([[E x]] p))
+     -> forall p, P p.
+Proof.
+intros L P HT HA HN HI HAx HEx.
+cut (forall p, (forall p', folPropLt L p' p -> P p') -> P p).
+intro H.
+apply induction_ltof1_T with (f := folPropDepth L); auto.
+intro p.
+
+case p; auto.
+Qed.
+
+End wf_ind.
+
+
 
 (*------------------------------------------------------------------------
  * LangExt

metalogic/Fol/Lang_facts1.v

 Require Import Arith.Max.
 Require Import metalogic.Util.Laws.
 Require Import Program.Equality.
-(**------------------------------------------------------------------------
+
+(**************************************************************************
  * Rownosci z ktorymi nie radzi sobie 'simpl'.
  *)
 
 Qed.
 Hint Rewrite folTermMap_eqApp: metalogic_db.
 
-(**------------------------------------------------------------------------
+Remark folTermSubstTs_eq L n t ts x s:
+        folSubstTs L (S n) (folTcons L n t ts) x s
+      = folTcons L n (folSubstT L t x s) (folSubstTs L n ts x s).
+Proof.
+auto.
+Qed.
+Hint Rewrite folTermSubstTs_eq: metalogic_db.
+
+(**************************************************************************
+ * Porzadek folPropLt
+ * 
+ * folPropLt L p q := (folPropDepth L p) < (folPropDepth L q)
+ *)
+
+Remark folPropLt_neg L p: folPropLt L p (!p).
+Proof.
+intros.
+red. simpl.
+auto with arith.
+Qed.
+Hint Resolve folPropLt_neg: metalogic_db.
+
+Remark folPropLt_implL L p q: folPropLt L p (p --> q).
+Proof.
+intros.
+red. simpl.
+auto with arith.
+Qed.
+Hint Resolve folPropLt_implL: metalogic_db.
+
+
+Remark folPropLt_implR L p q: folPropLt L q (p --> q).
+Proof.
+intros.
+red. simpl.
+auto with arith.
+Qed.
+Hint Resolve folPropLt_implR: metalogic_db.
+
+Remark folPropLt_Ax L x p: folPropLt L p ([[A x]] p).
+Proof.
+intros.
+red. simpl.
+auto with arith.
+Qed.
+Hint Resolve folPropLt_Ax: metalogic_db.
+
+Remark folPropLt_Ex L x p: folPropLt L p ([[E x]] p).
+Proof.
+intros.
+red. simpl.
+auto with arith.
+Qed.
+
+Remark folPropDepth_subst L p x t:
+       folPropDepth L (p <[ x ~> t ]>) = folPropDepth L p.
+Proof.
+intros.
+induction p; simpl; auto;
+destruct string_dec; simpl; auto.
+Qed.
+Hint Resolve folPropDepth_subst: metalogic_db.
+
+Remark folPropLt_subst L p q x t:
+       folPropLt L p q
+    -> folPropLt L (p <[ x ~> t]>) q.
+Proof.
+unfold folPropLt.
+intros.
+rewrite folPropDepth_subst.
+auto.
+Qed.
+Hint Resolve folPropLt_subst : metalogic_db.
+
+(**************************************************************************
+ * Zmienne wolne, zdania itp.
  *)
 
 Lemma folTerm_True_closed: forall L, folProp_closed L (folTrue L).
 Qed.
 Hint Resolve folTerm_neg_closed: metalogic_db.
 
+Lemma folTerm_negrev_closed: forall L p,
+      folProp_closed L (!p)
+   -> folProp_closed L p.
+Proof.
+intros.
+red; red in H. simpl in *; auto.
+Qed.
+Hint Resolve folTerm_negrev_closed: metalogic_db.
+
 (**------------------------------------------------------------------------
  *)
 
-
 Theorem folTerm_subst_onvar: forall L x s, folSubstT L (folVar L x) x s = s.
 Proof.
 intros.
 unfold folProp_noFV.
 auto with datatypes.
 Qed.
-Hint Resolve folProp_noFV_with_closed_implR: metalogic_db.
+Hint Resolve folProp_noFV_impl_distr: metalogic_db.
 
 (**------------------------------------------------------------------------
  *)
 (**------------------------------------------------------------------------
  *)
 
+Theorem folProp_closed_impl_distr: forall L p q,
+        folProp_closed L (p-->q)
+     -> folProp_closed L p /\ folProp_closed L q.
+Proof.
+intros.
+red in H.
+simpl in *.
+unfold folProp_closed.
+auto with datatypes.
+Qed.
+Hint Resolve folProp_closed_impl_distr: metalogic_db.
+
+(**------------------------------------------------------------------------
+ *)
+
+Theorem folProp_closed_impl_distrL: forall L p q ,
+        folProp_closed L (p-->q) 
+     -> folProp_closed L p .
+Proof.
+intros.
+destruct (folProp_closed_impl_distr L p q); auto.
+Qed.
+Hint Resolve folProp_closed_impl_distrL : metalogic_db.
+
+(**------------------------------------------------------------------------
+ *)
+
+Theorem folProp_closed_impl_distrR: forall L p q,
+        folProp_closed L (p-->q)
+     -> folProp_closed L q.
+Proof.
+intros.
+destruct (folProp_closed_impl_distr L p q); auto.
+Qed.
+Hint Resolve folProp_closed_impl_distrR : metalogic_db.
+
+(**------------------------------------------------------------------------
+ *)
+
 Theorem folProp_noFV_inA: forall L p x y,
         x <> y
      -> folProp_noFV L ([[A y]] p) x

metalogic/Fol/Lang_facts2.v

 rewrite IHp; eauto using folProp_noFV_inE.
 Qed.
 Hint Rewrite folProp_subst_noFV: metalogic_db.
-Hint Resolve folProp_subst_noFV: metalogic_db.
 
 (**------------------------------------------------------------------------
  * Podstawienie na formule.
- *
+ *)
 
 
-Theorem folProp_subst_const_noFV: forall L p x t,
+
+Remark folProp_Ex_FV_dec: forall L p x,
+        folProp_closed L ([[E x]] p)
+     -> {folPropFV L p = x::nil} + {folProp_closed L p}.
+Proof.
+admit.
+Qed.
+
+
+Theorem folProp_subst_const_FV: forall L p x t,
         folPropFV L p = (cons x nil)
      -> folTerm_closed L t
      -> folProp_closed L (p <[ x ~> t ]>).
 Proof.
 admit.
 Qed.
-Hint Rewrite folProp_subst_const_noFV: metalogic_db.
-Hint Resolve folProp_subst_const_noFV: metalogic_db.
-*)
+Hint Resolve folProp_subst_const_FV: metalogic_db.
 
+Theorem folProp_subst_const_closedE: forall L p x t,
+        folProp_closed L ([[E x]] p)
+     -> folTerm_closed L t
+     -> folProp_closed L (p <[ x ~> t ]>).
+Proof.
+intros.
+destruct folProp_Ex_FV_dec with L p x as [D|D]; auto.
+apply folProp_subst_const_FV; auto.
+
+autorewrite with metalogic_db; auto with metalogic_db.
+Qed.
+Hint Resolve folProp_subst_const_closedE: metalogic_db.
+

metalogic/Fol/Model_facts1.v

 Qed.
 Hint Resolve FolModel_closed: metalogic_db.
 
+Theorem FolModel_closed': forall L M p v,
+        folProp_closed L p
+     -> folInterp M v p
+     -> L@M |= p.
+Proof.
+intros.
+intro v'.
+apply FolModel_closed with v; auto.
+Qed.
+Hint Resolve FolModel_closed': metalogic_db.
+
 (**------------------------------------------------------------------------
  * Gdy p jest zdaniem to:
  *  (~ M |= p ) implikuje (M |= !p )
 absurd (folInterp M v p); auto.
 Qed.
 Hint Resolve FolModel_negrev : metalogic_db.
+
+(**------------------------------------------------------------------------
+ * Lemat o podstawianiu.
+ *)
+
+Lemma FolModel_Term_subst: forall L M t x s v,
+      folValueT L M v (folSubstT L t x s)
+    = folValueT L M (funcUpd v x (folValueT L M v s)) t.
+Proof.
+intros L M t.
+
+induction t using folTerm_indP with
+ (P := fun n ts => forall x s v f,
+       folValueGenApp L M v n (folSubstTs L n ts x s) f 
+     = folValueGenApp L M (funcUpd v x (folValueT L M v s)) n ts f).
+
+intros.
+auto.
+
+rename f into ts.
+intros x s v f.
+
+rewrite folTermSubstTs_eq.
+rewrite folValueGenApp_eq.
+rewrite IHt0.
+rewrite folValueGenApp_eq.
+rewrite IHt.
+auto.
+
+intros.
+simpl.
+destruct string_dec; subst; auto.
+rewrite folValueT_eqVar.
+unfold funcUpd.
+destruct string_dec; auto. absurd (s=s); auto.
+repeat rewrite folValueT_eqVar.
+unfold funcUpd.
+destruct string_dec. subst. absurd (s=s); auto.
+auto.
+
+intros.
+rename f0 into ts.
+simpl.
+repeat rewrite folValueT_eqApp.
+auto.
+Qed.
+Hint Rewrite FolModel_Term_subst: metalogic_db.
+
+Lemma FolModel_TermList_subst: forall L M n ts x s v,
+       folValueGenApp L M v n (folSubstTs L n ts x s) 
+     = folValueGenApp L M (funcUpd v x (folValueT L M v s)) n ts.
+Proof.
+intros L M n.
+intros.
+induction ts.
+autorewrite with metalogic_db; auto with metalogic_db.
+red; auto with metalogic_db.
+simpl.
+rename f into t.
+apply functional_extensionality; intro f.
+rewrite folValueGenApp_eq.
+rewrite IHts.
+rewrite FolModel_Term_subst. auto.
+Qed.
+Hint Rewrite FolModel_TermList_subst: metalogic_db.
+
+
+Lemma FolModel_rel_subst': forall L M n ts x s v r,
+      folValueGenRel L M v n (folSubstTs L n ts x s) r
+  <-> folValueGenRel L M (funcUpd v x (folValueT L M v s)) n ts r.
+Proof.
+intros.
+
+induction ts.
+split; intro H; auto.
+
+rewrite folValueGenRel_eq.
+rewrite folTermSubstTs_eq.
+rewrite folValueGenRel_eq.
+rewrite <- FolModel_Term_subst.
+auto.
+Qed.
+
+
+Lemma FolModel_Prop_subst: forall L M p x s v,
+      FolSubstCorr L x s p ->
+(      (folInterp M (funcUpd v x (folValueT L M v s)) p)
+       <->
+      (folInterp M v (p <[ x ~> s]>))
+).
+Proof.
+admit.
+Qed.

metalogic/Fol/Model_facts3.v

 intros L M T p HMT HTp.
 induction HTp.
 induction d; auto with metalogic_db.
+repeat red; auto.
 intros v.
 red in IHd1; simpl in IHd1.
 apply IHd1. auto.

metalogic/Fol/Proof.v

  | folDerivAX5: forall a, folDeriv T (FolAx5 a)
  | folDerivL1: forall x a, folDeriv T (FolGxL1 x a)
  | folDerivL2: forall x a, folDeriv T (FolGxL2 x a)
+ | folDerivT: folDeriv T (folTrue L)
 (*
  | folDerivGX0: forall x a, folDeriv T (FolGx0 x a)
  | folDerivGX1: forall x a b, folDeriv T (FolGx1 x a b)
  | folDerivAX5 _ => @Empty_set _
  | folDerivL1 _ _ => @Empty_set _
  | folDerivL2 _ _ => @Empty_set _
+ | folDerivT => @Empty_set _
 (*
  | folDerivGX0 _ _ => @Empty_set _
  | folDerivGX1 _ _ _ => @Empty_set _

metalogic/Fol/Tactics.v

 
 Ltac fol_prove_deriv_AXaxiom := solve [ 
        apply folDerivAX; fol_prove_InSubset_axiom
+     | apply folDerivT
      | apply folDerivAX1
      | apply folDerivAX2
      | apply folDerivAX3 

metalogic/Fol/TheoremModelExistence.v

 Require Import metalogic.Fol.Lang.
+Require Import metalogic.Fol.Lang_facts.
 Require Import metalogic.Fol.Proof.
 Require Import metalogic.Fol.Proof_facts.
+Require Import metalogic.Fol.Tactics.
 Require Import metalogic.Fol.Model.
 Require Import metalogic.Fol.Model_facts.
 Require Import metalogic.Fol.TheoremExtensionality.
+Require Import metalogic.Fol.TheoremDeduction.
 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.
 Require Import List.
 Require Import String.
-
+Require Import FunctionalExtensionality.
 
 (**------------------------------------------------------------------------
  *
 simpl. auto.
 Defined.
 
-Let Mfunc: forall f : folFuncs L, Defs.nAry (folFuncAr L f) Muniv.
-admit.
+
+(*------------------------------------------------------------------------
+ * Nadawanie interpretacji symbolom funkcyjnym i relacja.
+ *
+ * CEL: Nadac interpretacje symbolowi funkcyjnemu f, taka ze
+ *      jest to funkcja ktora zwraca zamkniety term
+ *      bedacy aplikacja danego symbolu funkcyjnego do termow
+ *      symoblizujacych argumenty.
+ *
+ *  f^M (x1^M, ..., xn^M) = f(x1, ..., xn)
+ * 
+ * CEL: Nadac interpretacje symbolowi relacyjnemu r, taka zeby
+ *      relacja byla spelniona wtedy i tylko wtedy gdy
+ *      term symbolizujacy te relacje jest dowodliwy.
+ *
+ *  M |= r^M (x1^M, ..., xn^M)  wtw T |= r(x1, ..., xn)
+ *
+ * Tworzymy pomocnicza funkcje, ktora dla danego n generuje
+ * funkcje, ktora zwraca n-liste termow bedacych jej argumentami.
+ *
+ * folCollectTermArgs n = \x1 ... xn. [x1, ..., xn]
+ *
+ * Nastepnie tworzymy druga pomocnicza funkcje ktora sklada
+ * poprzednia z jakas funkcja od tej listy.
+ *
+ * folCollectApp n f = \x1 ... xn. f ([x1,...,xn])
+ *
+ *
+ *)
+
+Let folTermListClosed n := { ts : folTermList L n & folTermList_closed L n ts }.
+
+Let folCollectTermArgs n : nAryB n (folTermListClosed n)  Muniv.
+refine (fix F n :=
+match n return (nAryB n (folTermListClosed n) Muniv) with
+| 0 => _ (* 1 *)
+| S n => nAryB_ExtDepS1 n _ _ 
+ (fun x xs => _ (* 2 *))
+ (F n)
+end
+).
+(* 1 *)
+exists (folTnil L); unfold folTermList_closed; auto.
+(* 2 *)
+destruct xs as [ts Hts].
+exists (folTcons L n0 (folTermClosed_unpack L x) ts).
+unfold folTermList_closed;
+autorewrite with metalogic_db.
+repeat red in Hts.
+rewrite Hts.
+rewrite <- app_nil_end.
+unfold folTermClosed_unpack.
+destruct x.
+auto.
 Defined.
 
-Let Mrel: forall r : folRels L, Defs.nAryP (folRelAr L r) Muniv.
-admit.
+(*
+Fixpoint folCollectTermArgs n : nAryB n (folTermList L n) Muniv :=
+match n return (nAryB n (folTermList L n) Muniv) with
+| 0 => folTnil L
+| S n => nAryB_ExtDepS1 n _ _ 
+ (fun x xs => folTcons L n (folTermClosed_unpack L x) xs) (folCollectTermArgs n)
+end.
+*)
+
+Let folCollectApp B n (f:folTermListClosed n -> B)
+        :  nAryB n B Muniv
+:= nAryB_ExtDep' n n
+   (folTermListClosed) B Muniv
+   (fun ts => f ts)
+   (folCollectTermArgs n)
+.
+
+Let folTermListClosed_unpack n (cts:folTermListClosed n)
+ : folTermList L n := projT1 cts.
+
+Let Mfunc: forall f : folFuncs L, nAry (folFuncAr L f) Muniv.
+refine (
+fun f => folCollectApp Muniv (folFuncAr L f)
+    (fun ts => 
+     folTermClosed_intro L (folApp L f (folTermListClosed_unpack _ ts)) _ (* 1 *)
+    )
+).
+(* 1 *)
+unfold folTermListClosed_unpack.
+red.
+destruct ts as [ts Hts].
+simpl.
+auto.
 Defined.
 
+Let Mrel: forall r : folRels L, Defs.nAryP (folRelAr L r) Muniv :=
+fun r => folCollectApp Prop (folRelAr L r) 
+         (fun ts => L@T ||-- folAtom L r (folTermListClosed_unpack _ ts)) 
+.
+
 Let M := folStruct L Muniv Minhb Mfunc Mrel.
+Let v_unpack v (x:string) := folTermClosed_unpack L (v x).
+
+
+Let Mfunc_correct: forall v t (H:folTerm_closed L t),
+    folValueT L M v t = folTermClosed_intro L t H.
+Proof.
+intros.
+admit.
+Qed.
+
+Let value_eq v (x:string) :
+    funcUpd v x (folValueT L M v (v_unpack v x)) = v.
+Proof.
+intros.
+apply functional_extensionality.
+intros y.
+unfold v_unpack.
+unfold funcUpd.
+destruct string_dec. subst.
+destruct (v y).
+simpl.
+rewrite <- Mfunc_correct with (v := v).
+auto.
+auto.
+Qed.
+
+
+Let Mrel_correct: forall r ts,
+        (L@M |= folAtom L r (folTermListClosed_unpack _ ts))
+    <-> (L@T ||-- folAtom L r (folTermListClosed_unpack _ ts)).
+Proof.
+intros.
+unfold folTermListClosed_unpack.
+destruct ts as [ts ts_closed]; simpl.
+split; intro H.
+
+admit.
+admit.
+Qed.
+
+(*
+Let FolTermModel_Prop_subst: forall p x s v,
+       FolSubstCorr L x s p  ->
+(      (folInterp M (funcUpd v x (folValueT L M v s)) p)
+       <->
+      (folInterp M v (p <[ x ~> s]>))
+).
+Proof.
+intros.
+apply FolModel_Prop_subst.
+Qed.
+*)
+
+Let Mrel_correct': forall r ts, folTermList_closed L _ ts -> (
+        (L@M |= folAtom L r ts)
+    <-> (L@T ||-- folAtom L r ts)).
+Proof.
+intros.
+pose (existT _ ts H: folTermListClosed _) as cts.
+assert (ts = folTermListClosed_unpack _ cts).
+auto.
+rewrite H0.
+apply Mrel_correct.
+Qed.
+
+Theorem FolModelExistence_correct: forall p, folProp_closed L p
+        -> ((L@M |= p) <-> (L@T ||-- p)).
+Proof.
+intro p.
+set (fun p => folProp_closed L p ->(L @ M |= p <-> L @ T ||-- p)) as P.
+change (P p).
+
+
+apply folProp_ind_wf with 
+ (P := P); clear p; subst P; cbv beta.
+
+(* T *)
+split; simpl in *; intro H';
+auto with metalogic_db; repeat red; auto.
+
+(* Atom *)
+apply Mrel_correct'; auto.
+
+(* ! *)
+intros p IHp.
+split; simpl in *; intro H';
+assert (folProp_closed L p) as Cp by (eauto with metalogic_db);
+destruct IHp with p as [IHp' IHp'']; auto with metalogic_db.
+
+(* T |- *)
+
+(* Cel:       M |= !p -> T |- !p
+ * Mamy       T |- p -> M |= p
+ * Zatem    ~ M |= p -> ~ T |- p
+ * Mamy      ~ T |- p, bo (M |= !p daje ~ M |= p)
+ * Poniewaz teoria jest niesprzeczna i zupelna to T |- p
+ *)
+
+assert ( ~ (L @ M |= p) -> ~ FolPrf T p ) as IH by (eauto using contraposition).
+assert ( ~ (L @ M |= p)); eauto using FolModel_negrev.
+destruct (complT p); auto.
+absurd (FolPrf T p); auto.
+
+(* M |= *)
+
+(*  Cel:       T |- !p -> M |= !p
+ *  Mamy:      M |= p -> T |- p
+ *  Zatem:    ~T |- p -> ~ M |= p
+ *  Mamy      ~T |- p bo teoria jest niesprzeczna i zupelna.
+ *  Mamy      M |= !p, bo wynika z ~ M |= p
+ *)
+
+assert ( ~ FolPrf T p -> ~ (L @ M |= p)) as IH by (eauto using contraposition).
+assert ( ~ FolPrf T p ).
+intro C. apply consT. exists p; auto.
+apply FolModel_neg; auto.
+
+(* -> *)
+intros p1 p2 IHp closed.
+(* T |- *) 
+
+(* Cel:  M |= (p1 --> p2) -> T |- (p1 --> p2)
+ * T jest zupelna wiec T |- p1 albo T |- !p1, rozwazmy przypadki.
+ * a)  T |- p1
+ *     Zatem M |= p1, oraz M |= p2 bo M |= p1 --> p2
+ *     Ponownie z zal ind. mamy T |- p2.
+ *     Mamy T |- p1 oraz T |- p2 dla zdan p1,p2 ...
+ *
+ *     Dowod T |- p1 --> p2 wewnatrz systemu ponizej.
+ *
+ * b)  T |- !p1
+ *    Z tw o deduckji wynika, ze wystarczy pokazac
+ *     T,p1 |- p2, poniewaz T |- !p1 to T,p1 jest sprzeczna.
+ *     Poniewaz jest sprzeczna to wszystko da sie udowodnic.
+ * 
+ *)
+assert (folProp_closed L p1) as Cp1; eauto with metalogic_db.
+assert (folProp_closed L p2) as Cp2; eauto with metalogic_db.
+split; simpl in *; intro H;
+destruct IHp with p1 as [IHp1' IHp1'']; auto with metalogic_db;
+destruct IHp with p2 as [IHp2' IHp2'']; auto with metalogic_db.
+destruct (complT p1); auto.
+(* T |- p *)
+assert (L@T ||-- p2) as Tp2.
+apply IHp2'.
+red in H. simpl in H.
+intro v.
+apply H.
+apply IHp1''.
+auto.
+inversion Tp2.
+
+fol_pose d1 a1 AX (!p2 --> p2 --> !p1).
+fol_pose d2 a2 TH (p2 --> !p2 --> !p1).
+fol_pose d3 a3 MP (!p2 --> !p1) from d2 d.
+fol_pose d4 a4 TH (p1 --> p2) eauto.
+fol_pose QED.
+
+(* T |- !p *)
+destruct FolDeduction with L T p1 p2 as [_ Ded]; auto.
+apply Ded.
+apply FolInconsistent_prove_all.
+eauto with metalogic_db.
+
+(* M |= *)
+
+admit.
+
+(* A *)
+admit.
+
+(* 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) ]
+ *)
+
+destruct Minhb as [u0].
+set (v0 := fun x:string => u0).
+assert (folInterp M v0 ([[E x]] p)) as M_Exp; auto.
+assert (exists v, folInterp M v p) as M_pv.
+simpl in M_Exp.
+destruct M_Exp as [u M_Exp].
+exists (funcUpd v0 x u); auto.
+
+destruct M_pv as [v M_pv].
+
+assert (folProp_closed L (p <[ x ~> v_unpack v x ]>)) as p'C.
+unfold v_unpack.
+destruct (v x).
+simpl; auto.
+apply folProp_subst_const_closedE; auto.
+
+assert (L@M |= (p <[x ~> v_unpack v x]>)) as M_p.
+apply FolModel_closed' with v; auto.
+destruct FolModel_Prop_subst with L M p x (v_unpack v x) v as [S1 _].
+apply folSubstCorr_const.
+unfold v_unpack.
+destruct (v x).
+simpl; auto.
+apply S1.
+rewrite value_eq. auto.
+
+assert (L@T ||-- p <[ x ~> v_unpack v x]>) as T_p.
+destruct IHp with (p <[ x ~> v_unpack v x ]>); auto.
+apply folPropLt_subst; auto using folPropLt_Ex; auto. 
+Qed.
 
 Theorem FolModelExistence'': exists M, L@M ||= T.
 Proof.
 exists M.
-admit.
+cut (forall p, (L@M |= p) <-> (L@T ||-- p) ).
+intro corr.
+intros p.
+destruct corr with p.
+intros pInT.
+apply H0.
+auto with metalogic_db.
+
 Qed.
 
 End ModelConstruction.

metalogic/Util/Defs.v

 Require Import String.
 Require Import Logic.FunctionalExtensionality.
 
+(*************************************************************************
+ * Funkcje obliczajace typ funkcji o ustalonej arnosci.
+ *
+ * nAryB n B U === U -> ... U -> B
+ *                 ^^^^^^^^^^^
+ *                      n
+ *)
+
 Fixpoint nAryB n B U :=
 match n with
  | 0 => B
 auto.
 Qed.
 
+(*------------------------------------------------------------------------
+ * Rozszerzanie funkcji o typach prostych
+ *
+ * (nAryB_Ext n B U f) g = \x0 x1 ... xn. f x0 (g x1 ... xn)
+ *
+ * Funkcja pozwala stworzyc nowa funkcje o n+1 argumentach, ktora
+ * powstaje poprzez zaaplikowanie funkcji 'f' do pierwszego argumentu
+ * i funkcji g do pozostalych argumentow.
+ *
+ * Przyklad wykorzystania: Stworzenie funkcji generujaca funkcje n-arne
+ * zwracajace n-elementowe listy swoich argumentow.
+ * gen 0 = nil
+ * gen 1 a = [a]
+ * gen 2 a b = [a,b]
+ * itd... (patrz zakomentowane 'testy' ponizej)
+ * 
+ * mozna te funkcje napisac jeszcze ogolniej (dac f: U -> B -> C),
+ *  ale ona byla mi jedynie potrzebna
+ * jako 'pierwszy krok' do zrobienia funckji do typow zaleznych.
+ *)
+
+Fixpoint nAryB_Ext n B U (f:U -> B -> B) : nAryB n B U -> nAryB (S n) B U :=
+match n return (nAryB n B U -> nAryB (S n) B U) with
+| 0 =>  fun g x => f x g
+| S n => fun g x u => nAryB_Ext n B U f (g u) x
+end.
+
+(*------------------------------------------------------------------------
+ * Rozszerzanie funkcji o typach zaleznych od liczb naturalnych.
+ * Pewnie prosto mozna zrobic ze nie tylko od liczb naturalnych, ale nie
+ * bylo to mi do niczego juz potrzebne.
+ *
+ * nAryB_ExtResDep pozwala z funkcji
+ *    g : U -> ... -> U -> B(m)
+ *        ^^^^^^^^^^^^^^
+ *             n
+ *
+ * stworzyc jakas funkcje o typie
+ *        U -> ... -> U -> C(m)
+ *        ^^^^^^^^^^^^^^
+ *             n
+ *
+ * (nAryB_ExtDep m n B C U f) g = \x1 ... \xn. f (g x1 ... xn)
+ * (czyli takie zlozenie ,,pod lambdami'')
+ * 
+ * Dostarczona tez wyspecjalizowana funkcja:
+ * (nAryB_ExtDepS2 m n B C U f) g = \x0 x1 ... \xn. f x0 (g x1 ... xn)
+ * gdzie f: U -> B n -> B (S n).
+ *
+ * Funkcja nAryB_ExtDepS1 jest jej specjalizacja dla m = n.
+ *
+ * Pzydatna przy robieniu funkcji co zwraca np wektor z argumentami
+ * (patrz testy ponizej)
+ *)
+
+Fixpoint nAryB_ExtDep (m n:nat) B C U (f:B m -> C m)
+        : nAryB n (B m) U -> nAryB n (C m) U
+:=
+match n return (nAryB n (B m) U -> nAryB n (C m) U) with
+| 0 =>  fun g => f g
+| S n => fun g u => nAryB_ExtDep m n B C U f (g u) 
+end.
+
+Definition nAryB_ExtDep' (m n:nat) B C U (f: B m -> C)
+:= nAryB_ExtDep m n B (fun n => C) U f.
+
+Definition nAryB_ExtDepS2 m n B U (f: U -> B m -> B (S m))
+         : nAryB n (B m) U -> nAryB (S n) (B (S m)) U
+:= fun g x => nAryB_ExtDep m n B (fun n => B (S n)) U (f x) g.
+
+Definition nAryB_ExtDepS1 n B U (f: U -> B n -> B (S n))
+         : nAryB n (B n) U -> nAryB (S n) (B (S n)) U
+:= nAryB_ExtDepS2 n n B U f.
+
+(*
+
+Fixpoint nAryB_ExtD' m n B U (f:forall n, U -> B n -> B (S n) ) (x:U)
+        : nAryB n (B m) U -> nAryB n (B (S m)) U
+:=
+match n return (nAryB n (B m) U -> nAryB n (B (S m)) U) with
+| 0 =>  fun g => f m x g
+| S n => fun g u => nAryB_ExtD' m n B U f x (g u) 
+end.
+
+Definition nAryB_ExtD n B U (f:forall n, U -> B n -> B (S n)) 
+         : nAryB n (B n) U -> nAryB (S n) (B (S n)) U
+:=
+fun g x => nAryB_ExtD' n n B U f x g
+.
+*)
+
+(* szybki test 
+Require Import List.
+
+Fixpoint gen n : nAryB n (list nat) nat := 
+match n with
+| 0 => nil
+| S n => nAryB_Ext n _ _ (fun x xs => cons x xs) (gen n)
+end.
+
+Eval compute in (gen 2 1).
+
+Eval compute in (gen 3 1 2 3).
+
+Inductive vector: nat -> Set :=
+ | vnil : vector 0
+ | vcons : forall n, nat -> vector n -> vector (S n)
+.
+
+Fixpoint vgen n : nAryB n (vector n) nat :=
+match n return (nAryB n (vector n) nat) with
+ | 0 => vnil
+ | S n => nAryB_ExtDepS1 n _ _ vcons (vgen n)
+end.
+
+Eval compute in (vgen 0).
+Eval compute in (vgen 2 9 99).
+Eval compute in (vgen 3).
+
+ *)
+
+
 Definition funcUpd U (f:string->U) x v := fun y => if string_dec x y then v else f y.
 Implicit Arguments funcUpd [U].
 

metalogic/Util/List.v

 
 Implicit Arguments ltl [A].
 
+(* Dowod z kodu zrodlowego Coqa, zmienilem tylko Set na Type *)
+
 Theorem induction_ltof1_T A f:
   forall P:A -> Type,
     (forall x:A, (forall y:A, ltof _ f y x -> P y) -> P x) -> forall a:A, P a.