TEORIJA GUSTIH UREDJENIH ABELOVIH GRUPA BEZ KRAJNJIH TACAKA
------------------------------------------------------------

* Jednakosna teorija (tj. signatura sadrzi =, a ogranicavamo se
  samo na normalne modele).
* Pored jednakosti, signatura sadrzi 0, +, -, <.
* Modeli teorije su sve strukture koje zadovoljavaju sledece aksiome:
  (Ax)(Ay)(Az) ( (x+y)+z = x + (y+z) ) [asocijativnost]
  (Ax) (x + 0 = 0 + x = x) [0 je neutral]
  (Ax) (x + (-x) = (-x) + x = 0)  [- je inverzni element]
  (Ax)(Ay) (x + y = y + x) [komutativnost]
  (Ax) (~(x < x)) [antirefleksivnost]
  (Ax)(Ay)(Az) (x < y /\ y < z => x < z) [tranzitivnost]
  (Ax)(Ay) (x < y \/ y < x \/ x = y) [totalni poredak]
  (Ax)(Ay)(Az) ( x < y => x + z < y + z) [saglasnost sa sabiranjem]
  (Ax)(Ay)(x < y => (Ez)(x < z /\ z < y)) [gusta grupa]
  (Ax)(Ey)(y < x) [ne postoji najmanji element]
  (Ax)(Ey)(x < y) [ne postoji najveci element]

* Ova teorija ima beskonacno mnogo modela. Neki od njih su (Q,+,<) kao
  i (R,+,<). Rezonovanje u ovoj teoriji omogucava rezonovanje u svim
  tim modelima.

* Teorija je potpuna: za svaku zatvorenu formulu A vazi da je ili A
  valjana u teoriji ili je njena negacija ~A valjana u teoriji (drugim
  recima, svaka zatvorena formula ima istu interpretaciju u svim
  modelima ove teorije: ili je svuda tacna ili je svuda netacna).
  Zbog toga se problem zadovoljivosti u ovoj teoriji svodi na problem
  valjanosti, jer je formula valjana u teoriji akko je zadovoljiva u
  njoj.

* Teorija je odluciva: postoji procedura odlucivanja koja za svaku
  zatvorenu formulu A odlucuje da li je A valjana (tj. zadovoljiva)
  u teoriji ili nije. Jedna takva procedura je Furije-Motckinova
  procedura. 


PRIMERI:

Dokazati da je data formula teorema teorije gustih uredjenih Abelovih grupa
bez krajnjih tacaka:

(Ax)(Ay)(Az)(2x < 3y /\ 3x < 2y /\ 7y < 5z ==> 14x < 10z)

RESENJE:

(Ax)(Ay)~(Ez)~(2x < 3y /\ 3x < 2y /\ 7y < 5z ==> 14x < 10z)

(Ax)(Ay)~(Ez)(2x < 3y /\ 3x < 2y /\ 7y < 5z /\ ((10z < 14x) \/ 14x = 10z))

(Ax)(Ay)~(Ez)((2x < 3y /\ 3x < 2y /\ 7y < 5z /\ 10z < 14x) \/ 
              (2x < 3y /\ 3x < 2y /\ 7y < 5z /\ 14x = 10z))

(Ax)(Ay)~((Ez)(2x < 3y /\ 3x < 2y /\ 7y < 5z /\ 10z < 14x) \/ 
          (Ez)(2x < 3y /\ 3x < 2y /\ 7y < 5z /\ 14x = 10z))

(Ax)(Ay)~((2x < 3y /\ 3x < 2y /\ (Ez)(7y < 5z /\ 10z < 14x)) \/ 
          (2x < 3y /\ 3x < 2y /\ (Ez)(7y < 5z /\ 14x = 10z)))

(Ax)(Ay)~((2x < 3y /\ 3x < 2y /\ (Ez)(14y < 14x)) \/ 
          (2x < 3y /\ 3x < 2y /\ (Ez)(14y < 14x)))

