Fórum studentů MFF UK

Jo,
uz mi je to jasny, tohle jsem potreboval videt... :)

diky

1) 		    |-(A -> B) -> (A -> B)	   (v1)
2) A, A -> B |- B                        2x VoD

A co treba zahajit ten dukaz takto:

[code]
1) |-(A -> B) -> (A -> B) (v1)
2) A, A -> B |- B 2x VoD
[/code]

K dokazování máš k dispozici (ve VL) 3 axiomy a 1 odvozovací pravidlo
A začátek důkazu je vždycky jedno z toho. To, že to není axiom, ale to pravidlo, vůbec nevadí. Prostě to platí a můžeš to použít.

Mylim, ze v tomhle smyslu muzes povazovat MP za axiom. Ono si do leva muzes nahazet cokoliv a pak to z toho odvodit, ale vzdycky to bude za predpokladu, ze to prvni platilo. A tady to prvni (diky pravidlu MP) plati. Ale mozna se pletu;)

1) A, A->B |- B                              MP
2)          A |- (A->B) -> B               (1) VD
.....

Zdravim,
uz se to tu lehce nakouslo v jednom threadu - proc muze byt MP pouzit misto axiomu pri dokazovani? Ve skriptech takto zacina treba dukaz vety 6.

[code]
1) A, A->B |- B MP
2) A |- (A->B) -> B (1) VD
.....
[/code]

Pouzit to uz pak umim, ale nechapu proc to muzu udelat - MP preci neni tautologie, nic mi negarantuje, ze implikace A->B je true a tim padem, ze B je true. Pokud pripustim, ze A a A->B plati, pak to funguje, ale opet - proc to muzu pripustit? :) Pze podle tohohle bych si na levou stranu dokazovatka mohl nahazet vicemene cokoli, rici o tom, ze to proste plati a postupne to presouvat napravo, az dostanu to co chci.
Mozna jde pred tim udelat nejaky krok, ktery tam neni uveden a ktery zaruci, ze ta implikace plati a ja to v tom jen nevidim, ale zacina me to stvat, pze uz nad tim premyslim 2 dny a na nic kloudneho jsem zatim neprisel :) Muzete mi to nekdo pls zkusit nejak polopaticky vysvetlit?
Dekuji :)