diff --git a/class_01_01082023/plan_cs621.pdf b/class_01_01082023/plan_cs621.pdf
new file mode 100644
index 0000000..088638c
Binary files /dev/null and b/class_01_01082023/plan_cs621.pdf differ
diff --git a/class_02_03082023/summary.txt b/class_02_03082023/summary.txt
new file mode 100644
index 0000000..9ffc266
--- /dev/null
+++ b/class_02_03082023/summary.txt
@@ -0,0 +1,5 @@
+Inductive definition of sets
+separation property : to prove that some element is not element of
+this set. 
+
+
diff --git a/class_03_08082023/summary.txt b/class_03_08082023/summary.txt
new file mode 100644
index 0000000..e7bc8bd
--- /dev/null
+++ b/class_03_08082023/summary.txt
@@ -0,0 +1,7 @@
+Definition of inductive sets
+Definition of wffs
+Definition of T1 : last symbol from right should be a ')' or a
+proposition. 
+
+violating example : (p and q)^r
+
diff --git a/class_04_10082023/summary.txt b/class_04_10082023/summary.txt
new file mode 100644
index 0000000..e38046c
--- /dev/null
+++ b/class_04_10082023/summary.txt
@@ -0,0 +1,7 @@
+Property T2 : : equal number of ('s and )'s
+Some example ((p)()
+Satisfies T2 but not T1
+
+Definition of PIS : proper initial segment
+Also called proper prefix.
+
diff --git a/class_05_14082023/summary.txt b/class_05_14082023/summary.txt
new file mode 100644
index 0000000..b41afbb
--- /dev/null
+++ b/class_05_14082023/summary.txt
@@ -0,0 +1,5 @@
+initial  proper segment contd.
+It captures mismatched parenthesis
+)(()
+this example satisfies property T2 : equal number of ('s and )'s
+
diff --git a/class_06_17082023/summary.txt b/class_06_17082023/summary.txt
new file mode 100644
index 0000000..78903b1
--- /dev/null
+++ b/class_06_17082023/summary.txt
@@ -0,0 +1,15 @@
+Semantics of propositional logic 
+
+Valuation
+Satisfiability
+unѕatisfiable
+validity
+contradiction
+tautology
+logical implication
+logical equivalence 
+
+claim : \alpha logically implies \beta  Iff (\alpha \implies \beta) is a tautology. 
+claim : If \alpha is a contradiction then for any \beta, \alpha logically implies \beta. 
+
+
diff --git a/class_07_21082023/summary.txt b/class_07_21082023/summary.txt
new file mode 100644
index 0000000..cacf392
--- /dev/null
+++ b/class_07_21082023/summary.txt
@@ -0,0 +1,14 @@
+Semantic notions for a set of formulas:
+
+\Sigma - satisfiable, examples.
+
+Logical implication \Sigma \entails \alpha
+
+complete -- \Sigma \entails \alpha (inclusive OR) \Sigma \entails (\neg \alpha)
+
+\Sigma is satisfiable and complete then 
+         \Sigma \entails \alpha (XOR) \Sigma \entails (\neg \alpha)
+
+Maximum Satisfiability 
+          In addition to being satisfiable, Sigma has the following property: 
+          \neg( \Sigma \entails \alpha) \implies \Sigma \cup \{ \alpha\} is not satisfiable. 
diff --git a/class_08_22082023/summary.txt b/class_08_22082023/summary.txt
new file mode 100644
index 0000000..c232dcb
--- /dev/null
+++ b/class_08_22082023/summary.txt
@@ -0,0 +1,19 @@
+Thm : \Sigma is Maximum Satisfiability 
+             iff 
+      \Sigma is satisfiable and complete.
+Proof of above theorem. 
+
+Claim: \Sigma \entails \alpha Iff \Sigma \cup \{ \neg \alpha\} is Not satisfiable. 
+
+
+Finite models theorem: (FMT)
+A set \Sigma \entails some wff \alpha 
+implies
+there is a finite subset of \Sigma which \entails \alpha.
+
+Proof of FMT using claim above. 
+
+Claim : \Sigma is maximally satisfiable  Iff 
+        \Sigma has a unique valuation. 
+Left as an exercise. 
+
diff --git a/class_09_24082023/summary.txt b/class_09_24082023/summary.txt
new file mode 100644
index 0000000..084dd76
--- /dev/null
+++ b/class_09_24082023/summary.txt
@@ -0,0 +1,11 @@
+Finite satisfiability
+Statement of Compactness theorem
+Proof :
+Godel Numbering
+Construction of \Delta from \Sigma
+Proving that \Delta is satisfiable. 
+Lemma : Given \Sigma is FS. Then for any formula \alpha 
+       \Sigma \cup \{ \alpha \} is satisfiable OR 
+       \Sigma \cup \{ \neg \alpha \} is satisfiable.
+Proof of this lemma is remaining. 
+
diff --git a/class_10_29082023/summary.txt b/class_10_29082023/summary.txt
new file mode 100644
index 0000000..64f88c8
--- /dev/null
+++ b/class_10_29082023/summary.txt
@@ -0,0 +1,15 @@
+Applications of compactness theorem:
+2-colorability of graphs
+ 
+Goal: Given a graph G=(V,E)  it is 2-colorable iff every finite subset of G is 2-colorable. 
+
+Proof outline:  
+Given a graph G=(V,E) construct a set \Sigma of wffs such that
+G is 2-colorable  
+iff  (step 1) 
+\Sigma is satisfiable. 
+iff  
+(by CT) \Sigma is finitely satisfiable
+iff (step 2) 
+Each finite subset of G is 2-colorable.
+