From 13f92b3386fa7bb3f6fcd3c93e7dfd7952c91035 Mon Sep 17 00:00:00 2001
From: jorenchik <jorens.stekels@gmail.com>
Date: Sun, 12 May 2024 16:37:38 +0300
Subject: [PATCH] initial commit

---
 .gitignore |   1 +
 main.typ   | 513 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 514 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 main.typ

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..f0de8a3
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+main.pdf
diff --git a/main.typ b/main.typ
new file mode 100644
index 0000000..1e68f65
--- /dev/null
+++ b/main.typ
@@ -0,0 +1,513 @@
+#set enum(numbering: "a)")
+
+
+= Logical axiom schemes
+
+$bold(L_1): B→(C →B)$
+
+$bold(L_2):  (B→(C →D))→((B→C)→( B→D))$
+
+$bold(L_3): B∧C→B$
+
+$bold(L_4): B∧C→C$
+
+$bold(L_5): B→(C →B∧C)$
+
+$bold(L_6): B→B∨C$
+
+$bold(L_7): C →B∨C$
+
+$bold(L_8): (B→D)→((C →D)→(B∨C →D))$
+
+$bold(L_9): (B→C)→((B→¬C )→¬B)$
+
+$bold(L_10): ¬B→( B→C)$
+
+$bold(L_12):  ∀x F (x)→F (t)$  (in particular, $∀x F (x)→F (x)$)
+
+$bold(L_13):  F (t)→∃ x F( x)$  (in  particular, $F (x)→∃ x F (x)$)
+
+$bold(L_14): ∀x(G →F (x))→(G→∀x F (x)) $
+
+$bold(L_15): ∀x(F (x)→G)→(∃z(x+z+1=y).x F (x)→G)$
+
+= Theorems
+
+$[L_1, L_2, #[MP]]$:
+
++ $((A→B)→(A→C))→(A→(B→C))$. Be careful when assuming hypotheses:
+  assume (A→B)→(A→C), A, B – in this order, no other possibilities! 
++ $(A→B)→((B→C)→(A→C))$. It's another version of the *Law of Syllogism* 
+  (by  Aristotle),  or  the  transitivity  property  of  implication.  
++ $(A→(B→C))→(B→(A→C))$.  It's  another  version  of  the  *Premise
+  Permutation Law*. Explain the difference between this formula and Theorem
+  1.4.3(a): A→(B→C)├ B→(A→C).
+
+== Theorem 1.5.1 (Deduction Theorem 1 AKA DT1)
+
+If $T$ is a first order theory, and there is a proof of
+$[T, #[MP]]: A_1, A_2, dots, A_n, B├ C$,
+ then there is a proof of
+$[L_1, L_2, T, #[MP]]: A_1, A_2, dots, A_n├ B→C$.
+
+
+== Theorem 1.5.2 (Deduction Theorem 2 AKA DT2)
+
+If there is a proof $[T, #[MP], #[Gen]]: A_1, A_2, dots, A_n, B├ C$,
+where, after B appears in the proof, Generalization is not applied to the
+variables that occur as free in $B$, then there is a proof of
+$[L_1, L_2, L_14, T, #[MP], #[Gen]]: A_1, A_2, dots, A_n├ B→C$.
+
+== Theorem 2.2.1.
+
++ (C-introduction): $[L_5, #[MP]]: A, B├ A∧B$;
++ (C-elimination): $[L_3, L_4, #[MP]]: A∧B ├ A, A∧B ├ B$.
+
+== Theorem 2.2.2.
+
++ $[L_1, L_2, L_5, #[MP]]: (A→(B→C)) ↔ ((A→B)→(A→C))$ (extension of the axiom L_2).
++ $[L_1-L_4, #[MP]]: (A→B)∧( B→C)→( A→C)$ (another form of the *Law of
+  Syllogism*, or *transitivity property of implication*).
+
+== Theorem 2.2.3 (properties of the conjunction connective).
+
+$[L_1- L_5, #[MP]]$:
+
++ $A∧B↔B∧A$ . Conjunction is commutative.
++ $ A∧(B∧C)↔( A∧B)∧C$. Conjunction  is associative.
++ $A∧A↔A$ . Conjunction is idempotent.
+
+== Theorem 2.2.4 (properties of the equivalence connective).
+
+$[L_1- L_5, #[MP]]$:
+
++ $A↔A$ (reflexivity),
++ $(A↔B)→(B↔A)$ (symmetry),
++ $(A↔B)→((B↔C) →((A↔C))$ (transitivity).
+
+
+== Theorem 2.3.1
+
++ (D-introduction)$[L_6, L_7, #[MP]]: A├ A∨B; B├ A∨B$; 
++ (D-elimination) If there is a proof $[T, #[MP]]: A_1, A_2, ..., A_n, B├ D$,
+  and a proof $[T, #[MP]]: A_1, A_2, ..., A_n, C├ D$, then there is a proof $[T,
+L_1, L_2, L_8, #[MP]]: A_1, A_2, dots, A_n, B∨C ├ D$. 
+
+
+== Theorem 2.3.4.
+
+Conjunction is distributive to disjunction, and disjunction is distributive to
+conjunction:
+
++ $[L_1-L_8, #[MP]]: (A∧B)∨C ↔(A∨C)∧(B∨C)$;
++ $[L_1-L_8, #[MP]]: (A∨B)∧C ↔(A∧C)∨(B∧C)$ .
+
+== Theorem 2.3.2
+
+a) $[ L_5, L_6-L_8, #[MP]]: A∨B↔B∨A$ . Disjunction is commutative.
+b) $[L_1, L_2, L_5, L_6-L_8, #[MP]]: A∨A↔A$ . Disjunction is idempotent.
+
+== Theorem 2.3.3.
+
+Disjunction is associative: $[L_1, L_2, L_5, L_6-L_8, #[MP]]: A∨(B∨C)↔(
+  A∨B)∨C$.
+
+== Theorem 2.3.4.
+
+Conjunction is distributive to disjunction, and disjunction is distributive to
+conjunction:
+
++ $[L_1-L_8, #[MP]]: (A∧B)∨C ↔(A∨C)∧(B∨C)$ .
++ $[L_1-L_8, #[MP]]: (A∨B)∧C ↔(A∧C)∨(B∧C)$ .
+
+
+== Theorem 2.4.1.
+
+(N-elimination) If there is a proof
+
+$[T, #[MP]]: A_1, A_2, ..., A_n, B├ C$, and a proof $[T, #[MP]]: A_1, A_2, ..., A_n,
+B├ ¬C$, then there is a  proof $[T, L_1, L_2, L_9, #[MP]]: A_1, A_2, ..., A_n├ ¬B$.
+
+== Theorem 2.4.2.
+
+a) $[L_1, L_2, L_9, #[MP]]: A, ¬B├ ¬(A→B)$. What does it mean?
+b) $[L_1-L_4, L_9, #[MP]]: A∧¬B→¬( A→B)$. 
+
+
+== Theorem 2.4.3.
+
+$[L_1, L_2, L_9, #[MP]]: (A→B)→(¬B→¬A)$. What does it mean?
+It's the so-called *Contraposition Law*.
+
+Note. The following rule form of Contraposition Law is called *Modus Tollens*:
+$[L_1, L_2, L_9, #[MP]]: A→B, ¬B├ ¬A, or, frac(A→B \; ¬B, ¬A)$
+
+== Theorem 2.4.4.
+
+$[L_1, L_2, L_9, #[MP]]: A→¬¬A$.
+
+== Theorem 2.4.5.
+
+$[L_1, L_2, L_9, #[MP]]: ¬¬¬A↔¬A$.
+
+== Theorem 2.4.5.
+
+a) $[L_1, L_2, L_9, #[MP]]: ¬¬¬A↔¬A$.
+b) $[L_1, L_2, L_6, L_7, L_9, #[MP]]: ¬¬( A∨¬A)$. What does it mean? This is a “weak
+  form”  of  the  *Law  of  Excluded  Middle*  that  can  be  proved
+  constructively. The formula $¬¬( A∨¬A)$ can be proved in the constructive logic,
+  but $A∨¬A$ can't – as we will see in Section 2.8.
+
+== Theorem 2.4.9.
+
++ $[L_1, L_2, L_8, L_9, #[MP]]: ¬A∨¬B→¬( A∧B)$ . It's the constructive half of the
+  so-called *First de Morgan Law*. What does it mean?
++ $[L_1-L_9, #[MP]]: ¬(A∨B)↔¬A∧¬B$. It's the so-called *Second de Morgan Law*.
+
+== Theorem 2.5.1.
+
++ $[L_1, L_8, L_10, #[MP]]: ¬A∨B→( A→B)$.
++ $[L_1, L_2, L_6, #[MP]]: A∨B→(¬A→B) ├¬A→(A→B)$ .  It means that the “natural”
+  rule $A∨B ;¬ A ├ B$ implies $L_10$!
+
+
+== Theorem 2.5.2. 
+
+$[L_1-L_10, #[MP]]$:
+
++ $(¬¬A→¬¬B)→¬¬(A→B)$. It's the converse of Theorem 2.4.7(b). Hence, $[L1-L10,
+  #[MP]]:├ ¬¬(A→B)↔(¬¬A→¬¬B)$.
++ $¬¬A→(¬A→A)$.  It's  the  converse  of  Theorem  2.4.6(a).  Hence, [L1-L10,
+  #[MP]]: $¬¬A↔(¬A→A)$. 
++ $A∨¬ A→(¬¬A→A)$ . 
++ $¬¬(¬¬A→A)$. What does it mean? It’s a “weak” form of the Double Negations
+  Law – provable in constructive logic. 
+
+== Theorem 2.6.1. (Double Negation Law)
+
+$[L_1, L_2, L_8, L_10, L_11, #[MP]]: ¬¬A → A$. Hence, $[L_1-L_11, #[MP]]: ¬¬A ↔
+A$.
+
+== Theorem 2.6.2.
+
+$[L_8, L_11, #[MP]]: A→B, ¬A→B├ B$. Or, by Deduction Theorem 1, $[L_1, L_2, L_8,
+L_11, #[MP]]: (A→B)→((¬A→B)→B)$.
+
+
+== Theorem 2.6.3.
+
+$[L_1-L_11, #[MP]]: (¬B→¬A)→(A→B)$. Hence, $[L_1-L_11, #[MP]]: (A→B) ↔ (¬B→¬A)$.
+
+
+== Theorem 2.6.3. 
+
+_(another one with the same number of because numbering error (it seems like it))_
+
+$[L_1-L_9, L_11, #[MP]]: ˫ ¬(A∧B)→¬A∨¬B$ . Hence, $[L_1-L_9, L_11, MP]: ˫
+¬(A∧B)↔¬A∨¬B$ .
+
+
+== Theorem 2.6.4.
+
+$[L_1-L_8, L_11, MP]: (A→B)→¬ A∨B $. Hence, (I-elimination) $[L_1-L_11, #[MP]]:
+(A→B)↔¬ A∨B$.
+
+
+== Theorem 2.6.5.
+
+$[L_1-L_11, MP]: ¬(A→B)→A∧¬B $. 
+
+== Theorem 2.7.1 (Glivenko's Theorem).
+
+$[L_1-L_11, #[MP]]:├ A$ if and only if $[L1-L10, #[MP]]:├ ¬¬A$.
+
+
+== Theorem 2.8.1.
+
+The axiom $L_9$: $(A→B)→((A→¬B)→¬A)$ can be proved in $[L_1, L_2, L_8, L_10,
+L_11, #[MP]]$.
+
+== Replacement Theorem 1
+
+Let us consider three formulas: $B$, $B'$, $C$, where $B$ is a sub-formula of
+$C$, and $o(B)$ is a propositional occurrence of $B$ in $C$. Let us denote by
+$C'$ the formula obtained from $C$ by replacing $o(B)$ by $B'$. Then, in the
+minimal logic,
+
+$[L_1-L_9, #[MP]]: B↔B'├ C↔C'$.
+
+== Replacement Theorem 2
+
+Let us consider three formulas: $B$, $B'$, $C$, where $B$ is a sub-formula of
+$C$, and $o(B)$ is any occurrence of $B$ in $C$. Let us denote by $C'$ the
+formula obtained from $C$ by replacing $o(B)$ by B'. Then, in the minimal
+logic,
+
+$[L_1-L_9, L_12-L_15, #[MP], #[Gen]]: B↔B'├ C↔C'$.
+
+
+== Theorem 3.1.1.
+
+$[L_1, L_2, L_12, L_13, #[MP]]: forall x B(x) arrow exists x B(x)$ . What does it
+mean? It prohibits "empty domains".
+
+
+Theorem 3.1.2.
+
++ [L1, L2, L12, L14, MP, Gen]: ∀x(B→C)→(∀x B→∀xC).
++ [L1, L2, L12-L15, MP, Gen]: ∀x(B→C)→(∃z(x+z+1=y).x B→∃z(x+z+1=y).xC).
+
+
+== Theorems 3.1.3.
+
+If F is any formula, then:
+
++ (U-introduction) [Gen]: F(x) ├∀x F(x) .
++ (U-elimination)  [L12, MP, Gen]: ∀x F(x) ├F(x) . What does it mean?
++ (E-introduction)  [L13, MP, Gen]: F(x) ├∃z(x+z+1=y).x F(x) . What does it mean?
+
+
+== Theorems 3.1.4. 
+
+If F is any formula, and G is a formula that does not contain free occurrences of x, then:
+
++ (U2-introduction) [L14, MP, Gen] G →F (x) ├G →∀x F (x) . What does it mean?
++ (E2-introduction) [L15, MP, Gen]: F (x)→G ├∃z(x+z+1=y).x F (x)→G . What does it mean?
+
+== Theorem 3.1.5.
+
++ [L1, L2, L5, L12, L14, MP, Gen]: $forall x forall y B(x,y) ↔ forall y forall x B(x,y)$
++ [L1, L2, L5, L13, L15, MP, Gen]: $exists x exists y B(x,y) ↔ exists y exists x B(x,y)$.
++ [L1, L2, L12-L15, MP, Gen]: $exists x forall y B(x,y) ↔ forall y exists x B(x,y)$.
+
+
+Theorem 3.1.6. If the formula B does not contain free occurrences of x, then
+[L1-L2,  L12-L15,  MP,  Gen]: (∀x B)↔B;(∃z(x+z+1=y).x B)↔B ,  i.e.,  quantifiers
+∀x ;∃z(x+z+1=y). x can be dropped or introduced as needed.
+
+Theorem 3.2.1. In the classical logic,
+ [L1-L15, MP, Gen]:  ¬
+x¬B 
+∀
+↔ xB.
+
+
+== Theorem 3.3.1. 
+
++ [L1-L5, L12, L14, MP, Gen]: ∀x(B∧C)↔∀x B∧∀xC .
++ [L1, L2, L6-L8, L12, L14, MP, Gen]: ├∀x B∨∀xC →∀x(B∨C) . The converse  formula ∀x(B∨C)→∀x B∨∀xC cannot  be  true.  Explain, why.
+
+
+== Theorem 3.3.2.
+
+a) [L1-L8, L12-L15, MP, Gen]: ∃z(x+z+1=y).x(B∨C)↔∃z(x+z+1=y). x B∨∃z(x+z+1=y).xC .
+b) [L1-L5, L13-L15, MP, Gen]: ∃z(x+z+1=y).x(B∧C)→∃z(x+z+1=y). x B∧∃z(x+z+1=y).xC . The converse implication ∃z(x+z+1=y).x B∧∃z(x+z+1=y). xC →∃z(x+z+1=y). x(B∧C) cannot be true. Explain, why. Exercise 3.3.3. a) Prove (a→) of Theorem 3.3.2. (Hint: start by assuming B∨C , apply D-elimination, etc., and finish by E2-introduction.)
+
+= Three-valued logic
+
+This is a general scheme (page 74) to define a three valued logic.
+
+For example, let us consider a kind of "three-valued logic", where 0 means
+"false", 1 – "unknown" (or NULL – in terms of SQL), and 2 means "true".
+Then  it  would  be  natural  to  define  “truth  values”  of  conjunction  and
+disjunction as
+
+$A∧B=min ( A, B)$ ;
+
+$A∨B=max (A , B)$ .
+
+But how should we define “truth values” of implication and negation?
+
+#table(
+  columns: 5,
+  [$A$], [$B$], [$A∧B$], [$A∨B$], [$A→B$],
+  [$0$], [$0$], [$0$], [$0$], [$i_1$],
+  [$0$], [$1$], [$0$], [$1$], [$i_2$],
+  [$0$], [$2$], [$0$], [$2$], [$i_3$],
+  [$1$], [$0$], [$0$], [$1$], [$i_4$],
+  [$1$], [$1$], [$1$], [$1$], [$i_5$],
+  [$1$], [$2$], [$1$], [$2$], [$i_6$],
+  [$2$], [$0$], [$0$], [$2$], [$i_7$],
+  [$2$], [$1$], [$1$], [$2$], [$i_8$],
+  [$2$], [$2$], [$2$], [$2$], [$i_9$],
+)
+
+#table(
+  columns: 2,
+  [$A$], [¬$A$],
+  [$0$], [$i_10$],
+  [$1$], [$i_11$],
+  [$2$], [$i_12$],
+)
+
+= Model interpreation
+
+== Interpretation of a language
+
+=== The language-specific part
+
+Let L be a predicate language containing:
+
+- (a possibly empty) set of object constants $c_1, dots, c_k, dots $;
+- (a possibly empty) set of function constants $f_1, dots, f_m, dots,$;
+- (a non empty) set of  predicate constants $p_1, ..., p_n, ...$.
+
+An interpretation $J$ of the language $L$ consists of the following two
+entities (a set and a mapping):
+
++ A non-empty finite or infinite set DJ – the domain of interpretation (it will
+  serve first of all as the range of object variables). (For infinite domains, set
+  theory comes in here.)
++ A mapping intJ that assigns: 
+  - to each object constant $c_i$ – a member $#[int]_J (c_i)$ of the domain
+    $D_J$ [contstant corresponds to an object from domain];
+  - to each function constant $f_i$ – a function $#[int]_J (f_i)$ from $D_J times dots 
+    times D_J$ into $D_J$ [],
+  - to each predicate constant $p_i$ – a predicate $#[int]_J (p_i)$ on $D_J$.
+
+Having an interpretation $J$ of the language $L$, we can define the notion of
+*true formulas* (more precisely − the notion of formulas that are true under
+the interpretation $J$).
+
+*Example.* The above interpretation of the “language about people” put in the
+terms of the general definition:  
+
+
++ $D = {#[br], #[jo], #[pa], #[pe]}$.
++ $#[int]_J (#[Britney])=#[br], #[int]_J (#[John])=#[jo], #[int]_J (#[Paris])=#[pa],
+  #[int]_J (#[Peter])=#[pe]$.
++ $#[int]_J (#[Male]) = {#[jo], #[pe]}; #[int]_J (#[Female]) = {#[br], #[pa]}$.
++ $#[int]_J (#[Mother]) = {(#[pa], #[br]), (#[pa], #[jo])}; #[int]_J (#[Father]) =
+  {(#[pe], #[jo]), (#[pe], #[br])}$.
++ $#[int]_J (#[Married]) = {(#[pa], #[pe]), (#[pe], #[pa])}$.
++ $#[int]_J (=) = {(#[br], #[br]), (#[jo], #[jo]), (#[pa], #[pa]), (#[pe],
+  #[pe])}$.
+
+=== Interpretations of languages − the standard common part 
+
+Finally, we define the notion of *true formulas* of the language $L$ under the
+interpretation $J$ (of course, for a fixed combination of values of their free
+variables – if any):
+
++ Truth-values of the formulas: $¬B , B∧C , B∨C , B →C$ [those are not
+  examples] must be computed. This is done with the truth-values of $B$ and $C$
+  by using the well-known classical truth tables (see Section 4.2).
+
++ The formula $∀x B$ is true under $J$ if and only if $B(c)$ is true under $J$
+  for all members $c$ of the domain $D_J$.
+
++ The formula $∃x B$ is true under $J$ if and only if there is a member c of the
+  domain $D_J$ such that $B(c)$ is true under $J$. 
+
+*Example.* In first order arithmetic, the formula 
+
+$
+y((x= y+ y)∨( x=y+ y+1))
+$
+
+is intended to say that "x is even or odd". Under the standard interpretation S
+of arithmetic, this formula is true for all values of its free variable x.
+
+Similarly, $∀x ∀y(x+ y=y+x)$ is  a  closed  formula  that  is  true  under
+this interpretation. The notion “a closed formula F is true under the
+interpretation J” is now precisely defined. 
+
+
+*Important − non-constructivity!* It may seem that, under an interpretation,
+any closed formula is "either true or false". However, note that, for an infinite
+domain  DJ,  the  notion  of  "true  formulas  under  J"  is  extremely  non-
+constructive.
+
+=== Example of building of an interpretation
+
+In Section 1.2, in our "language about people" we used four names of people
+(Britney, John, Paris, Peter) as object constants and the following predicate
+constants:
+
++ $#[Male] (x)$ − means "x is a male person"; 
++ $#[Female] (x)$ − means "x is a female person";
++ $#[Mother] (x, y)$ − means "x is mother of y";
++ $#[Father] (x, y)$ − means "x is father of y";
++ $#[Married] (x, y)$ − means "x and y are married";
++ $x=y$ − means "x and y are the same person".
+
+Now, let us consider the following interpretation of the language – a specific
+“small four person world”:
+
+The domain of interpretation – and the range of variables – is: $D = {#[br],
+#[jo], #[pa], #[pe]}$ (no people, four character strings only!).
+
+Interpretations of predicate constants are defined by the following truth
+tables:
+
+#table(
+  columns: 3,
+  [x], [Male(x)], [Female(x)],
+  [br], [false], [true],
+  [jo], [true], [false],
+  [pa], [false], [true],
+  [pe], [true], [false],
+)
+
+#table(
+  columns: 6,
+  [x], [y], [Father(x,y)], [Mother(x,y)], [Married(x,y)], [x=y],
+  [br], [br], [false], [false], [false], [true],
+  [br], [jo], [false], [false], [false], [false],
+  [br], [pa], [false], [false], [false], [false],
+  [br], [pe], [false], [false], [false], [false],
+  [jo], [br], [false], [false], [false], [false],
+  [jo], [jo], [false], [false], [false], [true],
+  [jo], [pa], [false], [false], [false], [false],
+  [jo], [pe], [false], [false], [false], [false],
+  [pa], [br], [false], [true], [false], [false],
+  [pa], [jo], [false], [true], [false], [false],
+  [pa], [pa], [false], [false], [false], [true],
+  [pa], [pe], [false], [false], [true], [false],
+  [pe], [br], [true], [false], [false], [false],
+  [pe], [jo], [true], [false], [false], [false],
+  [pe], [pa], [false], [false], [true], [false],
+  [pe], [pe], [false], [false], [false], [true],
+)
+
+== Three kinds of formulas
+
+If  one  explores  some  formula  F  of  the  language  L  under  various
+interpretations, then three situations are possible:
+
++ $F$ is true in all interpretations of the language $L$. Formulas of this kind are
+  called *logically valid formulas* (LVF, Latv. *LVD*).
+
++ $F$  is  true  in  some interpretations  of  $L$,  and  false  − in  some other
+  interpretations of $L$.
+
++ F is  false in all interpretations of L Formulas of this kind are called
+  *unsatisfiable formulas* (Latv. *neizpildāmas funkcijas*).
+
+Formulas that are "not unsatisfiable" (formulas of classes (a) and (b)) are
+called, of course, satisfiable formulas: a formula is satisfiable, if it is
+true in at least one interpretation [*satisfiable functions* (Latv. *izpildāmas
+funkcijas*)].
+
+
+=== Prooving an F is LVF (Latv. LVD)
+
+First, we should learn to prove that some formula is (if really is!) logically
+valid. Easiest way to do it by reasoning from the opposite: suppose that exists
+such interpretation J, where formula is false, and derive a contradiction from
+this. Then this will mean that formula is true in all interpretations, and so
+logically valid. Check pages 125-126 of the book for example of such proof
+(there is proven that axiom L12 is true in all interpretations). Definitely
+check it, because in such way you will need to solve tasks in homeworks and
+tests.
+
+=== Prooving an F is satisfiable but NOT LVF 
+
+== Gödel's Completeness Theorem
+
+*Theorem 4.3.1.* In classical predicate logic $[L_1−L_15,#[MP],#[Gen]]$ all
+logically valid formulas can be derived.
+
+*Theorem 4.3.3.* All formulas that can be derived in classical predicate logic
+$[L_1−L_15,#[MP],#[Gen]]$ are logically valid. In this logic it is not possible
+to derive contradictions, it is consistent.