Københavns Universitet

Naturvidenskabelig embedseksamen, første del Matematik & Beregninger

Skriftlig eksamen 1. februar 2005

Sættet består af 3 opgaver, som vægtes ens. I tilfælde af fejl eller unøjagtigheder i opgaveteksten forventes det, at eksaminanderne selv præciserer besvarelsens forudsætninger. Alle sædvanlige hjælpemidler er tilladt. Opgavesættet besvares på separate ark, der udleveres af eksamenstilsynet. Besvarelsen kan formuleres på dansk eller engelsk eller en blanding heraf. Indskrivning med blyant er tilladt. Opgaveteksten kan deltagerne tage med sig.

Mathematics and Computation Exam February 1, 2005

I define [f(x, y) ≐ if(x = 0, y, f(x − 1, ¬y))]

For each use of [Tautology], draw the associated truth table.

Exercise 1. Prove one of the following:

[Mac lemma L05.1.1A: x ∈ N → ∀y∈B: f(x, y) ∈ B]

[Mac antilemma L05.1.1B: x ∈ N → ∀y∈B: f(x, y) ∈ B]

Exercise 2. Prove one of the following:

[Mac lemma L05.1.2A: x ∈ B → ∀y∈B: ((x ⇒ y) ⇒ (¬x ⇒ ¬y))] [Mac antilemma L05.1.2B: x ∈ B → ∀y∈B: ((x ⇒ y) ⇒ (¬x ⇒ ¬y))]

Exercise 3. Prove one of the following:

[Mac lemma L05.1.3A: x ∈ B → ∀y∈B: ((x ⇒ y) ⇒ (¬y ⇒ ¬x))] [Mac antilemma L05.1.3B: x ∈ B → ∀y∈B: ((x ⇒ y) ⇒ (¬y ⇒ ¬x))] Mathematics and Computation Possible solutions to exam questions, February 1, 2005 A proof of Mac lemma L05.1.1A : x ∈ N → ∀y∈B: f(x, y) ∈ B could be as follows: Mac proof of L05.1.1A:

L01 : Definition ⊳  f(x, y) ≡ if(x = 0, y, f(x − 1, ¬y)) ;
L02 : SetB ⊳  B ∈ Set  ;
L03 : Block ⊳  Begin  ;
L04 : Hypothesis ⊳  x ∈ N  ;
L05 : Hypothesis ⊳  (x = 0) ∈ T  ;
L06 : IfT ⊳ L5 ⊳  if(x = 0, y, f(x − 1, ¬y)) ≡ y  ;
L07 : Transitivity ⊳ L1 ⊳ L6 ⊳  f(x, y) ≡ y  ;
L08 : Block ⊳  Begin  ;
L09 : Hypothesis ⊳  y ∈ B  ;
L10 : Reverse’ ⊳ L7 ⊳ L9 ⊳  f(x, y) ∈ B  ;
L11 : Block ⊳  End  ;
L12 : Gen ⊳ L2 ⊳ L10 ⊳  ∀y∈B: f(x, y) ∈ B  ;
L13 : Block ⊳  End  ;
L14 : Block ⊳  Begin  ;
L15 : Hypothesis ⊳  x ∈ N  ;
L16 : Hypothesis ⊳  (x = 0) ∈ F  ;
L17 : Hypothesis ⊳  ∀y∈B: f(x − 1, y) ∈ B  ;
L18 : IfF ⊳ L16 ⊳  if(x = 0, y, f(x − 1, ¬y))
≡ f(x − 1, ¬y)  ;
L19 : Transitivity ⊳ L1 ⊳ L18 ⊳  f(x, y) ≡ f(x − 1, ¬y)  ;
L20 : Block ⊳  Begin  ;
L21 : Hypothesis ⊳  y ∈ B  ;
L22 : Type¬B ⊳  (¬y) ∈ B  ;
L23 : ElimAll⊳L2⊳L17⊳L22 ⊳  f(x − 1, ¬y) ∈ B  ;
L24 : Reverse’ ⊳ L19 ⊳ L23 ⊳  f(x, y) ∈ B  ;
L25 : Block ⊳  End  ;
L26 : Gen ⊳ L2 ⊳ L24 ⊳  ∀y∈B: f(x, y) ∈ B  ;
L27 : Block ⊳  End  ;
L28 : Induction ⊳ L12 ⊳ L26 ⊳ x ∈ N → ∀y∈B: f(x, y) ∈ B

L05.1.1A ^{·} rule L05.1.1A

Mathematics and Computation Possible solutions to exam questions, February 1, 2005 A proof of Mac antilemma L05.1.2B : x ∈ B → ∀y∈B: ((x ⇒ y) ⇒ (¬x ⇒ ¬y)) could be as follows: Mac proof of L05.1.2B:

L1 : Antilemma ⊳  x ∈ B → ∀y∈B: ((x⇒y)⇒(¬x⇒¬y)) ;
L2 : SetB ⊳  B ∈ Set  ;
L3 : TypeTInB ⊳  T ∈ B  ;
L4 : TypeFInB ⊳  F ∈ B  ;
L5 : Replace ⊳ L01 ⊳  F ∈ B → ∀y∈B: ((F⇒y)⇒(¬F⇒¬y)) ;
L6 : L5 ⊵ L4 ⊳ ∀y∈B: ((F ⇒ y) ⇒ (¬F ⇒ ¬y)) ;
L7 : ElimAll ⊳ L2 ⊳ L6 ⊳ L3 ⊳ ((F ⇒ T) ⇒ (¬F ⇒ ¬T))  ;
L8 : Computation ⊳ ((F ⇒ T) ⇒ (¬F ⇒ ¬T)) ≡ F ;
L9 : CounterTF ⊳ L7 ⊳ L8 ⊳ ⊥

A proof of Mac lemma L05.1.3A : x ∈ B → ∀y∈B: ((x ⇒ y) ⇒ (¬y ⇒ ¬x)) could be as follows: Mac proof of L05.1.3A:

L1 : Tautology ⊳  x ∈ B → y ∈ B → ((x ⇒ y) ⇒ (¬y ⇒ ¬x)) ;
L2 : SetB ⊳  B ∈ Set  ;
L3 : Block ⊳  Begin  ;
L4 : Hypothesis ⊳  x ∈ B  ;
L5 : L1 ⊵ L4 ⊳  y ∈ B → ((x ⇒ y) ⇒ (¬y ⇒ ¬x))  ;
L6 : Gen ⊳ L2 ⊳ L5 ⊳  ∀y∈B: ((x ⇒ y) ⇒ (¬y ⇒ ¬x))  ;
L7 : Block ⊳  End
(( x ⇒ y ) ⇒ ( ¬ y ⇒ ¬ x ))
T T T T F T T F T
T F F T T F F F T
F T T T F T T T F
F T F T T F T T F

L05.1.2B ^{·} rule L05.1.2B L05.1.3A ^{·} rule L05.1.3A