Sugli alberi di derivazione

[marco2132k]

Ciao. Sto leggendo (qualcosa di simile a) https://link.springer.com/book/10.1007/978-981-13-7997-0. Ho in testa un'idea più o meno precisa di cosa sia una derivazione di un sequente, ma non vado d'accordo col modo sloppy di dirlo che è comune ai tre/quattro libri sull'argomento che ho consultato.

Come si potrebbe formulare più precisamente la Definizione 1.1 del libro citato?

Definition 1.1. A proof \( \mathsf P \) of a sequent \( \Gamma\implies \Delta \) is a finite tree-like figure defined inductively in the following way [...]:
[list=3]
[*:2hwkqvd5] every uppermost sequent in the proof \( \mathsf P \) is an initial sequent;[/*:m:2hwkqvd5]
[*:2hwkqvd5] every sequent except uppermost sequents in the proof \( \mathsf P \) is obtained by an application of any one of rules;[/*:m:2hwkqvd5]
[*:2hwkqvd5] \( \Gamma\implies \Delta \) is the single lowest sequent, which is called the end sequent of the proof \( \mathsf P \).[/*:m:2hwkqvd5][/list:o:2hwkqvd5]

[megas_archon]

Cosa ti sembra poco formale nella definizione uno punto uno? Ma soprattutto dov'è tusaicosa per tusaicosa aumma aumma ammicco ammicco?

[megas_archon]

Faccio uno speech-to-text dei vocali? E facciamo sto speech-to-text dei vocali.

"megas_archon su telegram, chiedendo foto zozze":la risposta è che dipende da cosa vuoi dimostrare ovviamente ossia se vuoi dimostrare delle cose di natura strutturale sulle proprietà grafteoretiche di questi alberi di derivazione questa è una classe di problemi che si addressa però con qualcosa che non ha niente a che fare con la deduzione naturale, perché sono delle proprietà grafteoretiche appunto -cosa ti ha detto quella definizione uno punto uno? Che un albero di derivazione è un albero la cui radice è la tesi di un asserto e le foglie sono gli assiomi. E ogni step dalle foglie alla radice consiste nell'applicazione di una regola, di una e una sola regola di derivazione. E in questa visione un albero di derivazione non è nient'altro che un elemento di una ehm un oggetto che è un sistema di riscrittura, che essenzialmente è un insieme con una certa relazione che è la "relazione di riscrittura" soggetta a delle regole a cui poi puoi chiedere delle robe -ti posso dire dove andare a leggere queste definizioni per formalizzare la nozione di albero di derivazione in maniera un po' più intrinseca e che non fa capo a deduzione naturale, non una roba di logica, una roba di algebra secondo me è semplicemente calcolo delle relazioni; quindi se vuoi una risposta di questo tipo eh ti dico tra un attimo appena ho un attimo dove andare a cercare. Se la tua domanda è ma io poi una dimostrazione all'interno del sistema deduttivo, come la faccio? Beh, la fai dipende, nel senso che eh dimmi una cosa che vuoi dimostrare, una proposizione che vuoi dimostrare, di solito tutti i testi, le note, i le dispense i libri che introducono la deduzione naturale o i gli alberi di derivazione lo fanno e subito dopo ti danno degli esempi che ti permettono di cincionare un po' con le definizioni e di capire che alla fine è un oggetto molto meccanico con cui operare e e non a caso meccanico proprio, è la diciamo meccanizzazione del processo di dimostrazione in una sequenza di operazioni che sono sempre le stesse pienamente codificate tutte formalizzate tutte pienamente sintattiche; a questo punto dipende anche dal linguaggio, dal sistema, la logica implicazionale avrà un suo sistema deduttivo, un suo sistema di riscrittura, la logica proposizionale classica, ne avrà un altro. Il poi ci sono tutte quelle cose, la logica la logica il sistema si chiama K LK non mi ricordo hanno dei nomi con delle degli acronimi e su questo ti posso segnalare un libretto breve di un giapponese tale ono cazzu qualcosa o no? Ehm che contiene diciamo tutto l'indispensabile. E e risponde un po' alla domanda, mi hai dato sta definizione e mo' che ci faccio? Cioè ci faccio le dimostrazioni. Sì, vabbè. Ma quali dimostrazioni? E come le eseguo? Cioè come qui dipende anche molto dal tuo gusto, io di libri che cercano di spiegarti sta roba, ne ho letti quindici e nessuno mi piace veramente tanto da dire ah e tutto qui dentro e questa è l'unica reference che terrò sempre nel mio cuore quindi diventa un po' la tua pazienza nel leggere la stessa cosa detta in quindici modi diversi per la quindicesima volta e ti sembrano tutti quindici modi diversi e poi in realtà scopri che in realtà stanno tutti dicendo la stessa fottuta cosa ora che ti ho risposto ci concentriamo per favore sulle cose importanti

I libri che dicevo: Kazzuimmano Ono https://link.springer.com/book/10.1007/ ... -13-7997-0
Sistemi di riscrittura: definiti nelle prime pagine di https://link.springer.com/book/10.1007/ ... 757-3661-8

[kaspar1]

La definizione non ti soddisfa in quale senso? La discussione qui sul forum è monca, perché evidentemente comunicate anche fuori di qui.