Teorie (Logica) Maietti PD

¬, ∀, ∃		∨, & 		→

Sia Tmon la teoria ottenuta estendendo LC= con la formalizzaione dei seguenti assiomi:
- Giacomo non va in montagna sse piove
Ax1: ⊢ (¬M(g) → P) & (P → ¬M(g))
- Pietro va in montagna se ci va Giacomo o non piove
Ax2: ⊢ M(g) v ¬P → M(p)
- Se Pietro non va in montagna allora Claudio e Giacomo ci vanno
Ax3: ⊢ ¬M(p) → M(c) & M(g)
- Se Claudio va in montagna, Pietro non ci va
Ax4: ⊢ M(c) → ¬M(p)
M(x) = x va in montagna
P = piove
c = Claudio, p = Pietro, g = Giacomo
Dedurre:
- Se non piove Giacomo va in montagna
Q1: ⊢ ¬P → M(g)
- Se non piove Pietro va in montagna
Q2: ⊢ ¬P → M(p)
- Pietro va in montagna
Q3: ⊢ M(p)
- Qualcuno non va in montagna
Q4: ⊢ ∃x ¬M(x)



Q1: ⊢ ¬P → M(g)
      ¬ax dx 2                                 ¬ax sx 2
¬P, P → ¬M(g) ⊢ ¬M(g), M(g)               ¬P, P → ¬M(g), P ⊢ M(g)
______________________________________________________________________ → -S
        ¬P, P → ¬M(g), ¬M(g) → P ⊢ M(g)
        ___________________________________ sc sx
        ¬P, ¬M(g) → P, P → ¬M(g) ⊢ M(g)
        ________________________________________ & -S
        ¬P, (¬M(g) → P) & (P → ¬M(g)) ⊢ M(g)
        ________________________________________ sc sx
⊢ Ax1   (¬M(g) → P) & (P → ¬M(g)), ¬P ⊢ M(g)
_______________________________________________ comp sx
¬P ⊢ M(g)
_____________ → -D
⊢ ¬P → M(g)


Q2: ⊢ ¬P → M(p)
      ax id
¬P ⊢ M(g), ¬P, M(p)
_____________________ v -D        ax id
¬P ⊢ M(g) v ¬P, M(p)         ¬P, M(p) ⊢ M(p)
_______________________________________________ → -S
          ¬P, M(g) v ¬P → M(p) ⊢ M(p)
         _______________________________ sc sx
⊢ Ax2     M(g) v ¬P → M(p), ¬P ⊢ M(p)
_______________________________________________ comp sx
¬P ⊢ M(p)
_____________ → -D
⊢ ¬P → M(p)


Q3: ⊢ M(p)
                  ax id
          M(c), M(g) ⊢ M(g), ¬P, M(p)
          ____________________________ & -S       ¬ax dx 2
          M(c) & M(g) ⊢ M(g), ¬P, M(p)       ⊢ ¬M(p), M(g), ¬P, M(p)
           __________________________________________________ → -S
⊢ Ax3      ¬M(p) → M(c) & M(g) ⊢ M(g), ¬P, M(p)
__________________________________________ comp sx
           ⊢ M(g), ¬P, M(p)
           __________________ v -D   ax id
           ⊢ M(g) v ¬P, M(p)        M(p) ⊢ M(p)
          _____________________________________ → -S
⊢ Ax2     M(g) v ¬P → M(p) ⊢ M(p)
_________________________________ comp sx
⊢ M(p)


Q4: ⊢ ∃x ¬M(x)
            ¬ax sx 1
⊢ Q3   M(p), ¬M(p) ⊢ ¬M(c)
_________________________ comp sx      ¬ax dx 1
          ¬M(p) ⊢ ¬M(c)              ⊢ M(c), ¬M(c)
          ________________________________________ → -S
⊢ Ax4     M(c) → ¬M(p) ⊢ ¬M(c)
________________________________ comp sx
⊢ ¬M(c)
___________ ∃ re
⊢ ∃x ¬M(x)




