Naturlig deduktion, formulera och lösa sekvent från text.

Hej, försöker lösa denna uppgift:

"Om Stefan inte kommer på festen så kommer Kalle dit. Om Kalle kommer på festen
så kommer också Nils dit. Om både Kalle och Nils är på festen så kommer inte
Stefan dit. Alltså är antingen Kalle men inte Stefan på festen, eller så är Stefan men
inte Kalle på festen.

Formalisera resonemanget som en satslogisk sekvent genom att använda följande variabler:

s : Stefan är på festen
k : Kalle är på festen
n : Nils är på festen

Bevisa sedan sekventen med naturlig deduktion."

Tror sekventen ser ut såhär: -s -> (k -> n) , k ^ n -> s ⊢ s v k.

För att lösa den börjar jag med att skriva upp båda premisserna men efter det är jag lite vilse då jag inte vet hur jag ska bevisa sekventet. Har jag formaliserat resonemanget fel?

-s|=(-s)^k
k|=k^n
k^n|=k^n^(-s)

...
|=(k^(-s))\/(((-k)^s)

Typ så skulle jag skriva kanske?? Och försöka leka med deduktionsregler? Tycker det är lättare om man skiljer på antaganden och slutsatser och antecedent och consequent i implikationer. Oj insåg att min mobil missade ett tecken du skrivit, var kanske därför jag inte förstod vad du skrev.

Jag tror att sekventen ser ut så här: -s → k, k → n, k ^ n → -s ⊢ (k ^ -s) v (-k ^ s)

Sedan tror jag att lagen om uteslutna tredje krävs för beviset.
Antingen gäller s eller -s.
Antag -s. Då ger -s → k att k gäller. Alltså gäller k ^ -s och därmed (k ^ -s) v (-k ^ s).
Antag s. Antingen gäller nu k eller -k.
Antag -k. Då får vi direkt -k ^ s.
Antag k. Eftersom k → n gäller även n så k ^ n. Men k ^ n → -s vilket ger falsum. Från falsum kan vi dra godtycklig slutsats, t.ex. -k ^ s.
Fallanalysen över k har i båda fallen gett -k ^ s och därmed gäller -k ^ s oberoende av k (men under antagandet s).
Från -k ^ s kan vi dra slutsatsen (k ^ -s) v (-k ^ s) som alltså gäller oberoende av k.
Fallanalysen över s har i båda fallet gett (k ^ -s) v (-k ^ s) och därmed gäller (k ^ -s) v (-k ^ s) oberoende av s.
Sålunda gäller (k ^ -s) v (-k ^ s) under villkoren -s → k, k → n, k ^ n.

Tack så mycket för ditt svar! Jag hänger med upp till detta, vilken lag använder vi för att se att antingen k eller -k gäller?


EDIT: Är det fortfarande lagen om det uteslutna tredje?

Japp, det är uteslutna tredje som behöver blandas in.