(Ax)(Ay)~((2x < 3y /\ 3x < 2y /\ 14y < 14x) \/ 
          (2x < 3y /\ 3x < 2y /\ 14y < 14x))

(Ax)(Ay)~(2x < 3y /\ 3x < 2y /\ y < x)

(Ax)~(Ey)~~(2x < 3y /\ 3x < 2y /\ y < x)

(Ax)~(Ey)(2x < 3y /\ 3x < 2y /\ y < x)

(Ax)~(Ey)(2x < 3x /\ 3x < 2x)

(Ax)~(2x < 3x /\ 3x < 2x)

~(Ex)~~(2x < 3x /\ 3x < 2x)

~(Ex)(2x < 3x /\ 3x < 2x)

~(Ex)(0 < x /\ x < 0)

~(Ex)(0 < 0)

~ (0 < 0)

True




Dokazati da je data formula teorema teorije gustih uredjenih Abelovih grupa
bez krajnjih tacaka:

(Ax)(Ay)(Az)(Au)(x < y /\ x + y = 2z /\ y - x = u) ==>  z + u > y)

RESENJE

(Ax)(Ay)(Az)(Au)(x < y /\ x + y = 2z /\ y - x = u) ==>  y < z + u)

(Ax)(Ay)(Az)~(Eu)(x < y /\ x + y = 2z /\ y - x = u /\  ~(y < z + u))

(Ax)(Ay)(Az)~(Eu)(x < y /\ x + y = 2z /\ y - x = u /\ (z + u < y \/ z + u = y))

(Ax)(Ay)(Az)~((Eu)(x < y /\ x + y = 2z /\ y - x = u /\ z + u < y)  \/
              (Eu)(x < y /\ x + y = 2z /\ y - x = u /\ z + u = y))

(Ax)(Ay)(Az)~((Eu)(x < y /\ x + y = 2z /\ z - x < 0)  \/
              (Eu)(x < y /\ x + y = 2z /\ z - x = 0))

(Ax)(Ay)(Az)~((x < y /\ x + y = 2z /\ z - x < 0)  \/
              (x < y /\ x + y = 2z /\ z - x = 0))

(Ax)(Ay)~(Ez)~~((x < y /\ x + y = 2z /\ z - x < 0)  \/
                (x < y /\ x + y = 2z /\ z - x = 0))

(Ax)(Ay)~((Ez)(x < y /\ x + y = 2z /\ z < x)  \/
          (Ez)(x < y /\ x + y = 2z /\ z = x))

(Ax)(Ay)~((Ez)(x < y /\ x + y < 2x)  \/
          (Ez)(x < y /\ x + y = 2x))

(Ax)(Ay)~((Ez)(x < y /\ y < x)  \/
          (Ez)(x < y /\ y = x))

(Ax)(Ay)~((x < y /\ y < x)  \/
          (x < y /\ y = x))

(Ax)~(Ey)~~((x < y /\ y < x)  \/
            (x < y /\ y = x))

(Ax)~((Ey)(x < y /\ y < x)  \/
      (Ey)(x < y /\ y = x))

(Ax)~((Ey)(x + y < y + x)  \/
      (Ey)(x < x))

(Ax)~((Ey)(x < x)  \/
      (Ey)(x < x))

(Ax)~((x < x)  \/
      (x < x))

~(Ex)~~((x < x)  \/
        (x < x))

~((Ex)(x < x)  \/
  (Ex)(x < x))


~((Ex)(0 < 0)  \/
  (Ex)(0 < 0))

~ (0 < 0 \/ 0 < 0)

~ (0 < 0)

~ False

True

Dokazati da je data formula teorema teorije gustih uredjenih Abelovih grupa
bez krajnjih tacaka:

(Ax)(Ay)(Az)(Au)(x < 2y /\ x + 2y = z /\ y - z > u) ==> 5y - 2z > u)  