Sia Tam la teoria ottenuta estendendo LC= con la formalizzaione dei seguenti assiomi:
- Alcuni amici di Aldo non sono europei
Ax1: ⊢ ∃x (A(x,a) & ¬E(x))
- Tutti gli amici di Aldo sono europei o asiatici
Ax2: ⊢ ∀x (A(a, x) → E(x) v S(x))
- Marcel non è né europeo né asiatico
Ax3: ⊢ ¬E(m) & ¬S(m)
- Jean è amico di Aldo e non è asiatico
Ax4: ⊢ A(a,j) & ¬S(j)
A(x,y) = x è amico di x
E(x) = x è europeo
S(x) = x è asiatico
T(x) = x è triste
a = Aldo, j = Jean, m = Marcel
Mostrare una derivazione nella teoria indicata
- Marcel non è amico di Aldo
Q1: ⊢ ¬A(a,m)
- Jean è europeo
Q2: ⊢ E(j)
- Se nessuno fosse amico di Aldo, Aldo sarebbe triste
Q3: ⊢ ¬∃x A(a,x) → T(a)
- Non tutti gli amici di Aldo sono asiatici
Q4: ⊢ ∃x (A(x,a) & ¬S(x))
- Qualcuno ha amici
Q5: ⊢ ∃x ∃y A(x,y)



Q1: ⊢ ¬A(a,m)
    ¬ax sx 2                            ¬ax sx 2
¬E(m), ¬S(m), E(m) ⊢ ¬A(a,m)    ¬E(m), ¬S(m), S(m) ⊢ ¬A(a,m)
____________________________________________________________ v -S
        ¬E(m), ¬S(m), E(m) v S(m) ⊢ ¬A(a,m)
        ____________________________________ sc sx
        E(m) v S(m), ¬E(m), ¬S(m) ⊢ ¬A(a,m)
        ____________________________________ & -S
        E(m) v S(m), ¬E(m) & ¬S(m) ⊢ ¬A(a,m)
        ____________________________________ sc sx
⊢ Ax3   ¬E(m) & ¬S(m), E(m) v S(m) ⊢ ¬A(a,m)
__________________________________________ comp sx     ¬ax dx 1
          E(m) v S(m) ⊢ ¬A(a,m)                    ⊢ A(a, m), ¬A(a, m)
          ___________________________________________________________ → -S
          A(a, m) → E(m) v S(m) ⊢ ¬A(a,m)
          ____________________________________ ∀ re
⊢ Ax2     ∀x (A(a, x) → E(x) v S(x)) ⊢ ¬A(a,m)
______________________________________________ comp sx
⊢ ¬A(a,m)


Q2: ⊢ E(j)
                            ¬ax sx 2
                     A(a,j), ¬S(j), S(j) ⊢ E(j)
                    ____________________________ & -S                 ax id
              Ax4    A(a,j) & ¬S(j), S(j) ⊢ E(j)              A(a,j), ¬S(j) ⊢ A(a, j), E(j)
  ax id       _______________________ comp sx                 _____________________________ & -S
E(j) ⊢ E(j)      S(j) ⊢ E(j)                           Ax4    A(a,j) & ¬S(j) ⊢ A(a, j), E(j)
_____________________________  v -S                    _____________________________________ comp sx
           E(j) v S(j) ⊢ E(j)                             ⊢ A(a, j), E(j)
           _______________________________________________________________ → S
           A(a, j) → E(j) v S(j) ⊢ E(j)
           ____________________________________ ∀ re
⊢ Ax2      ∀x (A(a, x) → E(x) v S(x)) ⊢ E(j)
_______________________________________________
⊢ E(j)


Q3: ⊢ ¬∃x A(a,x) → T(a)
                  ax id
        A(a,j), ¬S(j) ⊢ A(a,j), T(a)
        ______________________________ & -S
        A(a,j) & ¬S(j) ⊢ A(a,j), T(a)
        ______________________________ ¬ -S
⊢Ax4    A(a,j) & ¬S(j), ¬A(a,j) ⊢ T(a)
_________________ comp sx
¬A(a,j) ⊢ T(a)
____________________ → ∃ re
¬∃x A(a,x) ⊢ T(a)
____________________ → -D
⊢ ¬∃x A(a,x) → T(a)


Q4: ⊢ ∃x (A(x,a) & ¬S(x))
     ax 4
⊢ A(a,j) & ¬S(j)
________________ ∃ re
⊢ ∃x (A(x,a) & ¬S(x))


Q5: ⊢ ∃x ∃y A(x,y)
                ax id
           A(a,j), ¬S(j) ⊢ A(j,a)
           ________________________ & -S
⊢ Ax 4     A(a,j) & ¬S(j) ⊢ A(j,a)
___________________________________ comp sx
⊢ A(j,a)
______________ ∃ re
⊢ ∃y A(j,y)
______________ ∃ re
⊢ ∃x ∃y A(x,y)