Matematiska Institutionen Uppsala Universitet Anton Setzer

VT 2000 Övning 1

Övningar i Bevisteori

Anmärkning Problem 1, 2 (a), 3 kan lösas redan nu, de övriga rekommenderas lösa efter snitteliminationen ha bevisats i kursen.

Problem 1 (4 poäng) Formulera begreppen “bevissystem S” och “härledning i S” för någon version av Martin-Löf typ teori. Det finns olika system att skriver ner regler av typteorin, men bara ett system behövs formulera. Skissering av en typisk formulering av typ teori: Språket består av variabler och konstruktorer. Konstruktorer har en viss aritet. Uttryck är variabler, ((x)E) om E är ett uttryck och, om C är en konstruktor av aritet n, och E_{i} uttryck, så är också (CE_{1}, …, E_{n}) ett uttryck. Vi skriver till exempel λx.t för λ((x)t) och Σx : A.B för Σ(A, (x)B). Kontexter har formen x_{1} : A_{1}, …, x_{n} : A_{n}, varav x_{i} variabler, A_{i} uttryck. Kontexter betecknas med Γ, Δ. Omdömen (judgements) har formen Γ ⇒ θ, varav θ ≡ context eller θ ≡ A : B eller θ ≡ A = A′ : B eller θ ≡ B : Set eller θ ≡ B = B′ : Set, med A, A′, B, B′ uttryck. Regler härledar från vissa omdömen ett annat omdöme. Vi kan ersätta alla kontexter Γ_{i} som förekommer i en regel samtidigt av Δ, Γ_{i}, varvid Δ är en fixerad kontext. Här är Δ, Γ kontexten som består av konkatenationen av Δ och Γ. Men, om vi har ett axiom (regel utan prämisser) så behövs i så fall ytterliggare prämissen Δ ⇒ context. Det finns också några regler, som får inte utvidgas av en kontext Δ, till exempel ∅ ⇒ context.

Problem 2 (4 poäng) Visa:

(a) PL_{1} ⊢_{0}^{2·rk(A)} A, ¬A.

(b) If PL_{1} ⊢_{0}^{k} Γ, ∃x.A och Γ, ∃x.A innehåller ingen allkvantor, så finns termer t_{1}, …, t_{n} s.a. PL_{1} ⊢_{0}^{k} Γ, A_{x}(t_{1}), …, A_{x}(t_{n}).

Problem 3 (4 poäng) Låt S, 0 vara funktionssymbol av aritet 1, 0 respektive. Låt för n ∈ ℕ \underline{n} :=

\underbrace{S(⋯ S}_{n}(0) ⋯). Låt G := ¬∀x(F → F_{x}(Sx)), r := 2 · rk(F), k, m, n ∈ ℕ, k < 2^{n}.

Visa: PL_{1} ⊢_{0}^{r+2n} G, ¬F (\underline{m}), F (\underline{m + k}).

Problem 4 (4 poäng) Låt PL_{0} vara det kvantorfria fragmentet av PL_{1}. Visa:

(a) PL_{0} ⊢_{m}^{k} Γ, A_{0} ∧ A_{1} ⇒ PL_{0} ⊢_{m}^{k} Γ, A_{i} (i = 0, 1).

(b) PL_{0} ⊢_{m}^{k} Γ, A_{0} ∨ A_{1} ⇒ PL_{0} ⊢_{m}^{k} Γ, A_{0}, A_{1}.

(c) PL_{0} ⊢_{m+2}^{k} Γ ⇒ PL_{0} ⊢_{m+1}^{2k} Γ.