Sab 24 Agosto, 16:08:48 - 2019

Autore Topic: Costanti nei tableau predicativi  (Letto 1240 volte)

0 Utenti e 1 Visitatore stanno visualizzando questo topic.

Offline Dymios

  • Webmaster
  • Administrator
  • Ricercatore
  • *******
  • Post: 455
  • FeedBack: +41/-6
    • Mostra profilo
    • Dymios Personal Pages
Costanti nei tableau predicativi
« il: Sab 24 Novembre, 17:40:28 - 2007 »
Ciao,
nello sviluppo di un tableau predicativo mi trovo con 2 rami fatti così:

P(v_3), \neg P(c_3), \neg Q(c_4)  //  Q(v_3), \neg P(c_3), \neg Q(c_4)

ora, il ramo sx chiude mettendo c_3 / v_3, mentre nel ramo dx re-istanzio la \gamma-regola dalla quale proveniva Q(v_3) e ottengo:

P(v_4) \vee Q(v_4) che si divide in 2 rami:

P(v_4)  //  Q(v_4)

questo ramo dx chiude mettendo c_4 / v_4, ma nel ramo sx come devo fare?
Posso aggiungere un'altra costante per farlo chiudere o rimane aperto?  :-\
.:: Dymios ::.   -   WebMaster di SoloIngegneria - Minisumo.net

Offline otacon7b

  • Direttore di Dipartimento
  • ***
  • Post: 1218
  • FeedBack: +55/-723
  • -.-
    • Mostra profilo
Re: Costanti nei tableau predicativi
« Risposta #1 il: Sab 24 Novembre, 18:00:58 - 2007 »
Dimios se leggo bene in P(v4) hai una v4 quindi avevi un per ogni a  generare quel v4 in questo caso puoi sostituire v4 a c3 e farlo chiudere con not P(c3), almeno penso.
http://www.youtube.com/watch?v=oD0p7a3pPFQ
"Il signor Medvedev mi ha sorriso e mi ha detto di portargli le ostriche e lo champagne. Poi ha autografato il menu per mio figlio che quando sarà grande se lo ritroverà e potrà andarne fiero. È un russo molto potente, vero?" Tino Ruta, oste del Bistrot de l'Abbe di Cervinia (Ap Com, 25 luglio)

Offline Dymios

  • Webmaster
  • Administrator
  • Ricercatore
  • *******
  • Post: 455
  • FeedBack: +41/-6
    • Mostra profilo
    • Dymios Personal Pages
Re: Costanti nei tableau predicativi
« Risposta #2 il: Dom 25 Novembre, 15:22:20 - 2007 »
Quindi una costante può essere sostituita a più variabili libere...
In quest'altro tableau invece la situazione è diversa:

\neg (\forall x(P(x) \Leftrightarrow Q(x)) \rightarrow (\exists x P(x) \Leftrightarrow \exists x Q(x)))

\forall x(P(x) \Leftrightarrow Q(x)),\ \neg (\exists x P(x) \Leftrightarrow \exists x Q(x))

P(d_1) \Leftrightarrow Q(d_1)
\neg \exists x P(x),\ \exists x Q(x)                            \exists x P(x),\ \neg \exists x Q(x)
\neg P(d_2),\ Q(c_1)                                     P(c_2),\ \neg Q(d_3)
P(d_1),\ Q(d_1) // \neg P(d_1),\ \neg Q(d_1)         P(d_1),\ Q(d_1) // \neg P(d_1),\ \neg Q(d_1)
                                                                       **                                   **

Quei due rami chiudono con c_1/d_1 e c_2/d_1, ma gli altri due??
Posso dire d2 = d1 e d3 = d1 in qualche modo?? Forse facendo c_1/d_2 in modo tale che, induttivamente, siccome c1 = d1 e c1 = d2 allora d1 = d2??

P.S. il tableau deve chiudere.

.:: Dymios ::.   -   WebMaster di SoloIngegneria - Minisumo.net