Matematiska Institutionen Uppsala Universitet Anton Setzer

VT 2000 Övning 3

Övningar i Bevisteori

Övning 12 (4 poäng) Genomför i definition/teorem 6.4/6.5 definitionen och beviset av fallet I = R_{C}, C ≡ ∃x.A, A ∧ B, A ∨ B i detalj.

Övning 13 (4 poäng) Visa i detalj h^{∞} = tp(h)(h[i]^{∞})_{i∈|tp(h)|} om h = R_{C}(h_{0}, h_{1}) or h = E(h_{0}) (h_{0}, h_{1} Z^{∗}-härledningar av slutna sekvenser, C sluten; E skall vara definierad “med Rep-regeln”, dvs. som i Buchholz’ anteckningar).

Övning 14 (4 poäng) Låt (OT, ≺) vara ett ordinaltalbeteckningssystem (dvs. en primitiv rekursiv välordning) av ordningstyp α := ω^{β}, β > ω. Bestämmer några standardfunktioner på OT (som addition, multiplikation, exponentiation, inbäddning av naturliga tal eller uppdelning i komponenter) och några standardegenskaper av dem, så att det följer, om funktionerna är primitiv-rekursiva och standardegenskaperna kan bevisas i PRA:

(a) PRA + TI^{qf}(α) ⊢ TI^{Π_{1}^{0}}(α),

(b) PRA + TI^{qf}(α) ⊢ (Π_{1}^{0} − Ind).

(TI(α) menar transfinit induktion över (OT, ≺)). Visa att (a), (b) gäller.

Övning 15 (6 poäng) Definiera ett ordinaltalbeteckningssystem av ordningstyp Γ_{0}, dvs. en primitivrekursiv delmängd OT av ℕ, en primitiv rekursiv relation ≺ på OT och en funktion o : OT → Γ_{0} så att o är en ordningstrogen bijektion. Hänvisning:

• Definiera en mängd T av koder för uttryck av formen φ_{a_{1}}b_{1} + ⋯ + φ_{a_{n}}b_{n} och en linjär ordning på T.

• Gallra ut uttryck som inte är i normalform, dvs. med förekomst av φ_{a_{1}}b_{1}+ ⋯ + φ_{a_{n}}b_{n} med φ_{a_{i}}b_{i} ≺ φ_{a_{i+1}}b_{i+1} eller b_{i} = φ_{c}d med a_{i} ≺ c.

• Definiera o på T och visa ∀a, b ∈ OT(a ≺ b ↔ o(a) < o(b)).

• Visa o[OT] = Γ_{0}.

Övning 15 (4 poäng) Induktiv definition av X⃗-positiva formler i L_{0}[X⃗]:

• s ∈ X, s = t, ¬(s = t) är X⃗-positiva (s, t L_{0}-termer).

• Om A, B är X⃗-positiva, så också A ∧ B, A ∨ B, ∃x.A, ∀x.A. Visa för sekvenser Γ av X⃗-positiva slutna formler och slutna termer s:

(a) Z^{∞} ⊢_{0}^{α} Γ, s ∈ X ⇒ Z^{∞} ⊢_{0}^{α} Γ.

(b) Z^{∞} ⊢_{1}^{α} Γ ⇒ Z^{∞} ⊢_{0}^{α} Γ.