RESENJE:

(Ax)(Ay)(Az)(Au)(x < 2y /\ x + 2y = z /\ u < y - z) ==> u < 5y - 2z)  

(Ax)(Ay)(Az)~(Eu)~(x < 2y /\ x + 2y = z /\ u < y - z) ==> u  < 5y - 2z)  

(Ax)(Ay)(Az)~(Eu)(x < 2y /\ x + 2y = z /\ u < y - z /\ 
                 (5y - 2z < u \/ 5y - 2z = u))  

(Ax)(Ay)(Az)~(Eu)((x < 2y /\ x + 2y = z /\ u < y - z /\  5y - 2z < u) \/ 
                  (x < 2y /\ x + 2y = z /\ u < y - z  /\  5y - 2z = u))  

(Ax)(Ay)(Az)~((Eu)(x < 2y /\ x + 2y = z /\ u < y - z  /\  5y - 2z < u) \/ 
              (Eu)(x < 2y /\ x + 2y = z /\ u < y - z /\  5y - 2z = u))  

(Ax)(Ay)(Az)~(((x < 2y /\ x + 2y = z) /\ (Eu)(u < y - z /\  5y - 2z < u))  \/ 
              ((x < 2y /\ x + 2y = z) /\ (Eu)(u < y - z /\  5y - 2z = u)))  

(Ax)(Ay)(Az)~(((x < 2y /\ x + 2y = z) /\ (Eu)(5y - 2z < y - z))  \/ 
              ((x < 2y /\ x + 2y = z) /\ (Eu)(5y - 2z < y - z)))  

(Ax)(Ay)(Az)~(((x < 2y /\ x + 2y = z) /\ (Eu)(4y < z))  \/ 
              ((x < 2y /\ x + 2y = z) /\ (Eu)(4y < z)))  


(Ax)(Ay)(Az)~(((x < 2y /\ x + 2y = z) /\ 4y < z)  \/ 
              ((x < 2y /\ x + 2y = z) /\ 4y < z))  

(Ax)(Ay)(Az)~(x < 2y /\ x + 2y = z /\ 4y < z)

(Ax)(Ay)~(Ez)~~(x < 2y /\ x + 2y = z /\ 4y < z)
(Ax)(Ay)~(Ez)(x < 2y /\ x + 2y = z /\ 4y < z)
(Ax)(Ay)~(x < 2y /\ (Ez)(x + 2y = z /\ 4y < z))
(Ax)(Ay)~(x < 2y /\ (Ez)(4y < x + 2y))
(Ax)(Ay)~(x < 2y /\ (Ez)(2y < x))
(Ax)(Ay)~(x < 2y /\ 2y < x)

(Ax)~(Ey)~~(x < 2y /\ 2y < x)
(Ax)~(Ey)(x < 2y /\ 2y < x)
(Ax)~(Ey)(x < x)
(Ax)~(x < x)

~(Ex)~~(x < x)
~(Ex)(x < x)
~(Ex)(0 < 0)
~(Ex)False
~False
True

Ispitati zadovoljivost sledece bazne formule u teoriji gustih uredjenih
Abelovih grupa bez krajnjih tacaka:

2a + 3b > c /\ a > b /\ c = 3a /\ b < 0 

Najpre normalizujemo (tj. zamenjujemo > sa <)
c < 2a + 3b /\ b < a /\ c = 3a /\ b < 0

Eliminisemo a:

3c < 6a + 9b /\ 3v < 3a  /\ c = 3a /\ b < 0

3c < 2c + 9b /\ 3b < c /\ b < 0 

c < 9b  /\ 3b < c /\ b < 0

Eliminisemo c:

3b < 9b /\ b < 0

0 < 6b /\ b < 0

Eliminisemo b:

0 < 6b /\ 6b < 0

0 < 0

False

Formula je nezadovoljiva!!

