Logiche del primo ordine
La regola di $\forall$-formazione dice
$\Gamma, z \in D \vdash A(z) \implies \Gamma \vdash (\forall x \in D)A(x)$, con $z$ non libera nel dominio $D$. Poi Wikipedia dice
"Ciò significa che z non deve già comparire in qualche proposizione del sequente altrimenti si avrebbe un sistema inconsistente: asserire che, dato A per una certa variabile, valga A per tutti gli elementi del dominio è assolutamente folle."
Ok, ma non è quello che si sta facendo, quando si scrive $(\forall x \in D)A(x)$? Oppure $x$ ha qualche altra proprietà implicita?
$\Gamma, z \in D \vdash A(z) \implies \Gamma \vdash (\forall x \in D)A(x)$, con $z$ non libera nel dominio $D$. Poi Wikipedia dice
"Ciò significa che z non deve già comparire in qualche proposizione del sequente altrimenti si avrebbe un sistema inconsistente: asserire che, dato A per una certa variabile, valga A per tutti gli elementi del dominio è assolutamente folle."
Ok, ma non è quello che si sta facendo, quando si scrive $(\forall x \in D)A(x)$? Oppure $x$ ha qualche altra proprietà implicita?
Risposte
"TomSawyer":
modello numerabile di Peano e modello minimale di Peano sono la stessa cosa, vero?
Non so, non ho mai sentito la nozione di modello minimale dell'aritmetica. Mi servirebbe la definizione...
"TomSawyer":
Non ho ben capito cosa vuoi dire per "passare per la derivazione". Il contromodello di questo sequente è particolarmente semplice, ed è quello che differenzia LJ da LK.
Ti faccio un esempio su un'altra derivazione:
$not A -> not B |-- B -> A$
Se il sequente è derivabile in LJ, lo è per ogni A e per ogni B. Ponendo $B= not not A$ si ottiene
$not A -> not not not A |-- not not A -> A$
che non è derivabile in LJ.
Comunque mi sembra più semplice trovare un contromodello di Kripke
.
"jacopo":
La legge di Pierce dice che $(not A -> A) -> A$ vale per ogni A.
Una mia curiosità: quella proposta da wiki $((A -> B) -> A) -> A$ non è differente, giusto ?
Poni $B=_|_$ e diventa $((A \to _|_) \to A) \to A$, cioè $(\neg A \to A) \to A$.
"jacopo":
-Fornire una derivazione in LK
Io ho fatto così...
$A |-- A$
$not A, A |-- _|_$spac$A |-- A$
$not A |-- not A$space$not A, A |-- A$
$not A -> A, not A |-- A$
$(not A -> A )|-- A, not not A$
$(not A -> A) |-- A $
$|-- (not A -> A) -> A$
E' corretto?
Sì.
"jacopo":
Dimostrare che non è derivabile in LJ
Come lo dimostro ?
Costruisci un albero con due nodi ($x_0,x_1$), con $V(\neg A)=\emptyset$ e $V(A)=x_1$.
Ciao fields 
. Per dimostrare che due strutture differenti e minimali, $A$ e $B$, che soddisfano gli assiomi di Peano sono isomorfe, costruisco la seguente mappa ricorsiva: $f: A \to B$, con $f(0)=0'$ (essendo che sono strutture di Peano, sicuramente ognuna ha un elemento minimo, che denoto con $0$ e $0'$) e $f(S(a))=S(f(a))$ per ogni $a\in A$, con $S(*)$ la funzione successore.
Per dimostrare che è un isomorfismo, basta osservare che, se manda $a \in A$ in $b \in B$, allora preserva il successore, cioè che manda $S(a)$ in $S(b)$: $f(S(a))=S(f(a)) \implies f(S(a))=S(b)$.
E' abbastanza formale questa dimostrazione? O devo fare appello al teorema di ricorsione di Dedekind, per dire che questa mappa è unica etc?
PS: modello numerabile di Peano e modello minimale di Peano sono la stessa cosa, vero?
. Per dimostrare che due strutture differenti e minimali, $A$ e $B$, che soddisfano gli assiomi di Peano sono isomorfe, costruisco la seguente mappa ricorsiva: $f: A \to B$, con $f(0)=0'$ (essendo che sono strutture di Peano, sicuramente ognuna ha un elemento minimo, che denoto con $0$ e $0'$) e $f(S(a))=S(f(a))$ per ogni $a\in A$, con $S(*)$ la funzione successore.Per dimostrare che è un isomorfismo, basta osservare che, se manda $a \in A$ in $b \in B$, allora preserva il successore, cioè che manda $S(a)$ in $S(b)$: $f(S(a))=S(f(a)) \implies f(S(a))=S(b)$.
E' abbastanza formale questa dimostrazione? O devo fare appello al teorema di ricorsione di Dedekind, per dire che questa mappa è unica etc?
PS: modello numerabile di Peano e modello minimale di Peano sono la stessa cosa, vero?
Non ho ben capito cosa vuoi dire per "passare per la derivazione". Il contromodello di questo sequente è particolarmente semplice, ed è quello che differenzia LJ da LK.
"TomSawyer":
[quote="jacopo"]
L'esercizio chiedeva di fornire una derivazione in LJ, per cui non dovevo trovare un contromodello di Kripke...
Per dimostrare invece che un sequente non è derivabile in LJ, come devo procedere ?
Ti sei risposto da solo con la riga precedente
. Cioè, per dimostrare la non-validità in maniera formale, devi trovare un albero in cui non sia valido.[/quote]Giusto, una conseguenza del teorema di validità.
C'è un altro modo, ad esempio passare per la derivazione di un sequente palesemente non dimostrabile in LJ (ad esempio, $not not A -> A$) ? Non so se si è capito.
Non ci ha fregati no ](/datas/uploads/forum/emoji/eusa_wall.gif "Brick wall")
Anzi, a guardarlo sembra anche facile
Grazie infinite.
Posso approfittare della tua disponibilità (solo un altro po'
):
Una mia curiosità: quella proposta da wiki $((A -> B) -> A) -> A$ non è differente, giusto ?
Io ho fatto così...
$A |-- A$
$not A, A |-- _|_$spac$A |-- A$
$not A |-- not A$space$not A, A |-- A$
$not A -> A, not A |-- A$
$(not A -> A )|-- A, not not A$
$(not A -> A) |-- A $
$|-- (not A -> A) -> A$
E' corretto?
Come lo dimostro ?
Anzi, a guardarlo sembra anche facile
Grazie infinite.
Posso approfittare della tua disponibilità (solo un altro po'
):La legge di Pierce dice che $(not A -> A) -> A$ vale per ogni A.
Una mia curiosità: quella proposta da wiki $((A -> B) -> A) -> A$ non è differente, giusto ?
-Fornire una derivazione in LK
Io ho fatto così...
$A |-- A$
$not A, A |-- _|_$spac$A |-- A$
$not A |-- not A$space$not A, A |-- A$
$not A -> A, not A |-- A$
$(not A -> A )|-- A, not not A$
$(not A -> A) |-- A $
$|-- (not A -> A) -> A$
E' corretto?
Dimostrare che non è derivabile in LJ
Come lo dimostro ?
"jacopo":
L'esercizio chiedeva di fornire una derivazione in LJ, per cui non dovevo trovare un contromodello di Kripke...
Per dimostrare invece che un sequente non è derivabile in LJ, come devo procedere ?
Ti sei risposto da solo con la riga precedente
. Cioè, per dimostrare la non-validità in maniera formale, devi trovare un albero in cui non sia valido.
Il prof non vi ha fregati 
$B|--B$
$B, not not B|--B$
$B|-- (not not B->B)$
$not (not not B->B), B|--_|_$
$not (not not B->B)|--not B$
$not (not not B->B),not not B|--B$
$not (not not B->B)|--not not B->B $
$not (not not B->B),not (not not B->B)|--_|_$
$not (not not B->B)|--_|_$
$|-- not not (not not B->B)$
Figo, sembra un balletto
$B|--B$
$B, not not B|--B$
$B|-- (not not B->B)$
$not (not not B->B), B|--_|_$
$not (not not B->B)|--not B$
$not (not not B->B),not not B|--B$
$not (not not B->B)|--not not B->B $
$not (not not B->B),not (not not B->B)|--_|_$
$not (not not B->B)|--_|_$
$|-- not not (not not B->B)$
Figo, sembra un balletto
"jacopo":
Ma allora il prof ci ha fregati.
Durante il compito ci aveva detto che non era una derivazione banale, ma si riusciva a derivare in LJ.
Non credo che vi abbia fregati Più probabile che mi sbagli io... a dire il vero sono andato solo a intuito (mai fidarsi delle affermazioni non dimostrate! 
) Ci penso meglio.
"fields":
[quote="jacopo"]
$|-- not not (not not B -> B)$
Questo invece non è derivabile. Se richiesto, devi trovare un contromodello di Kripke.[/quote]
Ma allora il prof ci ha fregati.
Durante il compito ci aveva detto che non era una derivazione banale, ma si riusciva a derivare in LJ.
L'esercizio chiedeva di fornire una derivazione in LJ, per cui non dovevo trovare un contromodello di Kripke...
Per dimostrare invece che un sequente non è derivabile in LJ, come devo procedere ?
Grazie comunque per il tuo aiuto.
"jacopo":
$not A, A |-- B$spacespace$B, A |-- B$
$not A |-- A -> B$spacespace$B |-- A -> B
$not(A -> B), not A|-- _|_$spac$not(A -> B), B|-- _|_$
$not(A -> B)|-- not not A$space$not(A -> B)|-- not B$
spaces$not (A -> B)|-- not not A & not B$
Nella parte destra si arriva all'assioma tramite indebolimento, invece nella parte sinistra devo applicare la regola del falso, oppure c'è un altro modo ?
Ok, in alto a sinistra devi trasfomare $not A$ in $A to _|_$ e applicare la regola $to$
"jacopo":
$|-- not not (not not B -> B)$
Questo invece non è derivabile. Se richiesto, devi trovare un contromodello di Kripke.
Ciao a tutti,
non riesco a dare una derivazione in LJ di questi sequenti:
$|-- not not (not not B -> B)$
$not (A -> B)|-- not not A & not B$
Per quanto riguarda l'ultimo, non mi sembra un granchè difficile, infatti ovviamente avrei fatto in questo modo:
$not A, A |-- B$spacespace$B, A |-- B$
$not A |-- A -> B$spacespace$B |-- A -> B
$not(A -> B), not A|-- _|_$spac$not(A -> B), B|-- _|_$
$not(A -> B)|-- not not A$space$not(A -> B)|-- not B$
spaces$not (A -> B)|-- not not A & not B$
Nella parte destra si arriva all'assioma tramite indebolimento, invece nella parte sinistra devo applicare la regola del falso, oppure c'è un altro modo ?
non riesco a dare una derivazione in LJ di questi sequenti:
$|-- not not (not not B -> B)$
$not (A -> B)|-- not not A & not B$
Per quanto riguarda l'ultimo, non mi sembra un granchè difficile, infatti ovviamente avrei fatto in questo modo:
$not A, A |-- B$spacespace$B, A |-- B$
$not A |-- A -> B$spacespace$B |-- A -> B
$not(A -> B), not A|-- _|_$spac$not(A -> B), B|-- _|_$
$not(A -> B)|-- not not A$space$not(A -> B)|-- not B$
spaces$not (A -> B)|-- not not A & not B$
Nella parte destra si arriva all'assioma tramite indebolimento, invece nella parte sinistra devo applicare la regola del falso, oppure c'è un altro modo ?
Ok... grazie...
E' anche consultabile da internet...
http://books.google.it/books?id=TCIX3qi ... esult&cd=1
Se hai qualche altro link scrimelo pure!!!
E' anche consultabile da internet...
http://books.google.it/books?id=TCIX3qi ... esult&cd=1
Se hai qualche altro link scrimelo pure!!!
"maalla":
Mi puoi indicare un libro dove trovo le dimostrazioni (sperando poi di trovarlo in qualche biblioteca)...
Le dimostrazioni le trovi in molti libri di teoria degli insiemi. Comunque, io avevo consultato questo: "Basic set theory", Levy.
Mi puoi indicare un libro dove trovo le dimostrazioni (sperando poi di trovarlo in qualche biblioteca)...
...O me ne puoi scannerizzare le pagine ed inviarleme per e-mail???
Ths
...O me ne puoi scannerizzare le pagine ed inviarleme per e-mail???
Ths
"maalla":
Purtroppo nelle dispense che mi hai indicato ci sono sono gli enunciati... e non le dimostrazioni dei teoremi!!!
Be', ma li danno come esercizio!!
Vuol dire che nella dispensa c'è tutto quello che ti serve...Comunque, non saprei che altri link fornirti. Io quelle cose le ho lette su libri "cartacei".
Purtroppo nelle dispense che mi hai indicato ci sono sono gli enunciati... e non le dimostrazioni dei teoremi!!!
Su google sto cercando.. ma no trovo un granchè... per questo vi ho posto la domanda!!!
Grazie ancora
Su google sto cercando.. ma no trovo un granchè... per questo vi ho posto la domanda!!!
Grazie ancora
"maalla":
- Teorema di Hahn-Banach (con AS)
Esiste zio google, no?
Trovi parecchio..."maalla":
- Induzione su ordinali più ampi di w (teorema di Goodstein)
- Forma normale di Cantor (ordinali scritti in una certa base come per i naturali)
pag 55 della dispensa che ti ho già linkato per la forma normale di Cantor. Trovi anche l'induzione transfinita, lì nei pressi.
Salve... di nuovo!!!
Vi ringrazio dell'aiuto che mi avete dato e vi pongo un'altra domanda:
Avete un link d asegnalarmi o delle dispense da inviarmi su:
- Teorema di Hahn-Banach (con AS)
- Induzione su ordinali più ampi di w (teorema di Goodstein)
- Forma normale di Cantor (ordinali scritti in una certa base come per i naturali)
Grazie ancora!!!
Vi ringrazio dell'aiuto che mi avete dato e vi pongo un'altra domanda:
Avete un link d asegnalarmi o delle dispense da inviarmi su:
- Teorema di Hahn-Banach (con AS)
- Induzione su ordinali più ampi di w (teorema di Goodstein)
- Forma normale di Cantor (ordinali scritti in una certa base come per i naturali)
Grazie ancora!!!
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo