Matematické Fórum

m.bruna · 26. 01. 2013 22:28

Ahoj, mam trochu nejasnosti ohledne dukazu ve vyrokove logice. Byl bych moc vdecny za to, kdyby mi to nekdo osvetlil.

Dukaz:
Pro libovolne formule $\varphi,\psi$ plati $\{ \varphi, \neg \varphi \} \vdash \psi$
1) $\neg \varphi \rightarrow ( \neg \psi \rightarrow \neg \varphi)$ - Instance axiomu A1
...
Dukazy jsou mi jasne, tedy az na jednu vec. Obcas se v dukazu objevi podformule u ktere nevim, jak se k ni prislo. V tomto prikladu je to konkretne podformule tvaru $\neg \psi$ .
Instanciovani axiomu A1: $\varphi = \neg \varphi, \psi = \neg \psi$ . U podformule $\neg \varphi$ je to jasne, protoze ta je z predpokladu T. Kde se ale vzala negace u $\neg \psi$ ? Prednasejici to komentoval na prednasce stylem "tady dame negace psi, protoze to muzu, ...", ale uz nezduvodnil proc. Je mi jasne, ze si pravou stranu implikace upravil tak, aby ji mohl pozdeji pouzit pro ucely MP spolu s A3... Ale, ... proc to muzu?

-----------------------------------------------------------------------------------------------------------
Pro uplnost, zde jsou definice:

Logicky system $\mathcal{L} = (\rightarrow,\neg)$

Schema axiomu:
A1: $\varphi \rightarrow (\psi \rightarrow \varphi)$
A2: $(\varphi \rightarrow (\psi \rightarrow \xi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \xi))$
A3: $(\neg \varphi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \varphi)$
MP: Z $\varphi$ a $\varphi \rightarrow \psi$ odvod $\psi$

Bud T soubor formuli.
Dukaz formule $\psi$ z predpokladu T je konecna posloupnost formuli $\varphi_{1},\dots,\varphi_{k}$ , kde $\varphi_{k}$ je $\psi$ a pro kazde $\varphi_{i}$ , kde $1 \le i \le k$ , plati alespon jedna z nasledujicich podminek:
- $\varphi_{i}$ je prvek T;
- $\varphi_{i}$ je instanci jednoho ze schemat A1-A3;
- $\varphi_{i}$ vznikne aplikaci pravidla MP na formule $\varphi_{m}, \varphi_{n}$ pro vhodne $1 \le m,n < i$ .

Kondr · 26. 01. 2013 22:47

Pomohlo by, kdybyc první axiom byl
$\alpha \rightarrow (\beta \rightarrow \alpha)$
a místo "za psi dáme negaci psi" se řeklo "za alfa dáme negaci phi a za beta dáme negaci psi"? Tady se pouze dosazuje, v tomto kroku neřešíme, co je v předpokladech. Instance axiomu totiž vyplývá z libovolných předpokladů.

m.bruna

↑ Kondr:
Instance axiomu totiž vyplývá z libovolných předpokladů.

Dekuji mockrat, tohle mi nejak nedoslo - myslel jsem, ze se to instanciuje z predpokladu T a proto ty nejasnosti. Ted uz je mi vse jasne :-).

Matematické Fórum

#1 26. 01. 2013 22:28

Vyrokova logika - dukaz

#2 26. 01. 2013 22:47

Re: Vyrokova logika - dukaz

#3 27. 01. 2013 12:51 — Editoval m.bruna (27. 01. 2013 12:54)

Re: Vyrokova logika - dukaz

Zápatí